اجرای Safegcd به طور رسمی تأیید شد
به گزارش زوم ارز، امنیت بیت‌کوین و سایر بلاک‌چین‌ها، از الگوریتم‌های امضای دیجیتال مانند امضای ECDSA و Schnorr وابسته است. به منظور استفاده از این الگوریتم‌ها، کتابخانه C با نام libsecp256k1 به کار می‌رود که بر اساس منحنی بیضی کار می‌کند. این کتابخانه توسط Bitcoin Core و Liquid برای ارائه الگوریتم‌های امضای دیجیتال به کار می‌رود. این الگوریتم‌ها از یک محاسبات ریاضی به نام معکوس مدولار استفاده می‌کنند که به لحاظ محاسباتی هزینه‌بر می‌باشد.
برای اطلاع از تمامی اخبار کانال تلگرام ما را دنبال کنید
در «محاسبات سریع gcd با زمان ثابت و وارونگی مدولار»، دانیل جی. برنشتاین و بو-یین یانگ یک الگوریتم جدید برای محاسبه gcd به کمک وارونگی مدولار ارائه دادند. در سال ۲۰۲۱، این الگوریتم، که به آن “safegcd” معروف است، توسط پیتر دتمن برای libsecp256k1 پیاده‌سازی شد. به عنوان بخشی از ارزیابی این الگوریتم جدید، Blockstream Research اولین بار اثبات رسمی طراحی الگوریتم را با استفاده از دستیار اثبات Coq انجام داد تا تضمین کند که الگوریتم به درستی نتایج معکوس مدولار را در ۲۵۶ بیت ارائه می‌دهد.
شکاف بین الگوریتم و پیاده سازی
تجربه رسمی در سال ۲۰۲۱ نشان داد که الگوریتم ارائه شده توسط برنشتاین و یانگ با موفقیت عمل می‌کند. با این حال، اجرای این الگوریتم در libsecp256k1 نیازمند ارائه توضیحات ریاضی الگوریتم safegcd در زبان برنامه‌نویسی C است. به عنوان مثال، توضیح ریاضی الگوریتم، عملیات ضرب ماتریسی بردارهایی را انجام می‌دهد که ممکن است به اندازه‌ای باشند که شامل اعداد صحیح ۲۵۶ بیتی باشند، اما زبان برنامه‌نویسی C به صورت پیش‌فرض اعداد صحیح را تا ۶۴ بیت (یا حتی ۱۲۸ بیت با برخی افزونه‌های زبان) محدود می‌کند.
پیاده‌سازی الگوریتم safegcd از C باید بهینه‌سازی‌های مختلفی را شامل شود تا با استفاده از اعداد صحیح ۶۴ بیتی سریع اجرا شود. علاوه بر این، در libsecp256k1 چهار پیاده‌سازی جداگانه از الگوریتم safegcd وجود دارد. این شامل دو الگوریتم با زمان ثابت برای تولید امضا (یکی برای سیستم‌های ۳۲ بیتی و دیگری برای سیستم‌های ۶۴ بیتی) و دو الگوریتم با زمان متغیر برای تأیید امضا (یکی برای سیستم‌های ۳۲ بیتی و یکی برای سیستم‌های ۶۴ بیتی) می‌باشد.
C قابل تأیید
برای تضمین صحت پیاده‌سازی الگوریتم safegcd در زبان برنامه‌نویسی C، لازم است که تمام جوانب پیاده‌سازی دقیقا بررسی شود. ما از “Verifiable C” که جزء Verified Software Toolchain استفاده می‌کنیم تا با استفاده از اثبات‌های قضاوتی به کمک نرم‌افزار Coq، بر روی کد C استدلال کنیم.
تصدیق با تعیین پیش‌و پس‌شرط‌ها با استفاده از منطق جداسازی، برای هر تابع که تصدیق می‌شود، ادامه می‌یابد. منطق جداسازی یک منطق فنی برای استقرار استدلال درباره زیر روال‌ها، مدیریت حافظه، همزمانی و موارد دیگر می‌باشد.
هنگامی که مشخصاتی به یک تابع داده می‌شود، تایید از طریق یک شرط اولیه اجرا می‌شود و پس از هر عبارت در بدنه تابع، یک تغییر ناپذیر جدید ایجاد می‌شود. این فرآیند تا زمانی که شرط پایانی در انتهای بدنه تابع یا هر عبارت بازگشتی بیشتر تلاش کند، ادامه پیدا می‌کند. در این فرآیند، تمرکز عمده‌ی آن به سمت رسمی‌سازی «بین» خطوط کد می‌رود و از متغیرهای ثابت برای تقدیم عملیات کلی هر عبارت C به عبارات سطح بالاتر درباره‌ی ساختار داده‌های تغییر داده‌شده ریاضی استفاده می‌شود. به عنوان مثال، یک آرایه از اعداد صحیح ۶۴ بیتی در زبان C، ممکن است در واقع نمایشی از یک عدد صحیح ۲۵۶ بیتی باشد.
نهایتا، نتیجه‌ی یک اثبات رسمی است که توسط دستیار اثبات Coq تأیید شده‌است و نشان می‌دهد که اجرای الگوریتم معکوس مدولار safegcd libsecp256k1 با طول زمان ۶۴ بیتی، از لحاظ عملکردی صحیح است.
محدودیت های تایید
برای اثبات صحت عملکرد، برخی محدودیت ها وجود دارد. منطق جداسازی که در اثبات صحت عملکرد C استفاده می شود، فقط اثبات می کند که اگر کد C به نتیجه صحیح برسد، درست است. اما خود نهایت این را ثابت نمی کند. با استفاده از اثبات Coq قبلی خود در مورد کران های الگوریتم safegcd، ما این محدودیت را کاهش می دهیم تا اثبات کنیم که مقدار شمارنده حلقه حلقه اصلی هرگز از ۱۱ تکرار تجاوز نمی کند.
| شاید دنبال کردن این اخبار برای شما مفید باشد: |
یکی از مسائل دیگر این است که زبان C خود اصول رسمی مشخصی ندارد. برای ارائه یک مشخصه رسمی برای زبان C، پروژه تأییدپذیر C از CompCert Compiler استفاده می‌کند. این اطمینان را می‌دهد که هنگام کامپایل یک برنامه C تأییدشده با CompCert Compiler، کد اسمبلی نهایی با استانداردهای تعیین شده منطبق خواهد بود. با این حال، این تضمین نمی‌تواند تضمین کند که برنامه‌های کامپایل شده توسط کامپایلرهای دیگر مانند GCC یا clang به درستی عمل کنند. به عنوان مثال، کامپایلرهای C ممکن است ترتیب ارزیابی متفاوتی برای آرگومان‌های تابع داشته باشند. حتی اگر زبان C دارای استانداردهای رسمی باشد، هر کامپایلر غیررسمی ممکن است برنامه‌ها را با خطا کامپایل کند که این مسأله در عمل اتفاق می‌افتد.
در پایان، تأییدپذیر C از ساختارهای عبوری، ساختارهای بازگشتی یا ساختارهای اختصاصی پشتیبانی نمی‌کند. در libsecp256k1، ساختارها همواره با استفاده از اشاره گر منتقل می‌شوند (که در تأیید پذیر C مجاز است). با این حال، تعدادی موارد وجود دارند که از تخصیص ساختار استفاده می‌کنند. به منظور اثبات درستی معکوس مدولار، ۳ تخصیص بود که باید با یک فراخوانی تابع تخصیصی جایگزین می‌شدند که تخصیص ساختار را فیلد به فیلد انجام می‌داد.
خلاصه
Blockstream Research به صورت رسمی تأیید کرده است که دقت عملکرد معکوس مدولار libsecp256k1 اثبات شده است. این اثبات شواهد بیشتری ارائه می دهد که نشان می دهد کد C قابل تأیید در عمل است. به کمک یک ابزار اثبات، ما می‌توانیم به طور کلی هدف این نرم افزار را تأیید کنیم که بر اساس داشته‌های ریاضی پیچیده ایجاد شده است.
هیچ موانعی وجود ندارد که از تأیید سایر توابع پیاده‌سازی شده در کتابخانه libsecp256k1 جلوگیری کند. به همین دلیل، این کتابخانه قادر است به بالاترین سطح تضمین درستی نرم‌افزار دست یابد.
این یک پست مهمان از طرف راسل اوکانر و اندرو پولسترا است. نظرات اعلام شده تماماً به خود ایشان خصوصی و بدون نیاز به نماینده از جمله شرکت BTC Inc یا مجله Bitcoin می‌باشد.
منبع: bitcoinmagazine.com
بیشتر بخوانید
نظرات کاربران