laplace1002/tamarinagentHuman-in-the-loop-UI, die natürlichsprachliche oder C/C++-Protokollbeschreibungen in eine überprüfbare Protocol IR umwandelt und anschließend Sapic+/Tamarin-Modelle für die formale Sicherheitsverifikation generiert.
Dieses Repository enthält eine lokale Human-in-the-Loop-UI für LLM-gestützte Sicherheitsprotokollmodellierung. Sie unterstützt den in unserer Arbeit beschriebenen Workflow:
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
Das System führt eine Protokoll-Zwischendarstellung (IR) als semantischen Prüfpunkt zwischen natürlichsprachlichen Protokollbeschreibungen und der Sapic+/Tamarin-Generierung ein, wodurch Prüfer die semantische Korrektheit von LLM-generierten Protokollmodellen vor der formalen Verifikation auditieren können.
Die folgenden Screenshots zeigen den vorbereiteten Sigfox-Workflow, geladen in der Review-UI.
run_contract_review_ui.py: lokaler HTTP-Server und Workflow-API.contract_review_ui/: Browser-UI.protocol_ir_pipeline/: IR-Verarbeitung, Generierung von Modeling-Contracts, Sapic+-Generierung, Reparatur, Proof-Lint und Tamarin-Hilfsfunktionen.protocol_ir_pipeline/c_to_ir.py: stufenweise Extraktion von C/C++-Quellcode zu ProtocolIR mit eingebetteten Prompts.scripts/c_to_protocol_ir.py: Kommandozeilen-Einstiegspunkt für den C/C++-Extraktionsablauf.config/: Standardkonfiguration für lokales Lint/Retrieval.examples/ui_input_cases.json: UI-taugliche Benchmark-Eingaben, die für Experimente verwendet werden.examples/ui_inputs.md: kopierfreundliche Benchmark-Eingaben zum manuellen Befüllen der UI, gruppiert nach Schwierigkeitsgrad.examples/protocol-abstraction-cases.json: mitgelieferte Abstraktionshinweis-Bibliothek, die nur verwendet wird, wenn sie in der UI aktiviert ist.examples/prepared_workflows/gpt55/: Roh-IR- und human-reviewte IR-Snapshots für die Benchmark-Fälle.examples/user_tested_workflows/deepseek_ui_20260615/: Toy- und Sigfox-Workflows, die vom Autor manuell durch die UI getestet wurden.NOTICE.md: Hinweise zu Attribution und Artifact-Scope.LICENSE: GPLv3-Lizenztext.tamarin-prover in Ihrem PATH für Kompilierungs-/Proof-Verifikation. Installieren Sie Tamarin Prover gemäß den offiziellen Anweisungen für Ihre Plattform: https://tamarin-prover.com/manual/master/book/002_installation.html.Python-Abhängigkeiten installieren:
pip install -r requirements.txt
Anmeldedaten konfigurieren:
cp .env.example .env
# edit .env and set the provider API key
Mit einem leeren Workflow-Verzeichnis starten:
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--provider deepseek \
--host 127.0.0.1 \
--port 8765
Öffnen:
http://127.0.0.1:8765/
Typischer Workflow:
Save Reviewed klicken, um modeling_contract.reviewed.json zu schreiben.Generate Sapic+ klicken.tamarin-prover installiert ist.Save Reviewed erfordert nicht, dass jedes Review-Badge bestätigt wird. Das Bestätigen von Feldern ist nützlich für die Verfolgung des Review-Fortschritts und für proof-kritische Generierungshinweise, aber gespeicherte Bearbeitungen werden weiterhin von der Generierung verwendet.
Die Extraktionsstufen, JSON-Ausgabeverträge und Prompts befinden sich in protocol_ir_pipeline/c_to_ir.py.
Die stufenweise Extraktion mit einem LLM ausführen:
python3 scripts/c_to_protocol_ir.py \
--source path/to/protocol.c \
--output-dir runs/c_to_ir_demo \
--name MyProtocol \
--provider deepseek
Dieses Repository enthält ein bereinigtes C-to-IR-Demo-Artefakt von tpm2-sessions.c. Der folgende Befehl startet die UI und öffnet die Demo:
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 zeichnet die semantischen Entscheidungen auf, die korrekt sein müssen, damit das endgültige formale Modell aussagekräftig ist, darunter:
Die UI kann die mitgelieferte Abstraktionshinweis-Bibliothek nach dem Start lokalisieren, verwendet sie jedoch nicht, es sei denn, der Benutzer aktiviert Use abstraction hints vor der Generierung von Sapic+. Wenn dieses Kontrollkästchen aktiviert ist, ruft das Backend Proof-Engineering-Hinweise ab aus:
examples/protocol-abstraction-cases.json
Sie können diese Bibliothek ersetzen oder eine andere verwenden mit:
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--abstraction-hints-path /path/to/protocol-abstraction-cases.json
examples/prepared_workflows/gpt55/ enthält Roh-IR- und human-reviewte IR-Snapshots für die Benchmark-Fälle. Jeder Fall enthält nur:
ir/protocol_ir.json
ir/protocol_ir.reviewed.json
Diese Dateien sind kompakte Beispiele für die IR vor und nach der menschlichen Überprüfung.
examples/user_tested_workflows/deepseek_ui_20260615/ enthält zwei Workflows, die während manueller Tests tatsächlich durch die UI ausgeführt wurden:
Toy
Sigfox
Sie enthalten die leichtgewichtigen Artefakte aus diesen UI-Läufen: Eingabe-/Review-Artefakte, Prompts, LLM-Aufruf-Metadaten, generierte Tamarin-Modelle, Kompilierungs-/Reparaturausgaben und Proof-Logs. API-Anmeldedaten sind nicht enthalten.
Um sie in der UI zu inspizieren, starten Sie den Server mit dieser Workflow-Bibliothek:
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
Öffnen Sie dann die UI, verwenden Sie Select prepared workflow... und wählen Sie easy / Toy oder easy / Sigfox.
Sie können optional ein Verzeichnis mit vorbereiteten Workflows zum Import aus der UI bereitstellen:
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 enthält 18 Protokolleingaben, die für diese Review-UI vorbereitet wurden. Sie sind als natürlichsprachliche Beschreibungen, Annahmen, Ziele und erwartete Ergebnisse dargestellt, die in die UI kopiert werden können.