Hội nghị học giả Web3: Giáo sư Yale công khai mô hình LiDO, hỗ trợ nâng cao tính an toàn của giao thức nhận thức chung

Tại Hội nghị học giả Web3 năm 2025, giáo sư Shao Zhong từ Khoa Khoa học Máy tính của Đại học Yale đã có bài phát biểu chủ đề mang tên "Chứng minh tính an toàn và tính khả năng hoạt động của giao thức đồng thuận dựa trên tinh chế: LiDO và các mở rộng của nó". Ông đã lần đầu tiên giới thiệu mô hình LiDO và khung mở rộng LiDO-DAG do nhóm của ông phát triển. Thành tựu đổi mới này nhằm cung cấp chứng minh tính an toàn và tính khả năng hoạt động có thể xác minh cơ học cho các giao thức đồng thuận Byzantine Fault Tolerant (BFT) phức tạp, tạo nền tảng công nghệ cho sự phát triển độ tin cậy và khả năng mở rộng của hệ sinh thái Web3.

Giáo sư Shao Zhong trong bài phát biểu của mình đã chỉ ra rằng, mặc dù các giao thức nhận thức chung hiện có (như PBFT, Jolteon) được áp dụng rộng rãi, nhưng do độ phức tạp trong việc thực hiện, thường tồn tại các lỗ hổng bảo mật tiềm ẩn. Để giải quyết vấn đề này, mô hình LiDO đã đề xuất một khung xác minh tinh chỉnh ba lớp đổi mới:

1. Tầng trừu tượng an toàn: ánh xạ giao thức thành máy trạng thái tuyến tính, đảm bảo tính nhất quán của nhật ký (an toàn).
2. Lớp bảo đảm hoạt tính: Giới thiệu cơ chế "Pacemaker" để giải quyết vấn đề độ trễ mạng thông qua phát sóng quá thời gian và đồng bộ vòng.
3. Lớp mở rộng DAG: hỗ trợ các giao thức DAG mới nổi như Narwhal, Bullshark, thực hiện xác minh hiệu quả của Nhận thức chung không có người lãnh đạo.

Hiện tại, LiDO đã được áp dụng thành công vào giao thức công nghiệp Jolteon (BFT hai giai đoạn) và nhiều giao thức DAG, hoàn thành hơn 10,000 dòng mã Coq được chứng minh cơ học, trong đó số lượng mã kiểm tra an toàn và tính khả dụng lần lượt đạt 4,000 dòng và 1,700 dòng. Giáo sư Shao Zhong trong bài phát biểu nhấn mạnh: "Hiện nay, các giao thức đồng thuận PoS đang phải đối mặt với khó khăn trong việc đạt được đồng thời ba yếu tố an toàn, tính khả dụng và phi tập trung. Mô hình LiDO chính là giải pháp thiết kế hệ thống được đề xuất để phá vỡ tình huống này."

Đáng chú ý là, giáo sư Shao Zhong trước đó đã dẫn dắt đội ngũ phát triển CertiKOS, hệ điều hành "không có lỗ hổng" đầu tiên trên thế giới được xác minh bằng hình thức, được ca ngợi là "một cột mốc trong an ninh hệ thống mạng vật lý". Thành tựu này không chỉ thiết lập nền tảng vững chắc cho ông trong lĩnh vực an ninh hệ thống, mà còn cung cấp cơ sở vững chắc cho nghiên cứu tiếp theo trong lĩnh vực an ninh blockchain. Năm 2017, giáo sư Shao Zhong cùng với sinh viên của mình, giáo sư Gu Ronghui, đã đưa công nghệ xác minh hình thức vào lĩnh vực bảo đảm an ninh cho hợp đồng thông minh và giao thức trên chuỗi, cung cấp bảo vệ an ninh cho các tài sản tiền mã hóa có quy mô hàng tỷ đô la.

Mô hình LiDO hiện đã hoàn thành thiết kế và xác minh hình thức, đang khám phá khả năng tích hợp với các chuỗi công cộng chính và giao thức phi tập trung. Giáo sư Shao Trung cho biết, họ đang nỗ lực xác minh các cơ chế chính trong Web3.0 để cung cấp sản phẩm và dịch vụ toàn chu kỳ, hỗ trợ tốt hơn cho chiến lược phát triển dài hạn của các doanh nghiệp và hệ sinh thái Web3.

Vào cuối bài phát biểu, giáo sư Shao Trung nhấn mạnh: "Giao thức mạng tin cậy, an toàn và có thể xác minh sẽ là con đường quan trọng dẫn đến tương lai phi tập trung thực sự." Quan điểm này làm nổi bật ý nghĩa quan trọng của mô hình LiDO trong việc thúc đẩy sự phát triển công nghệ Web3 và đảm bảo an ninh.