Giáo sư Yale công bố công khai mô hình LiDO lần đầu tiên tại Hội nghị học giả Web3
Tại Hội nghị học giả Web3 năm 2025, 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ủ đề mang tên "Chứng minh an ninh và tính 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 giới thiệu mô hình LiDO mà nhóm của ông phát triển cùng với khung mở rộng LiDO-DAG. Thành tựu đổi mới này nhằm cung cấp chứng minh an ninh và tính hoạt động có thể được xác minh cơ học cho các giao thức đồng thuận chịu lỗi Byzantine (BFT) phức tạp, đặ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 của mình chỉ ra rằng các giao thức đồng thuận hiện có (như PBFT, Jolteon) mặc dù được ứng dụng rộng rãi, nhưng do việc triển khai phức tạp, 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 đã đề xuất một khung xác minh tinh chỉnh 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);
Lớp bảo đảm 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.
Tầng mở rộng DAG: Hỗ trợ giao thức DAG mới nổi, thực hiện xác minh hiệu quả mà không cần 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 việc chứng minh cơ học hơn một vạn dòng mã Coq, trong đó mã kiểm tra an toàn và tính khả dụng lần lượt đạt 4000 dòng và 1700 dòng. Giáo sư Shao Zhong đã nhấn mạnh trong buổi diễn thuyết: "Hiện nay, giao thức đồng thuận PoS đang phải đối mặt với tình huống khó khăn khi không thể đạ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 đưa ra nhằm vượt qua tình huống này."
Đội ngũ do giáo sư Shao Zhong lãnh đạo trước đây đã phát triển CertiKOS, hệ điều hành "không có lỗi" đầu tiên trên thế giới thông qua xác minh hình thức, được coi là "một cột mốc trong an toàn hệ thống mạng vật lý". Thành tựu này không chỉ thể hiện sự tích lũy sâu sắc của ông trong lĩnh vực an toàn hệ thống mà còn đặt nền tảng cho nghiên cứu tiếp theo trong lĩnh vực an toàn blockchain. Năm 2017, giáo sư Shao Zhong bắt đầu nghiên cứu sâu về an toàn blockchain, áp dụng công nghệ xác minh hình thức vào bảo đảm an toàn 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 một lượng lớn tài sản mã hóa.
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 Zhong cho biết, họ cam kết 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ỳ, nhằm 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 Zhong nhấn mạnh: "Các giao thức mạng đá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ự."
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.
8 thích
Phần thưởng
8
5
Đăng lại
Chia sẻ
Bình luận
0/400
SchrodingerWallet
· 10giờ trước
Yale cũng chơi Byzantine, có thể làm được.
Xem bản gốcTrả lời0
NftMetaversePainter
· 10giờ trước
cuối cùng... có ai đó đang đề cập đến thẩm mỹ thuật toán của các giao thức đồng thuận. đây là thơ máy tính thuần khiết không nói dối.
Xem bản gốcTrả lời0
PensionDestroyer
· 10giờ trước
Giờ đây web3 có thể tự sửa lỗi rồi.
Xem bản gốcTrả lời0
AirdropATM
· 10giờ trước
Đợi một chút, đây không phải là viết một lớp bảo mật sao? Cũ rượu trong chai mới.
Xem bản gốcTrả lời0
SerumSqueezer
· 10giờ trước
Quá mạnh rồi, lại một chuyên nghiệp trong thế giới tiền điện tử.
Giáo sư Yale ra mắt mô hình LiDO hỗ trợ xác minh an toàn giao thức Web3 Nhận thức chung
Giáo sư Yale công bố công khai mô hình LiDO lần đầu tiên tại Hội nghị học giả Web3
Tại Hội nghị học giả Web3 năm 2025, 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ủ đề mang tên "Chứng minh an ninh và tính 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 giới thiệu mô hình LiDO mà nhóm của ông phát triển cùng với khung mở rộng LiDO-DAG. Thành tựu đổi mới này nhằm cung cấp chứng minh an ninh và tính hoạt động có thể được xác minh cơ học cho các giao thức đồng thuận chịu lỗi Byzantine (BFT) phức tạp, đặ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 của mình chỉ ra rằng các giao thức đồng thuận hiện có (như PBFT, Jolteon) mặc dù được ứng dụng rộng rãi, nhưng do việc triển khai phức tạp, 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 đã đề xuất một khung xác minh tinh chỉnh 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, hoàn thành việc chứng minh cơ học hơn một vạn dòng mã Coq, trong đó mã kiểm tra an toàn và tính khả dụng lần lượt đạt 4000 dòng và 1700 dòng. Giáo sư Shao Zhong đã nhấn mạnh trong buổi diễn thuyết: "Hiện nay, giao thức đồng thuận PoS đang phải đối mặt với tình huống khó khăn khi không thể đạ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 đưa ra nhằm vượt qua tình huống này."
Đội ngũ do giáo sư Shao Zhong lãnh đạo trước đây đã phát triển CertiKOS, hệ điều hành "không có lỗi" đầu tiên trên thế giới thông qua xác minh hình thức, được coi là "một cột mốc trong an toàn hệ thống mạng vật lý". Thành tựu này không chỉ thể hiện sự tích lũy sâu sắc của ông trong lĩnh vực an toàn hệ thống mà còn đặt nền tảng cho nghiên cứu tiếp theo trong lĩnh vực an toàn blockchain. Năm 2017, giáo sư Shao Zhong bắt đầu nghiên cứu sâu về an toàn blockchain, áp dụng công nghệ xác minh hình thức vào bảo đảm an toàn 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 một lượng lớn tài sản mã hóa.
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 Zhong cho biết, họ cam kết 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ỳ, nhằm 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 Zhong nhấn mạnh: "Các giao thức mạng đá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ự."