Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

이 논문은 7 개의 최첨단 LLM 이 생성한 3,500 개의 코드 아티팩트를 Z3 SMT 솔버를 통해 형식 검증한 결과, 모든 모델이 평균 55.8% 의 취약점을 포함하며 기존 보안 도구들이 이 중 97.8% 를 놓치고 있음을 보여줍니다.

핵심

🛠️ "기본값으로 망가짐": AI 가 쓴 코드가 왜 위험한가? (간단 요약)

이 논문은 **"AI 가 코드를 짜주면, 우리가 안심하고 쓸 수 있을까?"**라는 질문에 대해 아주 엄격한 방법으로 답을 찾은 연구입니다. 결론부터 말하면, "아직은 절대 안 됩니다. 기본 설정 그대로라면 AI 는 보안 구멍이 숭숭 뚫린 코드를 만들어냅니다."

이 복잡한 연구를 일상적인 비유로 쉽게 설명해 드릴게요.

---

1. 연구의 배경: "요리사"와 "레시피"

지금 전 세계의 개발자들은 AI(인공지능) 를 마치 초고수 요리사처럼 쓰고 있습니다. "이거 만들어줘"라고 말하면 AI 가 바로 요리 (코드) 를 만들어줍니다. 하지만 문제는 이 요리사가 위생 기준을 전혀 지키지 않고 있다는 것입니다.

연구진 (Cobalt AI) 은 7 개의 최신 AI 모델에게 보안이 중요한 요리 (코드) 500 가지를 시켰습니다. 그리고 그 결과물을 수학적으로 검증했습니다.

2. 실험 방법: "수학으로 증명하는 폭탄 찾기"

기존의 보안 검사 도구들은 "이런 패턴이 나오면 위험해"라고 패턴만 보고 판단합니다. 마치 "빨간색 옷을 입으면 도둑일지도 몰라"라고 추측하는 것과 비슷하죠.

하지만 이 연구는 **Z3(SMT 솔버)**라는 수학의 두뇌를 사용했습니다.

• 비유: AI 가 만든 코드를 보고, "이 코드가 실제로 해킹당할 수 있을까?"라고 묻는 대신, **"이 코드가 해킹당하는 상황을 수학적으로 100% 증명해봐"**라고 시킨 것입니다.
• 수학이 "네, 이 입력값을 넣으면 바로 터집니다 (Exploit)"라고 증명하면, 그건 더 이상 '가능성'이 아니라 확실한 폭탄이 됩니다.

3. 충격적인 결과: "모든 요리사가 실패함"

7 개의 AI 모델 (GPT-4o, Gemini, Claude 등) 을 모두 테스트한 결과는 참담했습니다.

• 평균 실패율: AI 가 만든 코드 10 개 중 5.6 개는 보안 구멍이 있었습니다. (약 55.8%)
• 등급: 모든 AI 가 F 학점을 받았습니다. 가장 잘한 AI(Gemini 2.5 Flash) 도 D 학점 (약 48% 실패) 에 그쳤습니다.
• 가장 큰 문제: '정수 오버플로우' (숫자가 너무 커서 터지는 현상) 같은 실수가 가장 많았습니다. 마치 고무줄을 너무 많이 늘려서 끊어지게 만드는 실수를 AI 가 자꾸 저지르는 것입니다.

4. 추가 실험 3 가지: "왜 이렇게 안 되는 걸까?"

① "조금 더 조심해줘"라고 부탁했나? (Secure Prompt)

"제발 안전한 코드를 만들어줘"라고 AI 에게 특별히 부탁해봤습니다.

• 결과: 실패율이 64% 에서 60% 로 약 4% 포인트 줄었습니다.
• 중요한 점: 이 실험은 전체 500 개 코드가 아닌, **50 개 코드로 구성된 작은 하위 집합 (v1)**에서 진행된 것입니다. 즉, "안전하게 만들어줘"라는 지시어는 아주 제한적인 규모에서도 효과가 미미했음을 보여줍니다.
• 비유: "요리사야, 식중독 나지 않게 조심해!"라고 외쳐봤자, 요리사가 습관이 잘못되어 있으니 소용이 없었습니다. AI 는 "안전해"라고 말하면서도 여전히 위험한 재료를 섞어 넣습니다.

② "기존 보안 프로그램들은 뭘 하고 있었나?" (Static Tool Comparison)

우리가 평소 쓰는 보안 프로그램들 (Semgrep, CodeQL 등) 이 이 코드를 검사해봤습니다.

• 결과: AI 가 만든 수학적으로 증명된 폭탄 100 개 중 98 개를 찾아내지 못했습니다. (97.8% 놓침)
• 비유: 기존 보안 프로그램들은 눈으로 보이는 구멍만 찾습니다. 하지만 AI 가 만든 폭탄은 수학적으로만 터지는 보이지 않는 구멍이라, 기존 프로그램들은 "여긴 안전해"라고 오판했습니다.

③ "스스로 고칠 수 있나?" (Generation-Review Asymmetry)

AI 가 만든 위험한 코드를 다시 그 AI 에게 보여주고 "여기 위험한 점 있어?"라고 물었습니다.

• 결과: AI 는 **78%**의 확률로 "아, 여기 위험하네요!"라고 정확히 찾아냈습니다.
• 비유: 요리사 자신이 만든 요리에 독이 있다는 건 알지만, 막상 요리를 만들 때는 그걸 잊어버리고 독을 넣는 것입니다. 즉, AI 는 '지식'은 있지만, '실천'을 못 합니다.

5. 결론: 우리가 무엇을 해야 할까?

이 연구는 AI 코딩 도구가 **"기본값 (Default) 으로 망가져 있다"**고 선언합니다.

1. AI 가 쓴 코드는 '검증되지 않은 코드'로 생각하세요. 마치 낯선 사람이 만든 음식을 직접 맛보지 않고는 먹지 않는 것처럼, AI 코드는 반드시 사람이 다시 확인해야 합니다.
2. "안전하게 만들어줘"라고 말하는 것만으로는 부족합니다. AI 의 습관을 바꾸기엔 그 정도 지시어는 약하며, 실험 규모가 작더라도 효과가 미미했습니다.
3. 기존 보안 프로그램만 믿지 마세요. AI 가 만든 코드의 숨겨진 위험 (수학적 폭탄) 은 기존 프로그램이 찾아내지 못합니다.
4. 수학적 검증 (Formal Verification) 이 필요합니다. 코드가 실제로 터지지 않는지 수학적으로 증명하는 과정이 필수적입니다.

한 줄 요약:

"AI 는 코드를 짜는 데는 천재지만, 보안을 지키는 데는 아직 어린아이 수준입니다. 우리가 직접 안전장치를 설치하지 않으면, AI 가 만든 코드는 폭탄이 될 수 있습니다."

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

• 현황: GitHub Copilot 등 AI 코딩 어시스턴트가 보안이 중요한 영역 (웹 백엔드, 임베디드 시스템, 암호화 라이브러리 등) 의 프로덕션 코드 생성에 광범위하게 사용되고 있음.
• 문제점: AI 가 생성한 코드의 보안 속성은 충분히 연구되지 않았으며, 기존 연구들은 대부분 패턴 매칭이나 수동 검사를 기반으로 하여 실제 악용 가능성 (Exploitability) 을 수학적으로 증명하지 못함.
• 핵심 질문: 최신 LLM(대형 언어 모델) 이 보안 민감한 작업을 수행할 때 얼마나 많은 취약한 코드를 생성하는가? 그리고 기존 정적 분석 도구들은 이를 얼마나 잘 탐지하는가?

2. 연구 방법론 (Methodology)

이 연구는 COBALT 분석 파이프라인을 구축하여 7 개의 최첨단 LLM 과 3,500 개의 코드 아티팩트 (500 개의 프롬프트 × 7 개 모델) 를 분석했습니다.

• 데이터셋 구성:

  • 500 개의 자연어 프롬프트를 5 가지 CWE(취약점 분류) 카테고리에 걸쳐 구성 (각 100 개):
    • MEM: 메모리 할당, 배열 인덱싱 (CWE-131/190)
    • INT: 정수 연산, 타입 캐스팅 (CWE-190/195)
    • AUTH: 비밀번호 해싱, 인증 토큰 (CWE-916)
    • CRYPTO: 키 생성, 난수 사용 (CWE-327/330)
    • INP: SQL 구성, 파일 경로 처리 (CWE-89/22/78)
  • 모델: GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, Llama 4 Scout 등 7 개 모델.
  • 설정: 재현성을 위해 Temperature 0(결정적 모드) 사용.

• 분석 도구 (COBALT Pipeline):

  1. CWE 패턴 추출: AST(추상 구문 트리) 및 정규식을 통해 잠재적 취약점 지점 식별.
  2. Z3 SMT 솔버 적용: 취약점 조건을 Z3(만족 가능성 modulo theories) 수식으로 인코딩.
     • 예: malloc(n * sizeof(T))에서 n이 오버플로우를 일으키는 값인지 수학적으로 증명.
  3. 증거 (Witness) 추출: Z3 가 'SAT'(만족 가능) 를 반환하면, 구체적인 입력 값 (예: n = 2^30 + 1) 을 추출하여 수학적으로 증명된 악용 가능성으로 분류.

• 검증 단계:

  • 런타임 검증: Z3 로 증명된 7 개의 대표 사례에 대해 GCC AddressSanitizer(ASAN) 를 사용하여 실제 런타임 충돌 (Crash) 발생 여부를 확인.
  • 비교 실험:
    1. 보안 프롬프트 제거 (Ablation): 명시적인 보안 지시어가 포함된 프롬프트 사용 시 취약점 감소율 측정. 이 실험은 전체 500 개 프롬프트가 아닌, 재현성 확보를 위해 선별된 50 개 프롬프트의 서브 코퍼스 (v1) 에서 수행되었습니다.
    2. 정적 분석 도구 비교: Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL 등 6 가지 산업 표준 도구와의 탐지율 비교.
    3. 생성 - 검토 비대칭성 (Generation-Review Asymmetry): 모델이 생성한 취약 코드를 다시 모델에게 검토하게 하여 취약점을 인지하는지 확인.

3. 주요 결과 (Key Results)

A. 전반적인 취약점 발생률

• 평균 취약점률: 모든 모델에서 **55.8%**의 코드가 적어도 하나의 취약점을 포함함.
• 모델별 성능:
  • GPT-4o: 62.4% (등급 F, 가장 취약)
  • Gemini 2.5 Flash: 48.4% (등급 D, 가장 우수)
  • 결론: 어떤 모델도 C 등급 (30~44% 미만) 이상을 달성하지 못함.
• Z3 증명: 1,055 개의 취약점이 Z3 SMT 솔버를 통해 수학적으로 악용 가능함이 증명됨.
• 런타임 검증: 7 개 대표 사례 중 6 개가 ASAN 을 통해 실제 메모리 손상 (Heap overflow, OOB read 등) 을 일으키는 것으로 확인됨.

B. 취약점 분포 (CWE 카테고리별)

• 정수 연산 (INT): **87%**의 취약점률 (가장 높음). 할당 크기 계산 시 정수 오버플로우 방지 로직 누락이 주원인.
• 메모리 할당 (MEM): 67% 취약점률.
• 입력 처리 (INP): 56%, 인증 (AUTH): 44%, 암호화 (CRYPTO): 25%.

C. 보안 프롬프트의 효과 (RQ4)

• 명시적인 보안 지시어 ("보안 모범 사례 준수", "정수 오버플로우 방지" 등) 를 프롬프트에 추가했을 때, 50 개 프롬프트로 구성된 서브 코퍼스 (v1) 기준 평균 취약점률은 64.8% 에서 60.8% 로 4%p 감소에 그침.
• 5 개 모델 중 4 개는 여전히 F 등급을 유지. 메모리 할당 관련 취약점은 거의 개선되지 않음.

D. 정적 분석 도구와의 비교 (RQ5)

• 산업 표준 도구의 한계: 6 가지 도구 (Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL) 를 모두 합쳐도 아티팩트의 7.6% 만 탐지함.
• Z3 증명된 취약점 미탐지율: Z3 로 수학적으로 증명된 90 개 취약점 중 97.8% (88 개) 를 모든 도구가 놓침.
• CodeQL: 90 개 중 0 개 탐지 (100% 실패).
• 원인: 기존 도구들은 패턴 매칭이나 데이터 흐름 분석에 의존하며, malloc(n * sizeof(T))와 같은 연산에서 n이 오버플로우를 일으킬 수 있는지 수학적 (산술적) 추론을 수행하지 못함.

E. 생성 - 검토 비대칭성 (RQ6)

• 모델이 생성한 Z3 증명 취약 코드를 다시 모델에게 검토하게 했을 때, 78.7% (70/89) 의 경우 취약점을 정확히 식별함.
• 의미: 모델은 보안 지식을 가지고 있으나, 코드 생성 시에는 이를 적용하지 못함. 이는 보안에 대한 지식 부족이 아니라, 생성 과정에서의 적용 실패 (False Negative) 임을 시사.

4. 주요 기여 및 의의 (Contributions & Significance)

1. 형식적 검증의 도입: AI 생성 코드의 취약점 분석에 Z3 SMT 솔버를 적용하여, 단순한 패턴 매칭이 아닌 **수학적 증명 (Ground-truth exploitability)**을 제시한 최초의 대규모 연구 중 하나임.
2. "Broken by Default" 결론: 현재 LLM 기반 코딩 어시스턴트는 보안이 기본으로 결함이 있는 (Security-deficient) 상태로 코드를 생성하며, 단순한 프롬프트 엔지니어링 (보안 지시어 추가) 만으로는 해결되지 않음을 증명.
3. 도구의 구조적 한계 규명: 기존 정적 분석 도구 (CodeQL 등) 가 AI 가 생성한 정수 오버플로우와 같은 특정 유형의 취약점을 구조적으로 탐지할 수 없음을 입증. 이는 설정 문제 (Configuration issue) 가 아닌 방법론적 한계임.
4. 실무적 권고:
   • AI 가 생성한 C/C++ 코드는 검토되지 않은 코드로 간주하고 명시적인 보안 감사 필요.
   • -fsanitize=address,undefined 플래그를 사용하여 런타임 검증 필수.
   • 정수 오버플로우와 같은 복잡한 취약점 탐지를 위해 형식적 검증 (Formal Verification) 또는 인간 전문가의 검토를 병행해야 함.

5. 결론

이 연구는 AI 코딩 도구가 보안 민감한 분야에서 사용되기 전에 **형식적 검증 (Formal Verification)**이 필수적인 단계로 도입되어야 함을 강력히 주장합니다. 현재 LLM 들은 생성 모드와 검토 모드 간의 심각한 비대칭성을 보이며, 기존 자동화 도구들은 AI 가 생성한 코드의 핵심 취약점을 놓치고 있습니다. 따라서 AI 생성 코드의 안전성을 보장하기 위해서는 패턴 기반 분석을 넘어선 수학적 증명 기반의 검증 파이프라인 구축이 시급합니다.