본문으로 건너뛰기

스마트 계약의 형식 검증과 AI 보조 감사

· 약 33분
Dora Noda
Dora Noda
Software Engineer

스마트 계약 감사에서의 형식 검증​

형식 검증은 수학적 및 논리 기반 기술을 사용하여 스마트 계약의 정확성과 보안을 증명하는 것을 의미합니다. 실제로 이는 속성 기반 퍼즈 테스트와 심볼릭 실행부터 엄격한 정리 증명 및 모델 체킹에 이르기까지 다양한 방법론을 포함합니다. 목표는 계약이 명세를 충족하고 모든 가능한 입력과 상태에 걸쳐 악용 가능한 버그가 없음을 보장하는 것입니다. DeFi 프로토콜에 수십억 달러가 예치되어 있는 높은 위험을 고려할 때, 형식적 방법은 이더리움 및 기타 블록체인 플랫폼에서 점점 더 중요해지고 있습니다.

전통적인 접근 방식: 이더리움을 위한 초기 형식적 방법에는 Oyente 및 Mythril과 같은 심볼릭 실행 도구와 Slither 및 Securify와 같은 정적 분석기가 포함되었습니다. 심볼릭 실행은 심볼릭 입력을 사용하여 프로그램 경로를 탐색하여 재진입, 정수 오버플로우 등의 문제를 감지하는 반면, 정적 분석은 규칙 기반 패턴 매칭을 사용합니다. 이러한 도구들은 성공을 거두었지만 한계도 있었습니다. 예를 들어, Oyente는 간단한 계약에서도 많은 오탐을 발생시켰고, Slither의 패턴 기반 탐지기는 여러 오탐을 생성할 수 있습니다. 더욱이 2023년 한 연구에 따르면, 악용 가능한 계약 버그의 80% 이상 (특히 복잡한 "비즈니스 로직" 버그)이 현재 도구들로는 발견되지 못했다는 사실은 더 강력한 검증 기술의 필요성을 강조합니다.

완전 검증의 가능성과 과제: 이론적으로, 형식 검증은 모든 상태에 대한 불변성을 철저히 확인함으로써 버그가 없음을 증명할 수 있습니다. Certora Prover나 이더리움 재단의 KEVM 프레임워크와 같은 도구들은 스마트 계약을 형식 명세에 대해 수학적으로 검증하는 것을 목표로 합니다. 예를 들어, Certora의 "자동화된 수학적 감사기"는 명세 언어 (CVL)를 사용하여 사용자가 정의한 규칙을 증명하거나 반증합니다. 그러나 실제로는 실제 계약에서 속성을 완전히 증명하는 것은 종종 불가능하거나 매우 노동 집약적입니다. 코드를 검증을 위해 단순화된 형태로 다시 작성해야 할 수도 있고, 맞춤형 명세를 작성해야 하며, 루프와 복잡한 산술은 수동으로 경계를 설정하거나 추상화해야 할 수 있으며, SMT 솔버는 복잡한 로직에서 자주 시간 초과됩니다. Trail of Bits 엔지니어들이 언급했듯이, *“버그가 없음을 증명하는 것은 일반적으로 중요하지 않은 코드베이스에서는 달성 불가능”*하며, 이를 달성하기 위해서는 사용자의 많은 개입과 전문 지식이 필요합니다. 이 때문에 형식 검증 도구는 전통적으로 전체 계약을 종단 간으로 검증하기보다는 토큰의 불변성이나 합의 알고리즘 검증과 같은 중요한 코드 조각에 드물게 사용되어 왔습니다.

Foundry의 퍼즈 테스트와 불변성 테스트​

최근 몇 년 동안, 속성 기반 테스트가 완전한 형식 증명의 실용적인 대안으로 부상했습니다. 인기 있는 이더리움 개발 프레임워크인 Foundry는 퍼즈 테스트와 불변성 테스트를 내장 지원합니다. 이 기술들은 테스트 커버리지를 크게 향상시키며 경량 형식 검증으로 볼 수 있습니다. Foundry의 퍼즈 테스트는 지정된 속성을 위반하려는 다수의 입력을 자동으로 생성하며, 불변성 테스트는 이를 상태 변경 작업의 시퀀스로 확장합니다:

  • 퍼즈 테스트: 특정 입력에 대한 단위 테스트를 작성하는 대신, 개발자는 모든 입력에 대해 유지되어야 하는 속성이나 불변성을 지정합니다. 그러면 Foundry는 수백 또는 수천 개의 무작위 입력을 생성하여 함수를 테스트하고 속성이 항상 유지되는지 확인합니다. 이는 개발자가 수동으로 테스트할 생각을 하지 못할 수 있는 엣지 케이스를 잡는 데 도움이 됩니다. 예를 들어, 퍼즈 테스트는 함수의 반환 값이 항상 음수가 아니거나 특정 사후 조건이 입력에 관계없이 참임을 주장할 수 있습니다. Foundry의 엔진은 지능적인 휴리스틱을 사용합니다. 함수 시그니처를 분석하고 엣지 케이스 값 (0, max uint 등)을 도입하여 속성을 깨뜨릴 가능성이 있는 코너 케이스를 공략합니다. 만약 단언문이 실패하면, Foundry는 속성을 위반하는 반례 입력을 보고합니다.

  • 불변성 테스트: Foundry의 불변성 테스트 (또는 상태 기반 퍼징)는 한 걸음 더 나아가 여러 함수 호출과 상태 전환을 순차적으로 실행합니다. 개발자는 계약의 수명 주기 동안 항상 참이어야 하는 불변성 함수를 작성합니다 (예: 총자산 = 사용자 잔액의 합). 그러면 Foundry는 무작위 호출 시퀀스 (무작위 입력 포함)를 생성하여 가능한 많은 사용 시나리오를 시뮬레이션하고, 주기적으로 불변성 조건이 계속 참인지 확인합니다. 이는 특정 작업 시퀀스 후에만 나타나는 복잡한 버그를 발견할 수 있습니다. 본질적으로, 불변성 테스트는 계약의 상태 공간을 더 철저히 탐색하여 유효한 트랜잭션 시퀀스가 명시된 속성을 위반할 수 없음을 보장합니다.

Foundry가 중요한 이유: Foundry는 이러한 고급 테스트 기술을 쉽게 사용할 수 있도록 만들었습니다. 퍼징 및 불변성 기능은 개발자 워크플로우에 내재되어 있어 특별한 하네스나 외부 도구가 필요 없으며, 테스트는 단위 테스트와 함께 솔리디티로 작성됩니다. Rust 기반 엔진 덕분에 Foundry는 수천 개의 테스트를 신속하게 (병렬 처리하여) 실행하고 모든 불변성 위반에 대한 상세한 실패 추적을 제공할 수 있습니다. 개발자들은 Foundry의 퍼저가 사용하기 쉽고 성능이 뛰어나며, 반복 횟수를 설정하거나 입력을 제한하기 위한 가정을 추가하는 등 약간의 구성만 필요하다고 보고합니다. Foundry 문서의 간단한 예는 divide(a,b) 함수에 대한 퍼즈 테스트로, vm.assume(b != 0)을 사용하여 사소한 유효하지 않은 입력을 피하고 result * b <= a와 같은 수학적 사후 조건을 단언합니다. 이러한 테스트를 수천 개의 무작위 (a,b) 쌍으로 실행함으로써 Foundry는 수동 추론으로는 찾기 어려운 엣지 케이스 (예: 오버플로우 경계)를 신속하게 발견할 수 있습니다.

비교: Foundry의 접근 방식은 커뮤니티의 이전 작업을 기반으로 합니다. Trail of Bits의 Echidna 퍼저는 이더리움을 위한 초기 속성 기반 테스트 도구였습니다. Echidna도 마찬가지로 불리언을 반환하는 솔리디티 함수로 표현된 불변성 위반을 찾기 위해 무작위 트랜잭션을 생성합니다. 이는 "지능적인" 입력 생성 (커버리지 기반 퍼징 포함)으로 알려져 있으며 많은 버그를 찾는 데 사용되었습니다. 실제로 보안 연구원들은 Echidna의 엔진이 매우 효과적이라고 언급합니다. “Trail of Bits의 Echidna는 지능적인 난수 선택 덕분에 최고의 퍼저입니다” – 하지만 Foundry의 통합된 워크플로우는 개발자가 테스트를 더 간단하게 작성할 수 있게 해줍니다. 실제로 Foundry의 퍼즈 테스트는 종종 안전한 솔리디티 개발을 위한 새로운 **“최소한의 기본 요건”**으로 간주되며, 전통적인 단위 테스트를 보완합니다. 이는 무작위적이고 철저하지 않기 때문에 버그가 없음을 증명할 수는 없지만, 방대한 범위의 입력과 상태 조합을 커버함으로써 신뢰도를 크게 높입니다.

퍼징을 넘어: 형식 증명과 고급 도구​

퍼징과 불변성이 많은 문제를 잡아내지만, 더 강력한 형식적 방법이 사용되는 경우도 있습니다. 모델 체킹과 정리 증명은 원하는 속성을 형식 논리로 명시하고 자동화된 증명기를 사용하여 계약 코드에 대해 이를 확인하는 것을 포함합니다. Certora Prover (최근 오픈소스화)는 이 범주에서 두드러진 도구입니다. 개발자는 도메인 특화 언어 (CVL)로 규칙을 작성한 다음, 계약이 해당 규칙을 위반하는지 자동으로 확인할 수 있습니다. Certora는 MakerDAO 및 Compound와 같은 프로토콜에서 중요한 불변성을 검증하는 데 사용되었습니다. 예를 들어, MakerDAO에서 4년 동안 발견되지 않았던 "DAI 부채 불변성" 버그 (미묘한 회계 불일치)를 식별했습니다. 주목할 점은 Certora의 엔진이 이제 여러 플랫폼 (EVM, 솔라나의 VM, eWASM)을 지원하며, 2025년에 오픈소스화함으로써 이더리움, 솔라나, 스텔라에서 산업 등급의 형식 검증을 무료로 사용할 수 있게 되었다는 것입니다. 이 움직임은 형식 증명이 자금이 풍부한 팀만의 사치가 되어서는 안 된다는 인식을 반영합니다.

다른 형식 도구에는 런타임 검증 접근 방식 (예: 이더리움의 KEVM 시맨틱 또는 Move 기반 체인을 위한 Move Prover)이 포함됩니다. 특히 Move Prover는 Move 언어 (앱토스 및 수이 블록체인에서 사용)에 내장되어 있습니다. 이를 통해 코드와 함께 형식 명세를 작성하고, 린터나 타입 체커와 유사한 사용자 경험으로 특정 속성을 자동으로 증명할 수 있습니다. 이러한 긴밀한 통합은 해당 플랫폼의 개발자들이 개발의 일부로 형식 검증을 사용하는 장벽을 낮춥니다.

요약: 오늘날의 스마트 계약 감사는 이러한 방법론들을 혼합합니다. 퍼징 및 불변성 테스트 (Foundry 및 Echidna가 대표적)는 사용 용이성과 일반적인 버그를 잡는 효과 때문에 널리 채택되고 있습니다. 심볼릭 실행 및 정적 분석기는 여전히 알려진 취약점 패턴을 신속하게 스캔하는 데 사용됩니다 (Slither와 같은 도구는 종종 CI 파이프라인에 통합됨). 한편, 형식 검증 도구는 성숙해지고 여러 체인으로 확장되고 있지만, 복잡성 때문에 일반적으로 특정 중요 속성이나 전문 감사 회사에서 사용됩니다. 실제로 많은 감사는 이러한 접근 방식을 결합합니다. 예를 들어, 퍼저를 사용하여 런타임 오류를 찾고, 정적 도구를 사용하여 명백한 실수를 표시하고, "토큰 잔액이 총 공급량을 초과하지 않음"과 같은 주요 불변성에 대해 형식 명세 검사를 사용합니다.

대규모 언어 모델을 이용한 AI 보조 감사​

OpenAI의 GPT-3/4 (ChatGPT) 및 Codex와 같은 대규모 언어 모델 (LLM)의 등장은 스마트 계약 분석을 위한 새로운 패러다임을 도입했습니다. 방대한 양의 코드와 자연어로 훈련된 이 모델들은 프로그램 행동에 대해 추론하고, 코드를 설명하며, 패턴 인식과 "상식" 지식을 통해 특정 취약점을 탐지할 수도 있습니다. 문제는 AI가 스마트 계약 감사를 보강하거나 심지어 자동화할 수 있는가 하는 것입니다.

LLM 기반 취약점 분석 도구​

LLM을 스마트 계약 감사에 적용하는 여러 연구 노력과 프로토타입 도구들이 등장했습니다:

  • OpenAI Codex / ChatGPT (일반 모델): 초기 실험은 단순히 GPT-3나 Codex에 계약 코드를 프롬프트로 제공하고 잠재적인 버그를 물어보는 것이었습니다. 개발자들은 ChatGPT가 일부 잘 알려진 취약점 패턴을 식별하고 수정 제안까지 할 수 있다는 것을 발견했습니다. 그러나 응답은 일관성이 없고 신뢰할 수 있을 만큼 포괄적이지 않았습니다. 최근 한 학술 평가에 따르면, 취약점 탐지를 위해 ChatGPT에 순진하게 프롬프팅하는 것은 벤치마크 데이터셋에서 *“무작위 예측과 비교하여 크게 더 나은 결과를 내지 못했다”*고 합니다. 즉, 모델이 적절하게 유도되지 않으면 존재하지 않는 문제를 환각하거나 실제 취약점을 놓칠 수 있습니다. 이는 유용한 결과를 얻기 위해 신중하게 설계된 프롬프트나 미세 조정이 필요함을 강조했습니다.

  • AuditGPT (2024): 이것은 이더리움 계약에서 ERC 표준 준수를 확인하기 위해 특별히 ChatGPT (GPT-3.5/4)를 활용한 학술 도구입니다. 연구원들은 많은 ERC20/ERC721 토큰 계약이 표준의 미묘한 규칙을 위반한다는 것을 관찰했습니다 (이는 보안 또는 호환성 문제로 이어질 수 있음). AuditGPT는 감사를 작은 작업으로 나누고 각 규칙 유형에 대해 특화된 프롬프트를 설계하여 작동합니다. 결과는 인상적이었습니다. 실제 계약에 대한 테스트에서 AuditGPT는 *“418개의 ERC 규칙 위반을 성공적으로 찾아냈고, 단 18개의 오탐만 보고했다”*고 하며 높은 정확도를 보여주었습니다. 실제로 이 논문은 AuditGPT가 ERC 준수 버그를 찾는 데 있어 전문 감사 서비스를 능가했다고 주장하며, 비용도 더 저렴했습니다. 이는 표준 규칙 목록을 강제하는 것과 같이 잘 정의되고 좁은 영역에서는 좋은 프롬프트를 가진 LLM이 놀랍도록 효과적이고 정밀할 수 있음을 시사합니다.

  • LLM-SmartAudit (2024): 또 다른 연구 프로젝트인 LLM-SmartAudit는 솔리디티 코드를 감사하기 위해 다중 에이전트 대화 시스템을 사용하여 더 넓은 접근 방식을 취합니다. 이는 여러 특화된 GPT-3.5/GPT-4 에이전트 (예: 정확성에 초점을 맞춘 "감사자", 악용 방법을 생각하는 "공격자")를 설정하여 서로 대화하며 계약을 분석하게 합니다. 평가에서 LLM-SmartAudit는 광범위한 취약점을 탐지할 수 있었습니다. 주목할 점은, 기존 도구와의 비교 테스트에서 GPT-3.5 기반 시스템이 **가장 높은 전체 재현율 (74%)**을 달성하여, 테스트한 모든 전통적인 정적 및 심볼릭 분석기를 능가했다는 것입니다 (차선은 Mythril이 54% 재현율). 또한 테스트 스위트에 있는 10가지 유형의 취약점을 모두 찾을 수 있었습니다 (반면 각 전통적인 도구는 일부 카테고리에서 어려움을 겪었습니다). 더욱이, GPT-4로 전환하고 분석에 집중함으로써 (표적 분석 모드라고 부름), 시스템은 Slither나 Mythril과 같은 도구들이 완전히 놓친 복잡한 논리적 결함을 탐지할 수 있었습니다. 예를 들어, 실제 DeFi 계약 세트에서 LLM 기반 접근 방식은 수백 개의 로직 버그를 발견한 반면, 정적 도구들은 해당 문제를 *“탐지하는 데 효과가 없었다”*고 합니다. 이러한 결과는 LLM이 전통적인 분석기의 패턴 매칭 범위를 넘어서는 미묘한 버그를 잡을 수 있는 잠재력을 보여줍니다.

  • Prometheus (PromFuzz) (2023): 하이브리드 접근 방식은 LLM을 사용하여 다른 기술을 유도하는 것입니다. 한 예로 PromFuzz가 있는데, 이는 GPT 기반 "감사 에이전트"를 사용하여 코드에서 의심스러운 영역을 식별한 다음, 자동으로 불변성 검사기를 생성하여 퍼징 엔진에 공급합니다. 본질적으로, LLM은 (선의의 관점과 공격자 관점 모두에서) 1차 분석을 수행하여 퍼즈 테스트를 잠재적 취약점에 집중시킵니다. 평가에서 이 접근 방식은 매우 높은 버그 발견율을 달성했습니다. 예를 들어, 특정 벤치마크 세트에서 오탐 없이 86% 이상의 재현율을 기록했으며, 이는 단독 퍼저나 이전 도구들을 크게 능가하는 성능입니다. 이는 AI를 사용하여 퍼징과 같은 고전적인 기술을 조정하고 강화하여 양쪽의 강점을 결합하는 유망한 방향입니다.

  • 기타 AI 도구: 커뮤니티에서는 다양한 다른 AI 보조 감사 개념을 보았습니다. 예를 들어, Trail of Bits의 "Toucan" 프로젝트는 OpenAI Codex를 감사 워크플로우에 통합했습니다 (결과는 아래에서 자세히 설명). 일부 보안 스타트업들도 AI 감사기 (예: "ChainGPT Audit" 서비스)를 광고하고 있으며, 일반적으로 GPT-4를 맞춤형 프롬프트로 감싸 계약을 검토합니다. 오픈소스 애호가들은 포럼에 ChatGPT 기반 감사 봇을 만들어 솔리디티 스니펫을 입력하면 잠재적인 문제를 출력하도록 했습니다. 이들 중 다수가 실험적이지만, 일반적인 추세는 분명합니다. AI는 자동화된 코드 설명 및 문서 생성부터 취약점 탐지, 심지어 수정 제안에 이르기까지 보안 검토 프로세스의 모든 수준에서 탐색되고 있습니다.

LLM 감사기의 능력과 한계​

LLM은 스마트 계약 감사에서 주목할 만한 능력을 보여주었습니다:

  • 광범위한 지식: GPT-4와 같은 LLM은 수많은 코드와 취약점에 대해 훈련되었습니다. 이는 일반적인 보안 함정 (재진입, 정수 오버플로우 등)과 일부 과거의 공격 사례에 대해 "알고" 있습니다. 이를 통해 버그를 나타낼 수 있는 패턴을 인식하고, 문서에서 모범 사례를 상기할 수 있습니다. 예를 들어, ERC-20 transferFrom이 허용량을 확인해야 한다는 것을 기억하고 (그러한 확인이 없는 것을 위반으로 표시할 수 있음) 있습니다. 알려진 패턴만 표시하는 정적 도구와 달리, LLM은 새로운 코드에 추론을 적용하여 도구 개발자가 명시적으로 코딩하지 않은 문제를 추론할 수 있습니다.

  • 자연스러운 설명: AI 감사기는 잠재적인 문제에 대해 사람이 읽을 수 있는 설명을 제공할 수 있습니다. 이는 개발자 경험에 매우 중요합니다. 전통적인 도구는 종종 해석하는 데 전문 지식이 필요한 암호 같은 경고를 출력하는 반면, GPT 기반 도구는 평이한 영어로 버그를 설명하는 문단을 생성하고 심지어 해결책을 제안할 수도 있습니다. 예를 들어, AuditGPT는 ERC 규칙 위반을 표시했을 뿐만 아니라 코드가 규칙을 위반한 이유와 그 의미를 설명했습니다. 이는 경험이 적은 개발자들이 보안 개념에 익숙해지는 데 도움이 됩니다.

  • 유연성: 프롬프트 엔지니어링을 통해 LLM은 다른 측면에 집중하거나 맞춤형 보안 정책을 따르도록 지시받을 수 있습니다. 고정된 규칙 집합에 제한되지 않습니다. 속성이나 패턴을 말로 설명할 수 있다면 LLM은 이를 확인하려고 시도할 수 있습니다. 이는 고유한 불변성이나 로직을 가질 수 있는 새로운 프로토콜을 감사하는 데 매력적입니다 (처음부터 맞춤형 정적 분석을 작성하는 것이 비현실적인 경우).

그러나 상당한 과제와 신뢰성 문제가 관찰되었습니다:

  • 추론 능력의 한계: 현재 LLM은 때때로 보안 분석에 필요한 복잡한 논리적 추론에 어려움을 겪습니다. Trail of Bits는 *“모델들이 계약 소유권, 재진입, 함수 간 관계와 같은 특정 상위 수준 개념에 대해 잘 추론하지 못한다”*고 보고했습니다. 예를 들어, GPT-3.5/4는 이론적으로 재진입이 무엇인지 이해할 수 있지만 (심지어 설명할 수도 있음), 여러 함수 호출과 상태 변경의 순서를 이해해야 하는 재진입 취약점을 인식하지 못할 수 있습니다. 모델은 또한 다중 계약 상호작용이나 시간 의존적 로직과 관련된 취약점을 놓칠 수 있는데, 이는 단일 코드 스니펫 분석의 범위를 벗어나기 때문입니다.

  • 오탐과 환각: 주요 우려 사항은 LLM이 자신감 있게 들리지만 부정확한 결론을 내릴 수 있다는 것입니다. 감사에서 "환각"은 실제로는 없는 취약점을 표시하거나 코드를 잘못 해석하는 것일 수 있습니다. Trail of Bits가 Codex (GPT)로 실험한 결과, 더 큰 실제 계약으로 확장하자 “오탐 및 환각 비율이 너무 높아져” 감사자들을 너무 많은 허위 보고로 인해 속도를 늦출 정도가 되었다고 합니다. 이러한 예측 불가능성은 문제입니다. 너무 자주 늑대가 나타났다고 외치는 도구는 개발자들에게 신뢰받지 못할 것입니다. AuditGPT가 오탐을 낮게 유지한 성공 (수백 건의 발견 중 단 18건)은 고무적이지만, 이는 제한된 영역에서였습니다. 범용 사용에서는 AI 결과를 필터링하기 위해 신중한 프롬프트 설계와 아마도 인간의 검토 루프가 필요합니다.

  • 컨텍스트 제한: LLM은 컨텍스트 창 제한이 있어 한 번에 특정 양의 코드만 "볼" 수 있습니다. 복잡한 계약은 종종 여러 파일과 수천 줄에 걸쳐 있습니다. AI가 전체 코드베이스를 소화할 수 없다면 중요한 연결을 놓칠 수 있습니다. 코드 슬라이싱 (계약을 조각내어 공급)과 같은 기술이 사용되지만, 이는 더 넓은 그림을 잃을 위험이 있습니다. LLM-SmartAudit 팀은 GPT-3.5의 4k 토큰 제한으로는 일부 대규모 실제 계약을 분석할 수 없었고, 더 큰 컨텍스트를 가진 GPT-4로 전환해야 했다고 언급했습니다. 그럼에도 불구하고 분석을 부분으로 나누면 시스템 전체를 고려할 때만 나타나는 버그를 간과하게 될 수 있습니다. 이는 현재로서는 전체 프로토콜 (여러 상호작용하는 계약을 가진)의 AI 분석을 실제적인 과제로 만듭니다.

  • 통합 및 도구: AI 감사기를 둘러싼 강력한 개발자 도구가 부족합니다. LLM 분석을 실행하는 것은 린터를 실행하는 것만큼 간단하지 않습니다. 모델에 대한 API 호출, 프롬프트 엔지니어링 처리, 속도 제한, AI의 응답 구문 분석 등이 포함됩니다. 한 감사팀은 *“LLM을 전통적인 소프트웨어와 통합하는 소프트웨어 생태계가 너무 조잡하고 모든 것이 번거롭다”*고 말했습니다. 불확실성을 관리하면서 CI 파이프라인에 AI 감사기를 지속적으로 배포하기 위한 기성 프레임워크는 거의 없습니다. 이는 서서히 개선되고 있지만 (일부 프로젝트는 코드 검토에 GPT-4를 사용하는 CI 봇을 탐색 중), 아직 초기 단계입니다. 더욱이, AI가 특정 결과를 내놓은 이유를 디버깅하는 것은 어렵습니다. 결정론적 도구와 달리, 모델이 무언가를 표시하거나 놓치게 된 논리를 쉽게 추적할 수 없습니다.

  • 비용 및 성능: GPT-4와 같은 대규모 모델을 사용하는 것은 비싸고 느릴 수 있습니다. CI/CD 파이프라인에 AI 감사를 통합하려면 계약당 몇 분이 추가될 수 있으며 대규모 코드에 대해 상당한 API 비용이 발생할 수 있습니다. 미세 조정된 모델이나 오픈소스 LLM은 비용을 완화할 수 있지만, GPT-4만큼 성능이 좋지 않은 경향이 있습니다. 코드 보안을 위한 더 작고 특화된 모델에 대한 연구가 진행 중이지만, 현재 최고의 결과는 대규모 독점 모델에서 나왔습니다.

요약하자면, LLM 보조 감사는 유망하지만 만병통치약은 아닙니다. 우리는 AI가 전체 감사를 종단 간으로 수행하는 대신 테스트를 생성하거나 특정 측면을 분석하는 데 도움을 주는 하이브리드 접근 방식을 보고 있습니다. 예를 들어, AI가 잠재적인 불변성이나 위험 영역을 제안하면, 인간이나 다른 도구가 이를 조사할 수 있습니다. 한 보안 엔지니어가 말했듯이, 추론 격차와 통합 장애물을 고려할 때, 이 기술은 아직 중요한 작업에서 인간 감사자를 대체할 준비가 되어 있지 않습니다. 그러나 이미 유용한 보조자가 될 수 있습니다. 전통적인 도구가 부족한 경우 “불완전한 것이 아무것도 없는 것보다 훨씬 나을 수 있습니다”.

다양한 툴체인의 정확성과 신뢰성​

논의된 다양한 감사 접근 방식의 정확성, 커버리지, 신뢰성을 비교하는 것은 유익합니다. 다음은 연구 및 산업 평가에서 나온 결과 요약입니다:

  • 정적 분석 도구: Slither와 같은 정적 분석기는 빠른 피드백과 사용 용이성으로 가치가 있습니다. 이들은 일반적으로 높은 정밀도와 중간 정도의 재현율을 가집니다. 즉, 보고하는 문제의 대부분은 실제 문제이지만 (설계상 오탐이 거의 없음), 특정 종류의 취약점만 탐지합니다. 2024년 벤치마킹 연구 (LLM-SmartAudit의 RQ1)에 따르면 Slither는 테스트 스위트에서 알려진 취약점의 약 **46%**를 잡아냈습니다. Mythril (심볼릭 실행)은 54% 재현율로 약간 더 나은 성과를 보였습니다. 각 도구는 특정 버그 유형에서 강점을 가졌지만 (예: Slither는 산술 문제나 tx.origin 사용을 발견하는 데 매우 능숙하고, 심볼릭 도구는 간단한 재진입 시나리오를 찾는 데 탁월함), 포괄적인 커버리지를 가진 도구는 없었습니다. Slither와 같은 성숙한 도구의 오탐은 상대적으로 낮습니다. 개발자들은 *“최소한의 오탐과 신속한 실행 (계약당 1초 미만)”*을 광고하며, CI 사용에 적합하게 만듭니다. 그럼에도 불구하고, 정적 도구는 코드가 복잡한 패턴을 사용할 경우 잘못 작동할 수 있습니다. 실제로는 처리된 엣지 케이스를 표시하거나, 알려진 안티 패턴과 일치하지 않는 깊은 로직 버그를 놓칠 수 있습니다.

  • 퍼징 및 속성 테스트: Foundry의 퍼즈/불변성 테스트나 Trail of Bits의 Echidna와 같은 퍼저는 런타임 오류 및 불변성 위반을 찾는 데 매우 효과적임이 입증되었습니다. 이러한 도구들은 버그가 보고되면 (단언문 실패) 실제 반례 실행이므로 거의 0에 가까운 오탐을 가집니다. 트레이드오프는 미탐에 있습니다. 테스트된 입력 공간이나 실행 횟수 내에서 버그가 나타나지 않으면 빠져나갈 수 있습니다. 커버리지는 퍼저가 상태 공간을 얼마나 잘 탐색하는지에 따라 달라집니다. 충분한 시간과 좋은 휴리스틱을 사용하면, 퍼저는 정적 분석이 놓친 많은 고위험 버그를 발견했습니다. 예를 들어, Echidna는 형식 검증 노력이 필요했던 MakerDAO 및 Compound 버그를 신속하게 재현할 수 있었습니다. 그러나 퍼징이 모든 로직 실수를 찾을 것이라고 보장되지는 않습니다. 계약이 더 복잡해짐에 따라, 퍼저는 더 깊은 상태에 도달하기 위해 추가적인 불변성을 작성하거나 더 스마트한 검색 전략을 사용해야 할 수 있습니다. 메트릭 측면에서, 퍼징은 단일 "재현율" 숫자를 가지지 않지만, 일화적인 증거에 따르면 중요한 불변성은 깨질 수 있다면 퍼저에 의해 깨질 수 있다는 것을 보여줍니다. 발견한 것에 대한 신뢰성은 높지만 (오탐에 대한 수동 분류가 필요 없음), 퍼즈 테스트를 통과한 것이 정확성의 증명이 아니라 단지 신뢰도의 증가라는 것을 기억해야 합니다.

  • 형식 검증 도구: 적용 가능한 경우, 형식 검증은 가장 높은 보증을 제공합니다. 성공적인 증명은 100%의 상태가 속성을 만족한다는 것을 의미합니다. 정확성 측면에서, 증명할 수 있는 속성에 대해서는 사실상 **완벽 (건전하고 완전함)**합니다. 여기서 가장 큰 문제는 결과의 정확성이 아니라 사용의 어려움과 좁은 범위입니다. 형식 도구는 실제로 미탐을 가질 수도 있습니다. 복잡성 때문에 참인 속성을 증명하지 못할 수 있습니다 (결과 없음 또는 시간 초과, 이는 오탐은 아니지만 실제로는 안전한 것을 검증하지 못했다는 의미). 또한 명세 오류가 있을 수 있는데, 이 경우 도구는 의도하지 않은 속성을 "증명"합니다 (사용자 오류). 실제 감사에서, 형식적 방법은 일부 중요한 버그를 잡아냈습니다 (Certora의 성공 사례에는 배포 전 미묘한 SushiSwap 버그와 PRBMath 라이브러리 문제 포착이 포함됨). 그러나 그들의 실적은 얼마나 포괄적으로 적용되는지에 따라 제한됩니다. Trail of Bits가 언급했듯이, *“퍼징으로 발견된 많은 버그와 대조적으로, 형식 검증만으로 발견된 공개된 문제를 찾기 어려웠다”*고 합니다. 따라서 형식 검증은 성공했을 때 매우 신뢰할 수 있지만, 전체 툴체인 커버리지에 미치는 영향은 필요한 노력과 전문 지식에 의해 제한됩니다.

  • LLM 기반 분석: AI 감사기의 정확성은 새로운 기술 (그리고 새로운 모델)이 빠르게 한계를 밀어붙이고 있기 때문에 현재로서는 유동적입니다. 몇 가지 데이터를 얻을 수 있습니다:

    • ERC 규칙에 초점을 맞춘 AuditGPT 시스템은 매우 높은 정밀도 (오탐 수 기준 ≈96%)를 달성했으며, 정적 도구나 인간이 간과한 수백 개의 문제를 발견했습니다. 그러나 이것은 구조화된 프롬프트를 가진 좁은 영역에서였습니다. ChatGPT가 임의의 취약점 탐색에서 96% 정확할 것이라고 일반화해서는 안 됩니다. 통제된 설정 밖에서는 성능이 더 낮습니다.
    • 더 넓은 취약점 탐지에서, **LLM-SmartAudit (GPT-3.5)**는 중간 정도의 오탐률로 벤치마크에서 약 74%의 재현율을 보였으며, 이는 단일 전통적인 도구보다 낫습니다. 특화된 프롬프팅 (TA 모드)을 사용한 GPT-4로 업그레이드했을 때, 성능이 크게 향상되었습니다. 예를 들어, 1,400개의 실제 취약점 세트에서 GPT-4 에이전트는 특정 문제의 약 48%와 복잡한 로직 문제의 약 47%를 발견한 반면, Slither/Mythril/Conkas는 각각 해당 특정 복잡한 문제의 약 0% (없음)를 발견했습니다. 이는 LLM이 정적 분석이 완전히 놓치는 유형의 버그로 커버리지를 극적으로 확장할 수 있음을 보여줍니다. 반면에, LLM은 문제의 절반 이상을 찾지 못했으며 (따라서 상당한 미탐도 있음), 보고한 것들 중 오탐이 얼마나 많았는지는 명확하지 않습니다. 이 연구는 정밀도보다 재현율에 더 초점을 맞췄습니다.
    • Trail of Bits의 Codex/GPT-4 "Toucan" 실험은 신뢰성 문제를 잘 보여줍니다. 처음에는 작은 예제에서 Codex가 신중한 프롬프팅으로 알려진 취약점 (소유권 문제, 재진입)을 식별할 수 있었습니다. 그러나 규모를 확장하자마자 일관성 없고 부정확한 결과에 직면했습니다. 그들은 “평균 크기의 코드에서도 실패 횟수가 높았고” 예측하기 어려웠다고 보고했습니다. 궁극적으로, 그들은 GPT-4 (2023년 초 기준)가 단지 점진적인 개선에 불과하며, 여전히 함수 간 흐름에 대한 추론과 같은 *“핵심 기능이 부족하다”*고 결론 내렸습니다. 결과적으로 AI는 정적 도구의 오탐을 실질적으로 줄이지 못했으며, 감사 워크플로우를 신뢰성 있게 가속화하지도 못했습니다. 즉, 일반 LLM의 감사기로서의 현재 신뢰성은 해당 시험에서 전문 감사자들에 의해 불충분하다고 판단되었습니다.

요약하자면, 각 툴체인은 서로 다른 강점을 가지고 있습니다:

  • 정적 도구: 알려진 문제를 신속하게 탐지하는 데 신뢰할 수 있음. 노이즈가 적지만, 제한된 버그 유형 (벤치마크에서 중간 재현율 약 40-50%).
  • 퍼즈/불변성 테스트: 매우 높은 정밀도 (거의 오탐 없음) 및 기능적 및 상태 의존적 버그를 찾는 데 강함. 커버리지는 넓을 수 있지만 보장되지는 않음 (단순한 메트릭 없음, 시간과 불변성 품질에 따라 다름). 종종 충분한 지침이 주어지면 형식 증명이 찾을 수 있는 동일한 버그를 찾음.
  • 형식 검증: 특정 속성에 대한 절대적인 정확성의 황금 표준. 성공적으로 적용되면 해당 속성에 대해 본질적으로 100% 재현율/정밀도. 그러나 실제로는 좁은 문제에 제한되고 상당한 노력이 필요함 (아직 전체 감사를 위한 원버튼 솔루션이 아님).
  • AI (LLM) 분석: 잠재적으로 높은 커버리지 – 다른 도구가 놓친 것을 포함한 여러 카테고리의 버그를 찾을 수 있음 – 그러나 가변적인 정밀도. 특화된 설정에서는 정밀하고 넓을 수 있음 (AuditGPT가 ERC 검사에서 보여준 것처럼). 신중한 제약 없이는 넓은 그물을 던지고 결과에 대한 인간의 검증이 필요할 수 있음. 취약점 탐지에 대한 ChatGPT의 "평균" 정확도는 그다지 뛰어나지 않지만 (한 연구에서는 추측에 가까움), LLM을 사용하는 최상의 엔지니어링 시스템은 전통적인 도구를 능가하는 성능을 보여주고 있음. AI 출력을 더 신뢰할 수 있게 만들기 위한 활발한 연구가 진행 중임 (예: 여러 에이전트가 교차 검증하거나, LLM을 정적 추론과 결합하여 AI 결론을 재확인).

접근 방식을 결합하면 최상의 결과를 얻을 수 있다는 점은 주목할 가치가 있습니다. 예를 들어, Slither를 실행하여 (노이즈 없이 쉬운 문제를 잡고), Foundry/Echidna를 사용하여 더 깊은 동작을 퍼징하고, 아마도 LLM 기반 도구를 사용하여 고려되지 않은 패턴이나 불변성을 스캔할 수 있습니다. 각 도구는 다른 도구의 사각지대를 커버할 것입니다.

실제 도입의 과제와 한계​

실제로 개발 워크플로우에 형식 검증이나 AI 도구를 도입하는 데는 실용적인 과제가 따릅니다. 몇 가지 주요 문제는 다음과 같습니다:

  • 개발자 경험 및 전문성: 전통적인 형식 검증은 가파른 학습 곡선을 가지고 있습니다. 형식 명세 (CVL, Coq, Move의 명세 언어 등)를 작성하는 것은 코드를 작성하는 것보다 수학적 증명을 작성하는 것에 더 가깝습니다. 많은 개발자들이 이러한 배경 지식이 부족하며, 형식적 방법 전문가는 드뭅니다. 반면에, Foundry로 퍼징하거나 솔리디티로 불변성을 작성하는 것은 훨씬 더 접근하기 쉽습니다. 추가적인 테스트를 작성하는 것처럼 느껴집니다. 이것이 이더리움 커뮤니티에서 형식 증명보다 퍼즈 테스트가 더 빠르게 채택된 큰 이유입니다. Trail of Bits 팀은 퍼징이 많은 경우 형식적 방법보다 **“비슷한 결과를 내지만 훨씬 적은 기술과 시간이 필요하다”**고 명시적으로 언급했습니다. 따라서 형식 검증이 다른 버그를 잡을 수 있음에도 불구하고, 많은 팀은 더 적은 노력으로 충분히 좋은 결과를 얻는 더 쉬운 접근 방식을 선택합니다.

  • 개발 워크플로우에 통합: 도구가 널리 채택되려면 CI/CD 파이프라인과 일상적인 코딩에 적합해야 합니다. Slither와 같은 도구는 여기서 빛을 발합니다. “CI/CD 설정에 쉽게 통합되어 자동화를 간소화하고 개발자를 돕습니다.” 개발자는 Slither나 Mythril을 GitHub 액션에 추가하고 문제가 발견되면 빌드를 실패시킬 수 있습니다. Foundry의 퍼즈 테스트는 매번 forge test의 일부로 실행될 수 있습니다. 불변성 테스트는 CloudExec과 같은 도구를 사용하여 클라우드에서 지속적으로 실행될 수도 있으며, 모든 실패는 fuzz-utils를 사용하여 자동으로 단위 테스트로 변환될 수 있습니다. 이러한 통합은 개발자가 빠른 피드백을 받고 반복할 수 있음을 의미합니다. 반면에, Certora Prover와 같은 것은 역사적으로 별도의 프로세스로 (또는 외부 감사팀에 의해) 실행되었으며 결과를 생성하는 데 몇 시간이 걸릴 수 있었습니다. 이는 모든 커밋마다 실행할 만한 것이 아닙니다. AI 기반 도구도 통합 장애물에 직면합니다. API를 호출하고 CI에서 그 출력을 결정론적으로 처리하는 것은 간단하지 않습니다. 또한 보안 및 개인 정보 보호 문제도 있습니다. 많은 조직이 분석을 위해 독점적인 계약 코드를 제3자 AI 서비스에 보내는 것을 불안해합니다. 자체 호스팅 LLM 솔루션은 아직 대형 클라우드 API만큼 강력하지 않으므로, 이는 AI 감사기의 CI 도입에 걸림돌이 됩니다.

  • 오탐과 노이즈: 많은 오탐이나 낮은 심각도의 결과를 보고하는 도구는 개발자의 신뢰를 떨어뜨릴 수 있습니다. 정적 분석기는 과거에 이 문제로 어려움을 겪었습니다. 예를 들어, 일부 도구의 초기 버전은 사용자에게 경고를 쏟아냈고, 그중 다수는 관련이 없었습니다. 신호와 노이즈 사이의 균형이 중요합니다. Slither는 최소한의 오탐으로 칭찬받는 반면, Securify와 같은 도구 (연구 형태에서)는 종종 수동 필터링이 필요한 많은 경고를 생성했습니다. 논의된 바와 같이, LLM은 적절하게 타겟팅되지 않으면 노이즈를 생성할 수 있습니다. 이것이 현재 AI 제안이 절대적인 것이 아니라 보통 자문으로 받아들여지는 이유입니다. 팀들은 별도의 보안팀이나 감사 컨텍스트에서 실행될 경우 노이즈가 많은 도구를 채택할 가능성이 더 높지만, 일상적인 사용을 위해 개발자들은 노이즈가 적고 명확하며 실행 가능한 결과를 제공하는 도구를 선호합니다. 이상적인 것은 가설이 아닌 명확한 버그에 대해서만 **“빌드를 실패시키는 것”**입니다. 그 신뢰성을 달성하는 것은 특히 AI 도구에게 지속적인 과제입니다.

  • 확장성 및 성능: 형식 검증은 계산 집약적일 수 있습니다. 언급했듯이, 솔버는 복잡한 계약에서 시간 초과될 수 있습니다. 이로 인해 대규모 시스템으로 확장하기가 어렵습니다. 하나의 속성을 검증하는 데 몇 시간이 걸린다면, 각 코드 변경마다 수십 개의 속성을 확인하지는 않을 것입니다. 퍼즈 테스트도 확장성 한계에 직면합니다. 거대한 상태 공간이나 많은 메서드를 가진 계약을 조합적으로 탐색하는 것은 느릴 수 있습니다 (실제로는 퍼저가 백그라운드나 밤새 실행되어 검색을 심화시킬 수 있음). AI 모델은 고정된 컨텍스트 크기를 가지며 모델의 용량을 늘리는 것은 비쌉니다. GPT-4의 128k 토큰 컨텍스트는 큰 이점이지만, 수백 킬로바이트의 계약 코드를 공급하는 것은 비용이 많이 들고 매우 큰 프로젝트에는 여전히 충분하지 않습니다 (많은 계약을 가진 복잡한 프로토콜을 상상해 보세요. 그 한도를 초과할 수 있음). 또한 다중 체인 확장성도 있습니다. 프로젝트가 다른 체인 (이더리움 ↔ 다른 체인)의 계약 간 상호작용을 포함하는 경우, 해당 크로스체인 로직을 검증하거나 분석하는 것은 훨씬 더 복잡하며 현재 도구의 범위를 벗어날 가능성이 높습니다.

  • 인간의 감독 및 검증: 결국, 대부분의 팀은 최종 승인을 위해 전문가인 인간 감사자에게 의존합니다. 자동화된 도구는 대체물이 아닌 보조 도구입니다. 이 모든 도구의 한계 중 하나는 알려진 속성이나 패턴의 범위 내에서 작동한다는 것입니다. 완전히 새로운 유형의 버그나 DeFi 프로토콜 설계의 미묘한 경제적 결함을 놓칠 수 있습니다. 인간 감사자는 직관과 경험을 사용하여 공격자가 시스템에 어떻게 접근할지 고려하며, 때로는 어떤 도구도 명시적으로 프로그래밍되지 않은 방식으로 접근합니다. 모든 자동화된 검사를 통과했지만 나중에 인간이 비즈니스 로직이나 창의적인 공격 벡터에서 취약점을 발견한 사례가 있었습니다. 따라서 과제는 잘못된 안도감을 피하는 것입니다. 개발자는 형식 도구와 AI의 출력을 올바르게 해석하고 "문제가 발견되지 않음"이 코드가 100% 안전하다는 것을 의미한다고 가정해서는 안 됩니다.

  • 명세 및 테스트 유지 관리: 특히 형식 검증의 경우, 한 가지 실용적인 문제는 명세 드리프트입니다. 명세 (불변성, 규칙 등)는 코드가 진화함에 따라 구식이 될 수 있습니다. 코드와 형식 명세가 동기화되도록 보장하는 것은 간단하지 않은 관리 작업입니다. 개발자들이 주의를 기울이지 않으면, 증명은 단순히 코드의 실제 요구 사항과 더 이상 관련이 없는 것을 증명하기 때문에 "통과"할 수 있습니다. 마찬가지로, 불변성 테스트는 시스템의 예상 동작이 변경됨에 따라 업데이트되어야 합니다. 이는 모든 팀이 가지고 있지 않은 불변성 주도 개발 문화를 요구합니다 (비록 이를 장려하려는 움직임이 있지만).

요약하자면, 주요 한계는 기술의 순수한 능력보다는 사람과 프로세스입니다. 형식 및 AI 보조 방법은 보안을 크게 향상시킬 수 있지만, 개발자의 워크플로우와 기술 수준에 맞는 방식으로 배포되어야 합니다. 고무적이게도, 불변성 주도 개발 (첫날부터 중요한 불변성을 기록하는 것)과 같은 추세가 힘을 얻고 있으며, 도구는 고급 분석을 더 플러그 앤 플레이 방식으로 만들기 위해 서서히 개선되고 있습니다. 주요 도구 (예: Certora Prover)의 오픈소스화와 인기 있는 프레임워크 (Foundry)에 퍼징을 통합하는 것은 장벽을 낮추고 있습니다. 시간이 지남에 따라, "평균적인 개발자"가 할 수 있는 것과 "박사 연구원"이 할 수 있는 것 사이의 격차가 이러한 강력한 검증 기술을 사용하는 측면에서 좁혀질 것으로 예상됩니다.

오픈소스 vs 상용 감사 도구​

스마트 계약 보안 도구의 환경에는 오픈소스 프로젝트와 상용 서비스가 모두 포함됩니다. 각각의 역할이 있으며, 종종 서로를 보완합니다:

  • 오픈소스 도구: 이더리움 생태계에서 널리 사용되는 감사 도구의 대부분은 오픈소스입니다. 여기에는 Slither (정적 분석기), Mythril (심볼릭 실행), Echidna (퍼저), Manticore (심볼릭/콘콜릭 실행), Securify (ETH 취리히의 분석기), Solhint/Ethlint (린터), 그리고 물론 Foundry 자체가 포함됩니다. 오픈소스 도구는 몇 가지 이유로 선호됩니다: (1) 투명성 – 개발자는 도구가 어떻게 작동하는지 볼 수 있고 악의적이거나 숨겨진 것이 없다고 신뢰할 수 있습니다 (개방형 생태계에서 중요). (2) 커뮤니티 기여 – 규칙과 기능은 광범위한 커뮤니티에 의해 추가됩니다 (예를 들어 Slither에는 많은 커뮤니티 기여 탐지기가 있음). (3) 비용 – 무료로 사용할 수 있으며, 이는 Web3의 많은 소규모 프로젝트/스타트업에게 중요합니다. (4) 통합 – 오픈 도구는 일반적으로 법적 장애물 없이 로컬이나 CI에서 실행할 수 있으며, 종종 프로젝트별 요구에 맞게 사용자 정의하거나 스크립팅할 수 있습니다.

    오픈소스 도구는 빠르게 발전했습니다. 예를 들어, Slither의 새로운 솔리디티 버전 및 패턴 지원은 Trail of Bits에 의해 지속적으로 업데이트됩니다. ConsenSys가 개발한 Mythril은 이더리움뿐만 아니라 바이트코드에서 작동하여 모든 EVM 호환 체인을 분석할 수 있습니다. 이는 오픈 도구가 여러 체인에서 쉽게 재사용될 수 있음을 보여줍니다. 오픈 도구의 단점은 종종 *“사용에 따른 위험은 본인 책임”*이라는 것입니다. 공식적인 지원이나 보증이 없습니다. 상용 제품의 UI처럼 확장되거나 세련되지 않을 수 있습니다. 그러나 블록체인에서는 많은 회사조차도 내부적으로 오픈소스를 핵심 도구로 사용합니다 (때로는 약간의 사용자 정의 수정과 함께).

  • 상용 서비스 및 도구: 몇몇 회사는 보안 분석을 제품으로 제공했습니다. 예로는 MythX (ConsenSys Diligence의 클라우드 기반 스캐닝 API), Certora (오픈소스화하기 전에 프로버를 서비스로 제공), CertiK 및 SlowMist (감사에서 사용하거나 대시보드를 통해 제공하는 내부 스캐너와 AI를 보유한 회사), 그리고 Securify from ChainSecurity (회사가 인수되고 도구가 내부적으로 사용됨)나 SolidityScan (감사 보고서를 출력하는 클라우드 스캐너)과 같은 일부 새로운 진입자가 있습니다. 상용 도구는 종종 더 사용자 친화적인 경험이나 통합 서비스를 제공하는 것을 목표로 합니다. 예를 들어, MythX는 IDE 확장 및 CI 플러그인과 통합되어 개발자가 계약을 MythX로 보내고 취약점 점수와 문제 해결 세부 정보가 포함된 상세 보고서를 받을 수 있도록 했습니다. 이러한 서비스는 일반적으로 내부적으로 오탐을 최소화하도록 조정된 분석 기술 (패턴 매칭, 심볼릭 실행 등)의 조합을 실행합니다.

    상용 도구의 가치 제안은 보통 편의성과 지원입니다. 지속적으로 업데이트되는 취약점 지식 기반을 유지하고 결과 해석에 대한 고객 지원을 제공할 수 있습니다. 또한 클라우드에서 무거운 계산을 처리할 수도 있습니다 (따라서 로컬에서 솔버를 실행할 필요가 없음). 그러나 비용이 문제입니다. 많은 프로젝트가 무료 대안의 가용성을 고려하여 이러한 서비스에 비용을 지불하지 않기로 선택합니다. 또한, 탈중앙화 정신에 따라 일부 개발자는 보안을 위해 폐쇄 소스 서비스에 의존하는 것을 주저합니다 ("신뢰하지 말고 검증하라"는 정신). 2025년 Certora Prover의 오픈소스화는 주목할 만한 사건입니다. 고급 상용 도구였던 것을 커뮤니티 자원으로 전환했습니다. 이 움직임은 이제 누구나 유료 라이선스 없이 계약을 형식적으로 검증하려고 시도할 수 있고, 코드 개방성으로 인해 연구자들이 도구를 개선하거나 다른 체인에 적용할 수 있게 되므로 채택을 가속화할 것으로 예상됩니다.

  • 인적 감사 서비스: 소프트웨어 도구 외에도 많은 감사는 전문 회사 (Trail of Bits, OpenZeppelin, Certik, PeckShield 등)에 의해 수행된다는 점을 언급할 가치가 있습니다. 이 회사들은 위의 도구 (대부분 오픈소스)와 독점 스크립트를 혼합하여 사용합니다. 이러한 노력의 결과물은 종종 비공개로 유지되거나 감사 보고서에 요약만 됩니다. 상용 감사 회사조차도 오픈소스 도구에 크게 의존하기 때문에 여기에는 "오픈소스 vs 상용"의 이분법이 정확히 존재하지 않습니다. 차별화는 전문성과 수동 노력에 더 가깝습니다. 즉, 일부 회사는 우위를 점하기 위해 독점적인 AI 보조 감사 플랫폼을 개발하고 있습니다 (예를 들어, 내부 감사에 *“ChainGPT”*가 사용되었다는 보고나, CertiK가 온체인 모니터링을 위해 Skynet이라는 AI를 개발했다는 보고가 있었음). 이들은 공개된 도구가 아니므로 정확성과 방법이 널리 문서화되어 있지 않습니다.

실제로 일반적인 패턴은 오픈소스 우선, 상용은 선택 사항입니다. 팀들은 개발 및 테스트 중에 오픈 도구를 사용합니다 (쉽게 통합하고 필요할 때마다 실행할 수 있기 때문). 그런 다음, 배포 전에 추가 확인을 위해 하나 또는 두 개의 상용 서비스를 사용할 수 있습니다. 예를 들어, MythX 스캔을 실행하여 "두 번째 의견"을 얻거나, Certora와 같은 고급 도구를 사용하는 회사를 고용하여 중요한 구성 요소를 형식적으로 검증합니다. 경계가 모호해지면서 (Certora 오픈소스, MythX 결과가 종종 오픈 도구와 겹침), 구별은 능력보다는 지원과 편의성에 관한 것이 되고 있습니다.

한 가지 주목할 만한 교차점은 Certora의 다중 체인 지원입니다. 솔라나와 스텔라를 공식적으로 지원함으로써, 그들은 오픈 대안이 적은 플랫폼을 다룹니다 (예: 이더리움에는 많은 오픈 도구가 있지만, 솔라나에는 최근까지 거의 없었음). 보안 도구가 새로운 생태계로 확장됨에 따라, 적어도 오픈소스가 따라잡을 때까지 상용 제품이 격차를 메우는 것을 더 많이 볼 수 있습니다.

마지막으로, 오픈소스와 상용이 여기서는 적대적이지 않다는 점을 주목할 가치가 있습니다. 그들은 종종 서로에게서 배웁니다. 예를 들어, 학술/상용 도구에서 개척된 기술 (Securify에서 사용된 추상 해석과 같은)은 결국 오픈 도구에 도입되고, 반대로 오픈 도구 사용 데이터는 상용 도구 개선을 안내할 수 있습니다. 양측이 추구하는 최종 결과는 전체 생태계의 더 나은 보안입니다.

크로스체인 적용 가능성​

이더리움이 대부분의 이러한 도구들의 초점이었지만 (스마트 계약 활동에서의 우위 때문에), 형식 검증과 AI 보조 감사의 개념은 다른 블록체인 플랫폼에도 적용 가능합니다. 다음은 그것들이 어떻게 변환되는지입니다:

  • EVM 호환 체인: BSC, 폴리곤, 아발란체 C-Chain 등 이더리움 가상 머신을 사용하는 블록체인은 모든 동일한 도구를 직접 사용할 수 있습니다. 퍼즈 테스트나 정적 분석은 계약이 이더리움 메인넷에 배포될지 폴리곤에 배포될지 신경 쓰지 않습니다. 바이트코드와 소스 언어 (솔리디티/바이퍼)는 동일합니다. 실제로 Mythril과 Slither는 주소에서 바이트코드를 가져와 모든 EVM 체인의 계약을 분석할 수 있습니다 (Mythril은 RPC 엔드포인트만 필요함). 이러한 체인의 많은 DeFi 프로젝트는 이더리움 프로젝트와 마찬가지로 Slither와 Echidna를 실행합니다. BSC나 아발란체의 프로토콜 감사는 일반적으로 이더리움 감사와 동일한 툴킷을 사용합니다. 따라서 EVM 컨텍스트에서 크로스체인은 대부분 이더리움의 툴체인을 재사용하는 것을 의미합니다.

  • 솔라나: 솔라나의 스마트 계약은 Rust로 작성되고 (보통 Anchor 프레임워크를 통해) BPF 가상 머신에서 실행됩니다. 이는 이더리움과 매우 다른 환경이므로 이더리움 전용 도구는 즉시 작동하지 않습니다. 그러나 동일한 원칙이 적용됩니다. 예를 들어, Rust의 네이티브 퍼징 라이브러리나 cargo-fuzz와 같은 도구를 사용하여 솔라나 프로그램에 대한 퍼즈 테스트를 수행할 수 있습니다. 솔라나에서의 형식 검증은 최근까지 거의 존재하지 않았습니다. Certora와 솔라나 엔지니어 간의 협력으로 명세에 대해 Rust/Anchor 계약을 증명할 수 있는 솔라나 프로그램을 위한 자체 검증 도구가 탄생했습니다. 언급했듯이, Certora는 프로버를 솔라나의 VM으로 확장하여 개발자가 솔리디티에 대해 하듯이 솔라나 프로그램 동작에 대한 규칙을 작성하고 확인할 수 있게 되었습니다. 이는 솔라나의 빠른 개발 접근 방식이 많은 계약이 이더리움에서 볼 수 있는 엄격한 테스트 없이 출시되었음을 의미하기 때문에 중요합니다. 형식 도구는 이를 개선할 수 있습니다. 솔라나를 위한 AI 감사도 가능합니다. Rust를 이해하는 LLM은 소유권 확인 누락이나 산술 오류와 같은 취약점에 대해 솔라나 프로그램을 확인하도록 프롬프트될 수 있습니다. 솔라나 특정 패턴에 대한 미세 조정이 필요할 수 있지만, Rust의 인기를 고려할 때 GPT-4는 Rust 코드를 읽는 데 상당히 능숙합니다. 곧 "Anchor를 위한 ChatGPT" 스타일의 도구도 등장할 수 있습니다.

  • 폴카닷 및 Substrate 기반 체인: 폴카닷의 스마트 계약은 ink! 프레임워크를 사용하여 Rust로 작성될 수 있으며 (웹어셈블리로 컴파일됨), 또는 다시 솔리디티를 허용하는 EVM 팔레트 (문빔이 하는 것처럼)를 실행할 수 있습니다. ink!/Wasm의 경우, 검증 도구는 아직 초기 단계입니다. 일반적인 Wasm 검증 프레임워크 (예: Microsoft의 Project Verona 등)를 사용하여 Wasm 계약의 속성을 형식적으로 검증하려고 시도할 수 있습니다. Certora의 오픈소스 프로버는 또한 스텔라의 WASM 스마트 계약 지원을 언급하는데, 이는 모든 Wasm 기반 체인과 개념적으로 유사합니다. 따라서 폴카닷의 Wasm 계약에도 적용될 가능성이 높습니다. ink! 계약의 퍼즈 테스트는 Rust 테스트를 작성하여 수행할 수 있습니다 (Rust의 속성 테스트가 비슷한 역할을 할 수 있음). ink! 계약의 AI 감사는 Rust 코드를 분석하는 것을 수반하며, 이는 LLM이 올바른 컨텍스트로 다시 수행할 수 있습니다 (비록 특정 ink! 매크로나 트레이트에 대한 힌트 없이는 알지 못할 수 있음).

    또한, 폴카닷은 병렬 스마트 계약 개발을 위해 Move 언어를 탐색하고 있습니다 (일부 커뮤니티 포럼에서 암시됨). Move가 폴카닷 파라체인에서 사용된다면, Move Prover가 함께 제공되어 설계상 형식 검증 기능을 제공합니다. Move의 안전성 강조 (자원 지향 프로그래밍)와 내장된 프로버는 처음부터 형식적 방법의 크로스체인 전파를 보여줍니다.

  • 기타 블록체인: 테조스 (미켈슨 스마트 계약) 및 알고랜드 (TEAL 프로그램)와 같은 플랫폼은 각각 형식 검증 노력을 해왔습니다. 예를 들어, 테조스에는 미켈슨의 형식 시맨틱을 제공하고 속성을 증명할 수 있는 Mi-Cho-Coq라는 도구가 있습니다. 이들은 더 학술적인 측면에 있지만, 잘 정의된 계약 시맨틱을 가진 모든 블록체인이 형식 검증의 대상이 될 수 있음을 보여줍니다. AI 감사는 원칙적으로 모든 프로그래밍 언어에 적용될 수 있습니다. LLM을 적절하게 훈련하거나 프롬프트하는 문제입니다. 덜 일반적인 언어의 경우, LLM이 효과적이려면 충분한 예제에 대해 사전 훈련되지 않았을 수 있으므로 약간의 미세 조정이 필요할 수 있습니다.

  • 크로스체인 상호작용: 새로운 과제는 체인 간의 상호작용 (브리지나 체인 간 메시징 등)을 검증하는 것입니다. 여기서 형식 검증은 여러 체인의 상태와 통신 프로토콜을 모델링하는 것을 포함할 수 있습니다. 이는 매우 복잡하며 현재 대부분의 도구의 범위를 벗어나지만, 특정 브리지 프로토콜은 보안을 위해 수동으로 분석되었습니다. AI는 크로스체인 코드를 검토하는 데 도움이 될 수 있지만 (예를 들어, 코스모스의 IBC 프로토콜과 상호작용하는 솔리디티 계약 검토), 아직 즉시 사용 가능한 솔루션은 없습니다.

본질적으로, 이더리움의 도구는 다른 체인을 위한 길을 닦았습니다. 많은 오픈소스 도구들이 적용되고 있습니다. 예를 들어, 솔라나 (Rust)를 위한 Slither와 유사한 정적 분석기를 만들려는 노력이 있으며, 불변성 테스트의 개념은 언어에 구애받지 않습니다 (속성 기반 테스트는 많은 언어에 존재함). 강력한 엔진 (여러 VM을 위한 Certora의 엔진 등)의 오픈소스화는 크로스체인 보안에 특히 유망합니다. 동일한 플랫폼을 사용하여 솔리디티 계약, 솔라나 프로그램, Move 계약을 검증할 수 있으며, 각기 적절한 명세가 작성되어 있다면 가능합니다. 이는 업계 전반에 걸쳐 더 균일한 보안 태세를 장려합니다.

또한 AI 보조 감사는 모든 체인에 이익이 될 것이라는 점도 주목할 가치가 있습니다. 모델은 어떤 컨텍스트에서든 취약점에 대해 학습할 수 있기 때문입니다. AI에 올바른 정보 (언어 명세, 해당 생태계의 알려진 버그 패턴)가 제공되는 한, 유사한 추론을 적용할 수 있습니다. 예를 들어, ChatGPT는 적절한 프롬프트로 솔리디티 계약이나 Move 모듈을 감사하도록 요청받을 수 있으며, 둘 다 수행할 것입니다. 심지어 해당 개념이 있다면 *“이 Move 모듈은 자원 보존을 위반할 수 있습니다”*와 같은 것을 잡아낼 수도 있습니다. 한계는 AI가 해당 체인에 대한 충분한 훈련 데이터에 노출되었는지 여부입니다. 가장 인기 있는 이더리움은 모델이 솔리디티에 가장 능숙하도록 편향시켰을 가능성이 높습니다. 다른 체인이 성장함에 따라, 미래의 LLM이나 미세 조정된 파생물이 그것들도 커버할 수 있을 것입니다.

결론​

스마트 계약의 형식 검증과 AI 보조 감사는 빠르게 발전하는 분야입니다. 우리는 이제 코드 신뢰성을 향상시키는 결정론적 정적 분석기 및 퍼징 프레임워크부터, 인간과 유사한 방식으로 코드에 대해 추론할 수 있는 최첨단 AI에 이르기까지 풍부한 툴킷을 보유하고 있습니다. 한때 틈새 학문 분야였던 형식 검증은 더 나은 도구와 통합을 통해 더욱 실용적이 되고 있습니다. AI는 현재의 한계에도 불구하고 보안 분석을 자동화하는 데 있어 판도를 바꿀 수 있는 능력을 엿보여주었습니다.

아직 만능 해결책은 없습니다. 실제 감사는 심층 방어를 달성하기 위해 여러 기술을 결합합니다. Foundry의 퍼즈 및 불변성 테스트는 이미 배포 전에 기대되는 기준을 높이고 있습니다 (기본 테스트를 통과했을 많은 오류를 잡아냄). AI 보조 감사는 신중하게 사용될 때 감사자에게 전력 증강 요소 역할을 하여, 수동 검토만으로는 불가능한 규모와 속도로 문제를 강조하고 규정 준수를 확인할 수 있습니다. 그러나 이러한 도구를 구동하고, 그 결과를 해석하며, 확인할 올바른 속성을 정의하는 데는 인간의 전문성이 여전히 중요합니다.

앞으로 우리는 이러한 접근 방식의 더 큰 융합을 기대할 수 있습니다. 예를 들어, AI는 형식 명세를 작성하거나 불변성을 제안하는 데 도움이 될 수 있습니다 (“AI, 이 DeFi 계약에 대해 어떤 보안 속성이 유지되어야 합니까?”). 퍼징 도구는 입력을 더 지능적으로 생성하도록 AI를 통합할 수 있습니다 (PromFuzz가 하는 것처럼). 형식 검증 엔진은 어떤 보조정리나 휴리스틱을 적용할지 결정하기 위해 머신러닝을 사용할 수 있습니다. 이 모든 것은 이더리움뿐만 아니라 모든 블록체인 플랫폼에서 더 안전한 스마트 계약에 기여할 것입니다. 궁극적인 비전은 중요한 스마트 계약이 정확성에 대한 높은 신뢰를 가지고 배포될 수 있는 미래이며, 이 목표는 형식적 방법이나 AI 지원 중 하나만으로는 달성되지 않고, 둘의 시너지 효과를 통해 달성될 가능성이 높습니다.

протSources:

  • Foundry fuzzing and invariant testing overview
  • Trail of Bits on fuzzing vs formal verification
  • Trail of Bits on formal verification limitations
  • Patrick Collins on fuzz/invariant vs formal methods
  • Trail of Bits on invariants in audits
  • Medium (BuildBear) on Slither and Mythril usage
  • AuditGPT results (ERC compliance)
  • Trail of Bits on LLM (Codex/GPT-4) limitations
  • LLM-SmartAudit performance vs traditional tools
  • “Detection Made Easy” study on ChatGPT accuracy
  • PromFuzz (LLM+fuzz) performance
  • Certora open-source announcement (multi-chain)
  • Move Prover description (Aptos)
  • Static analysis background (Smart contract security literature)
Share on Twitter