Runtime Verification أثبتت أن Algorand لا يمكن أن تنقسم — وأداة KAVM الخاصة بها خاملة منذ 2023

2026-08-19

formal-verification · security · audits · consensus · kavm · discovery · web · updated

نظرية أمان مثبتة آليًا

في عام 2019، سلّم فريق Algorand بروتوكول الإجماع الخاص به إلى شركة ناشئة صغيرة في Champaign-Urbana وطلب شيئًا نادرًا ما كلّفت به أي بلوك تشين: إثباتًا آليًا أن البروتوكول لا يمكن أن ينقسم أبدًا. Runtime Verification، التي كانت حينها معروفة بتطبيق الأساليب الرسمية على أكواد الطيران والسيارات، قدّمت هذا الإثبات باستخدام Coq، وهي أداة تفاعلية للمساعدة في الإثبات.

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

الخاصية التي أثبتتها RV هي الأمان غير المتزامن: لا يمكن لعقدتين صادقتين أن تشهدا على كتل مختلفة لنفس الجولة، حتى عندما يتقسم الشبكة بشكل سيء لدرجة أن مجموعات العقد لا تستطيع الوصول إلى بعضها. هذا الضمان هو الأساس الرياضي لـ النهائية بكتلة واحدة - الخاصية التي تجعل الكتلة المؤكدة دائمة، دون فترة انتظار احتمالية لتأكيدات إضافية. إعلان Algorand في ذلك الوقت وصف السلسلة بأنها 'أول بلوك تشين توفر نهائية فورية للمعاملات.'

النموذج، الذي نشر في يونيو 2019 من قبل باحثي RV: Musab Alturki وBrandon Moore وKarl Palmskog وLucas Pena، قسم نظرية السلامة إلى حوالي 170 ليمّا وحدد الافتراضات التي يستند إليها الضمان، بما في ذلك أن أغلبية ساحقة من التخزين محتفظ بها من قبل مستخدمين صادقين. مستودع algorand-verification لا يزال عامًا، مع تحديثات صيانة حتى عام 2022. عمل خبراء بروتوكول Algorand: Jing Chen وNickolai Zeldovich وVictor Luchangco جنبًا إلى جنب مع فريق RV في هذا التعاقد.

من نظريات البروتوكول إلى منصة تدقيق DeFi

التعاقد الذي تم في عام 2019 تحول إلى علاقة دائمة. في يوليو 2020، منحت مؤسسة Algorand شركة RV منحة ضمن برنامج المنح البيئي بقيمة 250 مليون ALGO لبناء إطار دلالي رسمي لعقود Algorand الذكية باستخدام إطار K، وهو 'لغة برمجة لتعريف لغات البرمجة' من RV - نظام يتيح للمهندسين تحديد سلوك لغة ما مرة واحدة واشتقاق المفسرات والمصححات وأدوات التحقق تلقائيًا من هذا التعريف. اقتراح المشروع الأصلي كان يهدف إلى إضفاء الطابع الرسمي على لغة عالية المستوى مشتقة من Clarity الخاص بـ Blockstack؛ بحلول وقت إصدار النسخة التجريبية العامة في عام 2023، استقر العمل على آلة Algorand الافتراضية (AVM)، محرك التنفيذ للعقود الذكية في Algorand، وTEAL، اللغة الشبيهة بالتجميع التي يفسرها AVM، والتي كانت Algorand قد أطلقتها في هذه الأثناء.

في ديسمبر 2021، أعلنت RV أنها أصبحت الشريك الأمني للمؤسسة. قال آدي واجنكنخت، الذي كان حينها رئيس العمليات العالمية والتقنية في المؤسسة: 'نتطلع إلى شراكتنا ونرحب بشركة Runtime Verification Inc كشريك أمني لنا'. تبع ذلك عمل تدقيق على نطاق واسع: بين يوليو 2021 وديسمبر 2022، نشرت RV ثلاثة عشر مهمة تدقيق شملت الموجة الأولى من تطبيقات DeFi في النظام البيئي — مثل مجمعات AMM، وهي مجمعات عقود ذكية تسعّر الصفقات بمعادلة بدلاً من دفتر الأوامر، إلى جانب الإقراض، التخزين السائل والعملات المستقرة.

الفكرة	الأثر الواقعي
Tinyman AMM V2 (ديسمبر 2022)	أكبر AMM في Algorand خضع لمراجعة خمسة أسابيع قبل إطلاق مقايضات الفلاش وقروض الفلاش ورسوم المجمعات القابلة للتكوين
Pact وPact Router وPact Stableswap (فبراير-أغسطس 2022)	تم تدقيق مجمعات AMM الأساسية وعقد التوجيه متعدد المجمعات والثابت الرياضي لـ stableswap كل على حدة
Algofi Lending v2 (أغسطس 2022)	أسواق الإقراض لـ ALGO وASA، والعملة المستقرة STBL2، وخزينة ضمانات الحوكمة تمت مراجعتها في مهمة واحدة
xBacked (سبتمبر 2022)	الخزائن الرئيسية ومجمع الاستقرار لعملة مستقرة مضمونة بأكثر من قيمة الضمان، تم تدقيقها بـ Reach، وهي لغة عقود ذكية متخصصة
Hone Liquid Staking (سبتمبر 2022)	تخزين مكافآت الحوكمة الذي يسك الرمز السائل dALGO؛ أدى التدقيق إلى تقليل تصميم من عقدين إلى عقد واحد
EXA Finance Baskets (مايو 2022)	تداول نظير إلى نظير لسلال تصل إلى أربعة أصول عبر أربعة نماذج تبادل
Folks Finance وYieldly وXET وعقود مكافآت الحوكمة (2021-22)	الإقراض، والتخزين متعدد الرموز، ونشر الرموز، وآلية الحوكمة المجتمعية من الموجة الأولى

المنهجية كانت متسقة عبر المنصة: قام المدققون بإعادة بناء الثوابت — الخصائص التي يجب أن تتحقق لكي يكون النظام آمنًا — من وثائق البروتوكول، راجعوا الكود على السلسلة سطرًا سطرًا، ثم قاموا بمحاكاة أعداد كبيرة من السلوكيات الخصومية باستخدام أدوات داخلية مثل pyteal_eval وtstmodel. حيث كانت العقود مكتوبة بـ Tealish، راجعت RV أيضًا مخرجات TEAL من المترجم حتى لا يضطر التدقيق إلى الثقة بالمترجم. بموجب الشراكة، راجعت RV أيضًا StakerDAO وAlgoDex في عام 2021. أبرز نتيجة في هذه الدفعة: المراجعة الأولى لـ xBacked أظهرت خمسة اكتشافات عالية الخطورة، وواحد متوسط، وواحد إعلامي، مع جولة ثانية أضافت اكتشافين متوسطين وإعلامي آخر. في كل مهمة من مهام 2022، عالج الفريق المدقَق القضايا قبل الإطلاق.

KAVM: أداة الإثبات التي اكتشفت خطأ تقريب

المنتج الذي تم تمويله صار متاحًا للعموم في مارس 2023 باسم KAVM — وهو الدلالات الرسمية لآلة Algorand الافتراضية، المبنية على K — وقد قُدم كطريقة للتحقق الرسمي من عقود Algorand الذكية 'دون الحاجة بالضرورة إلى درجة الدكتوراه في علوم الحاسوب'. اندمج KAVM مع PyTeal، إطار Python الخاص بـ Algorand لكتابة العقود الذكية، ومع py-algorand-sdk؛ ونشرت التدوينة التعليمية لإطلاقه عقد K Coin Vault لبيان ما يمكن للأداة فعله.

العرض التوضيحي هو أوضح مثال على لماذا يبرر التحقق الرسمي وجوده على السلسلة. العقود الذكية تحسب بأعداد صحيحة ذات نقطة ثابتة، وليس بأعداد فاصلة عائمة، لذا فإن ترتيب العمليات في تعبير حسابي يغير النتيجة: X مضروبًا في Y ثم مقسومًا على Z ليس هو نفسه X مقسومًا على Z ثم مضروبًا في Y، بمجرد تدخل التقريب. طريقة الحرق في الخزينة كانت تقسم على سعر الصرف قبل التوسيع — كود يبدو صحيحًا لكنه يعيد صفرًا بصمت لمبالغ الحرق الصغيرة. مُثبت KAVM أشار إلى الطريقة لأن التعبير الرمزي لمخرجاتها لم يتطابق مع الشرط اللاحق الذي حدده المطور؛ مجموعة اختبار تقليدية باستخدام أرقام دائرية نجحت في اجتياز نفس الكود. إنها بالتحديد فئة الخطأ — خسارة أموال المستخدمين بسبب الحساب — التي تدرجها منهجية التدقيق في RV ضمن فحوصاتها القياسية.

الفكرة	الأثر الواقعي
مزخرفات @router.precondition و@router.postcondition على طرق ABI في PyTeal	يطور المطور الافتراضات والمخرجات المتوقعة مباشرة في كود العقد؛ يتحقق المُثبت من التطبيق وفقًا لها
تكامل kavm.algod مع py-algorand-sdk	يمكن للنصوص البرمجية للنشر والاختبار الحالية العمل مع KAVM كبديل عن عقدة حية، وليس فقط ضد صندوق الرمل
تكامل AlgoKit المخطط له	كان سيجعل KAVM بديلًا مباشرًا لصندوق رمل Algorand، مما يجلب التحقق إلى أي مشروع AlgoKit

ثم توقف التطوير. لا يزال ملف README الخاص بـ KAVM يحمل شارة 'عمل قيد التقدم'، ويسرد الإثبات الرمزي ('kavm prove') بأنه 'لم يُنفذ بعد'، ويحذر من أن إثباتات المواصفات 'لم تُنقل بعد بالكامل إلى الدلالات الحالية وهي فاشلة'. ليست كل أوامر TEAL مدعومة، والاستدعاءات من عقد إلى عقد غائبة. آخر التزام في المستودع هو تحديث تبعية روتيني بتاريخ 2 أغسطس 2023؛ آخر مساس بمستودع العرض التوضيحي كان في يناير 2024. أظهر KAVM النهج على عقد واحد ولم يصبح أداة مطور مدعومة وموثقة كما وعدت تدوينة الإطلاق — نسخة تجريبية صدرت ثم صمتت.

عقدة ترحيل للمراقبة اللحظية

بعد ثلاثة أسابيع من آخر التزام في KAVM، أعلنت RV عن نوع مختلف من المساهمات في Algorand: عقدة ترحيل مسجلة. عُقد الترحيل هي العمود الفقري للشبكة — عُقد أرشيفية تحتفظ بنسخ كاملة من السجل، وتتحقق من المعاملات وتعيد بثها، وتظهر في سجلات DNS SRV الخاصة بـ Algorand حتى تتمكن عُقد المشاركة من اكتشافها والاتصال بها. في ذلك الوقت كان هناك حوالي 110 عقدة ترحيل مسجلة، من بينها عقدة RV.

كانت عقدة الترحيل تخدم أجندة مراقبة. كانت خطة RV هي تحويل الثوابت المثبتة أثناء التدقيقات إلى مراقبين في وقت التشغيل يشاهدون العقود المنشورة ويمكنهم تشغيل معاملات استرداد عند انكسار خاصية — على سبيل المثال، الإشارة إلى قرض غير مضمون بدرجة كافية قبل أن يضر بروتوكول الإقراض. معظم خدمات الفهرسة بطيئة جدًا لهذه المهمة، لذا فإن تشغيل عقدة ترحيل أعطى RV مراقبة مباشرة منخفضة الكمون لتدفق معاملات الشبكة. ما إذا كانت عقدة الترحيل هذه لا تزال مسجلة اليوم غير مؤكد: انتقلت وثائقها خلف تسجيل دخول GitBook، ولا يوجد لقطة لها في Wayback Machine، ومجموعة سجلات SRV الحالية لا تحدد بوضوح اسم مضيف RV.

الشركة في عصر الذكاء الاصطناعي — وسلسلة أدوات Algorand الخاملة

تتصدر Runtime Verification اليوم صفحتها الرئيسية بعبارة 'ضمان البرمجيات لعصر الذكاء الاصطناعي' وأعادت تنظيم خدماتها حول ثلاثة خطوط.

الفكرة	الأثر الواقعي
ضمان جودة البرمجيات	عمل التدقيق الأساسي — النمذجة، تحديد الخصائص، الفيزينغ والتحقق الرسمي — للفرق التي 'لا يمكنها تحمل فشل البرمجيات'
شراكات البيانات	تقدم RV سنوات عملها في النمذجة والتحقق كبيانات تدريب لنماذج اللغات الكبيرة لتعلم ممارسات هندسية عالية الجودة
ضوابط الوكلاء	تطبيق سياسات الأمان للوكلاء الأذكياء: معرفة ما يمكن للوكيل فعله، وإثبات بقائه ضمن الحدود، واكتشاف الانتهاكات

الشركة حقيقية ومشغولة. تأسست عام 2010 من جامعة إلينوي في أوربانا-شامبين، وتضم أكثر من 25 مهندسًا كبيرًا، ومتوسط مدة عمل 4 سنوات، وإرث مع ناسا (ثلاث منح متتالية من SBIR) وشركة Boeing. أعمالها الحالية البارزة هي عبر السلاسل: مراجعة ما قبل الإطلاق لـ Monad، وتدقيقات لعقود التخزين في Espresso وVM الخاص بـ Stellar Soroban، وتقوية مترجم WASMI، وتحقق رسمي من برامج معيار الرموز في Solana. يصف الرئيس التنفيذي Everett Hildenbrandt معيار التعاقد بوضوح: 'تقرير تدقيق Runtime Verification هو ختم موافقة من فريقنا.' منتجها النشط للتحقق من العقود الذكية يركز على إيثريوم: Kontrol، المبني على دلالات KEVM، كان لديه التزامات حديثة حتى أغسطس 2026.

الجانب الخاص بـ Algorand يروي قصة مختلفة. لم يظهر أي منشور بوسم Algorand على مدونة RV منذ أغسطس 2023، وصفحة الشراكة المخصصة مع Algorand التي كانت تؤرشف الخط الزمني الكامل للتعاقد أصبحت الآن تُحوّل إلى الصفحة الرئيسية. لم ينسَ مجتمع Algorand العلاقة — فقد استشهدت خيوط المنتدى منذ 2019 مرارًا بإثبات الأمان ضد انتقادات البروتوكول، وفي يونيو 2026 نشر اقتراح حوكمة يوصي بتدقيق طرف ثالث اسم Runtime Verification — لكن الشهية للتحقق الرسمي من AVM تجاوزت تطوير KAVM. في مايو 2023، طلب اقتراح مجتمعي (xGov-18) مبلغ 250,000 ALGO لإكمال مكتبة AVM إصدار 8 مبنية على Coq، وتم تأطيره صراحةً كـ 'بديل لمكتبة دلالات AVM الخاصة بإطار K'؛ تم دمج طلب السحب للاقتراح في مستودع xGov، وكانت المكتبة في ذلك الوقت تدعم تنفيذ 25 أمرًا من أوامر AVM.

ما يبقى لـ Algorand هو تلك النظرية من عام 2019: الإثبات الآلي لا يزال علنيًا وغير ملغى، وتقارير التدقيق من موجة DeFi لا تزال في مستودع RV العام. لكن على المطور الذي يطلق عقد Algorand جادًا اليوم أن يعلم أن KAVM ليس خيار تحقق مدعومًا — مسار الضمان العملي هو تدقيق تقليدي، أو الاستدلال نصف الرسمي على الثوابت الذي تصفه إرشادات مطوري Algorand نفسها. الفجوة بين ما أثبته تعاقد 2019 وما قدمه مسار الأدوات في النهاية هي المقياس الصادق للعلاقة: إثبات تأسيسي، ومنصة تدقيق قوية، وأداة رئيسية لم تصل إلى الإنتاج.

المصادر

Source: https://runtimeverification.com/