트레일오브비츠, 에이전트로 만든 MASM 도구로 Miden VM에서 Falcon 서명 위조 취약점 발견
- 트레일오브비츠가 Miden VM 감사에서 검증되지 않은 프로버 제공 입력을 찾아냈고, 악성 프로버가 이걸로 Falcon 서명을 위조해 Miden 계정 보유자 자금을 빼앗을 수 있었음
- 감사 준비 기간 6개월 동안 에이전트가 masm-lsp(LSP 서버), masm-decompiler, 정적 분석 엔진, masm-lean(VM 실행기의 Lean 모델)을 전부 바닥부터 구현함
- 이 도구들이 실제 보안 문제를 잡아냈고, Lean 작업은 Miden 코어 라이브러리 상당 부분을 덮는 95개의 기계 검증 정정 증명을 산출함
- MASM은 스택 머신 구조라 명령 입출력이 스택에서 암시적으로 오가 리뷰가 어렵고, 완전히 새 아키텍처라 IDE 지원이나 LSP, 린터 같은 개발 도구가 거의 없었음
- MASM 디컴파일이 어려운 이유는 절차에 선언된 시그니처가 없고 호출 규약이 없어 정적 분석 실패가 호출 체인 위로 전파되며, while 루프가 스택 중립을 지키지 않아도 되기 때문임
Hacker News opinions
이게 AI를 그냥 빨리 쓰는 게 아니라 더 잘 쓰는 좋은 예시인 것 같음
근데 그 차이라는 게 결국 의미론이라는 얘기도 있음. 원래 일주일 걸릴 일을 AI 덕에 하루에 끝내면 결과는 좋아지고 내 투입 시간은 그대로니까.
보안 감사에 '그냥 쓸 만한' AI를 쓰자는 건 '그냥 쓸 만한' 브레이크를 달자는 얘기 같음. 빈틈 둘 데가 없는데.
비유가 잘 이해가 안 가는데 실은 브레이크도 '그냥 쓸 만한' 기준이 다 있음. 정정 증명 붙은 검증 구현에 기계적 번역, 감사하기 쉬운 정리까지 있으면 거의 충분하다고 봄. 부담은 Claude가 만든 번석기 쪽에 몰리지만 신뢰할 코드 덩어리가 2년 전에 비하면 엄청 작아짐.
그 브레이크 비유는 별로임. 시빅에 쓸 만한 브레이크가 소방차나 레이스카에 쓸 만한 건 아니지만 용도별 '충분한' 표준은 다 존재함.
AI 감사가 진짜 값을 하는 곳은 보안을 단 한 번도 들여다본 적 없는 소기업 같은 데임.
보안 업계는 이제 끝났다고 봐야 함. 결국 뚫린다는 전제하에 아키텍처를 다시 짜야 함. 그 방향으로 생각이 안 바뀌면 답이 없음.
FHE가 되면 좋겠지만 지금 당장 E2EE로 할 수 있는 제품이 수두룩함. 서버 쪽 파일이나 덤통째 털리는 유출이 널려 있는데 E2EE 클라우드 스토리지는 못 쓸 이유가 없음. 클라이언트 신뢰도는 대략 GrapheneOS, iOS/iPadOS, 픽셀 기본 안드로이드, ChromeOS, macOS, Windows, 데스크톱 리눅스 순으로 봄. 재현 가능한 빌드에 AI로 소스 감사를 원하는 만큼 돌리면 실행하는 게 그 소스라는 걸 확인할 수 있음.