‘충분히 좋은’ AI 시대의 보안 감사

AI 요약

Trail of Bits는 AI 에이전트의 역할이 코드 리뷰에만 그치지 않는다고 설명합니다. Miden VM 보안 감사를 앞두고 약 6개월 동안 에이전트를 활용해 개발 도구와 정적 분석기, 형식 모델을 마련했습니다. 그 결과 보안 결함을 발견하고, Miden 코어 라이브러리의 일부에 관한 정확성 증명 95개를 만들었습니다.

새 가상 머신에 필요한 개발 도구

Miden은 자체 어셈블리 언어인 Miden Assembly(MASM)를 쓰는 영지식 가상 머신입니다. 감사 대상인 코어 라이브러리에는 암호 프리미티브가 들어 있었지만, IDE 지원이나 언어 서버, 린터 같은 개발 도구는 거의 없었습니다. MASM은 스택 머신 방식이라 명령어의 입력과 출력이 스택에 암묵적으로 드러납니다. 코드의 데이터 흐름을 따라가며 검토하기 까다로운 구조입니다.

Trail of Bits는 먼저 Claude를 사용해 며칠 만에 VS Code용 언어 서버 프로토타입을 만들었습니다. 구문 강조, 정의로 이동, 참조 검색, 문서 표시 기능을 구현하고 명령어 설명과 스택 효과 표시도 추가했습니다. 이후 MASM 코드를 더 높은 수준의 표현으로 바꾸는 디컴파일러를 개발했습니다.

MASM 디컴파일은 간단하지 않았습니다. 대부분의 프로시저에 입력과 출력 서명이 없어서 문맥을 보고 추론해야 했습니다. 호출 규약이 정해져 있지 않아 호출 뒤 스택에 남는 값의 수를 정적으로 알아내기 어려웠습니다. 반복문과 조건문에서 분기마다 스택 변화가 달라지면 이후 명령어의 입력이 어느 스택 위치에서 오는지도 추적하기 어렵습니다. 모든 프로시저를 올바르게 디컴파일하기는 어렵다고 보고, 정확성을 유지할 수 있는 언어 부분집합을 대상으로 삼았습니다.

기능을 추가할 때마다 에이전트가 코어 라이브러리의 프로시저를 무작위로 골라 디컴파일하게 하고, 결과를 원본 MASM과 비교했습니다. 발견한 문제는 회귀 테스트에 넣었습니다. 개발 과정에서 AI가 생성한 커밋은 100개가 넘었습니다. 작성자는 완성된 디컴파일 파이프라인보다 그 과정에서 만든 내부 분석 프레임워크와 중간 표현이 더 큰 성과였다고 설명합니다. 이를 정적 분석에도 재사용했습니다.

추상 해석으로 입력 검증 검사

중간 표현에는 명령어의 입력과 출력이 식으로 나타납니다. 이를 바탕으로 데이터 흐름 분석을 적용해 증명자가 제공하는 조언 값이 검증되는지, 32비트 정수나 불리언 같은 타입 제약이 지켜지는지, 모든 실행 경로에서 지역 변수가 초기화되는지 검사했습니다.

분석에는 추상 해석을 사용했습니다. 실제 숫자를 실행하는 대신 각 단계에서 스택 값이 ‘32비트 정수’인지 ‘알 수 없음’인지처럼 가능한 값의 범위를 추적합니다. 분석은 새로운 정보가 더 나오지 않을 때까지 코드를 반복해서 살핍니다. 가능한 경우를 빠뜨리지 않도록 여유를 둔 채 추적하므로, 분석을 통과한 검사는 실제 실행에서도 성립한다고 설명합니다. Claude와 Codex는 분석 엔진과 개별 검사 기능을 만드는 데 쓰였고, 디컴파일러와 MASM 린터에는 명령줄 인터페이스도 추가해 에이전트 기반 코드 리뷰에서 활용하도록 했습니다.

서명 위조로 이어질 수 있는 결함

정적 분석은 타입 검증을 개선할 수 있는 위치 400곳 이상을 찾았습니다. 모두 라이브러리의 공개 API에서 접근할 수 있는 코드였습니다. 그중 심각도가 높은 결함은 mod_12289 프로시저에서 발견했습니다. 이 프로시저는 64비트 값을 12289로 나누고, 몫과 나머지를 증명자가 제공하는 조언 값으로 받습니다. 몫은 두 개의 32비트 값으로 표현되는 유효한 64비트 값인지 검사하지만, 나머지는 검증하지 않은 채 32비트 뺄셈 명령어 u32overflowing_sub에 전달했습니다.

연구진은 뺄셈 제약을 만족하는 범위에서 몫과 나머지를 조정하면 올바른 나머지가 아닌 값을 반환하게 만들 수 있음을 확인했습니다. 악의적인 증명자는 이를 이용해 Falcon 서명을 위조하고, Falcon 키 쌍으로 보호되는 Miden 계정의 자금을 빼낼 수 있었습니다.

Lean으로 정확성 증명

연구진은 버그를 찾는 데서 그치지 않고, 코어 라이브러리 프로시저가 올바르게 구현됐다는 점도 증명할 수 있는지 살폈습니다. Miden 명령어 집합은 작고 대부분의 명령어가 부수 효과가 없어 형식 모델을 만들기 적합했습니다. 먼저 Lean으로 최소한의 Miden VM 실행기를 구현하고, Claude를 사용해 MASM 프로시저를 Lean 코드로 옮기는 변환기를 만들었습니다. 여러 에이전트가 프로시저의 정확성을 증명하는 작업을 병렬로 진행했습니다.

Lean의 커널이 증명 자체를 검사하므로 연구진은 정리의 진술이 해당 프로시저의 올바른 성질을 표현하는지 직접 검토했습니다. 필드 원소와 코어 라이브러리의 정수 타입도 Lean 타입으로 정의해 정리를 읽고 검토하기 쉽게 했습니다. 그 결과 코어 라이브러리의 이진 산술 기능 전반을 다루는 정확성 증명 95개를 만들었습니다. 이 작업은 기존 단위 테스트가 놓친 버그 두 개도 찾았습니다. 64비트 우회전 rotr은 Goldilocks 소수보다 큰 입력에서 회전 이동량이 32의 배수일 때 잘못 동작했습니다. 256비트 곱셈 wrapping_mul은 반환 전에 호출자가 맡긴 스택 값을 버렸습니다.

AI가 바꾼 준비 작업의 비용

Trail of Bits는 언어 서버, 정적 분석 엔진, Lean 라이브러리와 증명 같은 작업을 1~2년 전에는 시간과 자원을 들여 진행하기 어려웠다고 말합니다. 이런 준비 작업은 결과를 미리 예측하기 힘들고, 고객에게 비용을 설명하기도 어렵습니다. 하지만 최근 에이전트가 가벼운 감독만으로 부수 프로젝트를 맡을 만큼 좋아지면서 시도할 만한 작업의 범위가 달라졌다는 설명입니다. 실패한 부수 프로젝트의 비용도 토큰 사용량에 한정된다고 덧붙입니다.

Miden 팀은 감사에서 만든 정적 분석 엔진을 채택했습니다. 따라서 이 도구는 이번 검토뿐 아니라 이후 코어 라이브러리 업데이트에도 쓰입니다. 작성자는 언어 서버와 정적 분석이 수동 검토와 에이전트 검토를 보강했고, Lean 증명이 라이브러리의 중요한 부분에 대한 확신을 높였다고 정리합니다.

Hacker News 반응

• @suhacker256 — AI를 단지 더 빠르게 일하는 데 그치지 않고, 실제로 일을 더 잘하는 데 활용하는 좋은 사례입니다.
  • @buu700 — 차이는 대개 의미상의 차이라고 생각합니다. 일반적으로 어떤 작업이든 하루보다 일주일을 쓰면 더 잘할 수 있습니다. 하루만 쓸 수 있는데 AI가 원래 일주일 걸릴 일을 하루 만에 하게 해준다면, 투입 시간은 그대로여도 결과는 더 좋아집니다.
• @Segv77 — 보안 감사에서 ‘충분히 좋은’ AI라니, ‘충분히 좋은’ 브레이크를 찾는다는 말처럼 들립니다. 방심할 여지가 없습니다.
  • @fovc — 비유를 잘 이해하지 못했습니다. 제가 반대로 읽었다면 죄송합니다. 그래도 브레이크에는 기준을 충족하는 수준이 있고, 브레이크를 끝없이 완벽하게 만들 필요는 없습니다. 마찬가지로 정확성 증명, 기계 번역, 검토하기 쉬운 정리가 있는 검증된 구현은 충분히 좋은 수준에 가까워 보입니다. Claude가 만든 변환기에 많은 것이 달려 있기는 합니다. 그래도 이 프로젝트에서 신뢰해야 하는 코드의 양은 2년 전보다 훨씬 적어 보입니다.
  • @thephyber — 두 분이 같은 단어를 서로 다른 의미나 뉘앙스로 쓰는 것 같습니다. 일상에서 ‘충분히 좋다’는 말은 보통 특정 요구사항을 만족하는 최소 수준을 뜻합니다. 하지만 보안에는 안전과 불안전을 가르는 정확한 기준이 없는 경우가 많습니다. 비용과 절충을 따르는 연속선이고, 그 판단에는 주관적인 가치가 들어갑니다. 고객이 없는 시드 이전 SaaS 스타트업과 수조 달러 자산을 관리하는 은행의 가치 판단은 크게 다릅니다. 따라서 두 조직의 보안 선택도 다르고, 각자의 업계에서 ‘충분히 좋다’는 말도 뜻이 달라집니다.
  • @aftbit — 비유가 이해되지 않습니다. 일반 속도로 달리는 혼다 시빅에는 충분한 브레이크가 소방차나 경주차에는 충분하지 않습니다. 그래도 각 용도에 맞는 ‘충분한’ 기준은 실제로 있습니다.
  • @firen777 — HN에서는 굳이 필요하지 않은 비유를 끼워 넣는 경향이 있습니다. 그보다 더 나쁜 건 그 비유가 말이 안 되는 경우가 많다는 점입니다.
• @AndrewKemendo — 보안 업계는 이제 끝났습니다. 결국 100% 해킹당할 거라는 전제 아래 새로운 사업 방식을 찾아야 합니다. 그걸 미리 가정하면 아키텍처를 다시 생각하게 될 겁니다.
  • @Cider9986 — 완전 동형 암호(FHE)가 좋겠지만, 지금도 종단 간 암호화(E2EE)를 적용할 수 있는 제품이 많습니다. Shinyhunters가 일으킨 침해 사고 중 상당수는 파일을 통째로 가져간 경우입니다. 제가 말하는 방법을 쓰면 이런 피해를 훨씬 잘 막을 수 있습니다. 데이터베이스는 더 까다롭지만, 큰 변화가 필요하다면 시도할 만한 계획입니다. 서버를 신뢰하는 방식은 분명 제대로 작동하지 않습니다. AI는 공격자와 방어자 모두를 빠르게 만들고 있습니다. 하지만 모바일 클라이언트는 이미 일반적인 데스크톱보다 앞서 있습니다. Android의 데스크톱 모드는 운영체제에 들어왔지만, 데스크톱을 대체하려면 개선과 더 강력한 칩이 필요합니다. 원격 공격 방어 기준으로 클라이언트의 순위를 매기면 GrapheneOS, iOS/iPadOS, Pixel 기본 Android, ChromeOS, macOS, Windows, 데스크톱 Linux 순입니다. 더 안전한 클라이언트를 항상 선호해야 합니다. 이제 콘텐츠를 신뢰할 수 있는 곳은 클라이언트뿐입니다. 네이티브 클라이언트는 웹에서 E2EE를 구현하는 문제를 피하고, 어느 때보다 쉽게 만들 수 있습니다. AI를 쓰면 원하는 만큼 자주 소스를 감사할 수 있고, 재현 가능한 빌드로 실제 실행 중인 코드가 그 소스와 같은지도 확인할 수 있습니다.

원문: Trail of Bits / 번역·요약: Trawling