في قمة علماء Web3، أطلق الأستاذ شاو تشونغ نموذج LiDO، لتعزيز أمان بروتوكول الإجماع.

عُقدت قمة علماء 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. في نهاية العرض، أكد البروفيسور شاو جونغ: "ستكون البروتوكولات الشبكية الموثوقة والآمنة والقابلة للتحقق هي المسار الرئيسي نحو مستقبل لامركزي حقيقي."