mlkem-native

mlkem-native هو تنفيذ آمن وسريع وقابل للنقل بلغة C90[^C90] لمعيار ML-KEM[^FIPS203]. وهو مشتق من التنفيذ المرجعي لـ ML-KEM[^REF].

جميع أكواد C في mlkem/src/* و mlkem/src/fips202/* مُثبتة أنها آمنة من حيث الذاكرة (بدون تجاوز للذاكرة) وآمنة من حيث الأنواع (بدون تجاوز للأعداد الصحيحة) باستخدام CBMC[^CBMC]. جميع أكواد التجميع (assembly) لمعماريّتي AArch64 و x86_64 مُثبتة أنها صحيحة وظيفيًا، وآمنة من حيث الذاكرة، وذات توقيت مستقل عن الأسرار (ثابت الزمن)، باستخدام HOL-Light[^HOL-Light].

يتضمن mlkem-native واجهات خلفية أصلية لمعمارية Arm (64-بت، Neon)، وIntel/AMD (64-بت، AVX2)، وRISC-V (64-بت، RVV)، وPOWER (ppc64le، VSX). راجع المعايير لبيانات الأداء.

mlkem-native مدعوم من تحالف التشفير ما بعد الكمي كجزء من مؤسسة Linux.

بدء سريع لـ Ubuntu

# تثبيت الحزم الأساسية
sudo apt-get update
sudo apt-get install make gcc python3 git

# استنساخ mlkem-native
git clone https://github.com/pq-code-package/mlkem-native.git
cd mlkem-native

# البناء وتشغيل الاختبارات
make build
make test

# نفس الأمر باستخدام `tests`، وهو غلاف ملائم حول `make`
./scripts/tests all
# عرض جميع الخيارات
./scripts/tests --help

راجع BUILDING.md لمزيد من المعلومات.

التطبيقات

يُستخدم mlkem-native في

• libOQS من مشروع Open Quantum Safe منذ 0.13.0 (كتنفيذ ML-KEM الافتراضي)
• مكتبة التشفير الخاصة بـ AWS AWS-LC منذ v1.50.0
• مكتبة TLS rustls المكتوبة بلغة Rust منذ 0.23.28 (عبر AWS-LC كمزوّد التشفير الافتراضي)
• Pavona - مكتبة من الكتل السيليكونية المفتوحة المعيارية والمُثبتة على مستوى التصنيع والآمنة افتراضيًا

التحقق الرسمي

جميع أكواد C في mlkem/src/* و mlkem/src/fips202/* مُثبتة أنها آمنة من حيث الذاكرة (بدون تجاوز للذاكرة) وآمنة من حيث الأنواع (بدون تجاوز للأعداد الصحيحة). يستخدم هذا المُدقّق النموذجي المحدود C (CBMC) ويستند إلى عقود الدوال وتعليقات حلقات الثبات (loop invariants) في الكود المصدري. راجع proofs/cbmc للتفاصيل.

جميع أكواد التجميع لمعماريّتي AArch64 و x86_64 مُثبتة أنها صحيحة وظيفيًا، وآمنة من حيث الذاكرة، وذات توقيت مستقل عن الأسرار (ثابت الزمن)، على مستوى كود الكائن. يستخدم هذا مُثبِت النظريات التفاعلي HOL-Light والبنية التحتية للتحقق s2n-bignum (التي تتضمن نماذج للأجزاء ذات الصلة من معماريّتي Arm و x86). راجع proofs/hol_light للتفاصيل.

ملاحظة: التحقق الرسمي ليس مطلقًا أبدًا. راجع SOUNDNESS.md لتحليل مفصّل لنطاق وافتراضات ومخاطر جهود التحقق الرسمي حول mlkem-native.

الأمان

جميع أكواد التجميع لمعماريّتي AArch64 و x86_64 في mlkem-native مُثبتة رسميًا في HOL Light أنها خالية من تدفق التحكم المعتمد على الأسرار، وأنماط الوصول إلى الذاكرة، والتعليمات ذات زمن الاستجابة المتغير، مما يحبط معظم القنوات الجانبية الزمنية (راجع proofs/hol_light للتفاصيل). كود C مُحصّن ضد القنوات الجانبية الزمنية التي يُدخلها المترجم (مثل KyberSlash[^KyberSlash] أو clangover[^clangover]) من خلال حواجز مناسبة وأنماط ثابتة الزمن.

يتم أيضًا اختبار غياب الفروع المعتمدة على الأسرار، وأنماط الوصول إلى الذاكرة، والتعليمات ذات زمن الاستجابة المتغير باستخدام valgrind مع مجموعات مختلفة من المترجمين وخيارات الترجمة.

هجمات أخرى. يستهدف mlkem-native مقاومة القنوات الجانبية الزمنية فقط. فئات الهجمات الأخرى، مثل القنوات الجانبية للطاقة والكهرومغناطيسية، والقنوات الجانبية المعمارية الدقيقة (مثل التنفيذ التخميني)، أو هجمات حقن الأخطاء، خارج النطاق حاليًا.

التصميم

ينقسم mlkem-native إلى واجهة أمامية و_واجهتين خلفيتين_ للحساب و FIPS202 / SHA3. الواجهة الأمامية ثابتة، مكتوبة بلغة C، وتغطي جميع الإجراءات غير الحرجة للأداء. الواجهات الخلفية مرنة، وتتولى الإجراءات الحساسة للأداء، ويمكن تنفيذها بلغة C أو كود أصلي (تجميع/تعليمات داخلية)؛ راجع mlkem/src/native/api.h للواجهة الخلفية الحسابية و mlkem/src/fips202/native/api.h للواجهة الخلفية FIPS-202.

يوفّر mlkem-native حاليًا الواجهات الخلفية التالية:

• الواجهة الخلفية الافتراضية المحمولة بلغة C
• واجهة خلفية لمعمارية Arm 64-بت (باستخدام Neon)
• واجهة خلفية لمعمارية Intel/AMD 64-بت (باستخدام AVX2)
• واجهة خلفية لمعمارية RISC-V 64-بت (باستخدام RVV)
• واجهة خلفية لمعمارية POWER 64-بت (ppc64le، باستخدام VSX؛ تدعم POWER8 وما فوق)
• واجهة خلفية لمعمارية Armv8.1-M 32-بت (باستخدام Helium/MVE) -- راجع #1501. لا تزال هذه الواجهة تجريبية ومعطّلة افتراضيًا.

إذا كنت ترغب في المساهمة بواجهات خلفية جديدة، يرجى التواصل أو فتح طلب سحب (PR).

تم تطوير كود التجميع الخاص بنا لمعمارية AArch64 باستخدام المُحسِّن الفائق SLOTHY، باتباع النهج الموصوف في ورقة SLOTHY[^SLOTHY_Paper]: نكتب كود التجميع "النظيف" يدويًا ونؤتمت التحسينات الدقيقة (على سبيل المثال، راجع النظيف مقابل المُحسَّن لـ AArch64 NTT). راجع dev/README.md لمزيد من التفاصيل.

متجهات الاختبار

يتم اختبار mlkem-native ضد جميع متجهات اختبار ACVP الرسمية لـ ML-KEM[^ACVP] ومتجهات اختبار Wycheproof[^wycheproof] لـ ML-KEM.

ACVP

يمكنك تشغيل اختبارات ACVP باستخدام سكربت tests أو عميل ACVP مباشرة:

# باستخدام سكربت الاختبارات
./scripts/tests acvp
# باستخدام إصدار ACVP محدد
./scripts/tests acvp --version v1.1.0.41

# باستخدام عميل ACVP مباشرة
python3 ./test/acvp/acvp_client.py
python3 ./test/acvp/acvp_client.py --version v1.1.0.41

# باستخدام ملفات متجهات اختبار ACVP محددة (تم تنزيلها من خادم ACVP)
# python3 ./test/acvp/acvp_client.py -p {PROMPT}.json -e {EXPECTED_RESULT}.json
# على سبيل المثال، بافتراض أنك قمت بتشغيل ما سبق
python3 ./test/acvp/acvp_client.py \
  -p ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/prompt.json \
  -e ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/expectedResults.json

Wycheproof