اجرای Safegcd به طور رسمی تأیید شد

مقدمه

امنیت بیت کوین و سایر بلاک چین ها مانند Liquid به استفاده از الگوریتم های امضای دیجیتال مانند امضای ECDSA و Schnorr بستگی دارد. کتابخانه AC به نام libsecp256k1، که از روی منحنی بیضی که کتابخانه روی آن کار می کند نامگذاری شده است، هم توسط Bitcoin Core و هم Liquid برای ارائه این الگوریتم های امضای دیجیتال استفاده می شود. این الگوریتم ها از یک محاسبات ریاضی به نام a استفاده می کنند معکوس مدولار، که جزء نسبتاً گران محاسبات است.

در «محاسبات سریع gcd با زمان ثابت و وارونگی مدولار»، Daniel J. Bernstein و Bo-Yin Yang یک الگوریتم وارونگی مدولار جدید توسعه دادند. در سال 2021، این الگوریتم که به آن “safegcd” گفته می شود، برای libsecp256k1 توسط پیتر دتمن پیاده سازی شد. به عنوان بخشی از فرآیند بررسی برای این الگوریتم جدید، Blockstream Research برای اولین بار تأیید رسمی طراحی الگوریتم را با استفاده از دستیار اثبات Coq انجام داد تا به طور رسمی تأیید کند که الگوریتم واقعاً با نتیجه معکوس مدولار صحیح در 256 بیت خاتمه می یابد. ورودی ها

شکاف بین الگوریتم و پیاده سازی

تلاش رسمی سازی در سال 2021 فقط نشان داد که الگوریتم طراحی شده توسط برنشتاین و یانگ به درستی کار می کند. با این حال، استفاده از آن الگوریتم در libsecp256k1 مستلزم پیاده‌سازی توضیحات ریاضی الگوریتم safegcd در زبان برنامه‌نویسی C است. برای مثال، توصیف ریاضی الگوریتم، ضرب ماتریسی بردارهایی را انجام می‌دهد که می‌تواند به اندازه اعداد صحیح علامت‌دار 256 بیتی باشد، با این حال زبان برنامه‌نویسی C به صورت بومی اعداد صحیح را تا 64 بیت (یا 128 بیت با برخی پسوندهای زبان) ارائه می‌کند.

پیاده سازی الگوریتم safegcd نیازمند برنامه ریزی ضرب ماتریس و سایر محاسبات با استفاده از اعداد صحیح 64 بیتی C است. علاوه بر این، بسیاری از بهینه‌سازی‌های دیگر اضافه شده‌اند تا پیاده‌سازی سریع انجام شود. در پایان، چهار پیاده‌سازی جداگانه از الگوریتم safegcd در libsecp256k1 وجود دارد: دو الگوریتم زمان ثابت برای تولید امضا، یکی بهینه‌سازی شده برای سیستم‌های 32 بیتی و دیگری بهینه‌سازی شده برای سیستم‌های 64 بیتی، و دو الگوریتم زمان متغیر برای تأیید امضا، دوباره یکی برای سیستم های 32 بیتی و دیگری برای سیستم های 64 بیتی.

C قابل تایید

برای تأیید اینکه کد C به درستی الگوریتم safegcd را پیاده سازی می کند، تمام جزئیات پیاده سازی باید بررسی شوند. ما از Verifiable C، بخشی از Verified Software Toolchain برای استدلال در مورد کد C با استفاده از اثبات قضیه Coq استفاده می کنیم.

راستی‌آزمایی با تعیین پیش‌شرط‌ها و پس‌شرط‌ها با استفاده از منطق جداسازی برای هر تابعی که تأیید می‌شود، انجام می‌شود. منطق جداسازی یک منطق تخصصی برای استدلال در مورد زیر روال ها، تخصیص حافظه، همزمانی و غیره است.

هنگامی که به هر تابع یک مشخصات داده می شود، تأیید با شروع از پیش شرط یک تابع، و ایجاد یک تغییر ناپذیر جدید پس از هر دستور در بدنه تابع، ادامه می یابد تا در نهایت شرط پست در انتهای بدنه تابع یا انتهای هر یک ایجاد شود. بیانیه بازگشت بیشتر تلاش رسمی‌سازی «بین» خطوط کد صرف می‌شود و از متغیرهای ثابت برای ترجمه عملیات خام هر عبارت C به عبارات سطح بالاتر در مورد آنچه که ساختارهای داده دستکاری شده از نظر ریاضی نشان می‌دهند، صرف می‌شود. به عنوان مثال، آنچه زبان C به عنوان آرایه ای از اعداد صحیح 64 بیتی در نظر می گیرد، ممکن است در واقع نمایشی از یک عدد صحیح 256 بیتی باشد.

نتیجه نهایی یک اثبات رسمی است که توسط دستیار اثبات Coq تأیید شده است که پیاده سازی زمان متغیر 64 بیتی libsecp256k1 از الگوریتم معکوس مدولار safegcd از نظر عملکردی صحیح است.

محدودیت های تایید

برای اثبات صحت عملکردی محدودیت هایی وجود دارد. منطق جداسازی مورد استفاده در تأیید پذیر C، آنچه را که به عنوان صحت جزئی شناخته می شود، پیاده سازی می کند. این بدان معناست که فقط ثابت می کند که کد C با نتیجه صحیح برمی گردد اگر برمی گردد، اما خود خاتمه را ثابت نمی کند. ما این محدودیت را با استفاده از اثبات Coq قبلی خود در مورد کران های الگوریتم safegcd کاهش می دهیم تا ثابت کنیم که مقدار شمارنده حلقه حلقه اصلی در واقع هرگز از 11 تکرار تجاوز نمی کند.

موضوع دیگر این است که خود زبان C هیچ مشخصات رسمی ندارد. در عوض، پروژه تأییدپذیر C از پروژه کامپایلر CompCert برای ارائه مشخصات رسمی یک زبان C استفاده می کند. این تضمین می کند که وقتی یک برنامه C تأیید شده با کامپایلر CompCert کامپایل می شود، کد اسمبلی حاصل با مشخصات آن مطابقت خواهد داشت (با توجه به محدودیت فوق). با این حال، این تضمین نمی کند که کد تولید شده توسط GCC، clang یا هر کامپایلر دیگری لزوماً کار خواهد کرد. به عنوان مثال، کامپایلرهای C مجاز هستند تا ترتیبات ارزیابی متفاوتی برای آرگومان های درون یک فراخوانی تابع داشته باشند. و حتی اگر زبان C دارای مشخصات رسمی باشد، هر کامپایلری که خودش به طور رسمی تایید نشده باشد، باز هم می‌تواند برنامه‌ها را اشتباه کامپایل کند. این در عمل رخ می دهد.

در نهایت، تأیید پذیر C از ساختارهای عبوری، ساختارهای بازگشتی یا ساختارهای اختصاصی پشتیبانی نمی کند. در حالی که در libsecp256k1، ساختارها همیشه با اشاره گر منتقل می شوند (که در تأیید پذیر C مجاز است)، چند مورد وجود دارد که از تخصیص ساختار استفاده می شود. برای اثبات درستی معکوس مدولار، 3 تخصیص وجود داشت که باید با یک فراخوانی تابع تخصصی که تخصیص ساختار را فیلد به فیلد انجام می‌داد، جایگزین می‌شد.

خلاصه

Blockstream Research به طور رسمی صحت عملکرد معکوس مدولار libsecp256k1 را تأیید کرده است. این کار شواهد بیشتری ارائه می دهد که تأیید کد C در عمل امکان پذیر است. استفاده از یک دستیار اثبات هدف کلی به ما امکان می دهد نرم افزار ساخته شده بر اساس استدلال های پیچیده ریاضی را تأیید کنیم.

هیچ چیز مانع از تأیید بقیه توابع پیاده سازی شده در libsecp256k1 نمی شود. بنابراین این امکان برای libsecp256k1 وجود دارد که بالاترین تضمین صحت نرم افزار ممکن را به دست آورد.

این یک پست مهمان توسط راسل اوکانر و اندرو پولسترا است. نظرات بیان شده کاملاً متعلق به خود آنها است و لزوماً نظرات BTC Inc یا مجله Bitcoin را منعکس نمی کند.

لینک منبع : هوشمند نیوز

آموزش مجازی مدیریت عالی حرفه ای کسب و کار Post DBA + مدرک معتبر قابل ترجمه رسمی با مهر دادگستری و وزارت امور خارجه	آموزش مجازی مدیریت عالی و حرفه ای کسب و کار DBA + مدرک معتبر قابل ترجمه رسمی با مهر دادگستری و وزارت امور خارجه	آموزش مجازی مدیریت کسب و کار MBA + مدرک معتبر قابل ترجمه رسمی با مهر دادگستری و وزارت امور خارجه
مدیریت حرفه ای کافی شاپ	حقوقدان خبره	سرآشپز حرفه ای
آموزش مجازی تعمیرات موبایل	آموزش مجازی ICDL مهارت های رایانه کار درجه یک و دو	آموزش مجازی کارشناس معاملات املاک_ مشاور املاک