💻 computer science

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

이 논문은 대규모 언어 모델이 보안 증명을 생성하고 수정하는 데 있어 현재 직면한 한계를 평가하고 드러내는 동시에, 모델의 성능을 향상시키기 위한 실질적인 전략을 제공하기 위해 677개의 암호화 체계와 7개의 형식 검증 언어에 걸친 700개의 인스턴스로 구성된 포괄적인 벤치마크인 CrypFormBench를 소개한다.

원저자: Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

게시일 2026-06-25

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

개요: "번역가" 문제

당신이 매우 안전한 금고(암호화 스킴)를 설계하는 숙련된 건축가라고 상상해 보세요. 당신은 누구나 이해할 수 있도록 영어로 설계도를 작성합니다. 하지만 이 금고의 약점을 실제로 구축하고 테스트하려면, 특정 하이테크 보안 로봇(Scyther나 Tamarin 같은 형식 검증 도구)만이 이해할 수 있는 매우 엄격하고 고대적인 언어로 그 설계도를 번역해야 합니다.

이 번역 작업은 매우 어렵습니다. 금고 설계와 로봇의 엄격한 언어를 모두 알고 있는 전문가가 필요합니다. 만약 쉼표 하나를 놓치거나 단어 하나를 잘못 사용하면, 로봇은 설계도를 거부하거나, 더 심각하게는 겉보기에는 안전해 보이지만 숨겨진 백도어가 있는 금고를 만들어 버릴 수도 있습니다.

질문: 거대 언어 모델(LLM)—우리가 오늘날 사용하는 AI 챗봇들—이 이러한 전문 번역가 역할을 할 수 있을까요? 평범한 영어로 된 보안 프로토콜 설명을 듣고, 보안 로봇을 위한 완벽하고 오류 없는 코드를 즉시 작성할 수 있을까요?

답변 (이 논문에 따르면): 아직은 아닙니다. 읽고 수정하는 능력은 좋아지고 있지만, 처음부터 직접 쓰는 것에는 여전히 어려움을 겪고 있습니다.

해결책: CrypFormBench ("AI를 위한 체육관")

이 AI 번역가들이 얼마나 뛰어난지 정확히 알아내기 위해, 연구진들은 CrypFormBench(또는 C.F.B)라고 불리는 거대한 테스트장을 구축했습니다.

이것은 700개의 서로 다른 운동 스테이션이 있는 체육관이라고 생각하면 됩니다.

장비: 연구진은 700개의 실제 세계 보안 프로토콜(당신의 휴대폰, 은행, 또는 인터넷에서 사용되는 것들)을 모았습니다.
언어: 이 프로토콜들을 7가지의 "로봇 언어"(SPDL, HLPSL, EasyCrypt 등과 같은 형식 언어)로 번역했습니다.
테스트: 단순히 AI에게 코드를 쓰라고 시킨 것이 아닙니다. 그들은 다섯 가지 특정 기술을 테스트했습니다:
1. 해석 (Interpretation): "여기 로봇 코드가 있습니다. 이것을 영어로 설명해 주세요." (읽기)
2. 생성 (Generation): "여기 영어 설명이 있습니다. 로봇 코드를 작성하세요." (처음부터 쓰기)
3. 완성 (Completion): "여기에 구멍이 뚫린 로봇 코드가 있습니다. 빈칸을 채우세요." (부분적인 작업 수정하기)
4. 변환 (Transformation): "여기에 언어 A의 코드가 있습니다. 이를 언어 B로 다시 쓰세요." (로봇 간의 언어 번역)
5. 교정 (Correction): "이 로봇 코드에 오류가 있습니다. 수정하세요." (디버깅)

결과: AI의 성적표

연구진은 가장 똑똑한 9개의 AI 모델(GPT-4o, Claude-3.5, DeepSeek 포함)을 테스트했습니다. 결과는 다음과 같습니다.

1. "읽기 능력" (해석 및 완성)

비유: 교과서를 잘 읽고, 문맥이 이미 존재하기 때문에 문장의 빠진 단어를 채울 수 있는 학생을 상상해 보세요.
결과: AI는 놀라울 정도로 이 작업에 능숙했습니다. 코드 조각이 일부 누락되었거나 코드의 일부가 무엇을 하는지 설명하라는 요청을 받았을 때, 성능이 매우 좋았습니다. 그들은 보안 언어의 "문법"을 이해하고 있었습니다.

2. "쓰기 능력" (생성 및 변환)

비유: 이제 그 똑같은 학생에게 완전히 새로운 교과서를 처음부터 쓰거나, 사전 없이 프랑스어를 일본어로 번역하라고 시킨다고 상상해 보세요. 학생은 환각 현상을 일으키거나, 규칙을 지어내거나, 엄격한 문법을 잊어버리기 시작할 것입니다.
결과: 이 부분이 AI가 실패한 지점입니다.
- 생성: 평범한 영어 설명으로부터 전체 보안 프로토콜을 작성하라는 요청을 받았을 때, 대부분의 AI는 로봇이 실행조차 할 수 없는 코드를 생성했습니다. 이는 마치 문법이 깨진 문장을 쓰는 것과 같았습니다.
- 변환: 한 로봇 언어에서 다른 로봇 언어로 코드를 번역하라는 요청을 받았을 때, AI는 자주 혼란을 겪었습니다. 그들은 두 언어의 규칙을 뒤섞어, 어느 쪽에서도 작동하지 않는 "프랑켄슈타인" 코드를 만들어냈습니다.
- 점수: 가장 뛰어난 AI인 Claude-3.5조차 100점 만점에 48.7점을 받았습니다. 이는 그들의 시도 중 절반 미만이 실제로 보안 도구에서 사용 가능하다는 것을 의미합니다.

3. "수정 능력" (교정)

비유: 만약 학생에게 명확한 오타(예: "receive" 대신 "recieve")가 있는 문장을 준다면, 그들은 쉽게 고칠 수 있습니다. 하지만 문장이 문법적으로는 맞지만 논리적으로 틀린 경우(예: "금고는 모든 이에게 열려 있지만, 안전하다"), 그들은 논리적 오류를 찾는 데 어려움을 겪습니다.
결과: AI는 단순한 구문 오류(오타)를 고치는 데는 능숙했습니다. 그러나 "의미론적(semantic)" 오류, 즉 보안 프로토콜 자체의 논리적 오류를 고치는 데는 어려움을 겪었습니다.

왜 이렇게 어려운가요?

이 논문은 이 "로봇 언어"들이 Python이나 Java와는 다르다는 점을 설명합니다. 이들은 극도로 엄격합니다.

"단 하나의 실수" 규칙: 일반적인 코딩에서는 세미콜론 하나를 빠뜨려도 컴퓨터가 그냥 불평하고 넘어갈 수 있습니다. 하지만 이러한 보안 언어에서는 단 하나의 단어 누락이 전체 보안 증명의 의미를 바꾸어, 안전한 금고를 불안전하게 보이게 하거나 그 반대로 만들 수 있습니다.
"문맥" 문제: 이러한 프로토콜은 종종 긴 사건의 사슬에 의존합니다 (예: "만약 앨리스가 단계 1에서 메시지를 보냈다면, 밥은 단계 2에서 답장을 보내야 하지만, 이는 그가 단계 0의 메시지를 보지 않았을 때만 가능하다"). AI는 이러한 긴 사슬을 놓치곤 합니다.

무엇을 할 수 있을까요? ("보조 바퀴")

논문은 우리가 아직 AI에게 전체 작업을 맡길 수는 없지만, 적절한 도움을 준다면 조수로 사용할 수 있다고 제안합니다.

퓨샷 프롬프팅 (Few-Shot Prompting): 단순히 "이것을 써라"라고 말하는 대신, 먼저 어떻게 쓰는지에 대한 세 가지 예시를 보여주세요. 이것은 치트 시트(컨닝 페이퍼) 역할을 합니다.
Pass@K: AI에게 코드를 5번 시도하게 한 다음, 가장 좋은 것을 선택하게 하세요. 이는 작동하는 버전을 얻을 확률을 높여줍니다.
인간 참여형 (Human-in-the-Loop): AI가 코드를 초안 작성하게 하되, 보안 로봇이 실행하기 전에 인간 전문가가 검토하도록 합니다.

결론

이 논문은 거대 언어 모델이 현재 보안 코드를 이해하고 수정하는 데 있어서는 훌륭한 연구 조수이지만, 처음부터 새로운 보안 프로토콜을 구축하는 신뢰할 수 있는 설계자는 아직 아니라고 결론짓습니다.

그들은 당신이 매뉴얼을 읽고 오타를 고치는 것을 도와줄 수는 있지만, 당신이 열쇠를 넘겨주기 전에 금고가 실제로 안전한지 확인하기 위해서는 여전히 인간 전문가가 필요합니다. 이 벤치마크(CrypFormBench)는 다른 연구자들이 새로운 AI 모델을 이 엄격한 기준에 따라 테스트할 수 있도록 공개되어 있습니다.

기술 요약: CrypFormBench

1. 문제 정의

암호 체계에 대한 수동 형식 분석(Manual formal analysis)은 암호학과 형식 명세 언어 모두에 대한 깊은 전문 지식을 요구하며 노동 집약적입니다. Scyther, Tamarin, CryptoVerif, EasyCrypt와 같은 자동화 도구들이 존재하지만, 이들은 여전히 전문가가 암호 체계의 로직을 특화된 형식 언어(예: HLPSL, SPDL, applied $\pi$ -calculus)로 추상화하는 과정에 의존하며, 이는 오류가 발생하기 쉽습니다. 대규모 언어 모델(LLM)은 자연어로부터 형식 명세를 도출하는 과정을 자동화할 수 있는 잠재적인 해결책을 제공합니다. 그러나 표준화된 평가 방법론의 부재로 인해, 이 분야에서 LLM의 효과는 아직 탐구되지 않은 상태입니다.

기존의 벤치마크들은 다음과 같은 이유로 불충분합니다:

심볼릭 보안(Symbolic security)만을 지원하며, 계산 보안(Computational security)은 간과함.
규모가 제한적이며(예: 약 18개의 프로토콜), 다양한 위협 모델이나 고급 프리미티브(예: 영지식 증명, 양자 내성 암호)를 포함하지 않음.
여러 형식 검증 언어 및 작업 유형(생성, 변환, 수정)에 걸쳐 LLM을 평가할 수 있는 통합된 프레임워크가 부족함.

2. 방법론: CrypFormBench (C.F.B)

저자들은 형식 암호 분석에서 LLM의 능력을 평가하기 위해 설계된 포괄적인 벤치마크인 CrypFormBench를 소개합니다. 이 방법론은 세 가지 핵심 구성 요소로 이루어집니다.

A. 데이터셋 구축

규모 및 다양성: 데이터셋은 4,549개의 오픈 소스 프로젝트 및 도구 데이터셋에서 추출한 700개의 큐레이션된 인스턴스로 구성됩니다. 이 인스턴스들은 677개의 고유한 암호 체계(고전적 인증부터 현대적 MPC, ZK, 양자 내성 설계에 이르기까지)와 160개의 보안 속성을 다룹니다.
언어 커버리지: Scyther(SPDL), Tamarin(SPTHY), AVISPA(HLPSL), ProVerif(PV/HORN), Maude-NPA(MAUDE), CryptoVerif(CV/OCV), EasyCrypt(EC)를 포함한 7가지 주요 형식 검증 언어를 포괄합니다.
적대 모델: 수동/능동 Dolev-Yao 모델부터 확장된 모델(CK, eCK) 및 도메인 특화 위협(예: IoT 비밀번호 추측)에 이르는 다양한 적대자 가정을 포함합니다.
품질 관리: 중복 제거, 실행 가능성 체크, 수동 검증을 포함하는 엄격한 파이프라인이 적용되었습니다. 인스턴스는 "안전(safe, 알려진 공격 없음)" 또는 "불안전(unsafe, 알려진 공격 있음)"으로 라벨링되었으며, 도구의 출력값은 암호학 문헌의 정형 라벨과 일치시켰습니다.

B. 작업 정의

본 벤치마크는 도구 사용이 가능한 형식 명세에 필수적인 다섯 가지 핵심 LLM 능력을 평가합니다:

해석(Interpretation): 형식 코드로부터 표기법 수준의 주석 및 전역 체계 요약을 생성함.
생성(Generation): 자연어 로직 설명을 바탕으로 완전한 형식 코드를 생성함.
완성(Completion): 부분적으로 마스킹된 형식 명세의 누락된 부분을 채움.
변환(Transformation): 의미론을 보존하면서 한 형식 언어에서 다른 형식 언어로 체계 명세를 번역함.
수정(Correction): 컴파일에 실패하는 코드(구문 오류) 또는 잘못된 검증 결과(의미론적 오류)를 생성하는 코드를 수리함.

C. 평가 파이프라인

자동 검증: 엔드 투 엔드 파이프라인은 여러 도구, 버전 및 실행 명령을 통합하여 LLM 출력을 검증합니다. 이는 다양한 호출 동작(예: AVISPA의 경우 여러 백엔드 처리)과 버전 불일치를 처리합니다.
스코어링 프레임워크: 다음 요소들의 균형을 맞춘 가중치 기반 스코어링 시스템을 통해 성능을 측정합니다:
- 실행 가능성(분석 가능성): 코드가 컴파일되고 실행되는지 여부.
- 기능적 정확성: 검증된 보안 속성이 실제 정답(SAFE/UNSAFE)과 일치하는지 여부 (Accuracy( $ACC_A$ ) 및 F1( $F1_A$ )로 측정).
- 유사도: 완성 작업에서의 코드 유사도 및 해석 작업에서의 임베딩을 통한 의미론적 유사도.
- 효율성: 실행 시간 및 파일 크기.

3. 주요 결과

저자들은 9개의 최첨단(SOTA) LLM(GPT-4o, Claude-3.5-Sonnet-Coder, DeepSeek-Coder, LLaMA4-Instruct 포함)을 평가했습니다.

전반적인 성능: 성능은 일반적으로 제한적입니다. 가장 높은 성능을 보인 모델인 Claude-3.5-Sonnet-Coder는 100점 만점에 48.7점의 종합 점수를 기록했습니다.
작업별 통찰:
- 강점: 모델들은 코드 인지 능력을 활용하여 해석과 완성 작업에서 좋은 성능을 보입니다. 예를 들어, DeepSeek-Coder와 GPT-4o는 기존 코드를 해석하는 데 높은 정확도를 보였습니다.
- 약점: 모델들은 생성, 변환, 수정 작업에서 크게 어려움을 겪습니다.
  - 생성: 상위 모델조차 낮은 분석 가능성 비율을 보이며(예: Claude-3.5의 경우 약 15%), EasyCrypt나 Maude와 같은 복잡한 언어의 엄격한 구문 및 의미론을 다루는 데 어려움을 겪습니다.
  - 변환: 가장 어려운 작업입니다. 교차 언어 간섭과 의미론적 불일치로 인해 매우 낮은 분석 가능성(종종 10% 미만)을 보이며, 모델들은 대상 언어의 관용구와 호환되지 않는 소스 조각을 빈번하게 복사합니다.
  - 수정: 모델은 국소적인 구문 오류(컴파일러 가이드 방식)는 수정할 수 있으나, 의미론적 수리(예: 보안 속성에 대한 허위 보고 수정)에는 어려움을 겪습니다.
- 언어별 변동성: 성능은 언어에 따라 급격히 달라집/니다. 모델들은 일반적인 프로그래밍 구문과 유사한 ProVerif(PV)에서는 더 나은 성능을 보이는 반면, Maude-NPA와 같은 재작성(rewriting) 기반 도구에서는 어려움을 겪습니다.
- 최적화 전략:
- Few-Shot 프롬프팅: 생성 작업의 분석 가능성(3-shot 적용 시 6.6%에서 24.9%로)과 수정 작업의 정확성을 유의미하게 향상시킵니다.
- Pass@K: 생성 시도 횟수( $K$ )를 늘리면 특히 어려운 작업에서 분석 가능한 출력을 얻을 확률이 높아지지만, 이것이 의미론적 정확성을 보장하지는 않습니다.
- 미세 조정(Fine-Tuning): Qwen2.5-Coder-3B에 대한 경량 LoRA 미세 조정은 완성 및 수정 능력을 개선했으나, 생성이나 변환에는 미미한 영향을 미쳤습니다.

4. 의의 및 주장

본 논문은 LLM의 암호 체계 분석 평가를 위해 심볼릭 및 계산 보안을 공동으로 다루는 최초의 포괄적인 벤치마크를 제공한다고 주장합니다.

근본적인 관점: 저자들은 LLM이 해석 및 국소적 수정을 위한 유망한 보조 도구이기는 하지만, 형식 체계 생성이나 교차 언어 변환의 엔드 투 엔드 자동화를 수행하기에는 아직 신뢰할 수 없다고 단언합니다.
병목 구간 식별: 주요 장벽은 단순한 의미론적 추론이 아니라 실행 가능성입니다. 즉, 타임아웃이나 파싱 에러를 유발하지 않고 엄격한 형식 구문 및 도구 특유의 제약 조건을 충족하는 코드를 생성하는 능력입니다.
실무적 가이드라인: 본 연구는 실행 가능성 병목 현상을 완화하기 위해 Few-shot 프롬프팅, Pass@K 샘플링, 경량 미세 조정을 포함한 LLM 지원 분석 개선을 위한 구체적인 방향을 제시합니다.
재현성: 벤치마크와 데이터셋을 공개하여 이 분야의 미래 모델들에 대한 체계적이고 표준화되며 재현 가능한 평가를 가능하게 합니다.

저자들은 현재의 LLM이 강력한 "초안 작성(drafting)" 도구 역할을 할 수는 있지만, 형식 암호 분석에 실질적으로 유용하기 위해서는 인간 참여형 검증(human-in-the-loop validation) 또는 도구 가이드 기반의 수리 워크플로우가 반드시 필요하다고 결론짓습니다.