Tại hội nghị học giả Web3, giáo sư Yale lần đầu tiên công bố mô hình LiDO
Tại hội nghị học giả Web3 2025 được tổ chức gần đây, giáo sư Shao Zhong của khoa khoa học máy tính Đại học Yale đã có bài phát biểu chính với tiêu đề "Bằng chứng an toàn và hoạt động của giao thức đồng thuận 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 đổi mới này nhằm cung cấp các bằng chứng an toàn và 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ừ đó đặt nền tảng công nghệ cho sự phát triển đáng tin cậy và 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, mặc dù các giao thức đồng thuận 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, thường ẩn chứa những lỗ hổng tiềm ẩn. Để giải quyết vấn đề này, mô hình LiDO đã đổi mới đề xuất một khung xác minh tinh vi ba lớp:
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);
Tầng bảo vệ hoạt động: 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.
Lớp mở rộng DAG: Hỗ trợ các giao thức DAG mới nổi như Narwhal, Bullshark, đạt được xác minh hiệu quả với sự đồng thuận không có 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 hơn một vạn dòng mã Coq được chứng minh cơ học, trong đó mã kiểm tra tính an toàn và tính khả thi lần lượt đạt 4000 dòng và 1700 dòng. Giáo sư Shao Zhong trong buổi diễn thuyết đã nhấn mạnh: "Hiện nay, 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 tính an toàn, tính khả thi và phi tập trung. Mô hình LiDO chính là giải pháp hệ thống được đưa ra để vượt qua nút thắt này."
Đáng chú ý, Giáo sư Shao Zhong đã dẫn dắt đội ngũ phát triển hệ điều hành "không lỗ hổng" CertiKOS, hệ điều hành đầu tiên trên thế giới được xác minh hình thức, được ngành công nghiệp ca ngợi là "mốc quan trọng trong an toàn hệ thống vật lý mạng". Thành tựu này không chỉ thể hiện sự tích lũy sâu sắc của đội ngũ trong lĩnh vực an toàn hệ thống, mà còn tạo nền tảng vững chắc cho các nghiên cứu tiếp theo. Trong những năm gần đây, Giáo sư Shao Zhong đã chuyển trọng tâm nghiên cứu sang an toàn blockchain và vào năm 2017, cùng với các đối tác, ông đã thành lập một công ty an toàn blockchain, chuyên ứng dụng công nghệ xác minh hình thức vào việc đảm bảo an toàn cho hợp đồng thông minh và các giao thức trên chuỗi, cung cấp sự bảo vệ an toàn cho tài sản tiền điện tử trị giá hàng trăm tỷ đô la.
Mô hình LiDO hiện đã hoàn thành thiết kế 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 và giao thức phi tập trung chính. Giáo sư Shao Trung cho biết, họ cam kết xác minh các cơ chế then chốt trong Web3.0, nhằm 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 cùng, giáo sư Shao Trung nhấn mạnh: "Xây dựng 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 then chốt dẫn đến tương lai thực sự phi tập trung."
Trang này có thể chứa nội dung của bên thứ ba, được cung cấp chỉ nhằm mục đích thông tin (không phải là tuyên bố/bảo đảm) và không được coi là sự chứng thực cho quan điểm của Gate hoặc là lời khuyên về tài chính hoặc chuyên môn. Xem Tuyên bố từ chối trách nhiệm để biết chi tiết.
Giáo sư Yale tiết lộ LiDO: Vượt qua rào cản xác thực an ninh của nhận thức chung giao thức
Tại hội nghị học giả Web3, giáo sư Yale lần đầu tiên công bố mô hình LiDO
Tại hội nghị học giả Web3 2025 được tổ chức gần đây, giáo sư Shao Zhong của khoa khoa học máy tính Đại học Yale đã có bài phát biểu chính với tiêu đề "Bằng chứng an toàn và hoạt động của giao thức đồng thuận 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 đổi mới này nhằm cung cấp các bằng chứng an toàn và 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ừ đó đặt nền tảng công nghệ cho sự phát triển đáng tin cậy và 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, mặc dù các giao thức đồng thuận 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, thường ẩn chứa những lỗ hổng tiềm ẩn. Để giải quyết vấn đề này, mô hình LiDO đã đổi mới đề xuất một khung xác minh tinh vi ba lớp:
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 hơn một vạn dòng mã Coq được chứng minh cơ học, trong đó mã kiểm tra tính an toàn và tính khả thi lần lượt đạt 4000 dòng và 1700 dòng. Giáo sư Shao Zhong trong buổi diễn thuyết đã nhấn mạnh: "Hiện nay, 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 tính an toàn, tính khả thi và phi tập trung. Mô hình LiDO chính là giải pháp hệ thống được đưa ra để vượt qua nút thắt này."
Đáng chú ý, Giáo sư Shao Zhong đã dẫn dắt đội ngũ phát triển hệ điều hành "không lỗ hổng" CertiKOS, hệ điều hành đầu tiên trên thế giới được xác minh hình thức, được ngành công nghiệp ca ngợi là "mốc quan trọng trong an toàn hệ thống vật lý mạng". Thành tựu này không chỉ thể hiện sự tích lũy sâu sắc của đội ngũ trong lĩnh vực an toàn hệ thống, mà còn tạo nền tảng vững chắc cho các nghiên cứu tiếp theo. Trong những năm gần đây, Giáo sư Shao Zhong đã chuyển trọng tâm nghiên cứu sang an toàn blockchain và vào năm 2017, cùng với các đối tác, ông đã thành lập một công ty an toàn blockchain, chuyên ứng dụng công nghệ xác minh hình thức vào việc đảm bảo an toàn cho hợp đồng thông minh và các giao thức trên chuỗi, cung cấp sự bảo vệ an toàn cho tài sản tiền điện tử trị giá hàng trăm tỷ đô la.
Mô hình LiDO hiện đã hoàn thành thiết kế 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 và giao thức phi tập trung chính. Giáo sư Shao Trung cho biết, họ cam kết xác minh các cơ chế then chốt trong Web3.0, nhằm 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 cùng, giáo sư Shao Trung nhấn mạnh: "Xây dựng 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 then chốt dẫn đến tương lai thực sự phi tập trung."