Berikut adalah terjemahan teks tersebut ke dalam bahasa Indonesia yang formal dan baku:
Sebuah makalah penelitian baru berjudul “Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking” menandai tonggak penting dalam penelitian perangkat keras kriptografi yang diverifikasi secara formal (formally-verified cryptographic hardware research). Makalah ini, yang merupakan bagian keenam dari seri analisis tentang perangkat keras NTT yang diberi masker (masked NTT hardware) untuk kriptografi pasca-kuantum, membuktikan untuk pertama kalinya teorema komposisi yang diverifikasi secara komputasi (machine-checked) untuk penyembunyian aritmatika (arithmetic masking) di atas lapangan prima (prime fields). Penelitian ini sangat relevan dalam konteks percepatan global menuju standardisasi dan implementasi kriptografi pasca-kuantum.
Konteks dari penelitian ini adalah peralihan global menuju algoritma kriptografi yang tahan terhadap serangan komputer kuantum. Kriptografi kunci publik tradisional seperti RSA dan ECC bergantung pada masalah matematis seperti faktorisasi bilangan bulat dan logaritma diskret yang dapat dipecahkan secara efisien oleh komputer kuantum menggunakan algoritma Shor. Algoritma kriptografi pasca-kuantum (Post-Quantum Cryptography atau PQC) dirancang agar tetap aman bahkan ketika penyerang memiliki akses ke komputer kuantum. National Institute of Standards and Technology (NIST) telah menyelesaikan proses standardisasi mereka untuk algoritma PQC, dan industri kini berada dalam tahap implementasi dan penyebaran.
Salah satu komponen mendasar dari banyak algoritma PQC adalah Number Theoretic Transform (NTT), yang merupakan analog dari Fast Fourier Transform (FFT) untuk lapangan hingga (finite fields). NTT digunakan secara ekstensif dalam kriptografi berbasis kisi (lattice-based cryptography), yang merupakan salah satu pendekatan paling menjanjikan untuk PQC. Namun, implementasi perangkat keras dari NTT rentan terhadap serangan saluran samping (side-channel attacks) seperti Differential Power Analysis (DPA), di mana penyerang dapat mengekstrak kunci rahasia dengan mengamati pola konsumsi daya dari perangkat keras kriptografi tersebut.
Penyembunyian (masking) adalah teknik penanggulangan yang paling umum digunakan untuk melindungi dari serangan saluran samping. Ide dasar dari penyembunyian adalah membagi setiap nilai rahasia menjadi beberapa bagian (shares) yang diacak sedemikian rupa sehingga tidak ada subset kecil dari bagian-bagian tersebut yang memberikan informasi tentang nilai rahasia asli. Penyembunyian Boolean (boolean masking), yang beroperasi pada operasi bit demi bit, telah dipahami dengan baik melalui teorema komposisi seperti NI (Non-Interference), SNI (Strong Non-Interference), dan PINI (Probe Isolating Non-Interference).
Namun, penyembunyian aritmatika di atas lapangan prima—yang merupakan fondasi dari kriptografi pasca-kuantum berbasis NTT—tidak memiliki teori analog yang mapan. Ini adalah kesenjangan teoretis yang signifikan karena tanpa teorema komposisi yang ketat, kita tidak dapat memastikan bahwa penyembunyian yang diimplementasikan dalam akselerator perangkat keras PQC benar-benar aman. Penelitian Prime-Field PINI menjawab kesenjangan ini dengan membuktikan teorema komposisi pertama yang diverifikasi secara komputasi untuk penyembunyian aritmatika di atas lapangan prima.
Wawasan utama dari penelitian ini adalah argumen pembaruan (renewal argument): ketika masker acak segar (fresh random mask) diterapkan di antara dua tahap pipa (pipeline stages), kabel perantara (intermediate wire) menjadi seragam sempurna terlepas dari parameter keamanan Tahap 1. Ini adalah hasil yang kuat karena menunjukkan bahwa dengan masker segar yang tepat, keamanan dari Tahap 1 dapat “diatur ulang” sehingga tidak memengaruhi keamanan dari output komposisi. Secara formal, untuk dua gawai (gadgets) PF-PINI dengan parameter $k1$ dan $k2$, pipa dua tahap yang dikomposisikan dengan masker segar memenuhi PF-PINI($k2$) — multiplisitas dari Tahap 1 sepenuhnya terhapus dari output yang dikomposisikan.
Sebaliknya, tanpa masker segar, kabel perantara memiliki multiplisitas hingga $k1$, menciptakan kondisi yang diperlukan untuk analisis daya diferensial. Ini adalah temuan penting karena menunjukkan bahwa penghematan dalam pembangkitan bilangan acak dapat memiliki konsekuensi keamanan yang serius. Dalam desain perangkat keras kriptografi, selalu ada pertukaran (trade-off) antara keamanan dan efisiensi — masker segar memerlukan keacakan tambahan, yang memerlukan sumber daya perangkat keras tambahan dan dapat mengurangi throughput. Namun, penelitian ini menunjukkan bahwa penghematan ini tidak sepadan jika dilihat dari perspektif keamanan.
Hal yang membuat penelitian ini sangat ketat adalah formalisasinya dalam Lean 4, sebuah interactive theorem prover. Seluruh pembuktian — 18 pembuktian — diverifikasi secara komputasi tanpa adanya “sorry stubs”. Dalam metode formal, “sorry” adalah penanda tempat (placeholder) yang menunjukkan bahwa pembuktian belum diselesaikan. Memiliki nol “sorry stubs” berarti seluruh pembuktian benar-benar lengkap dan diverifikasi oleh sistem pembuktian teorema. Ini adalah tingkat ketelitian yang jauh melampaui pembuktian tradisional di atas kertas, yang dapat mengandung kesalahan halus yang tidak terdeteksi selama bertahun-tahun.
Penelitian ini juga secara formal menjembatani model aritmatika aljabar dan model aritmatika yang setia terhadap perangkat keras (hardware-faithful) dari reduksi Barrett, sebuah algoritma reduksi modular yang umum digunakan dalam implementasi kriptografi. Penjembatanan ini penting karena memastikan bahwa jaminan keamanan yang dibuktikan pada tingkat aljabar benar-benar berlaku untuk implementasi perangkat keras yang sebenarnya. Banyak pembuktian keamanan gagal dalam praktiknya karena adanya kesenjangan antara model teoretis dan implementasi nyata.
Aplikasi praktis dari teorema ini ditunjukkan melalui diagnosis formal terhadap akselerator PQC Adams Bridge milik Microsoft. Penelitian ini mengidentifikasi bahwa ketiadaan masker antar-tahap yang segar (fresh inter-stage masking) pada Adams Bridge membuat kabel output Barrett tidak seragam di bawah model pengujian urutan pertama (first-order probing model). Ini adalah cacat arsitektural yang sama yang diidentifikasi oleh dua analisis empiris independen dan analisis struktural sebelumnya oleh tim peneliti yang sama. Temuan konvergen dari berbagai analisis independen memperkuat validitas dari temuan ini.
Bukti komputasi dari penelitian ini juga menunjukkan bahwa 1-Bit Barrier bersifat universal di seluruh reduksi Barrett dan Montgomery. 1-Bit Barrier mengacu pada fenomena di mana bahkan satu bit kebocoran pun dapat, dalam kondisi tertentu, memungkinkan pemulihan kunci rahasia. Jika 1-Bit Barrier memang universal, hal ini memiliki implikasi mendalam bagi desain perangkat keras kriptografi yang aman — bahkan kebocoran minimal harus dianggap sebagai kegagalan fatal.
Analisis Retasan
Penelitian Prime-Field PINI adalah contoh sempurna dari bagaimana metode formal dapat memberikan jaminan keamanan yang tidak mungkin dicapai dengan metode analisis tradisional. Di dunia di mana penyebaran kriptografi pasca-kuantum semakin meluas, memiliki pembuktian keamanan yang diverifikasi secara komputasi untuk implementasi penyembunyian (masking) bukan lagi sebuah kemewahan, melainkan kebutuhan.
Bagi Indonesia, penelitian ini memiliki implikasi penting untuk pengembangan keahlian kriptografi lokal. Ketika Indonesia mulai mengadopsi standar kriptografi pasca-kuantum, penting untuk memastikan bahwa implementasi yang digunakan memiliki jaminan keamanan yang ketat. Penelitian seperti Prime-Field PINI dapat menjadi model bagi inisiatif penelitian lokal dalam verifikasi kriptografi. Universitas dan lembaga penelitian di Indonesia dapat mulai membangun kapasitas dalam metode formal untuk kriptografi.
Temuan mengenai Adams Bridge milik Microsoft juga mengajarkan pelajaran penting: bahkan perusahaan teknologi terbesar dengan sumber daya yang signifikan dapat membuat kesalahan keamanan mendasar. Ini adalah pengingat bahwa keamanan kriptografi memerlukan pengawasan berkelanjutan dan verifikasi independen. Tidak ada vendor yang terlalu besar untuk diaudit, dan tidak ada implementasi yang terlalu kompleks untuk diverifikasi secara formal.
Sumber: arXiv:2604.25878 – Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking | Authors: Ray Iskander, Khaled Kirah
