신뢰도 기반 프로토콜 IR 검토 UI

이 저장소는 LLM 지원 보안 프로토콜 모델링을 위한 로컬 휴먼-인-더-루프 UI를 포함합니다. 이는 우리 연구에서 설명한 워크플로를 지원합니다:

LLM 지원 보안 프로토콜 모델링을 위한 신뢰도 기반 프로토콜 IR

이 시스템은 자연어 프로토콜 설명과 Sapic+/Tamarin 생성 사이의 의미론적 체크포인트로서 프로토콜 중간 표현(IR)을 도입하여, 검토자가 형식 검증 전에 LLM이 생성한 프로토콜 모델의 의미론적 정확성을 감사할 수 있게 합니다.

UI 미리보기

아래 스크린샷은 검토 UI에 로드된 Sigfox 준비된 워크플로를 보여줍니다.

워크플로 가져오기

필드 검토

Tamarin 결과

저장소 구조

• run_contract_review_ui.py: 로컬 HTTP 서버 및 워크플로 API.
• contract_review_ui/: 브라우저 UI.
• protocol_ir_pipeline/: IR 처리, 모델링 계약 생성, Sapic+ 생성, 복구, 증명 린트, Tamarin 헬퍼.
• protocol_ir_pipeline/c_to_ir.py: 임베디드 프롬프트를 사용한 단계별 C/C++ 소스에서 ProtocolIR 추출.
• 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/: 저자가 UI를 통해 수동으로 테스트한 Toy 및 Sigfox 워크플로.
• NOTICE.md: 저작자 표시 및 아티팩트 범위 노트.
• LICENSE: GPLv3 라이선스 텍스트.

요구 사항

• Python 3.10+
• DeepSeek, OpenAI, Anthropic 또는 OpenAI 호환 Llama 엔드포인트용 LLM API 키
• 컴파일/증명 검증을 위해 PATH에 tamarin-prover. 플랫폼에 맞는 공식 지침에 따라 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

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/

일반적인 워크플로:

1. 자연어 프로토콜 설명을 붙여넣고 원시 IR/모델링 계약을 생성합니다.
2. Messages, Checks, Events, Proof Targets, Attack Surface의 의미론적 필드를 검토하고 편집합니다.
3. Save Reviewed를 클릭하여 modeling_contract.reviewed.json을 작성합니다.
4. Generate Sapic+를 클릭합니다.
5. tamarin-prover가 설치되어 있으면 Tamarin으로 컴파일하고 증명합니다.

Save Reviewed는 모든 검토 배지가 확인될 것을 요구하지 않습니다. 필드 확인은 검토 진행 상황 추적 및 증명에 중요한 생성 힌트에 유용하지만, 저장된 편집은 여전히 생성에 사용됩니다.

C/C++ 소스 추출

추출 단계, 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

이 저장소에는 tpm2-sessions.c의 정제된 C-to-IR 데모 아티팩트가 포함되어 있습니다. 다음 명령은 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

프로토콜 IR 검토

프로토콜 IR은 최종 형식 모델이 의미 있으려면 정확해야 하는 의미론적 결정을 기록하며, 다음을 포함합니다:

• 프로토콜 역할 및 장기 설정 값;
• 메시지 구성, 파싱, 암호화, 서명 및 검증;
• 신선한 값, 수신된 값, 파생된 값 및 공개된 값을 포함한 값 출처;
• 증명 대상에서 사용되는 이벤트;
• 비밀성, 인증, 실행 가능성 및 예상 반례 대상;
• 공격 표면 가정.

추상화 힌트

UI는 시작 후 번들된 추상화 힌트 라이브러리를 찾을 수 있지만, 사용자가 Sapic+를 생성하기 전에 Use abstraction hints를 체크하지 않으면 사용하지 않습니다. 해당 체크박스가 활성화되면 백엔드는 다음에서 증명 엔지니어링 힌트를 검색합니다:

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

준비된 IR 스냅샷

examples/prepared_workflows/gpt55/에는 벤치마크 케이스에 대한 원시 IR 및 인간 검토 IR 스냅샷이 포함되어 있습니다. 각 케이스는 다음만 포함합니다:

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

이 파일들은 인간 검토 전후의 IR에 대한 간결한 예시입니다.

사용자 테스트 UI 워크플로

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에는 이 검토 UI를 위해 준비된 18개의 프로토콜 입력이 포함되어 있습니다. 이들은 UI에 복사할 수 있는 자연어 설명, 가정, 목표 및 예상 결과로 표현됩니다.

수동 테스트를 위해 examples/ui_inputs.md에는 동일한 케이스가 Easy, Medium, Hard 섹션으로 그룹화된 하나의 복사 친화적 Markdown 파일로 포함되어 있습니다.

포함된 케이스:

Example, NSPK, Naxos, Toy, Woo_Lam, sigfox, EDHOC, KEMTLS, LAK06, SPLICE,
SSH, CCITT_X509, Denning_Sacco, Kao_Chow, NSSK, Neuman_Stubblebine,
Otway_Rees, Yahalom

저작자 표시

examples/ui_input_cases.json의 벤치마크 입력은 AutoSM 18-케이스 벤치마크 입력에서 구성되었습니다. 전체 AutoSM 벤치마크 참조 Sapic+/Tamarin 파일은 이 패키지에 포함되어 있지 않습니다.

Ziyu Mao, Jingyi Wang, Jun Sun, Shengchao Qin, and Jiawen Xiong. "LLM-Aided Automatic Modeling for Security Protocol Verification." ICSE 2025. DOI: 10.1109/ICSE55347.2025.00197.

AutoSM 아티팩트 저장소: https://github.com/zerrymore/AutoSM

이 패키지는 LICENSE에 GPLv3 라이선스 텍스트와 함께 배포됩니다. 아티팩트 범위 저작자 표시 노트는 NOTICE.md를 참조하세요.