Google DeepMind mengumumkan pencapaian yang disebut sebagai tonggak penting bagi kriptografi sekaligus kecerdasan buatan: kerangka kerja baru bernama AlphaProof Code berhasil memverifikasi secara formal sejumlah jaminan kriptografis utama dari protokol Signal. 🔗 WIRED
Proyek proof-of-concept ini diselesaikan dalam waktu sekitar empat minggu. Menurut para peneliti, analisis tersebut tidak menemukan kerentanan baru pada bagian protokol yang diperiksa. 🔗 Oossa
Hasil ini memberikan validasi independen tambahan atas kriptografi yang melindungi komunikasi dalam jumlah besar di aplikasi Signal, Google Messages, dan WhatsApp. 🔗 WIRED
Apa Itu Verifikasi Formal dan Mengapa Penting
Verifikasi formal adalah pendekatan matematis untuk memeriksa bahwa perangkat lunak berfungsi sesuai dengan yang dimaksudkan, yakni tanpa kerentanan kritis. Para pendukungnya lama menyebut metode ini sebagai "cawan suci" keamanan perangkat lunak. 🔗 WIRED
Sebelum era AI, proses ini sangat memakan waktu: manusia harus mendeskripsikan karakteristik perangkat lunak yang ingin dibuktikan, mengubah ringkasan tersebut menjadi rumus, lalu menyusun pembuktian. AI agenik dapat memangkas waktu untuk tahap terakhir secara signifikan, sehingga memungkinkan analisis seperti evaluasi Signal oleh DeepMind. 🔗 WIRED
Apa yang Dilakukan AlphaProof Code
Tim DeepMind menggunakan AlphaProof Code untuk membuktikan sejumlah jaminan kriptografis utama protokol Signal. Selain tidak menemukan kerentanan baru pada bagian yang diperiksa, kerangka kerja tersebut juga diuji pada versi lama Signal yang memang mengandung kerentanan yang sudah diketahui dan lama diperbaiki. 🔗 Oossa
Dalam kasus tersebut, AlphaProof Code berhasil mengidentifikasi kerentanan tersebut dan menunjukkan bahwa versi protokol lama itu tidak dapat diverifikasi secara formal. Menurut para peneliti, kemampuan mendeteksi cacat nyata ini menunjukkan bahwa alat tersebut tidak hanya mengonfirmasi kode yang benar, tetapi juga mampu menemukan kesalahan. 🔗 WIRED
Sebagai bagian dari transparansi, para peneliti merilis spesifikasi dan pembuktian yang mereka kembangkan untuk analisis Signal, agar dapat menjadi acuan bagi upaya verifikasi formal lainnya. 🔗 WIRED
Ruang Lingkup dan Keterbatasan
Analisis ini tidak mencakup keseluruhan aplikasi mobile Signal. Para peneliti menekankan bahwa hasil ini hanyalah satu tonggak dalam proses yang lebih panjang. 🔗 Oossa
Mereka juga mengakui mendapat keuntungan awal karena adanya pekerjaan verifikasi formal sebelumnya yang dilakukan oleh Signal Foundation, sehingga angka empat minggu tidak menggambarkan proyek yang dimulai dari nol. 🔗 WIRED
Swarat Chaudhuri, ilmuwan peneliti DeepMind, mengatakan kepada WIRED: "Kami sangat bersemangat dengan hasil ini, tetapi masih ada jarak yang jauh sebelum kami dapat menskalakan ini ke seluruh perangkat lunak dunia, dan kami ingin melakukan itu." 🔗 WIRED
Reaksi Industri
Ehren Kret, chief technology officer Signal, menyatakan dalam siaran pers bahwa pendekatan DeepMind memungkinkan perluasan signifikan dibandingkan pekerjaan sebelumnya yang hanya mencakup bagian-bagian kecil dari kode. 🔗 WIRED
"Saat ancaman keamanan berbasis AI berkembang, memverifikasi implementasi protokol Signal secara ketat memberi kami keyakinan yang lebih besar atas jaminan privasi kode kami," katanya. 🔗 WIRED
Pushmeet Kohli, chief scientist Google Cloud dan vice president of research DeepMind, menyoroti pengguna dengan taruhan tinggi: bank dan perusahaan lain yang bergantung pada jaminan dan khawatir akan bug kini berpotensi dapat membuktikan properti tersebut. "Bayangkan bank, bayangkan semua perusahaan lain yang bergantung pada jaminan," ujarnya. 🔗 WIRED
Kolaborasi Manusia-AI, Bukan "Vibe World"
Para peneliti menekankan bahwa salah satu kemajuan krusial adalah pengembangan "proses kolaborasi manusia-AI", di mana agen dapat berkontribusi dan mengoreksi diri sendiri di hampir setiap fase, sambil tetap meminta masukan dan tinjauan manusia pada titik-titik kunci. 🔗 WIRED
Chaudhuri menegaskan mereka tidak ingin dunia di mana AI menghasilkan tujuan dan pembuktian sekaligus, serta melakukan pengujian yang ditulis sendiri. "Ada titik tengah," katanya. 🔗 WIRED
Pertanyaan Terbuka: Skala dan Biaya
Pertanyaan terbuka di seluruh sektor teknologi adalah apakah verifikasi formal berbantuan AI benar-benar dapat diskalakan dan dengan biaya yang layak. Analisis Signal dilakukan DeepMind secara gratis sebagai proyek penelitian, dan Google menolak membagikan biayanya. 🔗 WIRED
Perusahaan juga tidak berkomentar apakah ada rencana merilis produk atau layanan verifikasi formal komersial. Tanpa angka biaya, tim lain belum dapat menilai apakah pendekatan ini terjangkau untuk basis kode mereka sendiri. 🔗 WIRED
Fakta Kunci
- AlphaProof Code memverifikasi jaminan kriptografis utama protokol Signal dalam sekitar empat minggu.
- Tidak ditemukan kerentanan baru pada bagian protokol yang diperiksa.
- Pada versi lama Signal dengan kerentanan yang sudah diketahui, alat ini berhasil mengidentifikasinya dan menunjukkan protokol tidak dapat diverifikasi.
- Analisis tidak mencakup seluruh aplikasi mobile Signal; hasil adalah satu tonggak dalam proses yang lebih panjang.
- Spesifikasi dan pembuktian dirilis untuk membantu upaya verifikasi formal lainnya.
- Proyek dilakukan gratis sebagai penelitian; biaya tidak diungkapkan dan komersialisasi belum diumumkan.
Sumber
- WIRED — "A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure" (Lily Hay Newman, 10 Nov 2026): https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/
- Oossa — "DeepMind uses AI to formally verify parts of Signal protocol" (10 Nov 2026): https://oossa.com/en/deepmind-uses-ai-to-formally-verify-parts-of-signal-protocol
Tidak ada komentar:
Posting Komentar