تعتمد أمان البيتكوين والسلاسل الأخرى، مثل ليكويد، على استخدام خوارزميات التوقيعات الرقمية مثل ECDSA وتوقيعات شنور. تُستخدم مكتبة C تُسمى libsecp256k1، تحمل اسم المنحنى الإهليلجي الذي تعمل عليه المكتبة، من قبل كل من بيتكوين كور وليكويد لتقديم هذه الخوارزميات الرقمية للتوقيعات. تعتمد هذه الخوارزميات على عملية حسابية رياضية تسمى العكس المعياري، وهو جزء مكلف نسبيًا من الحساب.
الفجوة بين الخوارزمية والتطبيق
أظهرت جهود العام 2021 فقط أن الخوارزمية التي صممها برنستين ويانغ تعمل بشكل صحيح. ومع ذلك، يتطلب استخدام هذه الخوارزمية في libsecp256k1 تطبيق الوصف الرياضي لخوارزمية safegcd ضمن لغة البرمجة C. على سبيل المثال، يقوم الوصف الرياضي للخوارزمية بضرب المصفوفات التي يمكن أن تكون بعرض 256 بت، ولكن لغة C توفر أعداد صحيحة تصل إلى 64 بت (أو 128 بت مع بعض امتدادات اللغة).
- يتطلب تنفيذ خوارزمية safegcd برمجة ضرب المصفوفات والحسابات الأخرى باستخدام أعداد C ذات 64 بت.
- تمت إضافة العديد من التحسينات الأخرى لجعل التنفيذ سريعًا.
في النهاية هناك أربعة تطبيقات منفصلة لخوارزمية safegcd في libsecp256k1: خوارزميتان ثابتتا الوقت لتوليد التوقيعات، واحدة مخصصة للأنظمة ذات 32 بت والأخرى للأنظمة ذات 64 بت، وخوارزميتان متغيرتا الوقت للتحقق من صحة التوقيعات، مرة أخرى واحدة للأنظمة ذات 32 بت والأخرى للأنظمة ذات 64 بت.
C القابلة للتحقق
للتحقق من أن كود C ينفذ خوارزمية safegcd بشكل صحيح، يجب فحص كافة تفاصيل التنفيذ. نستخدم C القابلة للتحقق، وهي جزء من سلسلة أدوات البرمجيات الموثوقة للاستدلال على كود C باستخدام مثبت النظريات Coq.
يتم التحقق بتحديد الشروط المسبقة واللاحقة باستخدام منطق الفصل لكل وظيفة تخضع للتحقق. يبدأ التحقق من الشروط المسبقة للوظيفة، ويتم إنشاء حالة جديدة بعد كل عبارة في جسم الوظيفة، حتى إنشاء الشرط اللاحق في نهاية جسم الوظيفة أو نهاية كل عبارة إرجاع.
النتيجة النهائية هي إثبات رسمي، يتم التحقق منه بواسطة مساعد الإثبات Coq، أن تنفيذ libsecp256k1 لخوارزمية العكس المعياري safegcd ذات الوقت المتغير 64 بت صحيحة وظيفيًا.
قيود التحقق
هناك بعض القيود على إثبات الدقة الوظيفية. منطق الفصل المستخدم في C القابلة للتحقق ينفذ ما يعرف بالدقة الجزئية. هذا يعني أنه يثبت فقط أن كود C يعود مع النتيجة الصحيحة إذا عاد، ولكنه لا يثبت نفسه. نحن نتجاوز هذا القيد باستخدام إثبات Coq السابق لحدود على خوارزمية safegcd لإثبات أن قيمة عداد الحلقة الرئيسية لا تتجاوز في الواقع 11 دورة.
مسألة أخرى هي أن لغة C نفسها ليس لها مواصفات رسمية. بدلاً من ذلك، يستخدم مشروع C القابلة للتحقق مشروع المترجم CompCert لتوفير مواصفات رسمية للغة C. يضمن ذلك أنه عندما يتم تجميع برنامج C الذي تم التحقق منه باستخدام المترجم CompCert، فإن كود التجميع الناتج سيلبي مواصفاته. ومع ذلك، لا يضمن ذلك أن الكود الناتج عن GCC أو clang أو أي مترجم آخر سيعمل بالضرورة.
أخيرًا، لا تدعم C القابلة للتحقق تمرير التركيبات، إعادة التركيبات أو تعيين التركيبات. بينما في libsecp256k1، يتم دائمًا تمرير التركيبات بواسطة المؤشر (وهو ما يُسمح به في C القابلة للتحقق)، هناك بعض الحالات التي يتم فيها استخدام تعيين التركيبات. بالنسبة لإثبات صحة العكس المعياري، كان هناك 3 تعيينات كان يجب استبدالها باستدعاء وظيفة متخصصة تقوم بتنفيذ تعيين الحقل بواسطة الحقل.
الملخص
قامت Blockstream Research بالتحقق رسميًا من صحة وظيفة العكس المعياري في libsecp256k1. يقدم هذا العمل دليلًا إضافيًا على أن التحقق من كود C ممكن فعليًا. يتيح لنا استخدام مساعد الإثبات العام التحقق من البرمجيات التي تعتمد على حجج رياضية معقدة.
- لا شيء يمنع باقي الوظائف التي تم تنفيذها في libsecp256k1 من التحقق منها أيضًا.
- وبالتالي، يمكن لـ libsecp256k1 الحصول على أعلى ضمانات الدقة الممكنة للبرمجيات.
هذا مقال ضيف بقلم راسل أكونور وأندرو بويلسترا. الآراء المعبر عنها هي آراء خاصة بهم ولا تعكس بالضرورة آراء BTC Inc أو Bitcoin Magazine.
الأسئلة الشائعة
- ما هو الدور الأساسي لمكتبة libsecp256k1 في البيتكوين وليكويد؟
- كيف تتحقق C القابلة للتحقق من صحة خوارزمية safegcd؟
- ما هي القيود المرتبطة بالتحقق من خوارزمية safegcd؟
تستخدم مكتبة libsecp256k1 لتوفير خوارزميات التوقيعات الرقمية مثل ECDSA وتوقيعات شنور، والتي تعتبر أساسية لأمان البيتكوين وسلسلة ليكويد.
تتحقق C القابلة للتحقق من صحة خوارزمية safegcd عن طريق استخدام منطق الفصل لتحديد الشروط المسبقة واللاحقة لكل وظيفة، والبدء من الشرط المسبق للوصول إلى الشرط اللاحق في نهاية كل وظيفة.
تشمل القيود حقيقة أن دقة التحقق تكون جزئية ولا تضمن إنهاء الكود، بالإضافة إلى عدم وجود مواصفات رسمية للغة C نفسها.
