استجاب فيتاليك بوتيرين، المؤسس المشارك لشركة إيثريوم، للمخاوف المتزايدة من أن صيد الأخطاء القائم على الذكاء الاصطناعي سوف يطغى على المطورين ويخلق فرص استغلال متواصلة على بلوكتشين.
ووفقا له، في المستقبل القريب، فإن استخدام هذه التكنولوجيا قد يجعل أنظمة التشفير أكثر أمانًا. ويقول إن التحقق الرسمي بمساعدة الذكاء الاصطناعي قد يصبح أحد أقوى الدفاعات ضد الفشل الأمني في البنية التحتية للعملات المشفرة والإنترنت.
يمكن للذكاء الاصطناعي أن يعزز الأمن بدلاً من كسره
التحقق الرسمي هو ممارسة كتابة البراهين الرياضية حول البرامج التي يمكن للكمبيوتر التحقق منها تلقائيًا بدلاً من مراجعة الأشخاص لها. لقد كان هذا المفهوم متاحًا منذ عقود؛ ومع ذلك، لم ينتشر هذا الأمر أبدًا لأن إنشاء مثل هذه البراهين يدويًا كان أمرًا مملاً إلى حد ما بالنسبة لمطوري البرامج، لذلك لم يزعج الكثير منهم أبدًا.
الآن، يقول بوتيرين إن الذكاء الاصطناعي قد غيّر هذه المعادلة، وبدلاً من قيام المطورين بكتابة البراهين بأنفسهم، يمكنهم أن يطلبوا من الذكاء الاصطناعي كتابة كل من الكود والأدلة المصاحبة. ثم يتحققون ببساطة من أن البيان النهائي الذي تم إثباته هو في الواقع الشيء الذي يريدون إثباته.
وصف المطور سيناريو تصبح فيه نماذج الذكاء الاصطناعي قوية بما يكفي لأتمتة عملية العثور على الأخطاء في التعليمات البرمجية الموجودة، ثم تساءل عما قد يعنيه ذلك بالنسبة للأنظمة التي يمكن أن يكلف فيها خلل واحد المستخدمين كل شيء.
كانت إجابته هي أن التحقق الرسمي، الذي يتم إجراؤه من البداية إلى النهاية، يتيح لك إثبات رياضيًا أن جزءًا من التعليمات البرمجية يتصرف تمامًا كما هو مقصود، بحيث يبحث الذكاء الاصطناعي القوي بما فيه الكفاية عن العيوب في التعليمات البرمجية التي ثبت بالفعل أنها لا تحتوي على هذه العيوب.
كما أشار أيضًا إلى مشاريع محددة للبنية التحتية لإيثريوم حيث تتم تجربة هذا النهج بالفعل. إحدى هذه الشركات هي Arklib، التي تعمل على تنفيذ STARK تم التحقق منه رسميًا بالكامل. وهناك طريقة أخرى هي evm-asm، التي تقوم ببناء EVM مكتوبًا بتجميع RISC-V منخفض المستوى والتحقق من صحته مقابل تنفيذ مرجعي يمكن قراءته بواسطة الإنسان.
وفيما يتعلق بسؤال ما هي نماذج الذكاء الاصطناعي المفيدة بالفعل لهذا الغرض، قال بوتيرين إنه وجد كلود وديبسيك 4 برو كافيين لكتابة البراهين اللينة.
كما أشار أيضًا إلى Leanstral، وهو نموذج أصغر حجمًا للأوزان المفتوحة تم ضبطه خصيصًا ليناسب Lean، باعتباره قادرًا على التشغيل محليًا والتفوق في الأداء على نماذج الأغراض العامة الأكبر حجمًا وفقًا لمعايير التحقق الرسمية.
ولكن هناك قيود
وعلى الرغم من حماسه للتحقق الرسمي، فقد خصص بوتيرين أيضًا جزءًا كبيرًا من مقالته لشرح الطرق التي فشلت بها هذه العملية في الممارسة العملية.
يتضمن ذلك الأخطاء الموجودة في المترجمين الذين تم التحقق منهم؛ المكتبات التي تم إثبات جزء فقط من الكود فيها، وتبين أن الأجزاء غير المثبتة هي المشكلة؛ والمواصفات التي تم إثباتها تقنيًا ولكنها ببساطة لم تعكس ما أراد المطور ضمانه بالفعل.
ومع ذلك، فإن إطاره الأوسع هو أن التحقق الرسمي ليس بديلاً لجميع الممارسات الأمنية، ولكنه أداة قوية في اتجاه طويل الأمد نحو عدد أقل من الأخطاء لكل سطر من التعليمات البرمجية.
الخلفية ذات صلة هنا، مع الأخذ في الاعتبار أنه في اليوم الذي ظهر فيه منشور Buterin، كان قطاع العملات المشفرة يعاني من ثغرة كبرى ثالثة في أربعة أيام فقط بعد أن سرق أحد المتسللين ما قيمته أكثر من 76 مليون دولار من العملات المشفرة من الجسر عبر السلسلة لبروتوكول Echo.
وقبل ذلك بأيام، ظهرت تقارير بشأن اختراق THORChain، والذي كلف المنصة أكثر من 10 ملايين دولار.
وحدث هجوم آخر بعد ذلك الهجوم، استهدف جسر Verus-Ethereum، حيث استغل أحد المتسللين عدم وجود فحص التحقق من الصحة لسرقة 11.58 مليون دولار. هذا هو نوع الخلل الموضعي المحدد الذي ربما اكتشفه فحص الإثبات الرسمي.
يقول فيتاليك بوتيرين إن الذكاء الاصطناعي يمكن أن يعزز أمن العملات المشفرة ظهر لأول مرة على CryptoPotato.
