‏اپل درستی ریاضی رمزنگاری پساکوانتومی corecrypto رو اثبات کرد

اپل می‌گه با انتشار این هفته‌ی corecrypto — کتابخونه‌ی پایه‌ی رمزنگاری سیستم‌عامل‌هاش — پیاده‌سازی الگوریتم‌های پساکوانتومی ML-KEM و ML-DSA رو به‌همراه اثبات‌های ریاضی‌ای که نشون می‌ده این پیاده‌سازی وفادار به استانداردهای FIPS 203 و FIPS 204 هست، برای ارزیابی مستقل متخصص‌ها منتشر کرده. این حرکت ادامه‌ی همون مسیریه که با رمزنگاری امن دربرابر کوانتوم تو iMessage شروع شد.

چرا این‌قدر سخت‌گیری؟ به گفته‌ی اپل، corecrypto روی بیش از ۲.۵ میلیارد دستگاه فعال کار می‌کنه و کارهای رمزگذاری، هشینگ، تولید عدد تصادفی و امضای دیجیتال رو انجام می‌ده. یه باگ بحرانی توش می‌تونه امنیت و پایداری هر اپ و قابلیتی که بهش وابسته‌ست رو خراب کنه، برای همین اپل موقع اضافه‌کردن کد جدید خیلی محتاطه.

نکته‌ی اصلی مقاله formal verification ـه: یعنی به‌جای این‌که فقط با تست نرم‌افزاری امیدوار باشن کد درسته، با اثبات ریاضی نشون می‌دن فرمول پیاده‌سازی با فرمول مشخصات (specification) معادله. نویسنده می‌گه اگه بشه این معادل‌بودن رو ثابت کرد، اون‌وقت مطمئنیم خروجی همیشه درسته — چیزی که با تست معمولی به این درجه از اطمینان نمی‌رسی. زیرروتین‌هایی که با اعداد بزرگ و چندجمله‌ای‌ها کار می‌کنن و پر از carry و borrow هستن، دقیقاً همون‌جاییه که باگ‌های ظریف قایم می‌شن و تست از پسشون برنمیاد.

اپل برای این کار یه رویکرد سفارشی ساخته که چند ابزار رو ترکیب می‌کنه: Isabelle (دستیار اثبات که اپل ۱۵ ساله تو طراحی سیلیکون ازش استفاده می‌کنه)، SAW و زبان Cryptol از شرکت Galois، و یه مترجم جدید به اسم cryptol-to-isabelle. روند کار اینه که اول کد C قابل‌حمل به Cryptol ترجمه می‌شه و SAW چک می‌کنه که مدل با کد می‌خونه، بعد مدل به Isabelle ترجمه می‌شه و اون‌جا معادل‌بودنش با مشخصات FIPS اثبات می‌شه.

این کار اصلاً کوچیک نبوده — اثبات‌ها بیش از ۵۰٬۰۰۰ گام داشتن، برای همین اپل یه مجموعه کتابخونه‌ی Isabelle از لم‌های قابل‌استفاده‌ی مجدد ساخته تا کار سریع‌تر پیش بره. مرحله‌ی آخر هم اثبات زیرروتین‌های دست‌بهینه‌شده‌ی ARM64 assembly ـه؛ به‌جای مقایسه‌ی مستقیم اسمبلی با مشخصات ریاضی، هر زیرروتین اسمبلی با همتای C ـش که قبلاً اثبات شده مقایسه می‌شه.

مثال ساده‌ای که خود مقاله می‌زنه، اختلاف نگاه C و مشخصات Isabelle رو نشون می‌ده. تو C، جمع دو چندجمله‌ای با یه حلقه روی ضریب‌ها انجام می‌شه:

void ccmlkem_poly_add(int16_t coeffs[CCMLKEM_N], const int16_t a[CCMLKEM_N], const int16_t b[CCMLKEM_N])
{
    for (unsigned i = 0; i < CCMLKEM_N; i++) {
        coeffs[i] = a[i] + b[i];
    }
}

ولی مشخصات معادلش تو Isabelle خیلی انتزاعی‌تره: تعداد ضریب‌ها یا اندازه‌ی دقیق کلمه‌ها رو مشخص نمی‌کنه و به‌جای حلقه از عملگر map2 استفاده می‌کنه تا همه‌ی ضریب‌ها رو یک‌جا پردازش کنه.

به گفته‌ی اپل، همین روش چند مشکلی رو پیدا کرده که تست معمولی هیچ‌وقت نمی‌گرفت — مثلاً یه گام جا‌افتاده تو نسخه‌ی اولیه‌ی ML-DSA که در موارد نادر می‌تونست خروجی رو خراب کنه، و یه خطا تو یه اثبات شخص ثالث. نویسنده تأکید می‌کنه قوی‌ترین اطمینان وقتی به‌دست میاد که formal verification با تست‌های معمولی ترکیب بشه، نه این‌که جاش رو بگیره.

نکات کلیدی:

• corecrypto روی بیش از ۲.۵ میلیارد دستگاه فعاله
• الگوریتم‌های پساکوانتومی ML-KEM و ML-DSA مطابق FIPS 203 و FIPS 204
• اثبات ریاضی به‌جای تکیه‌ی صرف به تست برای تضمین درستی کد
• ابزارها: Isabelle، SAW، Cryptol و مترجم جدید cryptol-to-isabelle
• اثبات‌ها بیش از ۵۰٬۰۰۰ گام داشتن و باگ‌هایی پیدا کردن که تست نمی‌گرفت