Profesor Yale Berbagi Kemajuan Penelitian Keamanan Protokol Konsensus di KTT Cendekiawan Web3

Pada Konferensi Cendekiawan Web3 2025, Profesor Shao Zhong dari Departemen Ilmu Komputer Universitas Yale memberikan pidato utama berjudul "Bukti Keamanan dan Aktivitas Protokol Konsensus yang Diperhalus: LiDO dan Perluasannya", yang pertama kali memperkenalkan model LiDO yang dikembangkan oleh timnya serta kerangka perluasan LiDO-DAG. Hasil terobosan ini bertujuan untuk menyediakan bukti keamanan dan aktivitas yang dapat diverifikasi secara mekanis untuk protokol konsensus Byzantine Fault Tolerant (BFT) yang kompleks, meletakkan dasar teknologi untuk keandalan dan pengembangan skala ekosistem Web3.

Prof. Shao Zhong dalam pidatonya menunjukkan bahwa protokol konsensus yang ada (seperti PBFT, Jolteon) meskipun banyak digunakan, tetapi karena implementasinya yang kompleks sering menyembunyikan kerentanan yang potensial. Untuk mengatasi masalah ini, model LiDO secara inovatif mengusulkan kerangka verifikasi tiga lapis yang lebih rinci:

1. Lapisan abstraksi keamanan: memetakan protokol sebagai mesin status linier, memastikan konsistensi log (keamanan);
2. Lapisan jaminan aktif: Memperkenalkan mekanisme "Pacemaker" untuk memecahkan masalah keterlambatan jaringan melalui siaran timeout dan sinkronisasi putaran;
3. Lapisan ekstensi DAG: Mendukung protokol DAG baru seperti Narwhal, Bullshark, dan mewujudkan verifikasi yang efisien tanpa pemimpin dalam konsensus.

Saat ini, LiDO telah berhasil diterapkan pada protokol industri Jolteon (BFT dua tahap) dan beberapa protokol DAG, menyelesaikan lebih dari sepuluh ribu baris kode Coq untuk pembuktian mekanis, dengan jumlah kode verifikasi keamanan dan aktivasi masing-masing mencapai 4000 baris dan 1700 baris. Profesor Shao Zhong dalam pidatonya menunjukkan: "Saat ini, protokol konsensus PoS umumnya menghadapi kesulitan untuk mencapai keamanan, aktivasi, dan desentralisasi secara bersamaan. Model LiDO adalah solusi desain sistematis yang diusulkan untuk memecahkan masalah ini."

Perlu dicatat bahwa Profesor Shao Zhong memimpin tim yang mengembangkan CertiKOS, yang merupakan sistem operasi "tanpa celah" pertama di dunia yang melalui verifikasi formal, dan dianggap sebagai "tonggak keamanan sistem fisik jaringan". Prestasi ini tidak hanya meletakkan dasar yang kuat di bidang keamanan sistem, tetapi juga memberikan fondasi yang solid untuk penelitian keamanan blockchain di masa mendatang. Pada tahun 2017, Profesor Shao Zhong dan muridnya, Profesor Gu Ronghui, memperkenalkan teknologi verifikasi formal ke dalam bidang perlindungan keamanan kontrak pintar dan protokol di blockchain, memberikan dukungan penting untuk keamanan aset kripto.

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