في قمة علماء Web3، أستاذ من جامعة ييل يشارك تقدم أبحاث أمان بروتوكول الإجماع

في قمة علماء Web3 لعام 2025، ألقى الأستاذ شاو تشونغ من قسم علوم الكمبيوتر بجامعة ييل خطاباً بعنوان "إثبات الأمان والنشاط للبروتوكول المعتمد على التنقيح: LiDO وتوسيعه"، حيث كشف النقاب عن نموذج LiDO وإطار LiDO-DAG الذي طوره فريقه. تهدف هذه النتيجة المبتكرة إلى توفير إثباتات الأمان والنشاط القابلة للتحقق الآلي لبروتوكولات الإجماع المعقدة لتحمل أخطاء بيزنطية (BFT)، مما يضع الأساس التقني لموثوقية وتوسع بيئة Web3.

أشار البروفيسور شاو تشونغ في خطابه إلى أن بروتوكولات الإجماع الحالية (مثل PBFT و Jolteon) على الرغم من استخدامها على نطاق واسع، إلا أن تعقيد تنفيذها غالبًا ما يخفي ثغرات محتملة. لحل هذه المشكلة، قدم نموذج LiDO بشكل مبتكر إطار تحقق مفصل من ثلاث طبقات:

1. طبقة التجريد الآمنة: تحويل البروتوكول إلى آلة حالة خطية، لضمان اتساق السجلات (الأمان)؛
2. طبقة الضمان النشط: إدخال آلية "Pacemaker"، من خلال بث المهلة ومزامنة الجولات لحل مشكلة تأخير الشبكة؛
3. طبقة التوسع DAG: تدعم بروتوكولات DAG الناشئة مثل Narwhal و Bullshark، مما يحقق التحقق الفعال بدون قيادي للإجماع.

في الوقت الحالي، تم تطبيق LiDO بنجاح على بروتوكول صناعي Jolteon (BFT ذو المرحلتين) والعديد من بروتوكولات DAG، وتم إنجاز إثبات ميكانيكي لأكثر من عشرة آلاف سطر من كود Coq، حيث بلغ حجم كود التحقق من الأمان 4000 سطر وكود التحقق من النشاط 1700 سطر. أشار البروفيسور شاو تشونغ في حديثه إلى: "حالياً، تواجه بروتوكولات إجماع PoS عمومًا صعوبة في تحقيق الأمان والنشاط واللامركزية في آن واحد. نموذج LiDO هو بالضبط الحل التصميمي المنهجي المقترح لكسر هذه المعضلة."

من الجدير بالذكر أن البروفيسور شاو زونغ قاد فريقه لتطوير CertiKOS، وهو أول نظام تشغيل "خالي من الثغرات" يتم التحقق منه من خلال التحقق الرسمي على مستوى العالم، ويُعتبر "معلمًا في أمان الأنظمة الفيزيائية الشبكية". لا تضع هذه الإنجازات فقط الأساس العميق له في مجال أمان النظام، بل توفر أيضًا قاعدة قوية لأبحاث أمان blockchain المستقبلية. في عام 2017، أدخل البروفيسور شاو زونغ وطلابه البروفيسور غو رونغ هوي تقنية التحقق الرسمي في مجال أمان العقود الذكية وبروتوكولات السلسلة، مما قدم دعمًا مهمًا لأمان الأصول المشفرة.

لقد أكملت LiDO حاليًا تصميم النموذج والتحقق الرسمي، وبدأت في استكشاف إمكانية التكامل مع سلاسل الكتل الرئيسية وبروتوكولات اللامركزية. وذكر الأستاذ شاو تشونغ أنهم ملتزمون بالتحقق من الآليات الأساسية في Web3.0، لتقديم منتجات وخدمات على مدار الدورة الكاملة، ودعم الاستراتيجية طويلة الأجل لشركات Web3 والبيئة. في نهاية الخطاب، أكد الأستاذ شاو تشونغ: "ستكون البروتوكولات الشبكية القابلة للثقة والآمنة والقابلة للتحقق هي المسار الرئيسي نحو مستقبل لامركزي حقيقي."