UI de Revisão de IR de Protocolo Guiada por Confiança

Este repositório contém uma UI local human-in-the-loop para modelagem de protocolos de segurança auxiliada por LLM. Ela suporta o fluxo de trabalho descrito em nosso trabalho:

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

O sistema introduz uma representação intermediária de protocolo (IR) como um checkpoint semântico entre descrições de protocolo em linguagem natural e a geração de Sapic+/Tamarin, permitindo que revisores auditem modelos de protocolo gerados por LLM quanto à precisão semântica antes da verificação formal.

Pré-visualização da UI

As capturas de tela abaixo mostram o fluxo de trabalho preparado do Sigfox carregado na UI de revisão.

Importação do Fluxo de Trabalho

Revisão de Campos

Resultados do Tamarin

Estrutura do Repositório

• run_contract_review_ui.py: servidor HTTP local e API de fluxo de trabalho.
• contract_review_ui/: UI do navegador.
• protocol_ir_pipeline/: processamento de IR, geração de contrato de modelagem, geração de Sapic+, reparo, lint de prova e auxiliares do Tamarin.
• protocol_ir_pipeline/c_to_ir.py: extração em estágios de código-fonte C/C++ para ProtocolIR com prompts embutidos.
• scripts/c_to_protocol_ir.py: ponto de entrada de linha de comando para o fluxo de extração de C/C++.
• config/: configuração padrão local de lint/recuperação.
• examples/ui_input_cases.json: entradas de benchmark prontas para a UI usadas nos experimentos.
• examples/ui_inputs.md: entradas de benchmark fáceis de copiar para preencher manualmente a UI, agrupadas por dificuldade.
• examples/protocol-abstraction-cases.json: biblioteca de dicas de abstração incluída, usada apenas quando habilitada na UI.
• examples/prepared_workflows/gpt55/: snapshots de IR bruto e IR revisado por humanos para os casos de benchmark.
• examples/user_tested_workflows/deepseek_ui_20260615/: fluxos de trabalho Toy e Sigfox testados manualmente pelo autor através da UI.
• NOTICE.md: notas de atribuição e escopo do artefato.
• LICENSE: texto da licença GPLv3.

Requisitos

• Python 3.10+
• Uma chave de API de LLM para DeepSeek, OpenAI, Anthropic ou um endpoint Llama compatível com OpenAI
• tamarin-prover no seu PATH para compilação/verificação de prova. Instale o Tamarin Prover seguindo as instruções oficiais para sua plataforma: https://tamarin-prover.com/manual/master/book/002_installation.html.

Instale as dependências do Python:

pip install -r requirements.txt

Configure as credenciais:

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

Executar a UI

Comece com um diretório de fluxo de trabalho vazio:

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

Abra:

http://127.0.0.1:8765/

Fluxo de trabalho típico:

1. Cole uma descrição de protocolo em linguagem natural e gere o IR bruto/contrato de modelagem.
2. Revise e edite os campos semânticos em Messages, Checks, Events, Proof Targets e Attack Surface.
3. Clique em Save Reviewed para gravar modeling_contract.reviewed.json.
4. Clique em Generate Sapic+.
5. Compile e prove com Tamarin se tamarin-prover estiver instalado.

Save Reviewed não exige que todos os badges de revisão sejam confirmados. Confirmar campos é útil para o acompanhamento do progresso da revisão e para dicas de geração críticas para a prova, mas as edições salvas ainda são usadas pela geração.

Extração de Código-Fonte C/C++

Os estágios de extração, contratos de saída JSON e prompts estão em protocol_ir_pipeline/c_to_ir.py.

Execute a extração em estágios com um LLM:

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

Este repositório inclui um artefato de demonstração C-to-IR sanitizado de tpm2-sessions.c. O comando a seguir inicia a UI e abre a demonstração:

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

Revisão de IR de Protocolo

O IR de Protocolo registra as decisões semânticas que precisam estar corretas para que o modelo formal final seja significativo, incluindo:

• papéis do protocolo e valores de configuração de longo prazo;
• construção, análise, criptografia, assinatura e verificação de mensagens;
• proveniência de valores, incluindo valores frescos, valores recebidos, valores derivados e valores revelados;
• eventos usados por alvos de prova;
• alvos de sigilo, autenticação, executabilidade e contraexemplos esperados;
• suposições de superfície de ataque.

Dicas de Abstração

A UI pode localizar a biblioteca de dicas de abstração incluída após a inicialização, mas não a utiliza a menos que o usuário marque Use abstraction hints antes de gerar Sapic+. Quando essa caixa de seleção está habilitada, o backend recupera dicas de engenharia de prova de:

examples/protocol-abstraction-cases.json

Você pode substituir esta biblioteca ou usar outra com:

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

Snapshots de IR Preparados

examples/prepared_workflows/gpt55/ contém snapshots de IR bruto e IR revisado por humanos para os casos de benchmark. Cada caso inclui apenas:

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

Esses arquivos são exemplos compactos do IR antes e depois da revisão humana.

Fluxos de Trabalho da UI Testados pelo Usuário

examples/user_tested_workflows/deepseek_ui_20260615/ contém dois fluxos de trabalho que foram realmente executados através da UI durante testes manuais:

Toy
Sigfox

Eles incluem os artefatos leves dessas execuções da UI: artefatos de entrada/revisão, prompts, metadados de chamadas ao LLM, modelos Tamarin gerados, saídas de compilação/reparo e logs de prova. Credenciais de API não estão incluídas.

Para inspecioná-los na UI, inicie o servidor com esta biblioteca de fluxos de trabalho:

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

Em seguida, abra a UI, use Select prepared workflow... e escolha easy / Toy ou easy / Sigfox.

Biblioteca de Fluxos de Trabalho Existente

Opcionalmente, você pode expor um diretório de fluxos de trabalho preparados para importar da UI:

python3 run_contract_review_ui.py \
  --run-dir runs/local_demo \
  --workflow-library-dir /path/to/prepared/workflows \
  --provider deepseek

Entradas de Benchmark

examples/ui_input_cases.json contém 18 entradas de protocolo preparadas para esta UI de revisão. Elas são representadas como descrições em linguagem natural, suposições, objetivos e resultados esperados que podem ser copiados para a UI.