laplace1002/tamarinagentUI с участием человека в цикле, который преобразует описания протоколов на естественном языке или C/C++ в проверяемый Protocol IR, а затем генерирует модели Sapic+/Tamarin для формальной верификации безопасности.
Этот репозиторий содержит локальный UI с участием человека в цикле для моделирования протоколов безопасности с помощью LLM. Он поддерживает рабочий процесс, описанный в нашей работе:
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
Система вводит промежуточное представление протокола (IR) как семантическую контрольную точку между описаниями протоколов на естественном языке и генерацией Sapic+/Tamarin, позволяя рецензентам проверять семантическую точность сгенерированных LLM моделей протоколов до формальной верификации.
Приведённые ниже скриншоты показывают подготовленный рабочий процесс Sigfox, загруженный в UI проверки.
run_contract_review_ui.py: локальный HTTP-сервер и API рабочего процесса.contract_review_ui/: браузерный UI.protocol_ir_pipeline/: обработка IR, генерация контракта моделирования, генерация Sapic+, исправление, линтинг доказательств и вспомогательные средства Tamarin.protocol_ir_pipeline/c_to_ir.py: поэтапное извлечение ProtocolIR из исходного кода C/C++ со встроенными промптами.scripts/c_to_protocol_ir.py: точка входа командной строки для потока извлечения из C/C++.config/: конфигурация локального линтинга/поиска по умолчанию.examples/ui_input_cases.json: готовые для UI входные данные бенчмарка, использованные в экспериментах.examples/ui_inputs.md: удобные для копирования входные данные бенчмарка для ручного заполнения UI, сгруппированные по сложности.examples/protocol-abstraction-cases.json: встроенная библиотека подсказок абстракции, используется только при включении в UI.examples/prepared_workflows/gpt55/: снимки исходного IR и IR, проверенного человеком, для случаев бенчмарка.examples/user_tested_workflows/deepseek_ui_20260615/: рабочие процессы Toy и Sigfox, протестированные автором вручную через UI.NOTICE.md: примечания об атрибуции и области артефакта.LICENSE: текст лицензии GPLv3.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/
Типичный рабочий процесс:
Save Reviewed, чтобы записать modeling_contract.reviewed.json.Generate Sapic+.tamarin-prover.Save Reviewed не требует подтверждения каждого значка проверки. Подтверждение полей полезно для отслеживания прогресса проверки и для критичных для доказательства подсказок генерации, но сохранённые правки всё равно используются при генерации.
Этапы извлечения, контракты вывода 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-to-IR для tpm2-sessions.c. Следующая команда запускает 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 фиксирует семантические решения, которые должны быть корректными, чтобы итоговая формальная модель была осмысленной, включая:
UI может найти встроенную библиотеку подсказок абстракции после запуска, но не использует её, если пользователь не отметит 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
examples/prepared_workflows/gpt55/ содержит снимки исходного IR и IR, проверенного человеком, для случаев бенчмарка. Каждый случай включает только:
ir/protocol_ir.json
ir/protocol_ir.reviewed.json
Эти файлы представляют собой компактные примеры IR до и после проверки человеком.
examples/user_tested_workflows/deepseek_ui_20260615/ содержит два рабочих процесса, которые фактически были запущены через UI во время ручного тестирования:
Toy
Sigfox
Они включают облегчённые артефакты из этих запусков UI: артефакты ввода/проверки, промпты, метаданные вызовов LLM, сгенерированные модели Tamarin, результаты компиляции/исправления и журналы доказательств. Учётные данные 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 содержит 18 входных данных протоколов, подготовленных для этого UI проверки. Они представлены в виде описаний на естественном языке, предположений, целей и ожидаемых результатов, которые можно скопировать в UI.