Anthropic이 소프트웨어 검증 전문 업체 Theorem과 협업해, 자사 AI 모델 Claude를 이용해 123개의 실제 오픈소스 라이브러리에 대한 formal verification(정형 검증) 증명을 생성했다고 밝혔다. 그동안 수십 명의 전문가가 수년에 걸쳐야 했던 작업을 LLM이 대규모로 자동화할 수 있다는 걸 보여준 사례로, 이 과정에서 수조 번의 테스트에서도 발견되지 않았던 버그들까지 찾아냈다. AI가 버그를 찾아 공격하는 능력이 빠르게 발전하는 상황에서, 반대로 AI가 코드에 버그가 ‘없다’는 것을 수학적으로 증명하는 데 쓰일 수 있다는 점에서 보안 업계가 주목할 만한 소식이다.

정형 검증이란 무엇이고 왜 어려웠나

정형 검증은 소프트웨어 코드를 수학적 모델로 변환한 뒤, 그 코드가 특정 보안 규칙을 항상 만족한다는 것을 증명하는 기법이다. 증명에 실패하면 그 지점에 규칙을 위반할 수 있는 버그가 있다는 뜻이고, 실패 원인을 분석해 버그를 고친 뒤 다시 증명을 시도하는 과정을 반복한다. 이 과정을 끝까지 마치면 해당 규칙을 어기는 버그가 전혀 없다는 것을 수학적으로 보장받을 수 있다.

문제는 이 증명 작업이 원본 코드보다 몇 배나 더 크고 복잡해질 수 있고, 극히 전문적인 인력이 필요하다는 점이다. 원문에 따르면 seL4 운영체제 커널을 구현하는 데는 2명이 1년씩 일한 수준(2인년)이 걸렸지만, 이를 정형 검증하는 데는 20인년이 소요됐다. 이런 비용 때문에 정형 검증은 에어버스 항공 전자 소프트웨어처럼 단 하나의 결함도 용납할 수 없는 극히 일부 미션 크리티컬 분야에서만 제한적으로 쓰여왔다.

Claude는 어떻게 123개 라이브러리를 검증했나

Anthropic과 Theorem 연구팀은 Claude에게 123개 오픈소스 라이브러리에 대해 유용한 보안 속성을 증명하도록 요청했다. 구체적으로는 각 프로그램이 특정 조건에서 절대 비정상 종료되지 않는다는 것, 즉 메모리 안전성 오류나 어서션 실패 없이 항상 정상 종료된다는 것을 증명했다.

이 증명은 임의의 조건이 아니라 명확히 정의된 범위 안에서 이뤄졌다. 64MB 미만의 모든 입력값, 모델링된 모든 리눅스 운영체제 응답과 메모리 레이아웃에 대해, 프로그램이 RISC-V CPU에서 리눅스 OS를 사용하는 단일 스레드 정적 바이너리로 고정된 메모리 예산을 가지고 실행된다는 가정 하에 검증이 진행됐다. 특히 주목할 점은 이 검증이 소스 코드 수준이 아니라 RISC-V 어셈블리 코드 수준에서 이뤄졌다는 것인데, Anthropic은 이를 AI가 프로덕션 소프트웨어를 어셈블리 코드 레벨까지 대규모로 정형 검증한 첫 사례라고 설명했다.

물론 이것이 ‘모든’ 버그를 잡아낸다는 뜻은 아니다. 원문에서도 “아직 모든 가능한 버그를 고치는 것과는 거리가 멀다”고 명시하고 있다. 다만 기존보다 훨씬 가까워졌고, 그 목표로 가는 구체적인 경로를 제시했다는 데 의미를 둔다.

테스트로는 못 찾은 버그를 증명 과정에서 발견

흥미로운 부분은 Claude가 증명을 작성하는 과정에서 부수적으로 실제 버그를 발견했다는 점이다. 이 버그들은 수조 번의 테스트 실행(trillions of test runs)에서도 걸러지지 않고 수년간 숨어있던 것들이었다. 이는 정형 검증이 단순히 “버그 없음을 증명하는 사후 작업”이 아니라, 증명을 시도하는 과정 자체가 테스트로는 발견하기 어려운 결함을 찾아내는 효과적인 방법이 될 수 있다는 것을 보여준다.

원문은 리눅스 커널 사례를 함께 언급하며 맥락을 설명한다. 전 세계 수십억 대 기기에서 구동되며 가장 철저하게 테스트된 소프트웨어 중 하나로 꼽히는 리눅스 커널에서도 최근 1,000건이 넘는 취약점이 공개된 바 있다. 아무리 테스트를 많이 해도 모든 경로를 다 커버할 수는 없다는 현실을 보여주는 대목이며, 바로 이 지점에서 정형 검증 같은 수학적 증명 기반 접근이 테스트를 보완할 수 있다는 것이 연구팀의 주장이다.

기존 보안 기법과 무엇이 다른가

퍼징(fuzzing)이나 정적 분석 같은 기존 자동화 보안 도구들은 알려진 패턴의 버그를 빠르게 찾아내는 데는 강하지만, “더 이상 버그가 없다”는 것을 증명하지는 못한다. 반면 정형 검증은 정의된 규칙 범위 안에서는 버그가 ‘전혀 없다’는 수학적 보장을 제공한다. 그동안 이 강력한 보장을 얻는 비용이 너무 커서 실무에 적용하기 어려웠는데, LLM이 증명 작성이라는 노동 집약적 작업을 대신하면서 비용 구조 자체가 바뀌고 있다는 것이 이번 연구의 핵심 메시지다.

Anthropic은 공격자 역시 AI를 이용해 “겉보기에 무해한 버그들을 연결해 치명적인 익스플로잇으로 만드는” 능력이 점점 발전하고 있다고 경고하면서, 방어 측에서도 이에 대응할 만한 수준의 AI 기반 기법이 필요하다는 점을 강조한다. 즉 이번 연구는 AI 대 AI 보안 경쟁에서 방어 측이 활용할 수 있는 새로운 무기로 정형 검증을 제시한 셈이다.

한국 개발자에게 어떤 의미가 있나

Anthropic은 생성한 증명 중 일부를 RISC-V 및 OS 의미 체계와 함께 공개해 누구나 검증하고 재사용할 수 있도록 할 예정이라고 밝혔다. 또한 협업 파트너인 Theorem은 다른 오픈소스 프로젝트에 대해서도 동일한 파이프라인을 실행해주는 서비스를 제공할 의향이 있다고 언급했다. 이는 당장 상용화된 제품은 아니지만, 보안이 중요한 한국의 금융·인프라·임베디드 소프트웨어 개발팀이라면 앞으로 이런 서비스나 공개된 증명 자료를 눈여겨볼 만하다.

다만 현재 수준에서는 적용 범위가 특정 조건(단일 스레드, 고정 메모리 예산, RISC-V, 64MB 미만 입력 등)으로 제한돼 있어, 모든 소프트웨어에 바로 적용할 수 있는 범용 도구는 아니라는 점은 분명히 해둘 필요가 있다. 또한 원문에서 구체적인 성공률, 소요 시간, 비용 등 정량적 수치는 공개되지 않아, 실무 도입 가능성을 판단하려면 추가 정보가 더 필요해 보인다. 그럼에도 LLM이 이전에는 사람만 할 수 있다고 여겨졌던 고난도 수학적 증명 작업을 대규모로 수행했다는 사실 자체가, 소프트웨어 보안 검증의 패러다임이 바뀌고 있음을 보여주는 신호로 볼 수 있다.

원문: LLMs are making formal software verification feasible at a much larger scale