الباحثون في معهد الدولة للبحوث في المعلوماتية والأتمتة (INRIA), قدمت مايكروسوفت للأبحاث وجامعة كارنيجي ميلون الإصدار التجريبي الأول من مكتبة تشفير EverCrypt تم تطويره في إطار مشروع Everest وباستخدام الأساليب الرياضية للتحقق الرسمي من الموثوقية.
لقدراته وأدائه ، EverCrypt قريب جدًا من مكتبات التشفير الموجودة (OpenSSL) ولكن هذا ، على عكسهم ، يوفر ضمانات إضافية للموثوقية والأمان.
على سبيل المثال تتلخص عملية التحقق في تحديد المواصفات التفصيلية التي تصف جميع سلوكيات البرنامج والإثبات الرياضي أن الشفرة المكتوبة يفي بالمواصفات المعدة.
على عكس طرق مراقبة الجودة القائمة على الأدلة ، يوفر التحقق ضمانات موثوقة أن البرنامج سيعمل فقط كما أراد المطورون ولا توجد أنواع محددة من الأخطاء.
على سبيل المثال ، الامتثال للمواصفات يضمن العمل الآمن مع الذاكرة وعدم وجود أخطاء تؤدي إلى تجاوز سعة المخزن المؤقت، لمؤشرات dereference ، للوصول إلى مناطق الذاكرة المحررة بالفعل ، أو لمضاعفة تحرير كتل الذاكرة.
ما هو EverCrypt؟
إيفركربت يوفر نوعًا قويًا وفحصًا للقيمة- لن يمرر المكون أبدًا معلمات إلى المكون غير المتوافق الآخر ولن يتمكن من الوصول إلى الحالات الداخلية للمكونات الأخرى.
سلوك الإدخال / الإخراج يتوافق تمامًا مع إجراءات وظيفة الرياضيات البسيطة، والتي تم تعريفها في معايير التشفير.
للحماية من الهجمات في قنوات الطرف الثالث ، السلوك أثناء العمليات الحسابية (على سبيل المثال ، مدة التنفيذ أو وجود وصول إلى ذاكرة معينة) لا تعتمد على البيانات السرية التي تتم معالجتها.
كود المشروع مكتوب باللغة الوظيفية F * (نجمة F) , الذي يوفر نظامًا للأنواع والتحسينات التابعة، والتي تسمح بوضع المواصفات الدقيقة (النموذج الرياضي) للبرامج ولضمان صحة وغياب الأخطاء في التنفيذ عن طريق صيغ SMT وأدوات الاختبار المساعدة.
يتم توزيع الكود في F * بموجب ترخيص Apache 2.0 والوحدات النمطية النهائية في C والمجمع بموجب ترخيص MIT.
بناءً على الكود المرجعي F * ، المجمع ، C ، OCaml ، يتم إنشاء JavaScript ورمز تجميع الويب.
بعض أجزاء الكود استعداد بواسطة المشروع مستخدمة بالفعل في Firefox ، Windows kernel ، فإن blockchain من Tezos و VPN Wireguard.
مكونات EverCrypt
المضمون، يجمع EverCrypt بين مشروعين مختلفين سابقًا من HACL * و Vale، توفير واجهة برمجة تطبيقات موحدة تستند إليها وجعلها مناسبة للاستخدام في المشاريع الحقيقية.
HACL * مكتوب بلغة Low* وهدفها هو توفير أساسيات التشفير لاستخدامها في برامج C التي يستخدمون واجهات برمجة التطبيقات على غرار libsodium و NaCL.
المشروع طور Vale لغة معينة المجال لإنشاء عمليات التحقق في المجمع.
تم دمج حوالي 110 آلاف سطر من كود HACL * بلغة Low * و 25 ألف سطر من كود Vale وقد تمت إعادة كتابتها في حوالي 70 ألف سطر من التعليمات البرمجية باللغة العالمية F * ، والتي يتم تطويرها أيضًا كجزء من مشروع إيفرست.
الإصدار الأول من مكتبة EverCrypt ميزات التحقق من التطبيقات من خوارزميات التشفير التالية المقترحة في إصدارات C أو المجمّع (عند استخدام امتداد.
من بين هؤلاء ، يبرز ما يلي على صفحة المشروع:
- خوارزميات التجزئة: جميع متغيرات SHA2 و SHA3 و SHA1 و MD5
- رموز المصادقة: HMAC عبر SHA1 و SHA2-256 و SHA2-384 و SHA2-512 لمصادقة مصدر البيانات
- خوارزمية إنشاء المفتاح HKDF (الاستخراج المستند إلى HMAC ووظيفة اشتقاق المفتاح الموسعة)
- تشفير دفق ChaCha20 (يتوفر إصدار C غير محسن)
- خوارزمية مصادقة الرسائل Poly1305 (MAC) (إصدار C وإصدار المجمع)
- بروتوكول Diffie-Hellman على المنحنيات الإهليلجية Curve25519 (إصدارات C وإصدارات المجمّع مع التحسينات بناءً على تعليمات BMI2 و ADX)
- وضع تشفير الحظر AEAD (تشفير مصدق) ChachaPoly (الإصدار C غير محسّن)
- وضع تشفير كتلة AEAD AES-GCM (إصدار المجمع مع تحسينات AES-NI).
في الاول إصدار ألفا ، اكتمل التحقق من الرمز بالفعل إلى حد كبير ، ولكن لا تزال هناك بعض المناطق مكشوفة.
وبالإضافة إلى ذلك، لم يتم تثبيت API بعدالتي سيتم توسيعها في إصدارات ألفا التالية (من المخطط توحيد الهياكل لجميع واجهات برمجة التطبيقات.
من بين العيوب ، تم أيضًا إبراز دعم بنية x86_64 (في المرحلة الأولى ، الهدف الرئيسي هو الموثوقية ، بينما سيتم تنفيذ التحسين والأنظمة الأساسية في المرتبة الثانية).
مصدر: https://jonathan.protzenko.fr