laplace1002/tamarinagentInterfaccia utente human-in-the-loop che converte descrizioni di protocolli in linguaggio naturale o C/C++ in un Protocol IR revisionabile, quindi genera modelli Sapic+/Tamarin per la verifica formale della sicurezza.
Questo repository contiene una UI locale human-in-the-loop per la modellazione di protocolli di sicurezza assistita da LLM. Supporta il flusso di lavoro descritto nel nostro lavoro:
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
Il sistema introduce una rappresentazione intermedia (IR) del protocollo come checkpoint semantico tra le descrizioni in linguaggio naturale dei protocolli e la generazione Sapic+/Tamarin, consentendo ai revisori di verificare l'accuratezza semantica dei modelli di protocollo generati da LLM prima della verifica formale.
Gli screenshot seguenti mostrano il flusso di lavoro preparato per Sigfox caricato nella UI di revisione.
run_contract_review_ui.py: server HTTP locale e API del flusso di lavoro.contract_review_ui/: UI del browser.protocol_ir_pipeline/: elaborazione IR, generazione del contratto di modellazione, generazione Sapic+, riparazione, lint delle prove e helper Tamarin.protocol_ir_pipeline/c_to_ir.py: estrazione a stadi da sorgente C/C++ a ProtocolIR con prompt incorporati.scripts/c_to_protocol_ir.py: punto di ingresso da riga di comando per il flusso di estrazione C/C++.config/: configurazione locale predefinita di lint/retrieval.examples/ui_input_cases.json: input di benchmark pronti per la UI utilizzati per gli esperimenti.examples/ui_inputs.md: input di benchmark facili da copiare per compilare manualmente la UI, raggruppati per difficoltà.examples/protocol-abstraction-cases.json: libreria di suggerimenti di astrazione inclusa, utilizzata solo se abilitata nella UI.examples/prepared_workflows/gpt55/: snapshot IR grezzi e IR revisionati manualmente per i casi di benchmark.examples/user_tested_workflows/deepseek_ui_20260615/: flussi di lavoro Toy e Sigfox testati manualmente dall'autore tramite la UI.NOTICE.md: note di attribuzione e ambito dell'artefatto.LICENSE: testo della licenza GPLv3.tamarin-prover nel tuo PATH per la verifica di compilazione/prova. Installa Tamarin Prover seguendo le istruzioni ufficiali per la tua piattaforma: https://tamarin-prover.com/manual/master/book/002_installation.html.Installa le dipendenze Python:
pip install -r requirements.txt
Configura le credenziali:
cp .env.example .env
# edit .env and set the provider API key
Avvia con una directory di flusso di lavoro vuota:
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--provider deepseek \
--host 127.0.0.1 \
--port 8765
Apri:
http://127.0.0.1:8765/
Flusso di lavoro tipico:
Save Reviewed per scrivere modeling_contract.reviewed.json.Generate Sapic+.tamarin-prover è installato.Save Reviewed non richiede che ogni badge di revisione sia confermato. Confermare i campi è utile per il monitoraggio dell'avanzamento della revisione e per i suggerimenti di generazione critici per la prova, ma le modifiche salvate vengono comunque utilizzate dalla generazione.
Le fasi di estrazione, i contratti di output JSON e i prompt sono in protocol_ir_pipeline/c_to_ir.py.
Esegui l'estrazione a stadi con 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
Questo repository include un artefatto demo C-to-IR sanitizzato di tpm2-sessions.c. Il comando seguente avvia la UI e apre la 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
Il Protocollo IR registra le decisioni semantiche che devono essere corrette affinché il modello formale finale sia significativo, tra cui:
La UI può individuare la libreria di suggerimenti di astrazione inclusa dopo l'avvio, ma non la utilizza a meno che l'utente non selezioni Use abstraction hints prima di generare Sapic+. Quando quella casella è abilitata, il backend recupera i suggerimenti di proof-engineering da:
examples/protocol-abstraction-cases.json
Puoi sostituire questa libreria o usarne un'altra con:
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--abstraction-hints-path /path/to/protocol-abstraction-cases.json
examples/prepared_workflows/gpt55/ contiene snapshot IR grezzi e IR revisionati manualmente per i casi di benchmark. Ogni caso include solo:
ir/protocol_ir.json
ir/protocol_ir.reviewed.json
Questi file sono esempi compatti dell'IR prima e dopo la revisione umana.
examples/user_tested_workflows/deepseek_ui_20260615/ contiene due flussi di lavoro che sono stati effettivamente eseguiti tramite la UI durante i test manuali:
Toy
Sigfox
Includono gli artefatti leggeri di quelle esecuzioni della UI: artefatti di input/revisione, prompt, metadati delle chiamate LLM, modelli Tamarin generati, output di compilazione/riparazione e log delle prove. Le credenziali API non sono incluse.
Per ispezionarli nella UI, avvia il server con questa libreria di flussi di lavoro:
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
Poi apri la UI, usa Select prepared workflow... e scegli easy / Toy o easy / Sigfox.
Puoi opzionalmente esporre una directory di flussi di lavoro preparati da importare dalla 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 contiene 18 input di protocollo preparati per questa UI di revisione. Sono rappresentati come descrizioni in linguaggio naturale, assunzioni, obiettivi e risultati attesi che possono essere copiati nella UI.