Điểm nổi bật của Hội nghị học giả Web3: Mô hình xác minh an ninh giao thức nhận thức chung mới được công bố lần đầu tiên

Tại hội nghị học giả Web3 năm 2025 vừa diễn ra, một giáo sư đến từ khoa khoa học máy tính của Đại học Yale đã có bài phát biểu chủ đề với tiêu đề "Bảo mật và chứng minh hoạt động của giao thức đồng thuận tinh chỉnh: LiDO và các mở rộng của nó", lần đầu tiên giới thiệu công chúng về mô hình LiDO và khung mở rộng LiDO-DAG mà nhóm của ông phát triển. Thành tựu đổi mới này nhằm cung cấp sự chứng minh về bảo mật và hoạt động có thể cơ giới hóa cho các giao thức đồng thuận Byzantine Fault Tolerant (BFT) phức tạp, từ đó 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.

Trong bài phát biểu, giáo sư 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 triển khai cao, thường có những nguy cơ an ninh tiềm ẩn. Để giải quyết vấn đề này, mô hình LiDO đã sáng tạo đưa ra khung xác minh tinh vi 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 đả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ả nhận thức chung không có người lãnh đạo.

Hiện tại, LiDO đã thành công trong việc áp dụng cho 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 ninh và hoạt động lần lượt đạt 4,000 dòng và 1,700 dòng. Ngườ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 an ninh, hoạt độ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 để vượt qua giới hạn này."

Giáo sư này đã dẫn dắt đội ngũ phát triển hệ điều hành "không có lỗ hổng" CertiKOS thông qua xác minh hình thức, được ca ngợi là "mốc quan trọng trong an ninh hệ thống mạng vật lý". Thành tựu này không chỉ đặt nền tảng công nghệ cho công ty bảo mật mà ông sau này thành lập, mà còn thể hiện tích lũy sâu sắc của ông trong lĩnh vực an ninh hệ thống. Trong những năm gần đây, ông đã chuyển trọng tâm nghiên cứu sang an ninh blockchain, nỗ lực áp dụng công nghệ xác minh hình thức vào việ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 toàn cho tài sản tiền mã hóa trị giá hàng trăm tỷ đô la.

LiDO hiện đã hoàn thành thiết kế mô hình và xác thực 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. Người diễn thuyết cho biết họ cam kết xác thực các cơ chế quan trọng trong Web3.0 để cung cấp sản phẩm và dịch vụ theo chu kỳ đầy đủ, 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 bài phát biểu, ông nhấn mạnh: "Một ngăn xếp 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 một tương lai phi tập trung thực sự."