Trail of Bits Miden 감사, 에이전트가 부족한 도구를 만든 뒤 Falcon 결함 발견
Trail of Bits는 Miden 감사를 준비하는 데 6개월을 쓴 뒤, AI 에이전트가 처음부터 구축한 도구로 고위험 결함을 찾아냈다. Trail of Bits의 Miden 감사는 모델에 소스 코드를 단순히 입력하는 작업 이상의 것이었다. 정식 검토가 시작되기 전에 에이전트들은 LSP 서버, 디컴파일러, 정적 분석 엔진, Lean 모델을 만들었다.
이 준비 과정은 악의적 증명자가 Falcon 서명을 위조하고 영향을 받는 계정을 비울 수 있게 했다고 전해지는, 제약이 충분하지 않은 값을 드러냈다. 분석기는 유형 검증을 개선할 수 있는 위치도 400곳 이상 식별했다. 한편 형식 검증 작업은 기계 검증된 정확성 증명 95건을 만들고 기존 단위 테스트가 놓친 버그 두 가지를 찾아냈다.
중요한 경쟁 구도는 AI 에이전트와 인간 감사자의 대결이 아니다. 직접적인 AI 코드 검토와, 어려운 코드 검토를 가능하게 하는 인프라를 에이전트가 보조해 구축하는 방식의 차이다. Trail of Bits는 여전히 인간의 감독, 수동 정리 검토, 전통적인 보안 판단에 의존했다. 에이전트는 어떤 지원 프로젝트가 경제적으로 실현 가능한지를 바꿨다.
Trail of Bits Miden 감사는 6개월 전에 시작됐다
결정적인 작업은 감사자가 점검할 완성된 대상물을 받기 전부터 시작됐다.
회사의 상세한 Miden 감사 보고에 따르면, Miden 팀은 2025년 말 Trail of Bits에 접근했다. Miden은 출시 전 영지식 가상 머신의 일부를 검토받고자 했다. 대상 중 한 부분은 Miden Assembly, 즉 MASM으로 작성된 암호학적 기본 요소를 포함한 핵심 라이브러리였다.
흔히 zkVM으로 줄여 부르는 영지식 가상 머신은 모든 검증자가 해당 계산을 반복하지 않고도 프로그램이 올바르게 실행됐음을 증명한다. Miden은 스택 머신 아키텍처를 사용한다. 명령어는 스택에서 값을 소비하고 결과를 다시 스택에 올린다.
이 아키텍처가 중요한 이유는 MASM 코드에서 입력과 출력이 흔히 암묵적이기 때문이다. 검토자는 각 명령어가 스택을 어떻게 바꾸는지 추적하고, 그 상태를 분기, 루프, 프로시저 호출 전반에 걸쳐 이어가야 한다. 익숙한 소스 수준의 단서는 사라질 수 있다.
MASM에는 감사자가 일반적으로 기대하는 도구도 상당수 없었다. 편집기 지원은 제한적이었고, 검토에 특화된 성숙한 언어 서버도 없었으며, 핵심 라이브러리를 위한 자동화 분석도 제한적이었다. Trail of Bits는 구현이 아직 기능적으로 완성되지 않았다는 점을 알았지만, 감사까지 6개월이 남았다는 점도 알고 있었다.
이 회사는 그 기간을 활용해 자체 검토 환경을 구축했다. Trail of Bits에 따르면 Claude는 며칠 안에 초기 언어 서버 프로토타입을 만들었다. 그 결과물인 MASM 언어 서버는 탐색, 참조 검색, 호버 문서, 문법 진단, 명령어 설명, 스택 효과 정보를 제공한다.
이 기능들은 평범한 개발 편의 기능처럼 들릴 수 있다. 하지만 낯선 어셈블리 언어에서는 보안 방법론의 일부가 된다. 탐색 기능은 감사자가 프로시저 경계를 넘어 값을 추적하도록 돕는다. 인라인 스택 효과는 반복적인 수동 재구성을 줄인다. 진단은 가정이 발견 사항으로 이어지기 전에 드러낸다.
Trail of Bits는 이후 프로젝트를 디컴파일, 정적 분석, 명령줄 도구, 형식 모델링으로 확장했다. Claude는 계획 및 구현 작업을 맡았고, Codex는 코드 검토에 참여했다. 에이전트들은 역할도 바꿔가며 생성된 작업에 별도의 검토 단계를 부여했다.
이는 일회성 생성 프로세스가 아니었다. 기능을 구현한 뒤 팀은 에이전트에게 무작위 프로시저를 디컴파일하고 결과를 원래 MASM과 비교하도록 요청했다. 회귀는 테스트가 됐고, 모델은 그 테스트를 기준으로 다시 작업했다.
이 피드백 루프가 이 이야기의 핵심이다. 에이전트는 출력이 자동으로 신뢰받아야 하는 권위자로 취급되지 않았다. 이들은 테스트, 검토 단계, 분석기, 그리고 나중에는 증명 검사기로 구성된 점점 커지는 검증 시스템 안에서 작동했다.
따라서 감사는 통상적인 방식과 다른 질문에서 시작됐다. Trail of Bits는 에이전트가 취약점을 찾아낼 수 있는지만 묻지 않았다. 대신 감사자를 포함한 에이전트가 애초에 코드를 이해하지 못하게 하는 부족한 도구가 무엇인지 물었다.
이러한 범위의 변화가 궁극적인 발견을 위한 조건을 만들었다. 또한 AI 검토를 주로 더 빠른 소스 코드 스캔으로 홍보하는 보안 팀에도 압박을 가했다. Trail of Bits의 접근 방식은 더 많은 준비가 필요했지만, 그 준비를 재사용 가능한 기술 인프라로 전환했다.
디컴파일러는 출력물보다 더 가치 있어졌다
디컴파일러가 가장 중요했던 이유는 내부 표현이 다른 분석이 안정적으로 작동할 기반을 제공했기 때문이다.
MASM 디컴파일은 단순히 어셈블리 명령어를 읽기 쉬운 표현식으로 바꾸는 문제가 아니었다. 핵심 라이브러리의 대부분 프로시저에는 선언된 시그니처가 없었기 때문에, 도구는 문맥에서 입력과 출력을 추론해야 하는 경우가 많았다. 프로시저에는 통일된 호출 규약도 없었다.
루프는 또 다른 문제를 만들었다. MASM while 루프는 반복 간에 같은 스택 형태를 유지할 필요가 없다. 조건이 다른 스택 위치로 이동할 수 있어 명령어 입력에 안정적인 이름을 부여하려는 단순한 시도를 무너뜨린다.
조건부 분기도 서로 다른 스택 효과를 낼 수 있다. 한 분기가 항목을 추가하고 다른 분기가 항목을 제거한다면, 디컴파일러는 상태를 무작정 병합할 수 없다. 스택 효과 추론의 오류는 영향을 받는 코드를 호출하는 모든 프로시저로 전파될 수 있다.
Trail of Bits는 약속의 범위를 제한하는 방식으로 대응했다. MASM 디컴파일러는 모든 프로시저의 완벽한 복원을 주장하는 대신, 명확히 정의된 부분집합을 대상으로 한다. 이 선택은 피상적인 범위보다 정확성을 우선했다.
디컴파일러는 프로젝트에서 가장 큰 도구 개발 작업이 됐다. Trail of Bits는 수개월에 걸쳐 AI가 생성한 커밋이 100개 이상이라고 밝혔다. 그러나 완성된 의사 코드는 가장 중대한 결과물이 아니었다.
이 프로젝트는 프로시저의 입력과 출력을 분석 가능한 표현식으로 나타내는 중간 표현, 즉 IR을 만들었다. IR은 변환이나 분석을 위해 설계된 구조화된 코드 버전이다. MASM 명령어가 이 형태로 존재하게 되자, 팀은 확립된 데이터 흐름 및 정적 분석 기법을 적용할 수 있었다.
분석기는 증명자가 제공한 값이 사용 전에 검증됐는지 물을 수 있었다. 코드가 32비트 정수나 Boolean 값과 같은 예상 유형을 강제하는지도 추적할 수 있었다. 또한 모든 가능한 실행 경로에서 지역 변수가 초기화되는지도 판단할 수 있었다.
Trail of Bits는 이 작업의 일부에 추상 해석을 사용했다. 추상 해석은 하나의 구체적인 입력으로 프로그램을 실행하는 대신, 가능한 값의 범주를 평가한다. 값은 유효한 32비트 정수, Boolean, 또는 알 수 없는 값으로 표현될 수 있다.
분석은 새로운 정보가 더 이상 나타나지 않는 안정 상태에 도달할 때까지 반복된다. 건전하게 설계되면 실제 실행이 할 수 있는 일을 과대근사한다. 이로 인해 오탐이 생길 수 있지만, 모델이 포괄하는 실제 동작을 조용히 제외해서는 안 된다.
이는 Trail of Bits의 Miden 감사가 일반적인 AI 코딩 시연과 다른 이유를 보여준다. 에이전트가 생성한 디컴파일러는 코드가 안전하다고 선언하도록 신뢰받지 않았다. 대신 명시적이고 검사 가능한 분석이 실행될 기반을 구축하는 데 기여했다.
이 워크플로는 인간에게도 이점을 만들었다. 디컴파일된 프로시저는 편집기 안에서 고수준 제어 흐름과 데이터 흐름을 더 쉽게 검토하게 했다. 스택 주석은 정신적 추적 부담을 줄였다. 명령줄 인터페이스는 자동화된 검토 프로세스에도 같은 기능을 제공했다.
코딩 에이전트를 평가하는 팀에는 더 넓은 교훈이 있다. 가장 가치 있는 생성 산출물은 사용자가 보는 결과물이 아닐 수 있다. 부분적으로 범위가 제한된 디컴파일러도 파서, 제어 흐름 모델, IR이 여러 고가치 검사를 가능하게 한다면 비용을 정당화할 수 있다.
이 결론은 팀이 프로젝트 맥락을 보존하는 방식도 바꾼다. 에이전트 프롬프트, 회귀 사례, 아키텍처 결정, 검토자 의견은 지속적인 엔지니어링 입력이 된다. 검색 가능한 지식 기반은 긴 보안 프로젝트 전반에서 이러한 자료를 계속 활용할 수 있도록 돕는다.
직접 AI 검토는 일반적으로 대상 코드에서 시작해 결함을 묻는다. Trail of Bits는 대신 에이전트를 사용해 검토 표면 자체를 바꿨다. 다음 결과는 이 구분이 왜 중요했는지를 보여줬다.
하나의 누락된 검사가 Falcon 인증까지 이어졌다
검증되지 않은 나머지 하나가 산술 보조 함수를 위조된 인증 경로로 바꿨다고 전해진다.
감사 과정에서 정적 분석은 유형 검증을 개선할 수 있는 고유 위치를 400곳 이상 식별했다. Trail of Bits에 따르면 이들은 모두 핵심 라이브러리의 공개 API에서 도달 가능했다. 다수는 공개로 노출된 프로시저가 원래 작성자가 예상한 가정 없이 호출될 수 있었기 때문에 발생했다.
공개 프로시저는 모든 호출자가 의도된 유형의 값을 제공한다고 안전하게 가정할 수 없다. 증명 시스템에서는 특히 증명자가 제공한 값과 증명으로 제약된 값을 구분하는 일이 중요하다. 데이터를 계산에 넣는 것만으로 그것이 주장된 정수나 Boolean을 나타낸다는 사실이 성립하는 것은 아니다.
고위험 발견은 64비트 값을 12,289로 모듈러 연산하는 프로시저 mod_12289에 집중됐다. 증명자는 어드바이스 메커니즘을 통해 몫과 나머지를 제공했다. 어드바이스 값은 VM 외부에서 계산되는 실행 힌트로, 비용이 많이 드는 VM 내 작업을 피하기 위해 흔히 사용된다.
몫은 예상된 64비트 표현에 맞는지 확인하는 검사를 받았다. 하지만 나머지는 32비트 뺄셈 명령어인 u32overflowing_sub에 들어가기 전에 동등한 검증을 받지 않았다.
Trail of Bits는 공격자가 뺄셈 제약을 만족하면서도 몫과 나머지를 바꿀 수 있었다고 밝혔다. 그 결과 mod_12289는 수학적으로 올바른 나머지와 다른 값을 반환할 수 있었다.
이 버그의 영향은 잘못된 산술 결과에 그치지 않았다. 해당 프로시저는 Falcon 서명 검증을 지원했다. Falcon은 포스트양자 디지털 서명 체계이며, Miden은 계정 인증에 그 변형을 사용했다.
Trail of Bits에 따르면 악의적 증명자는 제약이 부족한 값을 악용해 Falcon 서명을 위조하고 Falcon 키 쌍이 제어하는 계정을 비울 수 있었다. 이는 공개 기사에서 독립적으로 재현된 익스플로잇이 아니라 해당 회사의 기술적 주장이다.
심각성은 Miden의 실행 모델에서 비롯된다. Miden VM 설계는 증명 생성 중 제공되는 비결정적 입력을 지원한다. 이러한 입력은 효율성을 높일 수 있지만, 프로그램은 이를 신중히 제약해야 한다.
검증자는 개발자의 의도를 추론하지 않는다. 제출된 증명이 인코딩된 제약을 충족하는지 확인한다. 이러한 제약이 유효하지 않은 나머지를 허용한다면, 주장된 산술 관계가 거짓이더라도 증명은 유효하게 유지될 수 있다.
이것이 핵심적인 반전이다. 영지식 증명은 명시된 시스템의 충실한 실행을 확립할 수 있지만, 불완전한 명세를 고칠 수는 없다. 제약이 부족한 프로그램에 대한 암호학적 증명은 잘못된 속성에 대한 확신을 제공할 수 있다.
후속 Miden 컨트랙트 감사의 독립적인 맥락도 이 일반적인 요지를 뒷받침한다. OpenZeppelin은 대응되는 증명이 존재할 때 Miden 트랜잭션이 유효하다고 설명했으며, 이에 따라 모든 MASM 검사는 증명자가 충족해야 하는 제약 조건의 일부가 된다.
이 별도 작업은 다른 리포지터리 범위를 다뤘으므로 Trail of Bits의 검토와 혼동해서는 안 된다. 그러나 두 사례 모두 인증 로직, 증명자가 제어하는 입력, 온체인 가정에 대한 명시적 검토가 필요한 이유를 보여 준다.
400곳이 넘는 타입 검증 위치 역시 신중하게 해석해야 한다. 이는 악용 가능한 취약점 400개로 설명된 것이 아니다. 검증을 개선할 수 있는 지점을 나타낸 것이며, 그중 보고된 고심각도 이슈는 하나였다.
이 구분은 정적 분석이 흔히 선별 검토가 필요한 조건을 발견하기 때문에 중요하다. 건전한 분석기는 궁극적으로 보안 결함이 되는 사례보다 더 많은 사례를 의도적으로 보고할 수 있다. 그 가치는 점검할 가치가 있는 가정을 체계적으로 찾아내는 데 있다.
보안 팀에 이 결과는 흔한 지름길에 제동을 건다. 즉, 대상 언어의 값 규칙을 먼저 모델링하지 않은 채 에이전트로 의심스러운 함수를 요약하는 방식이다. 모델은 코드가 무엇을 하는 것으로 보이는지 설명할 수 있다. 분석기는 허용되는 모든 실행이 실제로 요구된 타입을 준수하는지 물을 수 있다.
Falcon 발견은 두 역량을 결합한 결과였다. 에이전트는 구축 속도를 높였고, 정적 의미론은 증명자 제어 데이터에 대한 직관을 반복 가능한 검사로 전환했다.
Lean 증명은 단위 테스트가 놓친 것을 찾아냈다
형식 검증은 테스트를 대체하지 않았지만, 팀이 동작을 충분히 정확하게 명시하도록 강제해 테스트되지 않은 두 가지 실패를 드러냈다.
Trail of Bits는 에디터와 정적 분석 도구를 구축한 뒤에도 형식 모델링을 추진했다. 질문은 의도적으로 달랐다. 라이브러리 프로시저에 명백한 결함이 없다면, 팀은 그 구현이 의도된 산술 동작과 일치함을 증명할 수 있을까?
이 회사는 Lean으로 최소한의 Miden VM 실행기를 구축했다. Lean은 제출된 증명이 정의와 가정에서 논리적으로 도출되는지 작은 신뢰 커널로 검사하는 대화형 정리 증명기다. Claude는 MASM 프로시저를 Lean 표현으로 변환하는 번역기 구축에도 도움을 줬다.
이후 여러 에이전트가 프로시저 증명을 병렬로 작업했다. 그 결과물인 MASM Lean model에는 실행 가능한 VM 의미론, 변환된 프로시저, 공통 증명 지원, 개별 정확성 정리가 포함됐다.
리포지터리에는 검증된 프로시저 증명 95개가 나열돼 있다. 64비트 연산 31개, 128비트 연산 36개, 256비트 연산 17개, 워드 연산 11개다. 이들은 Trail of Bits가 설명한 이진 산술 영역을 함께 포괄한다.
이는 Miden의 모든 부분이 안전하다는 증명이 아니었다. 특정 프로시저에 대해 정의된 정확성 속성을 다뤘다. 정리 증명기는 개발자 머릿속에 있는 암묵적 의도가 아니라 자신에게 제공된 정리를 검증하므로, 이 경계는 필수적이다.
따라서 Trail of Bits에 따르면 인간 검토자는 정리 문장을 감사하는 데 집중했다. 에이전트가 핵심 사전조건을 누락했거나 잘못된 결과를 표현한 정리를 증명했다면, 커널의 승인만으로 소프트웨어가 올바르게 되는 것은 아니다.
높은 수준에서 보면 많은 정리는 알아보기 쉬운 패턴을 따랐다. 특정 입력을 담은 스택이 주어졌을 때 프로시저를 실행하면 종료되어야 하며, 수학적으로 기대되는 결과가 맨 위에 남아야 한다. 호출자가 소유한 관련 없는 스택 값은 기대된 위치에 유지돼야 한다.
이 명세 압력은 기존 단위 테스트가 놓친 두 결함을 드러냈다. 첫 번째는 rotr이라는 이름의 64비트 오른쪽 회전 프로시저에 영향을 미쳤다. 회전량이 32의 배수일 때 Goldilocks 소수보다 큰 입력에서 잘못 동작했다.
Goldilocks 소수는 VM이 사용하는 필드를 정의하므로, 그 경계에 가깝거나 이를 넘는 값은 신중한 표현이 필요하다. 증명 작업 중 문제가 되는 시프트 사례를 제외하는 가정을 추가하지 않으면 원하는 정리가 성립하지 않았다.
증명 실패가 자동으로 코드 버그의 증거가 되는 것은 아니다. 정리, 모델 또는 보조 보조정리도 잘못됐을 수 있다. 이 사례에서는 장애 요인에 대한 수동 검토가 팀을 구현의 경계 사례로 이끌었다.
두 번째 버그는 256비트 wrapping_mul 프로시저에서 나타났다. Trail of Bits에 따르면 이 프로시저는 반환 전에 호출자가 소유한 값을 스택에서 제거했다. 곱셈 결과만을 검사하는 일반적인 테스트는 통과할 수 있지만, 주변 스택 상태의 보존 여부는 확인하지 못할 수 있다.
이 결함은 정확한 사후조건이 중요한 이유를 보여 준다. 프로시저는 올바른 수치 답을 계산하면서도 호출 계약을 위반할 수 있다. 스택 머신에서는 맨 위 항목이 올바르게 보여도 인접한 상태를 손상하면 이후 실행에 영향을 줄 수 있다.
단위 테스트는 여전히 핵심적인 역할을 한다. 빠르게 실행되고, 알려진 회귀를 막으며, 아직 형식 모델이 없는 통합 동작을 다룬다. Lean 작업은 명시적으로 기술된 속성 전반에 걸쳐 다른 종류의 보증을 제공했다.
핵심 이점은 조합 가능성이었다. 에이전트는 대규모로 증명 시도를 만들어낼 수 있었고, Lean의 커널은 유효하지 않은 도출을 거부했다. 인간은 모델의 자신감 있는 서술을 신뢰할 필요가 없었다. 정의를 검토하고 승인된 정리가 의도한 보장을 나타내는지 확인하면 됐다.
이는 생성된 코드가 올바르게 보이는지 다른 언어 모델에 묻는 것보다 더 강력한 통제 경계다. 인간의 판단을 없애지는 않지만, 그 판단의 초점을 명세와 가정으로 옮긴다.
엔지니어링 리더에게 이 사례는 실용적인 역할 분담을 시사한다. 에이전트는 반복적인 증명 골격, 번역기, 후보 보조정리를 생성할 수 있다. 인간 전문가가 무엇을 증명해야 하는지 결정하고 중요한 문장이 실패하는 이유를 조사한다.
이 결과가 자율 감사의 신뢰성을 보장하지는 않는다
이 프로젝트가 뒷받침하는 것은 에이전트 보조 감사 엔지니어링이지, 비감독 보안 인증이 아니다.
Trail of Bits는 경제적 변화를 직접적으로 설명한다. 몇 년 전이었다면 하나의 작업을 위해 수개월간 탐색적 도구 개발을 정당화하기 어려웠을 것이다. 이런 부수 프로젝트는 결과가 불확실했고 가치가 드러나기 전에는 판매하기 어려웠다.
이 회사는 에이전트가 탐색 비용을 충분히 낮춰 이 계산을 바꿨다고 주장한다. 실패한 실험의 비용은 전문 엔지니어링 인력을 전면 배정하는 대신 토큰과 감독 시간으로 점차 대체되고 있다.
이 주장은 신중히 읽어야 한다. 감사 전까지 여전히 6개월이 걸렸고, 디컴파일러만 해도 AI가 생성한 커밋이 100개를 넘게 축적됐다. 공개된 설명은 기존 작업과 비교한 인력 시간, 전체 모델 비용, 결함 발견 수율의 통제된 비교를 제공하지 않는다.
또한 에이전트가 모든 특수 언어에 동등한 도구를 구축할 수 있음을 입증하지도 않는다. MASM은 분석과 형식 모델링에 유리한 특성을 제공했다. Miden VM은 명령어 집합이 작고, 많은 연산이 복잡한 부작용을 피한다.
이처럼 유리한 대상 안에서도 디컴파일러는 모든 프로시저를 안전하게 다룰 수 없었다. Trail of Bits는 일관되지 않은 스택 효과와 누락된 시그니처 때문에 완전하고 신뢰할 수 있는 디컴파일이 비현실적이어서 지원 범위를 좁혔다.
Lean 워크플로에는 또 다른 한계가 있었다. 커널 검증 증명은 모델링된 의미론 아래에서 진술된 정리만 확립한다. 잘못 번역된 명령어, 불완전한 VM 모델 또는 약한 정리는 증명된 동작과 실제 배포 사이의 격차를 유지할 수 있다.
인간 검토는 전 과정에서 분명하게 남아 있었다. 감사자는 에이전트 생성 코드를 검토하고, 회귀를 테스트로 전환하며, 정리 문장을 점검하고, 실패한 증명을 분석했다. Claude와 Codex는 관찰되지 않는 권위자로 작동한 것이 아니라 개발과 검토를 번갈아 수행했다.
이로써 핵심 비교는 더 선명해진다. 직접적인 AI 검토는 모델에게 기존 표현에서 취약점을 인식하도록 요구한다. 도구 구축 에이전트는 전문가가 누락된 제약, 유효하지 않은 타입, 잘못된 사후조건을 명시적으로 드러내는 표현을 만들도록 돕는다.
어느 접근법도 단독으로 서서는 안 된다. 모델은 정적 분석기가 인코딩하지 않은 가설을 제시할 수 있다. 정적 분석은 확률적 검토자가 놓칠 수 있는 실행 경로를 다룰 수 있다. 형식 증명은 이후 선택된 속성을 기계 검증 가능한 기준으로 다룰 수 있다.
이 과정은 유지보수 의무도 만든다. 파서는 언어 변경을 따라가야 한다. 분석기에는 회귀 테스트 모음이 필요하다. 형식 모델은 VM 의미론과 정렬된 상태를 유지해야 한다. 오래된 생성 도구는 잘못된 보증을 만들어낼 수 있다.
Trail of Bits는 Miden 팀이 향후 핵심 라이브러리 업데이트를 위해 정적 분석 엔진을 채택했다고 보고했다. 이는 도구가 단일 감사 시점의 스냅샷을 넘어섰다는 점에서 중요한 신호다. 지속적인 사용은 언어와 라이브러리가 진화함에 따라 분석기가 계속 유용한지 시험하게 된다.
유사한 워크플로를 고려하는 조직은 출처 관리도 계획해야 한다. 팀은 어떤 모델이 변경을 생성했는지, 어떤 인간이 이를 검토했는지, 어떤 테스트가 실행됐는지, 어떤 가정이 증명에 들어갔는지 알아야 한다. engineering workflow는 그 주변에 보존된 기록만큼만 검토 가능하다.
따라서 공개된 증거는 제한된 결론을 뒷받침한다. 에이전트는 이 작업에서 야심 찬 준비 프로그램을 실현 가능하게 만들었다. 보안 보증은 여전히 도메인 전문가, 테스트, 명시적 분석, 증명 검사의 결합 시스템에서 나왔다.
이 시스템은 AI가 버그를 발견했다는 주장보다 더 흥미롭다. 불완전한 에이전트의 자신감을 증거로 취급하지 않고 활용하는 구체적인 모델을 제시한다.
이 감사 모델의 지속성은 세 가지 신호가 시험할 것이다
다음 시험은 에이전트가 구축한 보증 도구가 주요 발견 이후에도 올바르고, 채택되며, 생산성을 유지하는지 여부다.
첫 번째 신호는 MASM 분석기가 Miden 개발 프로세스에 계속 통합되는지다. Trail of Bits에 따르면 Miden 팀은 향후 핵심 라이브러리 변경을 위해 정적 분석 엔진을 채택했다. 지속적 통합에서 일상적으로 사용된다면 감사 도구가 예방적 인프라가 될 수 있다는 근거가 강화될 것이다.
중요한 측정 기준은 경고를 몇 개 내는지가 아니다. 새로운 공개 프로시저가 릴리스 전에 필요한 검증을 받는지, 분석기 업데이트가 MASM 의미론의 변화를 추적하는지다. 지속적인 오탐이나 오래된 모델은 결과를 약화할 것이다.
두 번째 신호는 95개 Lean 증명의 확장과 유지보수다. 추가로 검증된 프로시저는 초기 모델이 고정된 시연이 아니라 지속적인 작업을 지원함을 보여 줄 것이다. 기존 산술 코드의 변경도 증명 업데이트나 실패를 유발해야 한다.
변환된 코드와 사람이 검토한 명세 사이의 경계를 지켜봐야 한다. 정리 적용 범위를 강화하지 않은 채 증명 수만 늘리는 자동화는 같은 수준의 보증을 제공하지 못한다. 가정의 명확한 문서화는 원시 총계만큼 중요해질 것이다.
세 번째 신호는 다른 감사 팀과 언어 생태계에서의 재현이다. Miden은 이례적으로 적합한 조합을 제시했다. 맞춤형 언어, 부재한 도구, 명시적인 증명 의미론, 그리고 수개월의 준비 시간이 그것이다.
서로 다른 zkVM이나 저수준 언어에서 반복되는 패턴은 Trail of Bits의 더 광범위한 경제적 주장을 뒷받침할 것이다. 동시성, 복잡한 메모리 또는 대규모 의존성 그래프를 갖춘 시스템에서 재현하지 못한다면 그 한계가 드러날 것이다.
Trail of Bits의 Miden 감사는 이미 추측성 워크플로 이상을 만들어냈다. 에디터 통합, 디컴파일러, 분석기, VM 모델, 검증된 증명, 구체적인 보안 발견을 제공했다.
지속되는 핵심 질문은 팀이 이러한 산출물을 보호 대상 시스템과 계속 일치시킬 수 있는가이다. 에이전트 지원 보안을 평가하는 개발자는 리포지토리를 검토하고, 모델링된 가정을 살피며, 기계 검증 가능한 통제가 모델에 대한 신뢰를 대체하는 지점이 어디인지 물어야 한다. 그것이 다음 감사까지 이어가야 할 기준이다.
