Tại hội nghị học giả Web3, giáo sư Yale chia sẻ tiến triển trong nghiên cứu an ninh 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 "Bằng chứng về sự an toàn và hoạt động của giao thức nhận thức chung dựa trên tinh chỉnh: LiDO và các mở rộng của nó", lần đầu tiên công bố 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 đột phá này nhằm cung cấp bằng chứng về sự an toàn và hoạt động có thể được xác minh cơ học cho các giao thức đồng thuận Byzantine Fault Tolerant (BFT) phức tạp, đặt nền tảng công nghệ cho sự tin cậy và phát triển quy mô của hệ sinh thái Web3.

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

1. Lớp 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 vệ hoạt tính: Giới thiệu cơ chế "Pacemaker", thông qua phát sóng quá thời gian và đồng bộ vòng để giải quyết vấn đề độ trễ mạ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 thực hiệu quả với 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 khác, hoàn thành việc chứng minh cơ học hơn mười ngàn dòng mã Coq, với mã chứng minh an toàn và tính năng lần lượt đạt 4000 dòng và 1700 dòng. Giáo sư Shao Zhong trong bài phát biểu đã chỉ ra: "Hiện nay, giao thức đồng thuận PoS đang phải đối mặt với tình trạng khó khăn khi không thể đạt được đồng thời an toàn, tính nă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 nhằm phá vỡ tình trạng khó khăn này."

Đáng chú ý là, giáo sư Shao Zhong cùng đội ngũ của ô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 chứng minh thông qua xác minh hình thức, được ca ngợi là "cột mốc an ninh trong hệ thống vật lý mạng". Thành tựu này không chỉ củng cố nền tảng vững chắc của ông trong lĩnh vực an ninh hệ thống mà còn cung cấp nền tảng vững chắc cho nghiên cứu an ninh blockchain sau này. Năm 2017, giáo sư Shao Zhong cùng học trò của ông là 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 của hợp đồng thông minh và giao thức trên chuỗi, cung cấp hỗ trợ quan trọng cho an ninh tài sản tiền mã hóa.

LiDO hiện đã hoàn thành thiết kế mô hình và xác minh hình thức, và bắt đầu khám phá khả năng tích hợp với các chuỗi công khai chính và giao thức phi tập trung. Giáo sư Shao Zhong cho biết, họ cam kết xác minh các cơ chế then chốt trong Web3.0 để cung cấp sản phẩm và dịch vụ trong toàn bộ chu kỳ, hỗ trợ tốt hơn cho chiến lược phát triển lâu dài của các doanh nghiệp và hệ sinh thái Web3. Cuối buổi thuyết trình, giáo sư Shao Zhong nhấn mạnh: "Chồng giao thức mạng đáng tin cậy, an toàn và có thể xác minh sẽ là con đường chính dẫn đến tương lai phi tập trung thực sự."