DeFi Security Summit 2026 AI 보안 발표 정리, 첫째 날
11월 1~2일 뭄바이에서 열린 DeFi Security Summit 2026에서는 발표 106개 중 28개가 AI를 다뤘습니다. 첫째 날 AI 발표를 하나씩 짧게 정리해 주제별로 묶고, 마지막에 배울 점을 적었습니다.
올해 DeFi Security Summit(DSS)은 Devcon 주간에 맞춰 11월 1일과 2일 뭄바이 Courtyard by Marriott Mumbai International Airport에서 열렸습니다. Amber와 Pearl 두 방에서 모두 106개의 발표가 있었는데 그중 28개가 제목에 AI나 LLM, 에이전트를 달고 나왔습니다. 이번 글에서는 첫째 날인 11월 1일 발표를 정리합니다.
개막 기조연설에서 Peter Kacherginsky가 꺼낸 한마디가 이날 분위기를 잘 보여 줍니다. AI가 버그를 찾아내기 시작하면서 해킹이 일주일에 서너 건에서 하루에 서너 건으로 늘었다는 겁니다.
한눈에 보기
- AI 혼자서는 아직 감사가 안 됩니다. Dedaub 실험에서 에이전트 하나가 찾은 버그는 45%, 모두 합쳐도 73%였습니다. 그런데 사람 감사자가 놓친 버그도 16개나 찾아냈습니다.
- 모델마다 놓치는 게 다릅니다. ack3 벤치마크에서 아홉 모델이 모두 찾은 이슈는 40개 중 9개뿐이었습니다. 여러 모델을 여러 번 돌리자 재현율이 75%에서 100%까지 올라갔습니다.
- 복잡하게 짤수록 손해였습니다. 한 문장짜리 프롬프트가 에이전트 40개를 엮은 구성보다 나았고 결과를 크게 바꾼 건 구성이 아니라 컨텍스트였습니다.
- 형식 검증의 증명은 이제 AI가 씁니다. 무엇을 증명할지 정하고 확인하는 일만 사람에게 남았습니다.
- 내 에이전트도 공격 대상입니다. Polygon에서 나온 가장 심각한 문제는 에이전트 주변의 평범한 접근 제어였습니다.
- 하나만 본다면 Gustavo Dutra의 "We Gave AI the Keys to Our CI"를 추천합니다. 실제 회사가 에이전트 17개를 어떻게 지키는지 볼 수 있습니다.
목차
- AI가 컨트랙트를 감사할 수 있나 (발표 4개)
- 에이전트를 어떻게 굴리나 (발표 4개)
- 에이전트도 공격받는다 (발표 2개)
- 감사로 끝나지 않는 보안 (발표 2개)
- AI와 형식 검증 (발표 5개)
- 배울 점
영상 링크를 누르면 그 방의 종일 스트림(Amber, Pearl)에서 해당 발표가 시작하는 시점으로 바로 이동합니다.
AI가 컨트랙트를 감사할 수 있나
네 발표가 AI 감사 도구를 사람의 감사 결과와 비교했습니다. 결론은 비슷했습니다. AI는 사람이 놓친 버그까지 꽤 많이 찾지만 숫자는 어떻게 재느냐에 따라 크게 달라집니다.
Can AI Audit Your Smart Contract? We Tested It on Real Audits.
Mohamad MansouriDedaub
핵심: 답은 "혼자서는 아직 아니다"입니다. 하지만 격차는 빠르게 줄고 있습니다.
Dedaub은 예전에 수행한 고객 감사 8건을 골라 자기네 보고서를 가린 채 같은 코드를 여러 에이전트에게 맡겼습니다. "이 코드를 감사해"라는 프롬프트만 준 기본 모델부터 가볍게 손본 설정, 스캐너 결과를 LLM이 걸러 주는 공개 도구, Dedaub이 직접 만든 파이프라인까지 다양하게 넣었습니다. 보고서에 있던 버그는 모두 61개였습니다.
- Solidity 프로젝트에서 에이전트 하나가 찾은 Medium 이상 버그는 평균 45%였습니다. 에이전트를 전부 합치면 73%까지 올라갔고 Critical은 하나도 놓치지 않았습니다.
- Sui(Move) 프로젝트와 TON 프로젝트를 포함한 8건 전체로 보면 61개 중 29개를 찾았습니다.
- 사람이 놓친 Medium 이상 버그도 16개 나왔습니다. High가 2개, Medium이 14개입니다.
- 6월에 같은 실험을 했을 때는 Dedaub 파이프라인이 기본 모델보다 두 배쯤 잘 찾았습니다. 지금은 최신 플래그십 모델에 프롬프트 한 줄만 줘도 그때 파이프라인보다 낫고 격차도 두 배가 안 됩니다.
버그 바운티라면 심각한 버그 하나만 찾아도 보상이 나오니 AI가 이미 충분히 쓸모 있습니다. 반면 감사는 프로토콜 전체를 책임져야 해서 아직 AI에게만 맡길 단계는 아니라는 게 Mansouri의 결론입니다.
Benchmarking Frontier Models: Which One Is the Best EVM Auditor?
Josef Gattermayerack3
핵심: 모든 버그를 찾는 모델은 없습니다. 여러 모델을 여러 번 돌려야 합니다.
ack3는 코드도 보고서도 한 번도 공개된 적 없는 감사 5건으로 벤치마크를 만들었습니다. 정답이 학습 데이터에 들어갔을 리 없는 조건입니다. 이 감사에서 사람이 찾은 Critical과 High는 32개였습니다.
- 검증된 이슈 40개 가운데 아홉 설정이 모두 찾은 건 9개뿐입니다.
- 전체 점수는 낮았던 Kimi K3가 사람을 포함해 아무도 못 찾은 High 하나를 혼자 찾았습니다.
- 두 번째 실험에서는 swarm이라는 도구로 모델 6개를 큰 코드베이스 하나에 5시간 동안 붙였습니다. 같은 프롬프트를 여러 차례("웨이브") 반복하면서 매번 발견을 서로 공유하게 했더니, 재현율이 첫 회차 뒤 75%에서 모든 회차를 합쳐 100%가 됐습니다.
- GPT 모델 하나는 세 번째 회차까지 계속 새 이슈를 찾아서 이 모델은 세 번은 돌려 보라는 조언까지 나왔습니다.
"대부분을 찾는 것으로 충분할까요? 아닙니다. 전부 찾는 게 필요합니다."
Benchmarking Security Intelligence: Why Web3 AI Security Eval Is Broken
Suryansh SinghOpenZeppelin
핵심: 공개 벤치마크로는 이미 알려진 답밖에 확인할 수 없습니다. 평가 세트는 직접 감사한 비공개 코드로 만들어야 합니다.
올해 화제가 된 웹3 보안 벤치마크는 공개 감사 대회를 문제로 썼는데 이런 대회는 학습 데이터에 들어가 있었을 가능성이 큽니다. 게다가 정답지가 고정돼 있어서 모델이 새로 찾아낸 버그는 점수에 반영되지 않았습니다. 발표에서 제시한 평가 원칙은 이렇습니다.
- 직접 감사한 비공개 코드베이스를 여러 개 씁니다. 물론 고객의 허락을 받아야 합니다.
- 새로 나온 발견은 모두 검토해서 정답지나 알려진 오탐 목록에 추가합니다. 그래야 평가 세트가 계속 자랍니다.
- 오탐은 따로 세고 심각도에 따라 가중치를 둡니다.
- 에이전트에게는 실전에서 쓸 도구를 모두 줍니다.
- 일부러 심은 버그나 작은 연습용 컨트랙트는 쓰지 않습니다. 요즘 모델에게는 너무 쉽습니다.
Why is AI missing these bugs?
Robert ReithAccretion, hackhack
핵심: AI는 사람 감사자가 찾은 버그의 80~90%를 찾습니다. 놓치는 나머지는 대부분 컨텍스트가 부족해서입니다.
Accretion이 지난 Solana 감사들에 자사 AI를 다시 돌려 보면, 사람이 찾은 High와 Critical 가운데 80~90%, 많을 때는 100%를 찾습니다. 유동성 프로토콜 수수료를 써야 할 자리에 제공자 수수료를 쓴 실수처럼 사람이 쉽게 지나치는 것도 잘 잡습니다. 반대로 AI가 놓친 버그는 크게 다섯 가지였습니다.
- 의존성. 관리자 호출이 MetaDAO futarchy를 거쳐 Squads로 이어지는 구조였습니다. 관리자가 Squads 멀티시그라면 호출이 Squads로 되돌아 들어가는데 Solana에서는 이런 재진입이 막혀 있어 실패합니다. 관리자가 Squads일 수 있다는 정보가 컨텍스트에 없었으니 AI가 알 수 없었습니다.
- 생태계 단위의 공격. 어떤 브리지가 Token-2022 기능을 고려하지 않았습니다. 공격자는 민트의 토큰을 브리지로 넘기고 민트를 닫은 뒤, 같은 주소에 Pump.fun 토큰을 새로 만들어 나중에 들어오는 진짜 예치금을 가로챌 수 있습니다.
- 업그레이드 이력. Light Protocol이 Anchor에서 Pinocchio로 옮겨 가면서 예전 버전에서 만든 계정을 업그레이드 뒤에 다시 쓸 수 있게 됐습니다.
- 빠르게 바뀌는 체인. Solana가 슬롯 시간을 절반으로 줄였을 때 시간을 슬롯 수로 계산하는 코드를 짚은 건 사람뿐이었습니다.
- 심각도 판단. 진짜 Critical을 찾고도 Informational로 매긴 경우가 있었습니다. 소수점을 잘못 읽어 공격에 USDC가 18,000이 아니라 184억 개 필요하다고 판단한 탓입니다.
Reith는 이렇게 덧붙였습니다. 모델에게 어떤 컨텍스트를 더 줘야 할지 고민하고 있다면 그 자체로 이미 코드를 감사하고 있는 셈이라고요.
에이전트를 어떻게 굴리나
방법론을 다룬 네 발표는 하나같이 구성은 단순하게, 발견은 스스로 증명하게 하라고 말했습니다.
Don't Trust the First Model: A Methodology for Adversarial AI Audits
Christian VariOak Security
핵심: 모델은 다 봤다고 말하지만 믿으면 안 됩니다. 실제로 읽었는지 확인하고 다른 모델이 발견을 반박하게 해야 합니다.
Oak는 단계마다 통과 조건을 둔 다섯 단계로 감사를 진행합니다.
- 범위 확인. 여러 모델이 나눠서 저장소를 다 봤는지가 아니라, 모델 하나하나가 모든 파일을 읽었는지 확인합니다.
- 탐색. 여러 회사의 모델이 서로 따로 작업하는데 Oak의 과거 발견 자료 없이 한 번, 자료를 주고 한 번 돌립니다. 발견은 공격자, 전제 조건, 위치, 찾은 모델까지 적은 검증 가능한 주장 형태로 남깁니다.
- 중복 제거. 근본 원인이 같은 발견끼리 합칩니다.
- 검증. 다른 모델이 새 컨텍스트에서 각 주장을 반박해 보고 실제로 공격 경로가 닿는지 확인합니다. Vari가 가장 중요하게 꼽은 단계입니다. 검증 안 된 발견 200개를 넘겨받는 건 연구자에게 시간 낭비일 뿐이니까요.
- 누락 점검. 판정을 내지 못했거나 범위를 다 읽지 않은 실행은 다시 돌리고 그래도 안 되면 사람이 직접 보도록 넘깁니다.
"보안 연구자로서 보안 연구자들에게 부탁합니다. 첫 번째 모델을 믿지 마세요."
Certiflai: orchestrating swarms for certifications
George KobakhidzeConsensys Diligence
핵심: 한 줄짜리 프롬프트가 에이전트 40개짜리 구성을 이겼습니다. 최종적으로 쓴 건 에이전트 둘에 늘 같은 결과를 내는 분석 도구와 작업 기록을 붙인 구성이었습니다.
Kobakhidze는 코드가 보안 표준을 지키는지 확인하는 인증 업무를 에이전트에게 맡겼습니다. 전문가들이 가장 지루해하는 일이죠. 그래서 "에이전트에게는 재미라는 개념이 없고, 지시만 있으면 잘 해낸다"고 했습니다. Uniswap v2와 Morpho Blue를 대상으로 45번쯤 돌리며 세 가지 구성을 비교했습니다.
- 에이전트 하나에 한 문장 프롬프트. 점수가 가장 높았고 비용도 쌌습니다. 한 번에 30센트쯤 든 적도 있습니다. 다만 돌릴 때마다 결과가 달랐고 판단 근거가 빈약했으며 평가해야 할 코드를 멋대로 고치기도 했습니다.
- 마크다운 파일 17개 정도로 짠 서브에이전트 계층. 본인 표현으로는 "재앙"이었습니다. 한때 에이전트 40개 정도가 동시에 돌면서 실행 한 번에 수백 달러가 나갔고 DNS 오류 하나가 전체로 번지기도 했습니다. 모든 에이전트가 같은 컨텍스트를 매번 읽어야 하니 비용이 불어난 겁니다. 100명이 2개씩 보는 것보다 2명이 100개를 보는 게 낫다는 비유가 딱 맞습니다.
- Certiflai. 작성자와 검토자, 에이전트 둘로만 짠 LangGraph 구성입니다. 격리된 VM에서 퍼저와 정적 분석기를 함께 돌립니다. 점수는 가장 좋은 구성과 같았고 사람이 다시 확인할 수 있는 근거도 남았습니다. 에이전트는 판정을 제안만 하고 보고서는 Python 프로그램이 씁니다. 에이전트가 정말 일을 했는지는 파일 해시, 읽기 기록, 일부러 심어 둔 함정(canary)으로 확인합니다.
개인적으로는 "에이전트는 많을수록 좋다"는 통념을 뒤집는 사례로 이날 들은 발표 가운데 가장 설득력이 있었습니다.
Patch the Planet: Three Lessons for DeFi from AI Bug Hunting
nisedoTrail of Bits
핵심: 찾는 방법을 일일이 알려 주기보다 목표를 잘 정하고 일을 잘 나누는 데 힘을 써야 합니다.
Patch the Planet은 Trail of Bits가 OpenAI와 함께 핵심 오픈소스 소프트웨어의 버그를 찾아 고치는 프로그램입니다. 목표를 달성할 때까지 에이전트가 알아서 작업을 이어 가는 Codex의 /goal 기능을 씁니다. 발표에서는 이 경험을 DeFi에 맞게 세 가지로 정리했습니다.
- 목표는 에이전트가 직접 쓰고 스스로 따져 보게 합니다. "find bugs in the vault" 같은 막연한 목표를 "권한 없는 사용자가 남의 자금을 훔칠 수 있음을 PoC로 증명하라"처럼 구체적으로 다듬는 식입니다. 공격자는 관리자가 아니라 위협 모델에 맞는 사람이어야 하고 증거도 말이 아니라 실제로 돌아가는 익스플로잇이어야 합니다.
- 버그 하나보다 버그 유형을 쫓습니다. share inflation 공격 같은 알려진 익스플로잇에서 출발해 유형을 한 문장("rounding errors in share math")으로 정리한 다음, 새 에이전트에게 다른 곳에서 같은 유형을 찾게 합니다.
- 에이전트 하나에는 공격 표면 하나만 맡깁니다. 모든 에이전트가 같은 위협 모델을 공유하고 먼저 에이전트가 가장 유망한 공격 표면 다섯 곳을 고르면 곳마다 세션을 하나씩 엽니다. 나머지를 자유롭게 살피는 세션도 하나 따로 둡니다.
Fuzzing with Coding Agents: What Works in Practice
Josef Gattermayerack3
핵심: 에이전트가 짠 퍼즈 테스트는 버그 대부분을 빠르게 잡지만 시간 순서에 따라 생기는 버그는 놓칩니다.
ack3는 코딩 에이전트에게 자사 Python 프레임워크 Wake로 퍼즈 테스트를 짜게 했습니다.
- 인위적인 미로 벤치마크. 기존 퍼저들은 8시간을 돌려도 목표 153개 중 70~75개 정도에 그쳤습니다. 에이전트가 짠 테스트는 한 시간 남짓 만에 전부 도달했습니다.
- 현실에 가까운 벤치마크. 사람이 짠 테스트가 찾은 버그 6개를 에이전트도 모두 재현했지만 결과가 들쭉날쭉했습니다. 한 번에 가장 많이 찾은 게 4개였습니다.
- 약점은 시간. 에이전트는 시스템을 지금 상태 그대로만 테스트합니다. 그래서 경쟁 조건이나 "결제가 시작된 뒤에 무슨 일이 생기나" 같은 시나리오를 놓칩니다.
Gattermayer의 말을 빌리면 "버그의 80~90%를 잡는 데는 정말 잘 통하는" 방식입니다.
에이전트도 공격받는다
두 발표는 방향을 바꿔 AI를 지켜야 할 대상으로 봤습니다. 공격받는 에이전트와 인프라, 그리고 AI가 쏟아내는 리포트를 어떻게 감당할지에 관한 이야기입니다.
We Gave AI the Keys to Our CI — Then We Tried to Hack It
Gustavo DutraPolygon Labs
핵심: "모델의 거절은 보안 경계가 아닙니다." 에이전트는 처음부터 이미 탈취됐다고 가정하고 설계해야 합니다.
Polygon에는 AI 덕분에 버그 리포트가 한 달에 200건 넘게 들어오고 엔지니어들은 클라우드 에이전트로 일주일에 풀 리퀘스트를 200개 넘게 엽니다. 이걸 사람이 다 볼 수 없으니 보안 에이전트 17개가 리포트 분류, 모든 PR 리뷰, 위협 모델 작성, 레드팀 작업을 나눠 맡습니다. 설계 원칙은 네 가지입니다.
- 입력은 언제나 데이터로만 다루고 명령으로 해석하지 않습니다.
- 쓰기 권한은 꼭 필요한 곳에만 주고 전부 샌드박스 안에서 돌립니다.
- 위험한 작업은 사람이 직접 실행합니다.
- 에이전트 출력에는 사람 태그나 링크를 넣을 수 없게 막아, 에이전트가 직원을 낚는 통로가 되지 않게 합니다.
팀이 직접 자기 에이전트를 공격해 보니 모델은 프롬프트 인젝션을 대부분 걸러 냈습니다. 그런데 메시지 끝에 붙인 꼬리말 하나가 검사를 통과해 에이전트에서 에이전트로 번졌습니다. 해결책은 모델이 아니라 인프라에 있었습니다. 다른 에이전트가 만든 입력에는 그렇다는 표시를 붙였습니다. 가장 심각했던 문제는 초기에 쓰던 사내 코딩 에이전트에서 나왔습니다. 세션이 회사 전체에 공개돼 있었고 세션마다 Git 자격 증명과 셸이 붙어 있어서 회사 사람이라면 누구든 다섯 단계만 거치면 남의 세션을 가로채 다른 엔지니어 이름으로 코드를 올릴 수 있었습니다.
첫째 날 발표 중 하나만 꼽으라면 개인적으로는 이 발표입니다. 가장 심각한 버그가 "에이전트 자체가 아니라 평범한 접근 제어"에 있었다는 점이 특히 와닿았습니다.
What a libp2p Gossipsub Crash Taught Us About AI Security and DeFi Infrastructure
Manu Sheel Guptalibp2p
핵심: AI 때문에 인프라 쪽 보안 리포트가 폭증했습니다. 리포트 처리 체계는 AI가 실제로 필요한 곳을 중심으로 짜야 합니다.
gossipsub의 정수 오버플로 하나로 합의 노드가 멈출 수 있었습니다. 발표는 이것이 동기화 중단, 오라클 피드 정지, 청산 실패로 어떻게 번지는지 짚었습니다.
- 최근 석 달 사이 libp2p에 들어온 보안 리포트는 Gupta가 경력 전체에서 받은 양과 맞먹고 앞으로 여섯 달 동안은 그 열 배가 올 수 있습니다. 그중 상당수는 사소하거나 남이 이미 낸 것과 겹치는 리포트입니다.
- libp2p 구현체는 17개이고 그중 7개를 이더리움 합의 클라이언트가 씁니다. 수정이 모든 구현체에 반영돼야 의미가 있는데 Gupta는 바로 이 작업에 AI가 가장 쓸모 있다고 봅니다.
"일단 AI를 도입하자"가 아니라 "어디에 AI가 필요한가"부터 따져 보라는 조언이었습니다.
감사로 끝나지 않는 보안
Lido의 짧은 발표 두 개는 한 문장으로 요약됩니다. "감사는 한순간의 스냅숏이고, 보안은 계속 살아 있어야 한다."
Evergreen: continuous AI-augmented security by Lido x Nethermind
Eugene MaminLido
핵심: AI를 쓸모 있게 만든 건 어떤 모델을 쓰느냐가 아니라 어떤 컨텍스트를 주느냐였습니다.
- Lido는 올해 보안 회사 8곳에서 감사를 30번 받았는데 Critical과 High는 하나도 나오지 않았습니다.
- 버그 바운티로는 지금까지 $410,000를 지급했습니다. 하지만 화이트햇들이 Critical이라고 낸 리포트 약 180건 가운데 실제로 보상한 건 3건뿐입니다. "안타깝게도 일의 대부분은 '아니요'라고 답하는 겁니다."
- Nethermind와 함께 핵심 코드 약 1만 9,000줄을 대상으로 4주짜리 AI 파일럿을 진행했습니다.
파일럿에서 얻은 교훈은 세 가지입니다.
- 결과를 좌우한 건 컨텍스트였습니다. 시간 대부분은 모델을 고르는 데가 아니라 문서를 모으는 데 들었습니다.
- 설계 의도는 반드시 글로 남겨야 합니다. 에이전트든 감사자든 의도까지 짐작할 수는 없습니다.
- 엔진 하나에 의존하면 안 됩니다. 실제로 Lido의 내부 도구는 서로 다른 모델 4개로 저장소 39개를 24시간 돌립니다.
The Audit That Never Ends: Evergreen Security in the Age of LLMs
Sergey KhomutininLido
핵심: 감사를 개발 과정 안으로 끌어들이고 출시 뒤에도 멈추지 않아야 합니다.
Lido의 내부 시스템 Lens는 거창한 게 아니라 "안에 Claude Code나 Codex 같은 평범한 코딩 에이전트"를 두고 거기에 알맞은 컨텍스트와 질문을 주는 구조입니다. 코드나 문서가 바뀌거나 하드포크가 다가오거나 새 모델이 나오면 그때마다 점검을 다시 돌립니다. 공개된 성과는 두 가지입니다.
- Glamsterdam 하드포크 호환성을 점검하다가 합의 명세의 버그를 찾았습니다. 대기 중인 검증자 예치금이 공개 키가 같은 빌더에게 잘못 귀속돼 자금이 사라질 수 있는 문제였고 수정은 이미 반영됐습니다.
- Lido의 크로스체인 거버넌스가 의존하던 Wormhole 전달 서비스가 중단됐습니다. 코드를 한 줄도 바꾸지 않았어도 계속 점검해야 하는 이유입니다.
공격자도 똑같은 LLM을 쓰는 만큼 "보안 수준도 계속 올라가야 한다"는 게 Khomutinin의 말입니다. 설계 문서에 적힌 원칙도 같습니다. "도구는 제안하고, 결정은 팀이 한다."
AI와 형식 검증
다섯 발표가 AI 덕분에 형식 검증(formal verification)을 실무에서 쓸 수 있게 됐는지 물었습니다. 답은 반반이었습니다. 증명은 이제 AI가 써 주지만 무엇을 증명할지는 여전히 사람이 정해야 합니다.
AI-FV: Slop or Prop? Explorations in Agentic Formal Verification
Jonathan MevsQuantstamp
핵심: "숫자만 보면 쓰레기(slop) 쪽에 가깝다"지만 감사자 입장에서는 여전히 쓸모가 있습니다.
Mevs는 형식 검증 전문가가 아닌 일반 감사자도 AI의 도움을 받으면 형식 검증 도구를 쓸 수 있는지 실험했습니다. 대상은 2023년 감사에서 버그 11개가 알려진 700줄 남짓의 Aave 볼트였습니다. Claude로 Certora AutoProver, Runtime Verification의 Kontrol, Solidity 컴파일러의 SMTChecker, 세 도구의 하네스를 작성했습니다.
- AutoProver가 가장 좋아서 Medium 4개 중 2개를 잡았고 SMTChecker는 AutoProver가 놓친 Medium 하나를 찾았습니다.
- 찾은 것 대부분은 실제로 일어날 수 있는 문제였지만 보고서에 올릴 만한 건 많지 않았습니다.
- 한 번 돌리는 데 수십 시간과 수백 달러어치 토큰이 들었습니다.
그래도 찾아낸 엣지 케이스는 수동 리뷰의 좋은 길잡이가 되고 고객이 고친 코드에 명세를 다시 돌려 볼 수도 있습니다. 다만 감사자 혼자 형식 검증까지 끝내는 수준은 아직 아닙니다.
Symbolic Execution of Math-Heavy Code in the Age of AI
Neville GrechDedaub
핵심: DeFi의 수학 코드 앞에서는 대부분의 기호 실행 엔진이 멈춥니다. Dedaub은 검증할 수 있는 부분에만 AI를 써서 훨씬 많은 경로를 분석합니다.
Uniswap V3에서 틱을 가격으로 바꾸는 함수 하나에만 분기가 20개 정도 있어 실행 경로가 약 백만 개로 늘어납니다. Dedaub 엔진은 이걸 이렇게 풉니다.
- 바이트코드를 더 높은 수준의 표현으로 바꾸고 컴파일러 최적화를 되돌려 원래 수식에 가깝게 복원합니다.
- 경로가 "확실히 불가능한지" "가능할 수도 있는지"만 빠르게 판단합니다.
- 수학 라이브러리 함수의 요약은 AI에게 쓰게 하고 퍼징으로 실제 코드와 맞는지 검증합니다. "당연히 AI를 그대로 믿지는 않습니다."
- 그 대가로 늘어난 오탐은 AI 에이전트가 걸러 냅니다.
From Production Rust to Lean 4 Proofs: A Verification Pipeline with AI Provers
Natalia KlausRuntime Verification
핵심: AI 증명기는 증명 작업을 떠받치는 "외골격"이지만 아무것도 증명하지 않는 빈 명세를 쓰기도 합니다.
실제 서비스에 쓰이는 Rust 암호 코드를 Lean 4 증명으로 옮기는 이더리움 재단 프로젝트입니다.
- 증명은 AI 증명기 Aristotle과 Aleph가 마무리합니다. 어려운 보조정리 하나에 약 $200와 24시간이 들었습니다.
- Klaus는 AI 이전에 증명을 손으로 쓰던 시절을 "맨손으로 땅을 파는 일"에 비유했습니다.
- 문제는 AI가 "증명하기는 쉽지만 아무 내용도 없는 공허한 명세를 자주 쓴다"는 점입니다. 그런 명세는 증명해 봐야 아무것도 보장하지 않으니, 명세는 사람이 하나하나 확인해야 합니다.
Formal Verification in the Age of AI: New Powers, New Traps
Petar CalicSpectra
핵심: 형식 검증으로 버그를 더 찾지는 못했지만 더 근본적인 수정을 이끌어 냈습니다.
Calic은 실제 운영 코드에 인플레이션 공격의 변형을 심어 두고 문서를 주는 수준을 세 단계로 나눠 서로 독립된 에이전트 실행을 6번 했습니다. 절반은 Foundry 테스트로, 나머지 절반은 Certora CVL로 검증하게 했습니다.
- 공격자가 이득을 볼 수 있다고 분명히 짚은 에이전트는 하나도 없었습니다. 이 한 가지로 심각도가 완전히 달라지는데 여러 번 다시 물어본 뒤에야 나왔습니다.
- 불가능한 상태에서 나온 반례는 사람이 걸러 내야 했습니다. 증명을 통과시키려고 모델을 "단순화"하다가 버그 자체를 지워 버린 에이전트도 있었습니다.
- 차이는 수정 방식에서 났습니다. 다른 실행들은 decimal offset을 키우는 데 그쳤는데 이건 공격 비용을 높일 뿐입니다. 형식 검증을 거친 에이전트는 예치금을 내부에서 따로 추적하게 바꿔 오류가 수학적으로 불가능하게 만들었습니다.
그래서 Calic은 명세에 훨씬 많은 시간을 쓰고 명세만큼은 "가장 휘기 어려운 기준"으로 지키라고 조언했습니다. "AI는 테스트를 구현에 맞춰 고쳐 버리는 일이 잦기" 때문입니다.
Formal Verification in the Age of AI
Benjamin FloresVerity
핵심: 요즘 형식 검증이 갑자기 화제인 건 LLM이 증명을 쓸 수 있게 됐기 때문입니다. 사람에게는 명세를 쓰는 일이 남습니다.
명세를 쓰는 일이 크게 쉬워진 건 아닙니다. 달라진 건 증명입니다. 이제는 SMT 솔버에 더해 LLM이 수학자처럼 증명을 씁니다. Flores의 표현으로는 "수학 박사 10명보다 낫고" 비용도 쌉니다. 그래서 이제 "올바른 코드라면 전부 증명할 수 있다"고 말합니다. Flores는 AI 코딩 시대의 병목을 코드 리뷰로 보는데 형식 검증을 쓰면 리뷰할 대상이 명세로 줄어든다고 설명합니다. GPT 5.4가 약 $45로 만들어 낸 Lido V3 볼트 지급 능력 증명이 지금 어디까지 왔는지 보여 줍니다.
배울 점
- AI만으로는 아직 감사가 아니지만 AI 없이 감사하는 것도 이제는 답이 아닙니다. Mansouri의 실험에서 에이전트는 혼자서 버그의 절반쯤, 합치면 73%를 찾았고 사람이 놓친 것도 16개 찾았습니다. Reith의 AI는 사람 팀이 찾은 것의 80~90%를 찾습니다. 둘 다 돌리고 서로 무엇을 놓쳤는지 비교해야 합니다.
- 모델은 여러 개, 실행은 여러 번. ack3 벤치마크에서 모델들이 함께 찾은 이슈는 40개 중 9개뿐이었고 점수가 낮은 모델이 혼자 High를 찾기도 했습니다. 실행을 반복하자 재현율은 75%에서 100%로 올랐습니다. 모델 하나를 한 번 돌린 결과는 표본 하나에 불과합니다.
- 구성을 복잡하게 짜는 것보다 컨텍스트를 채우는 게 먼저입니다. Lido가 가장 큰 효과를 본 건 컨텍스트 자료와 글로 남긴 설계 의도였고 Reith의 사례에서 AI가 놓친 버그도 모두 컨텍스트가 빠져서였습니다. Kobakhidze의 실험에서는 한 줄 프롬프트가 에이전트 40개를 이겼습니다.
- 발견은 스스로 증명하게 해야 합니다. 새 컨텍스트에서 반박해 보고 PoC를 요구하고 에이전트가 무엇을 읽었는지 기록으로 남겨야 합니다. Vari의 검증 단계, nisedo의 "PoC로 증명하라", Kobakhidze의 함정은 모두 같은 문제를 겨냥합니다. 확인했다고 말하는 모델이 실제로는 확인하지 않았을 수 있다는 점입니다.
- AI 도구는 내 비공개 코드로 평가해야 합니다. 공개 벤치마크는 학습 데이터에 섞여 들어가기 쉽고 이미 알려진 답만 확인합니다. 지난 감사로 평가 세트를 만들고 새 발견이 나올 때마다 추가하고 오탐은 따로 세는 게 좋습니다.
- 형식 검증에서 명세는 사람의 몫입니다. 증명은 AI가 쓰지만 그 AI가 빈 명세를 쓰거나 증명이 통과할 때까지 모델을 바꿔 버리기도 합니다. Klaus, Calic, Flores 모두 결국 이 지점을 강조했습니다.
- 내 에이전트는 이미 뚫렸다고 가정하고 설계해야 합니다. 입력은 데이터로만 다루고 쓰기 권한은 최소한으로 주고 에이전트가 만든 내용에는 표시를 붙이고 위험한 작업은 사람이 맡아야 합니다.
- 리포트 홍수에 대비해야 합니다. Lido는 Critical이라던 리포트 약 180건 중 3건에만 보상했고 Polygon에는 한 달에 200건 넘는 리포트가 들어오며 libp2p는 석 달 만에 경력 전체만큼의 리포트를 받았습니다. 리포트 처리는 별도 파이프라인으로 꾸리고 여러 모델로 거르되 최종 판단은 사람이 해야 합니다.
- 보안은 배포로 끝나지 않습니다. 의존성은 바뀌고 하드포크는 오고 새 모델은 계속 나옵니다. Lido처럼 릴리스 직전만이 아니라 이런 변화가 생길 때마다 점검을 다시 돌려야 합니다.
