Interface de révision IR de protocole guidée par la confiance

Ce dépôt contient une interface locale human-in-the-loop pour la modélisation de protocoles de sécurité assistée par LLM. Elle prend en charge le flux de travail décrit dans nos travaux :

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

Le système introduit une représentation intermédiaire de protocole (IR) comme point de contrôle sémantique entre les descriptions de protocoles en langage naturel et la génération Sapic+/Tamarin, permettant aux relecteurs d'auditer les modèles de protocoles générés par LLM pour leur exactitude sémantique avant la vérification formelle.

Aperçu de l'interface

Les captures d'écran ci-dessous montrent le flux de travail préparé Sigfox chargé dans l'interface de révision.

Import du flux de travail

Révision des champs

Résultats Tamarin

Organisation du dépôt

• run_contract_review_ui.py : serveur HTTP local et API de flux de travail.
• contract_review_ui/ : interface navigateur.
• protocol_ir_pipeline/ : traitement IR, génération de contrat de modélisation, génération Sapic+, réparation, lint de preuve et assistants Tamarin.
• protocol_ir_pipeline/c_to_ir.py : extraction par étapes du code source C/C++ vers ProtocolIR avec prompts intégrés.
• scripts/c_to_protocol_ir.py : point d'entrée en ligne de commande pour le flux d'extraction C/C++.
• config/ : configuration locale par défaut de lint/récupération.
• examples/ui_input_cases.json : entrées de benchmark prêtes pour l'interface utilisées pour les expériences.
• examples/ui_inputs.md : entrées de benchmark faciles à copier pour remplir manuellement l'interface, regroupées par difficulté.
• examples/protocol-abstraction-cases.json : bibliothèque d'indices d'abstraction fournie, utilisée uniquement lorsqu'elle est activée dans l'interface.
• examples/prepared_workflows/gpt55/ : instantanés IR bruts et IR révisés par un humain pour les cas de benchmark.
• examples/user_tested_workflows/deepseek_ui_20260615/ : flux de travail Toy et Sigfox testés manuellement par l'auteur via l'interface.
• NOTICE.md : notes d'attribution et de périmètre de l'artefact.
• LICENSE : texte de la licence GPLv3.

Prérequis

• Python 3.10+
• Une clé API LLM pour DeepSeek, OpenAI, Anthropic, ou un point de terminaison Llama compatible OpenAI
• tamarin-prover dans votre PATH pour la compilation/vérification de preuve. Installez Tamarin Prover en suivant les instructions officielles pour votre plateforme : https://tamarin-prover.com/manual/master/book/002_installation.html.

Installez les dépendances Python :

pip install -r requirements.txt

Configurez les identifiants :

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

Lancer l'interface

Démarrez avec un répertoire de flux de travail vide :

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

Ouvrez :

http://127.0.0.1:8765/

Flux de travail typique :

1. Collez une description de protocole en langage naturel et générez l'IR brut/le contrat de modélisation.
2. Révisez et modifiez les champs sémantiques dans Messages, Checks, Events, Proof Targets et Attack Surface.
3. Cliquez sur Save Reviewed pour écrire modeling_contract.reviewed.json.
4. Cliquez sur Generate Sapic+.
5. Compilez et prouvez avec Tamarin si tamarin-prover est installé.

Save Reviewed ne nécessite pas que chaque badge de révision soit confirmé. Confirmer les champs est utile pour le suivi de la progression de la révision et pour les indices de génération critiques pour la preuve, mais les modifications enregistrées sont tout de même utilisées par la génération.

Extraction de code source C/C++

Les étapes d'extraction, les contrats de sortie JSON et les prompts se trouvent dans protocol_ir_pipeline/c_to_ir.py.

Lancez l'extraction par étapes avec un LLM :

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

Ce dépôt inclut un artefact de démonstration C-to-IR assaini de tpm2-sessions.c. La commande suivante démarre l'interface et ouvre la démo :

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

Révision de l'IR de protocole

L'IR de protocole enregistre les décisions sémantiques qui doivent être correctes pour que le modèle formel final ait du sens, notamment :

• les rôles du protocole et les valeurs de configuration à long terme ;
• la construction, l'analyse, le chiffrement, la signature et la vérification des messages ;
• la provenance des valeurs, y compris les valeurs fraîches, les valeurs reçues, les valeurs dérivées et les valeurs révélées ;
• les événements utilisés par les cibles de preuve ;
• les cibles de secret, d'authentification, d'exécutabilité et de contre-exemple attendu ;
• les hypothèses de surface d'attaque.

Indices d'abstraction

L'interface peut localiser la bibliothèque d'indices d'abstraction fournie après le démarrage, mais elle ne l'utilise pas tant que l'utilisateur ne coche pas Use abstraction hints avant de générer Sapic+. Lorsque cette case est cochée, le backend récupère les indices d'ingénierie de preuve depuis :

examples/protocol-abstraction-cases.json

Vous pouvez remplacer cette bibliothèque ou en utiliser une autre avec :

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

Instantanés IR préparés

examples/prepared_workflows/gpt55/ contient des instantanés IR bruts et IR révisés par un humain pour les cas de benchmark. Chaque cas inclut uniquement :

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

Ces fichiers sont des exemples compacts de l'IR avant et après révision humaine.

Flux de travail testés par l'utilisateur

examples/user_tested_workflows/deepseek_ui_20260615/ contient deux flux de travail qui ont réellement été exécutés via l'interface lors de tests manuels :

Toy
Sigfox

Ils incluent les artefacts légers de ces exécutions de l'interface : artefacts d'entrée/révision, prompts, métadonnées d'appels LLM, modèles Tamarin générés, sorties de compilation/réparation et journaux de preuve. Les identifiants API ne sont pas inclus.

Pour les inspecter dans l'interface, démarrez le serveur avec cette bibliothèque de flux de travail :

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

Ouvrez ensuite l'interface, utilisez Select prepared workflow..., et choisissez easy / Toy ou easy / Sigfox.

Bibliothèque de flux de travail existante

Vous pouvez éventuellement exposer un répertoire de flux de travail préparés à importer depuis l'interface :