UI de Revisión de IR de Protocolo Guiada por Confianza

Este repositorio contiene una UI local con intervención humana para el modelado de protocolos de seguridad asistido por LLM. Admite el flujo de trabajo descrito en nuestro trabajo:

IR de Protocolo Guiada por Confianza para el Modelado de Protocolos de Seguridad Asistido por LLM

El sistema introduce una representación intermedia (IR) de protocolo como punto de control semántico entre las descripciones de protocolos en lenguaje natural y la generación de Sapic+/Tamarin, lo que permite a los revisores auditar los modelos de protocolo generados por LLM en busca de precisión semántica antes de la verificación formal.

Vista Previa de la UI

Las capturas de pantalla a continuación muestran el flujo de trabajo preparado de Sigfox cargado en la UI de revisión.

Importación del Flujo de Trabajo

Revisión de Campos

Resultados de Tamarin

Estructura del Repositorio

• run_contract_review_ui.py: servidor HTTP local y API del flujo de trabajo.
• contract_review_ui/: UI del navegador.
• protocol_ir_pipeline/: procesamiento de IR, generación de contratos de modelado, generación de Sapic+, reparación, lint de pruebas y asistentes de Tamarin.
• protocol_ir_pipeline/c_to_ir.py: extracción por etapas de código fuente C/C++ a ProtocolIR con prompts integrados.
• scripts/c_to_protocol_ir.py: punto de entrada de línea de comandos para el flujo de extracción de C/C++.
• config/: configuración local predeterminada de lint/recuperación.
• examples/ui_input_cases.json: entradas de benchmark listas para la UI utilizadas en los experimentos.
• examples/ui_inputs.md: entradas de benchmark fáciles de copiar para rellenar manualmente la UI, agrupadas por dificultad.
• examples/protocol-abstraction-cases.json: biblioteca de pistas de abstracción incluida, utilizada solo cuando se habilita en la UI.
• examples/prepared_workflows/gpt55/: instantáneas de IR sin procesar y de IR revisada por humanos para los casos de benchmark.
• examples/user_tested_workflows/deepseek_ui_20260615/: flujos de trabajo Toy y Sigfox probados manualmente por el autor a través de la UI.
• NOTICE.md: notas de atribución y alcance del artefacto.
• LICENSE: texto de la licencia GPLv3.

Requisitos

• Python 3.10+
• Una clave de API de LLM para DeepSeek, OpenAI, Anthropic, o un endpoint de Llama compatible con OpenAI
• tamarin-prover en tu PATH para la compilación/verificación de pruebas. Instala Tamarin Prover siguiendo las instrucciones oficiales para tu plataforma: https://tamarin-prover.com/manual/master/book/002_installation.html.

Instala las dependencias de Python:

pip install -r requirements.txt

Configura las credenciales:

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

Ejecutar la UI

Comienza con un directorio de flujo de trabajo vacío:

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

Abre:

http://127.0.0.1:8765/

Flujo de trabajo típico:

1. Pega una descripción de protocolo en lenguaje natural y genera el IR/contrato de modelado sin procesar.
2. Revisa y edita los campos semánticos en Messages, Checks, Events, Proof Targets y Attack Surface.
3. Haz clic en Save Reviewed para escribir modeling_contract.reviewed.json.
4. Haz clic en Generate Sapic+.
5. Compila y prueba con Tamarin si tamarin-prover está instalado.

Save Reviewed no requiere que se confirme cada insignia de revisión. Confirmar los campos es útil para el seguimiento del progreso de la revisión y para las pistas de generación críticas para la prueba, pero las ediciones guardadas siguen siendo utilizadas por la generación.

Extracción de Código Fuente C/C++

Las etapas de extracción, los contratos de salida JSON y los prompts están en protocol_ir_pipeline/c_to_ir.py.

Ejecuta la extracción por etapas 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

Este repositorio incluye un artefacto de demostración de C-a-IR saneado de tpm2-sessions.c. El siguiente comando inicia la UI y abre la demostración:

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

Revisión del IR de Protocolo

El IR de Protocolo registra las decisiones semánticas que deben ser correctas para que el modelo formal final sea significativo, incluyendo:

• roles del protocolo y valores de configuración a largo plazo;
• construcción de mensajes, análisis, cifrado, firma y verificación;
• procedencia de valores, incluyendo valores frescos, valores recibidos, valores derivados y valores revelados;
• eventos utilizados por los objetivos de prueba;
• objetivos de secreto, autenticación, ejecutabilidad y contraejemplo esperado;
• suposiciones de superficie de ataque.

Pistas de Abstracción

La UI puede localizar la biblioteca de pistas de abstracción incluida después del inicio, pero no la utiliza a menos que el usuario marque Use abstraction hints antes de generar Sapic+. Cuando esa casilla está habilitada, el backend recupera pistas de ingeniería de pruebas de:

examples/protocol-abstraction-cases.json

Puedes reemplazar esta biblioteca o usar otra con:

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

Instantáneas de IR Preparadas

examples/prepared_workflows/gpt55/ contiene instantáneas de IR sin procesar y de IR revisada por humanos para los casos de benchmark. Cada caso incluye solo:

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

Estos archivos son ejemplos compactos del IR antes y después de la revisión humana.

Flujos de Trabajo de la UI Probados por el Usuario

examples/user_tested_workflows/deepseek_ui_20260615/ contiene dos flujos de trabajo que se ejecutaron realmente a través de la UI durante las pruebas manuales:

Toy
Sigfox

Incluyen los artefactos ligeros de esas ejecuciones de la UI: artefactos de entrada/revisión, prompts, metadatos de llamadas al LLM, modelos Tamarin generados, salidas de compilación/reparación y registros de pruebas. Las credenciales de la API no están incluidas.

Para inspeccionarlos en la UI, inicia el servidor con esta biblioteca de flujos de trabajo:

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

Luego abre la UI, usa Select prepared workflow... y elige easy / Toy o easy / Sigfox.

Biblioteca de Flujos de Trabajo Existente

Opcionalmente, puedes exponer un directorio de flujos de trabajo preparados para importar desde la UI:

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

Entradas de Benchmark