في قمة علماء Web3، أستاذ ييل يكشف عن نموذج LiDO لأول مرة
في القمة الأكاديمية Web3 لعام 2025 التي عُقدت مؤخرًا، ألقى الأستاذ تشاو زونغ من قسم علوم الحاسوب بجامعة ييل خطابًا بعنوان "التحقق من الأمان والحيوية في بروتوكولات الإجماع المعتمدة على التكرير: LiDO وتوسيعاتها"، حيث قدم للجمهور لأول مرة نموذج LiDO وإطار LiDO-DAG الذي طوره فريقه. تهدف هذه النتيجة الابتكارية إلى تقديم إثباتات قابلة للتحقق آليًا للأمان والحيوية لبروتوكولات الإجماع المعقدة المعروفة بالتحمل البيزنطي (BFT)، مما يمهد الطريق لموثوقية النظام البيئي Web3 وتطويره على نطاق واسع.
أشار البروفيسور شاو تشونغ في خطابه إلى أنه على الرغم من أن بروتوكولات الإجماع الحالية (مثل PBFT و Jolteon) تستخدم على نطاق واسع، إلا أن التعقيد في التنفيذ غالبًا ما يؤدي إلى مخاطر أمان محتملة. لحل هذه المشكلة، اقترح نموذج LiDO إطار تحقق مبتكر ثلاثي الطبقات:
طبقة التجريد الآمن: تحويل البروتوكول إلى آلة حالة خطية، لضمان تناسق السجلات، وضمان الأمان؛
طبقة ضمان النشاط: إدخال آلية "Pacemaker" لحل مشكلة تأخير الشبكة من خلال البث في حالة المهلة والتزامن عبر الجولات;
طبقة توسيع DAG: تدعم بروتوكولات DAG الناشئة مثل Narwhal و Bullshark، مما يحقق تحقق فعّال من الإجماع بدون قيادة.
حاليًا، تم تطبيق LiDO بنجاح على بروتوكول صناعي من الدرجة الأولى Jolteon (BFT من مرحلتين) بالإضافة إلى عدة بروتوكولات DAG، حيث تم إنجاز أكثر من عشرة آلاف سطر من إثباتات Coq الآلية، بلغ حجم الشيفرة الخاصة بالتحقق من الأمان والحيوية 4000 سطر و1700 سطر على التوالي. وأكد البروفيسور شاو تشونغ في حديثه: "حاليًا، تواجه بروتوكولات توافق PoS عمومًا صعوبة في تحقيق الأمان والحيوية واللامركزية في آن واحد. إن نموذج LiDO هو عبارة عن خطة تصميم منهجية تهدف إلى كسر هذه المعضلة."
قادت البروفيسورة شاو جونغ فريقًا طور CertiKOS، وهو أول نظام تشغيل "خالي من الثغرات" تم التحقق منه بشكل رسمي على مستوى العالم، والذي تمت الإشادة به من قبل الصناعة باعتباره "معلمًا في أمان الأنظمة الفيزيائية الشبكية". لا يقتصر هذا الإنجاز على وضع الأساس للتقنيات ذات الصلة، ولكنه يظهر أيضًا التراكم العميق لفريق العمل في مجال أمان الأنظمة. في السنوات الأخيرة، قامت البروفيسورة شاو جونغ بدراسة أمان blockchain بعمق، وفي عام 2017، أسست شركة أمان مع زملائها، حيث أدخلت تقنية التحقق الرسمي في ضمان أمان العقود الذكية وبروتوكولات السلسلة، مما وفر حماية أمنية لأصول تشفير تبلغ قيمتها آلاف الملايين من الدولارات.
لقد أكملت LiDO حاليًا تصميم النموذج والتحقق الرسمي، وبدأت في استكشاف إمكانية التكامل مع سلاسل الكتل الرئيسية والبروتوكولات اللامركزية. قال الأستاذ شاو تشونغ إنهم ملتزمون بالتحقق من الآليات الرئيسية في Web3.0 لتقديم منتجات وخدمات على مدار الدورة الكاملة، لدعم الاستراتيجيات طويلة الأجل لشركات وبيئات Web3 بشكل أفضل. في نهاية حديثه، أكد الأستاذ شاو تشونغ: "ستكون الشبكات البروتوكول الموثوقة والآمنة والقابلة للتحقق هي الطريق الرئيسي نحو مستقبل لامركزي حقيقي."
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
أصدر أستاذ جامعة ييل نموذج LiDO: لتوفير التحقق الرسمي لبروتوكول الإجماع في Web3
في قمة علماء Web3، أستاذ ييل يكشف عن نموذج LiDO لأول مرة
في القمة الأكاديمية Web3 لعام 2025 التي عُقدت مؤخرًا، ألقى الأستاذ تشاو زونغ من قسم علوم الحاسوب بجامعة ييل خطابًا بعنوان "التحقق من الأمان والحيوية في بروتوكولات الإجماع المعتمدة على التكرير: LiDO وتوسيعاتها"، حيث قدم للجمهور لأول مرة نموذج LiDO وإطار LiDO-DAG الذي طوره فريقه. تهدف هذه النتيجة الابتكارية إلى تقديم إثباتات قابلة للتحقق آليًا للأمان والحيوية لبروتوكولات الإجماع المعقدة المعروفة بالتحمل البيزنطي (BFT)، مما يمهد الطريق لموثوقية النظام البيئي Web3 وتطويره على نطاق واسع.
أشار البروفيسور شاو تشونغ في خطابه إلى أنه على الرغم من أن بروتوكولات الإجماع الحالية (مثل PBFT و Jolteon) تستخدم على نطاق واسع، إلا أن التعقيد في التنفيذ غالبًا ما يؤدي إلى مخاطر أمان محتملة. لحل هذه المشكلة، اقترح نموذج LiDO إطار تحقق مبتكر ثلاثي الطبقات:
حاليًا، تم تطبيق LiDO بنجاح على بروتوكول صناعي من الدرجة الأولى Jolteon (BFT من مرحلتين) بالإضافة إلى عدة بروتوكولات DAG، حيث تم إنجاز أكثر من عشرة آلاف سطر من إثباتات Coq الآلية، بلغ حجم الشيفرة الخاصة بالتحقق من الأمان والحيوية 4000 سطر و1700 سطر على التوالي. وأكد البروفيسور شاو تشونغ في حديثه: "حاليًا، تواجه بروتوكولات توافق PoS عمومًا صعوبة في تحقيق الأمان والحيوية واللامركزية في آن واحد. إن نموذج LiDO هو عبارة عن خطة تصميم منهجية تهدف إلى كسر هذه المعضلة."
قادت البروفيسورة شاو جونغ فريقًا طور CertiKOS، وهو أول نظام تشغيل "خالي من الثغرات" تم التحقق منه بشكل رسمي على مستوى العالم، والذي تمت الإشادة به من قبل الصناعة باعتباره "معلمًا في أمان الأنظمة الفيزيائية الشبكية". لا يقتصر هذا الإنجاز على وضع الأساس للتقنيات ذات الصلة، ولكنه يظهر أيضًا التراكم العميق لفريق العمل في مجال أمان الأنظمة. في السنوات الأخيرة، قامت البروفيسورة شاو جونغ بدراسة أمان blockchain بعمق، وفي عام 2017، أسست شركة أمان مع زملائها، حيث أدخلت تقنية التحقق الرسمي في ضمان أمان العقود الذكية وبروتوكولات السلسلة، مما وفر حماية أمنية لأصول تشفير تبلغ قيمتها آلاف الملايين من الدولارات.
لقد أكملت LiDO حاليًا تصميم النموذج والتحقق الرسمي، وبدأت في استكشاف إمكانية التكامل مع سلاسل الكتل الرئيسية والبروتوكولات اللامركزية. قال الأستاذ شاو تشونغ إنهم ملتزمون بالتحقق من الآليات الرئيسية في Web3.0 لتقديم منتجات وخدمات على مدار الدورة الكاملة، لدعم الاستراتيجيات طويلة الأجل لشركات وبيئات Web3 بشكل أفضل. في نهاية حديثه، أكد الأستاذ شاو تشونغ: "ستكون الشبكات البروتوكول الموثوقة والآمنة والقابلة للتحقق هي الطريق الرئيسي نحو مستقبل لامركزي حقيقي."