Di KTT Sarjana Web3, Profesor Shao Zhong meluncurkan model LiDO untuk mendorong verifikasi keamanan protokol konsensus

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

Profesor Shao Zhong dalam presentasinya menunjukkan bahwa protokol konsensus yang ada seperti PBFT dan Jolteon meskipun banyak digunakan, tetapi karena kompleksitas implementasinya yang tinggi, seringkali menyimpan kerentanan yang potensial. Untuk mengatasi masalah ini, model LiDO secara inovatif mengusulkan kerangka verifikasi yang terperinci dalam tiga lapisan:

1. Lapisan abstraksi keamanan: Memetakan protokol menjadi mesin status linier, memastikan konsistensi log (keamanan);
2. Lapisan perlindungan aktif: 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 industri Jolteon (BFT dua tahap) dan beberapa protokol DAG, menyelesaikan lebih dari sepuluh ribu baris kode Coq sebagai bukti mekanis, di mana jumlah kode untuk verifikasi keamanan dan aktivasi masing-masing mencapai 4000 baris dan 1700 baris. Profesor Shao Zhong menekankan: "Saat ini, protokol konsensus PoS secara umum menghadapi tantangan untuk mencapai keamanan, aktivasi, dan desentralisasi secara bersamaan. Model LiDO adalah skema desain sistematis yang diusulkan untuk mengatasi kendala ini."

Sebagai pengembang utama sistem operasi "tanpa celah" CertiKOS yang melalui verifikasi formal pertama di dunia, Profesor Zhao Zhong telah mengumpulkan pengalaman mendalam di bidang keamanan sistem. Prestasi ini tidak hanya memberikan dasar yang kokoh untuk penelitian selanjutnya tetapi juga menunjukkan kontribusinya yang luar biasa di bidang keamanan sistem. Dalam beberapa tahun terakhir, Profesor Zhao Zhong telah mengalihkan fokus penelitiannya ke keamanan blockchain, dan pada tahun 2017, ia bersama mitranya mendirikan sebuah perusahaan keamanan yang berkomitmen untuk menerapkan teknologi verifikasi formal dalam perlindungan keamanan kontrak pintar dan protokol on-chain, memberikan perlindungan keamanan untuk aset kripto yang bernilai ratusan miliar dolar.

Model LiDO saat ini telah menyelesaikan desain dan verifikasi formal, dan mulai menjelajahi kemungkinan integrasi dengan rantai publik utama dan 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 perusahaan dan ekosistem Web3 dengan lebih baik. Di akhir presentasi, 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."