Sorotan Konferensi Cendekiawan Web3: Model Verifikasi Keamanan Protokol Konsensus Baru Pertama Kali Dipublikasikan

Pada konferensi Akademisi Web3 2025 yang diadakan baru-baru ini, seorang profesor dari Departemen Ilmu Komputer Universitas Yale menyampaikan pidato utama berjudul "Keamanan dan Pembuktian Aktivitas Protokol Konsensus yang Diperhalus: LiDO dan Perluasannya", memperkenalkan kepada publik model LiDO dan kerangka perluasan LiDO-DAG yang dikembangkan oleh timnya. Hasil inovatif ini bertujuan untuk memberikan pembuktian keamanan dan aktivitas yang dapat diverifikasi secara mekanis untuk protokol konsensus toleran kesalahan Bizantium (BFT) yang kompleks, menetapkan dasar teknis untuk pengembangan keandalan dan skalabilitas ekosistem Web3.

Dalam pidatonya, profesor tersebut menunjukkan bahwa meskipun protokol konsensus yang ada (seperti PBFT, Jolteon) banyak digunakan, sering kali terdapat potensi risiko keamanan karena kompleksitas implementasinya yang tinggi. Untuk mengatasi masalah ini, model LiDO secara inovatif mengusulkan kerangka verifikasi yang diperhalus dalam tiga lapisan:

1. Lapisan abstraksi keamanan: Memetakan protokol menjadi mesin status linier, memastikan konsistensi log (keamanan);
2. Lapisan Jaminan Aktivitas: Memperkenalkan mekanisme "Pacemaker", untuk mengatasi masalah keterlambatan jaringan melalui siaran waktu habis dan sinkronisasi putaran;
3. Lapisan Ekstensi DAG: Mendukung protokol DAG baru seperti Narwhal, Bullshark, untuk mewujudkan verifikasi efisien tanpa pemimpin dalam konsensus.

Saat ini, LiDO telah berhasil diterapkan pada protokol tingkat industri Jolteon (BFT dua tahap) dan beberapa protokol DAG, menyelesaikan lebih dari 10.000 baris kode Coq yang dibuktikan secara mekanis, di mana jumlah kode untuk verifikasi keamanan dan aktivitas masing-masing mencapai 4.000 baris dan 1.700 baris. Pembicara menekankan: "Saat ini, protokol konsensus PoS secara umum menghadapi kesulitan untuk mendapatkan ketiga aspek keamanan, aktivitas, dan desentralisasi. Model LiDO adalah solusi desain sistematis yang diusulkan untuk mengatasi keterbatasan ini."

Profesor ini pernah memimpin tim yang mengembangkan sistem operasi "tanpa celah" pertama di dunia melalui verifikasi formal, CertiKOS, yang dianggap sebagai "tonggak keamanan sistem fisik jaringan". Prestasi ini tidak hanya meletakkan dasar teknologi untuk perusahaan keamanan yang didirikannya kemudian, tetapi juga menunjukkan akumulasi mendalamnya di bidang keamanan sistem. Dalam beberapa tahun terakhir, ia telah mengalihkan fokus penelitiannya ke keamanan blockchain, berkomitmen untuk menerapkan teknologi verifikasi formal untuk perlindungan keamanan kontrak pintar dan protokol on-chain, menyediakan perlindungan keamanan untuk aset kripto senilai ratusan miliar dolar.

LiDO saat ini telah menyelesaikan desain model dan verifikasi formal, dan mulai menjajaki kemungkinan integrasi dengan blockchain utama dan protokol desentralisasi. Pembicara menyatakan bahwa mereka berkomitmen untuk memverifikasi mekanisme kunci dalam Web3.0, untuk menyediakan produk dan layanan sepanjang siklus, serta mendukung strategi pengembangan jangka panjang bagi perusahaan dan ekosistem Web3. Di akhir pidatonya, ia menekankan: "Tumpukan protokol jaringan yang dapat dipercaya, aman, dan dapat diverifikasi, akan menjadi jalur kunci menuju masa depan yang benar-benar terdesentralisasi."