واجهة مراجعة IR للبروتوكولات الموجهة بالثقة

يحتوي هذا المستودع على واجهة محلية تفاعلية بشرية (human-in-the-loop) لنمذجة بروتوكولات الأمان بمساعدة LLM. وهي تدعم سير العمل الموصوف في عملنا:

Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling

يقدّم النظام تمثيلاً وسيطاً للبروتوكول (IR) كنقطة تحقق دلالية بين أوصاف البروتوكول باللغة الطبيعية وتوليد Sapic+/Tamarin، مما يمكّن المراجعين من تدقيق نماذج البروتوكولات المولّدة بواسطة LLM للتأكد من دقتها الدلالية قبل التحقق الرسمي.

معاينة الواجهة

تُظهر لقطات الشاشة أدناه سير عمل Sigfox المُجهّز محمّلاً في واجهة المراجعة.

استيراد سير العمل

مراجعة الحقول

نتائج Tamarin

تخطيط المستودع

• run_contract_review_ui.py: خادم HTTP محلي وواجهة برمجة تطبيقات سير العمل.
• contract_review_ui/: واجهة المتصفح.
• protocol_ir_pipeline/: معالجة IR، وتوليد عقد النمذجة، وتوليد Sapic+، والإصلاح، وفحص البراهين، وأدوات Tamarin المساعدة.
• protocol_ir_pipeline/c_to_ir.py: استخلاص مُراحل من مصدر C/C++ إلى ProtocolIR مع مطالبات مضمّنة.
• scripts/c_to_protocol_ir.py: نقطة دخول سطر الأوامر لتدفق الاستخلاص من C/C++.
• config/: التكوين المحلي الافتراضي للفحص/الاسترجاع.
• examples/ui_input_cases.json: مدخلات معيارية جاهزة للواجهة استُخدمت في التجارب.
• examples/ui_inputs.md: مدخلات معيارية سهلة النسخ لملء الواجهة يدويًا، مجمّعة حسب الصعوبة.
• examples/protocol-abstraction-cases.json: مكتبة تلميحات التجريد المضمّنة، تُستخدم فقط عند تمكينها في الواجهة.
• examples/prepared_workflows/gpt55/: لقطات IR الخام وIR المراجَع بشريًا لحالات المعيار.
• examples/user_tested_workflows/deepseek_ui_20260615/: سير عمل Toy وSigfox المختبَرة يدويًا من قبل المؤلف عبر الواجهة.
• NOTICE.md: ملاحظات الإسناد ونطاق العمل الفني.
• LICENSE: نص ترخيص GPLv3.

المتطلبات

• Python 3.10+
• مفتاح API لنموذج LLM من DeepSeek أو OpenAI أو Anthropic أو نقطة نهاية Llama متوافقة مع OpenAI
• tamarin-prover في PATH الخاص بك للتحقق من الترجمة/البرهان. ثبّت Tamarin Prover باتباع التعليمات الرسمية لمنصتك: https://tamarin-prover.com/manual/master/book/002_installation.html.

ثبّت تبعيات Python:

pip install -r requirements.txt

اضبط بيانات الاعتماد:

cp .env.example .env
# edit .env and set the provider API key

تشغيل الواجهة

ابدأ بدليل سير عمل فارغ:

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --provider deepseek \
  --host 127.0.0.1 \
  --port 8765

افتح:

http://127.0.0.1:8765/

سير العمل النموذجي:

1. الصق وصف بروتوكول باللغة الطبيعية وولّد IR الخام/عقد النمذجة.
2. راجع وحرّر الحقول الدلالية في Messages وChecks وEvents وProof Targets وAttack Surface.
3. انقر على Save Reviewed لكتابة modeling_contract.reviewed.json.
4. انقر على Generate Sapic+.
5. ترجم وأثبت باستخدام Tamarin إذا كان tamarin-prover مثبّتًا.

لا يتطلب Save Reviewed تأكيد كل شارة مراجعة. تأكيد الحقول مفيد لتتبع تقدم المراجعة ولتلميحات التوليد الحرجة للبرهان، لكن التعديلات المحفوظة لا تزال تُستخدم في التوليد.

استخلاص مصدر C/C++

مراحل الاستخلاص وعقود مخرجات JSON والمطالبات موجودة في protocol_ir_pipeline/c_to_ir.py.

شغّل الاستخلاص المُمرحل باستخدام LLM:

python3 scripts/c_to_protocol_ir.py \
  --source path/to/protocol.c \
  --output-dir runs/c_to_ir_demo \
  --name MyProtocol \
  --provider deepseek

يتضمن هذا المستودع عيّنة تجريبية مُنقّاة لتحويل C إلى IR من tpm2-sessions.c. يبدأ الأمر التالي الواجهة ويفتح العيّنة التجريبية:

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --provider deepseek \
  --host 127.0.0.1 \
  --port 8765

http://127.0.0.1:8765/c-code-demo

مراجعة Protocol IR

يسجّل Protocol IR القرارات الدلالية التي يجب أن تكون صحيحة لكي يكون النموذج الرسمي النهائي ذا معنى، بما في ذلك:

• أدوار البروتوكول وقيم الإعداد طويلة الأمد؛
• بناء الرسائل وتحليلها وتشفيرها وتوقيعها والتحقق منها؛
• مصدر القيم، بما في ذلك القيم الطازجة والقيم المستلمة والقيم المشتقة والقيم المكشوفة؛
• الأحداث المستخدمة بواسطة أهداف البرهان؛
• أهداف السرية والمصادقة وقابلية التنفيذ والمثال المضاد المتوقع؛
• افتراضات سطح الهجوم.

تلميحات التجريد

يمكن للواجهة تحديد موقع مكتبة تلميحات التجريد المضمّنة بعد بدء التشغيل، لكنها لا تستخدمها إلا إذا حدّد المستخدم Use abstraction hints قبل توليد Sapic+. عند تمكين مربع الاختيار هذا، يسترجع الواجهة الخلفية تلميحات هندسة البرهان من:

examples/protocol-abstraction-cases.json

يمكنك استبدال هذه المكتبة أو استخدام مكتبة أخرى عبر:

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --abstraction-hints-path /path/to/protocol-abstraction-cases.json

لقطات IR المُجهّزة

يحتوي examples/prepared_workflows/gpt55/ على لقطات IR الخام وIR المراجَع بشريًا لحالات المعيار. تتضمن كل حالة فقط:

ir/protocol_ir.json
ir/protocol_ir.reviewed.json

هذه الملفات أمثلة مدمجة على IR قبل المراجعة البشرية وبعدها.

سير عمل الواجهة المختبَر من المستخدم

يحتوي examples/user_tested_workflows/deepseek_ui_20260615/ على سيرَي عمل شُغّلا فعليًا عبر الواجهة أثناء الاختبار اليدوي:

Toy
Sigfox

وهما يتضمنان العناصر الخفيفة من تلك التشغيلات عبر الواجهة: عناصر الإدخال/المراجعة، والمطالبات، وبيانات وصفية لاستدعاءات LLM، ونماذج Tamarin المولّدة، ومخرجات الترجمة/الإصلاح، وسجلات البراهين. لا تتضمن بيانات اعتماد API.

لفحصها في الواجهة، ابدأ الخادم بمكتبة سير العمل هذه:

python3 run_contract_review_ui.py \
  --run-dir runs/tmp_user_tested_review \
  --workflow-library-dir examples/user_tested_workflows/deepseek_ui_20260615 \
  --provider deepseek \
  --host 127.0.0.1 \
  --port 8765

ثم افتح الواجهة، واستخدم Select prepared workflow...، واختر easy / Toy أو easy / Sigfox.

مكتبة سير العمل الموجودة

يمكنك اختياريًا كشف دليل من سير العمل المُجهّز للاستيراد من الواجهة:

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --workflow-library-dir /path/to/prepared/workflows \
  --provider deepseek

مدخلات المعيار

يحتوي examples/ui_input_cases.json على 18 مدخل بروتوكول مُجهّز لواجهة المراجعة هذه. وهي ممثّلة كأوصاف باللغة الطبيعية وافتراضات وأهداف ونتائج متوقعة يمكن نسخها إلى الواجهة.

للاختبار اليدوي، يحتوي examples/ui_inputs.md على الحالات نفسها في ملف Markdown واحد سهل النسخ، مجمّعة في أقسام Easy وMedium وHard.

الحالات المضمّنة:

Example, NSPK, Naxos, Toy, Woo_Lam, sigfox, EDHOC, KEMTLS, LAK06, SPLICE,
SSH, CCITT_X509, Denning_Sacco, Kao_Chow, NSSK, Neuman_Stubblebine,
Otway_Rees, Yahalom

الإسناد

نُظّمت مدخلات المعيار في examples/ui_input_cases.json من مدخلات معيار AutoSM المكوّنة من 18 حالة. لا تتضمن هذه الحزمة ملفات Sapic+/Tamarin المرجعية الكاملة لمعيار AutoSM.

Ziyu Mao, Jingyi Wang, Jun Sun, Shengchao Qin, and Jiawen Xiong. "LLM-Aided Automatic Modeling for Security Protocol Verification." ICSE 2025. DOI: 10.1109/ICSE55347.2025.00197.

مستودع عمل AutoSM الفني: https://github.com/zerrymore/AutoSM

تُوزّع هذه الحزمة مع نص ترخيص GPLv3 في LICENSE. راجع NOTICE.md لملاحظات الإسناد المتعلقة بنطاق العمل الفني.