Confidence-Guided Protocol IR Review UI

इस रिपॉज़िटरी में LLM-सहायता प्राप्त सुरक्षा प्रोटोकॉल मॉडलिंग के लिए एक स्थानीय human-in-the-loop UI शामिल है। यह हमारे कार्य में वर्णित वर्कफ़्लो का समर्थन करता है:

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

यह सिस्टम प्राकृतिक-भाषा प्रोटोकॉल विवरणों और Sapic+/Tamarin जनरेशन के बीच एक सिमेंटिक चेकपॉइंट के रूप में एक प्रोटोकॉल इंटरमीडिएट रिप्रेज़ेंटेशन (IR) प्रस्तुत करता है, जिससे समीक्षक औपचारिक सत्यापन से पहले LLM-जनित प्रोटोकॉल मॉडलों की सिमेंटिक सटीकता का ऑडिट कर सकें।

UI पूर्वावलोकन

नीचे दिए गए स्क्रीनशॉट समीक्षा UI में लोड किए गए Sigfox तैयार वर्कफ़्लो को दर्शाते हैं।

वर्कफ़्लो आयात

फ़ील्ड समीक्षा

Tamarin परिणाम

रिपॉज़िटरी लेआउट

• run_contract_review_ui.py: स्थानीय HTTP सर्वर और वर्कफ़्लो API।
• contract_review_ui/: ब्राउज़र UI।
• protocol_ir_pipeline/: IR प्रोसेसिंग, modeling-contract जनरेशन, Sapic+ जनरेशन, मरम्मत, proof lint, और Tamarin हेल्पर।
• protocol_ir_pipeline/c_to_ir.py: एम्बेडेड प्रॉम्प्ट के साथ चरणबद्ध C/C++ स्रोत से ProtocolIR निष्कर्षण।
• scripts/c_to_protocol_ir.py: C/C++ निष्कर्षण प्रवाह के लिए कमांड-लाइन एंट्री पॉइंट।
• config/: डिफ़ॉल्ट स्थानीय lint/retrieval कॉन्फ़िगरेशन।
• examples/ui_input_cases.json: प्रयोगों के लिए उपयोग किए गए UI-तैयार बेंचमार्क इनपुट।
• examples/ui_inputs.md: UI को मैन्युअल रूप से भरने के लिए कॉपी-फ़्रेंडली बेंचमार्क इनपुट, कठिनाई के अनुसार समूहीकृत।
• examples/protocol-abstraction-cases.json: बंडल किया गया abstraction-hint लाइब्रेरी, जिसका उपयोग केवल तब किया जाता है जब UI में सक्षम किया जाए।
• examples/prepared_workflows/gpt55/: बेंचमार्क केसों के लिए कच्चे IR और मानव-समीक्षित IR स्नैपशॉट।
• examples/user_tested_workflows/deepseek_ui_20260615/: UI के माध्यम से लेखक द्वारा मैन्युअल रूप से परीक्षण किए गए Toy और Sigfox वर्कफ़्लो।
• NOTICE.md: एट्रिब्यूशन और artifact-scope नोट्स।
• LICENSE: GPLv3 लाइसेंस टेक्स्ट।

आवश्यकताएँ

• Python 3.10+
• DeepSeek, OpenAI, Anthropic, या OpenAI-संगत Llama एंडपॉइंट के लिए एक LLM API कुंजी
• compile/proof सत्यापन के लिए आपके PATH में tamarin-prover। अपने प्लेटफ़ॉर्म के लिए आधिकारिक निर्देशों का पालन करके 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

UI चलाएँ

खाली वर्कफ़्लो डायरेक्टरी के साथ शुरू करें:

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/modeling contract जनरेट करें।
2. Messages, Checks, Events, Proof Targets, और Attack Surface में सिमेंटिक फ़ील्ड की समीक्षा करें और संपादित करें।
3. modeling_contract.reviewed.json लिखने के लिए Save Reviewed पर क्लिक करें।
4. Generate Sapic+ पर क्लिक करें।
5. यदि tamarin-prover इंस्टॉल है तो Tamarin के साथ compile और prove करें।

Save Reviewed के लिए हर review badge की पुष्टि आवश्यक नहीं है। फ़ील्ड की पुष्टि करना review-progress ट्रैकिंग और proof-critical generation hints के लिए उपयोगी है, लेकिन सहेजे गए संपादन अभी भी जनरेशन द्वारा उपयोग किए जाते हैं।

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

इस रिपॉज़िटरी में tpm2-sessions.c का एक sanitized C-to-IR डेमो artifact शामिल है। निम्नलिखित कमांड UI शुरू करता है और डेमो खोलता है:

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 उन सिमेंटिक निर्णयों को रिकॉर्ड करता है जिन्हें अंतिम औपचारिक मॉडल के अर्थपूर्ण होने के लिए सही होना आवश्यक है, जिनमें शामिल हैं:

• प्रोटोकॉल भूमिकाएँ और दीर्घकालिक सेटअप मान;
• संदेश निर्माण, पार्सिंग, एन्क्रिप्शन, साइनिंग, और सत्यापन;
• मान की provenance, जिसमें fresh values, प्राप्त मान, व्युत्पन्न मान, और प्रकट किए गए मान शामिल हैं;
• proof targets द्वारा उपयोग किए जाने वाले events;
• secrecy, authentication, executability, और expected-counterexample targets;
• attack-surface मान्यताएँ।

Abstraction Hints

UI स्टार्टअप के बाद बंडल किए गए abstraction-hint लाइब्रेरी का पता लगा सकता है, लेकिन यह इसका उपयोग तब तक नहीं करता जब तक उपयोगकर्ता Sapic+ जनरेट करने से पहले Use abstraction hints को चेक न करे। जब वह चेकबॉक्स सक्षम होता है, तो बैकएंड यहाँ से proof-engineering hints प्राप्त करता है:

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 के संक्षिप्त उदाहरण हैं।

उपयोगकर्ता-परीक्षित UI वर्कफ़्लो

examples/user_tested_workflows/deepseek_ui_20260615/ में दो वर्कफ़्लो शामिल हैं जो मैन्युअल परीक्षण के दौरान वास्तव में UI के माध्यम से चलाए गए थे:

Toy
Sigfox

इनमें उन UI रनों के हल्के artifacts शामिल हैं: input/review artifacts, prompts, LLM call metadata, जनरेट किए गए Tamarin मॉडल, compile/repair आउटपुट, और proof logs। API क्रेडेंशियल शामिल नहीं हैं।

UI में उन्हें देखने के लिए, इस वर्कफ़्लो लाइब्रेरी के साथ सर्वर शुरू करें:

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

फिर UI खोलें, Select prepared workflow... का उपयोग करें, और easy / Toy या easy / Sigfox चुनें।

मौजूदा वर्कफ़्लो लाइब्रेरी

आप वैकल्पिक रूप से UI से आयात करने के लिए तैयार वर्कफ़्लो की एक डायरेक्टरी उजागर कर सकते हैं:

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 में इस समीक्षा UI के लिए तैयार किए गए 18 प्रोटोकॉल इनपुट शामिल हैं। इन्हें प्राकृतिक-भाषा विवरणों, मान्यताओं, लक्ष्यों, और अपेक्षित परिणामों के रूप में दर्शाया गया है जिन्हें UI में कॉपी किया जा सकता है।

मैन्युअल परीक्षण के लिए, 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

एट्रिब्यूशन