"blockchain security" 태그로 연결된 8 개 게시물 개의 게시물이 있습니다.

GitHub 역사상 가장 빠르게 성장한 리포지토리가 82개국에 걸쳐 135,000개 이상의 취약한 AI 에이전트를 노출시켰습니다. 그리고 암호화폐 사용자가 주요 표적이 되었습니다. AI 게이트웨이를 배포하기 위해 경쟁하던 중국 기술 대기업들이 블록체인 보안의 규칙을 새로 쓰고 있는 대규모 공급망 공격과 충돌하면서 발생한 OpenClaw 보안 위기에 오신 것을 환영합니다.

보안의 악몽이 된 바이럴 현상​

2026년 1월 말, OpenClaw는 전례 없는 기록을 세웠습니다. 단 하루 만에 GitHub 스타 20,000개 이상을 획득하며 플랫폼 역사상 가장 빠르게 성장한 오픈 소스 프로젝트가 되었습니다. 2026년 3월까지 이 AI 비서는 250,000개 이상의 스타를 모았으며, 전 세계 기술 애호가들은 개인용 AI의 미래처럼 보이는 이 프로그램을 설치하기 위해 앞다투어 달려들었습니다.

클라우드 기반 AI 비서와 달리, OpenClaw는 사용자의 컴퓨터에서 직접 실행되며 파일, 이메일 및 애플리케이션에 대한 전체 액세스 권한을 가집니다. 사용자는 WhatsApp, Telegram 또는 Discord를 통해 메시지를 보낼 수 있으며, OpenClaw는 24시간 내내 작동하여 쉘 명령 실행, 웹 브라우징, 이메일 발송, 캘린더 관리 등 디지털 생활 전반에 걸친 작업을 수행합니다. 이 모든 것은 휴대전화에서 보내는 일상적인 메시지 하나로 트리거됩니다.

"로컬에서 실행되고, 항상 사용 가능하며, 무한한 능력을 갖춘 나만의 개인 AI 에이전트"라는 홍보 문구는 거부하기 힘들었습니다. 하지만 현실은 훨씬 더 위험한 것으로 드러났습니다.

135,000개의 노출된 인스턴스: 보안 재앙의 규모​

2026년 2월경, 보안 연구원들은 충격적인 사실을 발견했습니다. 82개국에 걸쳐 135,000개 이상의 OpenClaw 인스턴스가 공용 인터넷에 노출되었으며, 그중 **50,000개 이상이 원격 코드 실행(Remote Code Execution, RCE)**에 취약한 상태였습니다. 원인은 OpenClaw의 기본 설정에 있는 근본적인 보안 결함 때문이었습니다.

OpenClaw는 기본적으로 0.0.0.0:18789에 바인딩됩니다. 이는 보안 모범 사례에서 요구하는 127.0.0.1(로컬 호스트 전용)이 아니라, 공용 인터넷을 포함한 모든 네트워크 인터페이스에서 요청을 대기한다는 것을 의미합니다. 상황을 비유하자면, 대문에 "자유롭게 들어오세요"라는 표지판을 걸어두고 문을 활짝 열어둔 것과 같습니다. 문제는 그 문이 사용자의 디지털 생활 전체로 이어진다는 점입니다.

"ClawJacked" 취약점은 상황을 더욱 악화시켰습니다. 공격자는 사용자가 악성 웹사이트를 방문하도록 유도하는 것만으로도 AI 비서를 탈취할 수 있었습니다. 일단 침해되면, 공격자는 AI 에이전트와 동일한 수준의 권한, 즉 사용자의 파일, 자격 증명, 브라우저 데이터, 그리고 암호화폐 지갑에 대한 액세스 권한을 갖게 됩니다.

보안 기업인 Kaspersky, Bitsight, Oasis Security 등은 모두 긴급 경고를 발표했습니다. 업계의 공통된 의견은 분명했습니다. OpenClaw는 심각한 원격 코드 실행 취약점, 아키텍처적 약점, 그리고 무엇보다 우려스러운 플러그인 마켓플레이스에서의 대규모 공급망 오염 캠페인을 포함하는 "보안의 악몽"이었습니다.

ClawHavoc: 암호화폐 사용자를 노린 공급망 공격​

연구원들이 OpenClaw의 핵심 취약점에 집중하는 동안, 사용자가 AI 에이전트를 위한 서드파티 "스킬(플러그인)"을 쉽게 찾고 설치할 수 있도록 설계된 마켓플레이스인 ClawHub에서는 더 교활한 위협이 전개되고 있었습니다.

2026년 2월, ClawHavoc으로 명명된 보안 조사에 따르면 ClawHub에서 감사된 2,857개의 스킬 중 341개가 악성인 것으로 밝혀졌습니다. 2월 중순 마켓플레이스가 10,700개 이상의 스킬로 성장함에 따라 악성 스킬의 수는 824개로 두 배 이상 늘어났으며, 일부 보고에 따르면 1,184개에 달하기도 했습니다.

공격 메커니즘은 매우 영리했습니다.

1. 가짜 필수 구성 요소: 335개의 스킬이 가짜 설치 요구 사항을 사용하여 사용자가 Atomic macOS Stealer(AMOS) 멀웨어를 다운로드하도록 유도했습니다.
2. 플랫폼별 페이로드: Windows에서는 침해된 GitHub 리포지토리에서 "openclaw-agent.zip"을 다운로드하게 했고, macOS에서는 glot.io에 호스팅된 설치 스크립트를 터미널에 직접 복사하도록 했습니다.
3. 정교한 사회 공학: 문서를 통해 사용자가 정당한 설정 단계인 것처럼 속아 악성 명령을 실행하도록 설득했습니다.
4. 통합 인프라: 모든 악성 스킬이 동일한 명령 및 제어(C2) 인프라를 공유하고 있었으며, 이는 조직적인 캠페인임을 시사합니다.

주요 표적은 바로 암호화폐 사용자였습니다.

이 멀웨어는 다음과 같은 정보를 탈취하도록 설계되었습니다.

• 거래소 API 키
• 지갑 개인 키 (Private Keys)
• SSH 자격 증명
• 브라우저 비밀번호
• Solana 지갑 및 지갑 추적기(Wallet Trackers)의 암호화폐 관련 데이터

악성 스킬 중 111개는 Solana 지갑 연동 및 암호화폐 추적기를 포함하여 명백히 암호화폐에 특화된 도구였습니다. 공격자들은 브라우저 확장 프로그램과 지갑 도구 설치에 익숙한 암호화폐 사용자들이 AI 에이전트 공급망 공격의 가장 수익성 높은 타겟이라는 점을 정확히 파악하고 있었습니다.

중국 기술 대기업들의 배포 경쟁​

보안 연구원들이 경고를 보내는 동안, 중국의 거대 기술 기업들은 이를 기회로 보았습니다. 2026년 3월 초, Tencent, Alibaba, ByteDance, JD.com, Baidu는 모두 경쟁적으로 무료 OpenClaw 설치 캠페인을 시작했습니다. 평소라면 수개월이 걸릴 경쟁 구도가 단 며칠 만에 형성되었습니다.

전략은 명확했습니다. 무료 배포를 고객 확보의 수단으로 활용하여, 상업용 AI 프로젝트가 확장되기 전에 사용자를 선점하는 것이었습니다. 각 기업은 "차세대 AI 개발자를 위한 첫 번째 인프라 접점"이 되기 위해 경쟁했습니다.

• Tencent는 OpenClaw를 WeChat과 통합한 QClaw를 출시하여 사용자가 휴대전화로 명령을 보내 노트북을 원격 제어할 수 있게 했습니다.
• Alibaba Cloud는 자사의 Qwen AI 모델 시리즈와 연결하여 플랫폼 전반에 OpenClaw 지원을 배포했습니다.
• ByteDance의 Volcano Engine은 설정 없이 바로 사용할 수 있는 OpenClaw 버전인 ArkClaw를 공개했습니다.

보안 연구원들이 135,000개의 노출된 인스턴스와 대규모 공급망 공격을 경고하는 와중에, 중국 최대의 기술 기업들이 수백만 명의 사용자에게 대량 설치를 적극적으로 홍보하고 있었다는 점은 매우 아이러니합니다. 기술적 열광과 보안 현실 사이의 충돌이 이토록 극명하게 드러난 적은 없었습니다.

Web3의 AI 에이전트 문제: MCP가 암호화폐 지갑을 만날 때​

OpenClaw 위기는 Web3 빌더들이 더 이상 무시할 수 없는 심각한 문제를 드러냈습니다. AI 에이전트가 온체인 자산을 관리하는 사례가 늘고 있지만, 그 보안 모델은 위험할 정도로 미성숙하다는 점입니다.

AI 에이전트를 외부 시스템에 연결하는 새로운 표준인 모델 컨텍스트 프로토콜 (Model Context Protocol, MCP) 은 AI가 블록체인과 상호작용하는 관문이 되고 있습니다. MCP 서버는 전체 Web3 스택에 대한 통합 API 게이트웨이 역할을 수행하며, AI 에이전트가 블록체인 데이터를 읽고, 트랜잭션을 준비하며, 온체인 작업을 실행할 수 있도록 지원합니다.

현재 대부분의 암호화폐 MCP 서버는 개인 키 (private key) 설정을 요구하며, 이는 단일 장애점 (single point of failure) 을 생성합니다. 수만 개의 OpenClaw 인스턴스처럼 AI 에이전트가 침해당하면, 공격자는 자금에 직접 접근할 수 있게 됩니다.

현재 두 가지 경쟁적인 보안 모델이 등장하고 있습니다:

1. 위임 서명 (사용자 제어형)​

AI 에이전트가 트랜잭션을 준비하지만, 사용자가 서명에 대한 독점적인 제어권을 보유합니다. 개인 키는 사용자의 기기를 절대로 떠나지 않습니다. 이는 가장 안전한 접근 방식이지만 에이전트의 자율성을 제한합니다.

2. 에이전트 제어 허용 한도 (Allowances)​

에이전트가 자체 키를 보유하고 사용자를 대신해 지출할 수 있는 허용 한도 (allowance) 를 부여받습니다. 개인 키는 에이전트 호스트에 의해 안전하게 관리되며 지출은 제한됩니다. 이는 자율적인 운영을 가능하게 하지만 호스트의 보안에 대한 신뢰가 필요합니다.

아직 두 모델 모두 널리 채택되지 않았습니다. 대부분의 암호화폐 MCP 구현은 여전히 "에이전트에게 개인 키를 제공하는" 위험한 방식을 사용하고 있으며, 이는 바로 ClawHavoc 공격자들이 노렸던 시나리오입니다.

2026년 추정치에 따르면, 암호화폐 지갑의 60%가 포트폴리오 관리, 트랜잭션 추적 및 보안 강화를 위해 에이전트형 AI를 사용할 것으로 보입니다. 업계는 이러한 상호작용을 보호하기 위해 다자간 연산 (MPC), 계정 추상화 (account abstraction), 생체 인식 인증 및 암호화된 로컬 스토리지를 도입하고 있습니다. 이더리움 재단, 메타마스크 (MetaMask), 구글이 공동 주도하는 ERC-8004 와 같은 표준은 온체인에서 AI 에이전트를 위한 검증 가능한 신원 및 신용 이력을 구축하려 노력하고 있습니다.

하지만 OpenClaw 사건은 이러한 보호 장치가 아직 마련되지 않았음을 증명했으며, 공격자들은 이미 그 틈새를 악용하고 있습니다.

NVIDIA의 기업용 해답: GTC 2026에서 공개된 NemoClaw​

OpenClaw 보안 위기가 확산됨에 따라 NVIDIA는 기회를 포착했습니다. 3월 중순 GTC 2026에서 NVIDIA는 설계 단계부터 보안과 프라이버시가 내장된 기업 자동화 전용 오픈 소스 AI 에이전트 플랫폼인 NemoClaw를 발표했습니다.

소비자 우선의 어디에나 설치 가능한 OpenClaw의 방식과 달리, NemoClaw는 다음과 같은 기능을 통해 기업을 공략합니다:

• 내장된 보안 및 프라이버시 도구: OpenClaw를 괴롭혔던 취약점 해결
• 기업용 인증 및 액세스 제어: "인터넷에 공개된" 기본 설정으로 인한 재앙 방지
• 멀티 플랫폼 지원: NVIDIA 칩뿐만 아니라 회사의 NeMo, Nemotron 및 Cosmos AI 프레임워크를 활용하여 구동
• 파트너십 생태계: 세일즈포스 (Salesforce), 구글 (Google), 시스코 (Cisco), 어도비 (Adobe), 크라우드스트라이크 (CrowdStrike) 등과의 논의 포함

타이밍은 이보다 더 전략적일 수 없습니다. OpenClaw의 "랍스터 열풍 (Lobster Fever)" 이 소비자 중심 AI 에이전트의 위험성을 드러냈을 때, NVIDIA는 NemoClaw를 안전한 기업용 대안으로 포지셔닝하여 비즈니스 AI 에이전트 시장에서 OpenAI에 잠재적인 도전장을 내밀었습니다.

AI 통합 인프라를 구축하는 Web3 기업들에게 NemoClaw는 OpenClaw가 노출한 보안 문제에 대한 잠재적 해결책을 제시합니다. 즉, 고가치 블록체인 자산과 안전하게 상호작용할 수 있도록 전문적으로 관리되고, 감사되며, 보호되는 AI 에이전트 배포를 가능하게 합니다.

Web3에 필요한 경종​

OpenClaw 위기는 단순한 AI 보안 이야기가 아닙니다. 이는 블록체인 인프라에 관한 이야기입니다.

다음과 같은 시사점을 고려해 보십시오:

• 135,000개 이상의 노출된 AI 에이전트: 암호화폐 지갑에 접근할 가능성이 있음
• 1,184개의 악성 플러그인: 특히 암호화폐 사용자를 표적으로 삼음
• 중국의 5대 테크 거인: 적절한 보안 검토 없이 수백만 건의 설치를 추진
• 암호화폐 지갑의 60%: 연말까지 AI 에이전트를 사용할 것으로 예상
• 널리 채택된 보안 표준 부재: AI와 블록체인 간 상호작용을 위한 표준 미비

이것은 전통 금융 (TradFi) 의 2020년 SolarWinds 공격이나 암호화폐 업계의 2016년 DAO 해킹에 비견되는 Web3의 "공급망 보안의 순간" 입니다. 이는 근본적인 진실을 드러냅니다. 블록체인 인프라가 더 강력해지고 자동화됨에 따라 공격 표면은 기하급수적으로 확대된다는 점입니다.

업계의 대응은 AI 에이전트가 Web3 기능의 안전한 관문이 될지, 아니면 이 분야에서 본 적 없는 가장 큰 취약점이 될지를 결정할 것입니다. 위임 서명 모델, 에이전트 허용 한도, MPC 솔루션, 계정 추상화 사이의 선택은 단순한 기술적 선택이 아니라 생존의 문제입니다.

Web3 빌더가 지금 해야 할 일​

Web3 분야에서 AI 에이전트를 통합하고 있거나 계획 중이라면, 다음 체크리스트를 확인하십시오:

1. MCP 서버 보안 감사: AI 에이전트 액세스에 개인 키를 요구하고 있다면, ClawHavoc 스타일의 공격 벡터를 생성하고 있는 것입니다.
2. 위임 서명 구현: AI가 트랜잭션을 준비하더라도 트랜잭션 서명에 대한 독점적 권한은 항상 사용자가 보유해야 합니다.
3. 자율 에이전트를 위한 허용 한도 기반 모델 사용: 에이전트가 독립적으로 행동해야 하는 경우, 엄격한 지출 제한이 있는 전용 키를 부여하십시오.
4. 기본 네트워크 설정으로 AI 에이전트를 설치하지 마십시오: 기업 수준의 인증이 없는 한 항상 로컬 호스트 (127.0.0.1) 에 바인딩하십시오.
5. AI 에이전트 마켓플레이스를 앱 스토어처럼 취급하십시오: 제3자 기술 (skills) 을 신뢰하기 전에 코드 서명, 보안 감사 및 평판 시스템을 요구하십시오.
6. 사용자에게 AI 에이전트 위험 교육: 대부분의 암호화폐 사용자는 AI 에이전트에게 권한을 주는 것이 누군가에게 컴퓨터의 루트 권한을 주는 것과 기능적으로 동일하다는 점을 이해하지 못합니다.

OpenClaw 위기는 기능보다 기본 보안 (security-by-default) 이 더 중요하다는 교훈을 주었습니다. AI 에이전트를 배포하려는 속도가 보안을 확보하려는 속도를 앞질러서는 안 됩니다.

AI 에이전트와 연결되는 블록체인 인프라를 구축하고 계신가요? BlockEden.xyz는 고위험 통합을 위해 설계된 보안 우선 아키텍처를 바탕으로 40개 이상의 블록체인에 기업용 API 인프라를 제공합니다. 서비스 둘러보기 를 통해 지속 가능한 기반 위에서 빌드해 보세요.

---

출처:

• Meet OpenClaw: 모든 기록을 경신하고 보안 패닉을 일으킨 AI 어시스턴트
• OpenClaw: GitHub에서 가장 빠르게 성장한 스타가 2026년 첫 주요 AI 보안 재앙이 된 이유
• 새로운 OpenClaw AI 에이전트 사용 부적합 판명 | Kaspersky 공식 블로그
• OpenClaw 보안: 노출된 AI 에이전트의 위험성 설명 | Bitsight
• ClawJacked: 에이전트 전체 탈취를 가능하게 하는 OpenClaw 취약점
• 연구원들, OpenClaw 사용자 데이터를 훔치는 341개의 악성 ClawHub 스킬 발견
• Atomic MacOS Stealer 배포에 사용된 악성 OpenClaw 스킬 | Trend Micro
• ClawHavoc, 1,184개의 악성 스킬로 OpenClaw의 ClawHub 오염
• Web3에서 MCP 사용하기: 블록체인 상호작용 에이전트 보안 방법 | Google Cloud 블로그
• 2026년 AI 기반 Web3 암호화폐 지갑 구축 방법
• 모델 컨텍스트 프로토콜 (MCP): 스마트한 크립토 프로젝트를 위한 AI와 블록체인의 가교
• 중국 테크 거인들, OpenClaw AI 게이트웨이 채택 경쟁
• 중국의 AI 홍바오 전쟁: 바이트댄스, 텐센트, 알리바바, 바이두의 기본 게이트웨이 쟁탈전
• NVIDIA, 새로운 오픈 소스 NemoClaw 플랫폼으로 기업용 AI 에이전트 공략
• NVIDIA, 기업용 AI 에이전트 구동을 위한 NemoClaw 준비
• NVIDIA, GTC 2026에서 오픈 소스 AI 에이전트 "NemoClaw" 출시 예정: 현재까지 알려진 내용

커피 한 잔 가격보다 저렴한 1.22달러로 이제 AI 에이전트가 스마트 컨트랙트를 스캔하고, 취약점을 식별하며, 작동 가능한 익스플로잇을 생성할 수 있습니다. 이는 보안 백서에 나오는 이론적인 시나리오가 아닙니다. Anthropic과 MATS Fellows 연구원들이 2025년 말에 발표한, 실제 스마트 컨트랙트 공격 능력을 평가하는 최초의 벤치마크인 SCONE-bench의 측정 결과입니다. 2020년부터 2025년 사이 실제로 익스플로잇된 405개의 컨트랙트를 대상으로 한 테스트에서, 10개의 프런티어 AI 모델은 총 207개에 대해 즉각 실행 가능한 익스플로잇을 생성했으며, 시뮬레이션 결과 5억 5,010만 달러의 도난 자금이 발생했습니다.

그 영향은 연구실을 훨씬 뛰어넘습니다. 디파이(DeFi) 프로토콜은 총 1,000억 달러 이상의 총 예치 자산(TVL)을 보유하고 있습니다. Anthropic의 데이터가 보여주는 궤적처럼 익스플로잇 능력이 1.3개월마다 두 배씩 계속 증가한다면, 온체인 금융을 뒷받침하는 보안 가정이 변곡점에 도달하고 있는 것입니다.

이제 컨트랙트당 1.22달러의 비용으로 AI 에이전트가 스마트 컨트랙트의 악용 가능한 취약점을 스캔할 수 있으며, 공격용 익스플로잇 능력은 1.3개월마다 두 배로 증가하고 있습니다. 탈중앙화 금융(DeFi)에서 가장 중대한 군비 경쟁에 오신 것을 환영합니다.

2026년 2월, OpenAI와 Paradigm은 AI 에이전트가 스마트 컨트랙트 취약점을 얼마나 효과적으로 탐지, 패치 및 익스플로잇하는지 평가하는 오픈 소스 벤치마크인 EVMbench를 공동 출시했습니다. 결과는 충격적이었습니다. GPT-5.3-Codex는 알려진 취약한 컨트랙트의 72.2%를 성공적으로 익스플로잇했으며, 이는 불과 6개월 전의 31.9%에서 크게 상승한 수치입니다. 한편, 특화된 AI 보안 에이전트는 9,680만 달러 규모의 90개 DeFi 익스플로잇 사례 중 92%에서 취약점을 탐지해냈는데, 이는 기본 GPT-5.1 코딩 에이전트의 탐지율인 34%보다 거의 3배나 높은 수치입니다.

그 시사점은 분명합니다. DeFi 보안을 위한 싸움은 AI 대 AI의 대결이 되었으며, 현재로서는 경제학적으로 공격자에게 압도적으로 유리합니다.

공격자가 8 USDC를 담보로 예치하고 약 390,000 달러에 달하는 187 ETH를 챙겨 떠났습니다. 스마트 컨트랙트는 설계된 대로 정확하게 작동했습니다. 오라클도 제 역할을 다했습니다. 하지만 누군가 USDC 자리에 BTC / USD 체인링크(Chainlink) 가격 피드를 연결했습니다. 이 단 한 줄의 설정 오류가 정상적인 대출 프로토콜을 공짜 돈 인출기로 바꾸어 놓았습니다.

가장 치명적인 취약점이 솔리디티(Solidity) 바이트코드가 아닌 관리자 대시보드, 배포 스크립트, 그리고 파라미터 파일에 숨어 있는 DeFi 보안의 새로운 전선에 오신 것을 환영합니다.

2025년, 대부분의 공격받은 프로토콜이 감사를 받았음에도 불구하고 (일부는 여러 번), DeFi는 스마트 컨트랙트 취약점으로 인해 33억 달러의 손실을 입었습니다. 2월의 15억 달러 규모 Bybit 침해, 4200만 달러 규모의 GMX 익스플로잇, 그리고 수많은 재진입 공격은 불편한 진실을 증명했습니다. 바로 전통적인 보안 감사는 필요하지만 충분하지 않다는 것입니다. 수학적 정밀도가 중요할 때, 예외 사례 (edge cases)를 테스트하는 것만으로는 부족합니다. 그것들을 증명해야 합니다.

이것이 Sui Prover의 오픈 소스 전환이 단순한 GitHub 릴리스 그 이상의 의미를 갖는 이유입니다. Asymptotic에 의해 개발되어 이제 Sui 개발자 커뮤니티에 무료로 제공되는 Sui Prover는 항공 제어 시스템과 프로세서 설계가 실패하지 않도록 보장하는 것과 동일한 수학적 기법인 형식 검증 (formal verification)을 일상적인 스마트 컨트랙트 개발에 도입합니다. 단 하나의 간과된 예외 사례가 수억 달러를 유출시킬 수 있는 환경에서, 코드가 올바르게 작동함을 수학적으로 증명하는 능력은 더 이상 사치가 아닙니다. 그것은 필수 요소가 되고 있습니다.

2025년 2월 21일, 북한 해커들이 두바이 기반 거래소 바이비트(Bybit)에서 약 30분 만에 15억 달러 상당의 암호화폐를 탈취했습니다. 이는 단순히 역사상 최대 규모의 암호화폐 해킹 사건에 그치지 않습니다. 바이비트가 은행이었다면 기네스 세계 기록에 등재된 역대 최대 규모의 은행 강도 사건으로 기록되었을 것입니다.

이번 공격은 스마트 컨트랙트의 버그를 악용하거나 프라이빗 키를 무차별 대입(brute-force)한 것이 아니었습니다. 대신 해커들은 제3자 지갑 제공업체의 개발자 노트북 한 대를 해킹한 후 몇 주 동안 인내심을 갖고 기다렸고, 바이비트 직원이 일반적인 내부 이체처럼 보이는 거래를 승인하는 순간을 노려 공격을 감행했습니다. 무언가 잘못되었다는 사실을 깨달았을 때는 이미 500,000 ETH가 북한 라자루스 그룹(Lazarus Group)이 관리하는 복잡한 지갑 네트워크 속으로 사라진 뒤였습니다.

다음은 이 사건이 어떻게 발생했는지, 왜 중요한지, 그리고 2025년 현재 암호화폐 보안의 실태에 대해 무엇을 시사하는지에 대한 이야기입니다.

공격: 인내와 정밀함의 정수​

바이비트 해킹은 단순한 강도 사건이 아니었습니다. 몇 주에 걸쳐 전개된 정밀한 작전이었습니다.

1단계: 개발자 포섭​

2025년 2월 4일, 바이비트가 고액 이체 보안을 위해 사용하던 널리 알려진 멀티시그(multi-signature) 지갑 플랫폼 Safe{Wallet}의 한 개발자가 "MC-Based-Stock-Invest-Simulator-main"이라는 합법적인 Docker 프로젝트처럼 보이는 파일을 다운로드했습니다. 이 파일은 채용 제안이나 투자 도구로 위장한 사회 공학적 공격(social engineering attack)을 통해 전달되었을 가능성이 높습니다.

악성 Docker 컨테이너는 즉시 공격자가 제어하는 서버와 연결을 설정했습니다. 그곳에서 해커들은 개발자의 워크스테이션으로부터 Safe{Wallet}의 클라우드 인프라에 접근할 수 있는 임시 자격 증명인 AWS 세션 토큰을 추출했습니다.

이 토큰들을 사용해 공격자들은 다요소 인증(MFA)을 완전히 우회했습니다. 이제 그들은 Safe{Wallet}의 핵심 시스템에 접근할 수 있는 열쇠를 손에 넣었습니다.

2단계: 잠복 코드​

공격자들은 즉시 행동에 나서는 대신 Safe{Wallet}의 웹 인터페이스에 교묘한 자바스크립트(JavaScript) 코드를 삽입했습니다. 이 코드는 바이비트만을 위해 특별히 설계되었으며, 바이비트 직원이 Safe 계정을 열고 거래를 승인하려는 것을 감지할 때까지 잠복 상태를 유지했습니다.

여기서 주목할 점은 정교함입니다. 전체 Safe{Wallet} 애플리케이션은 다른 모든 사용자에게는 정상적으로 작동했습니다. 오직 바이비트만이 표적이 되었습니다.

3단계: 거액 탈취​

2025년 2월 21일, 바이비트 직원들은 콜드 월렛(보안된 오프라인 저장소)에서 웜 월렛(활성 거래용)으로 통상적인 이체를 시작했습니다. 이를 위해서는 권한이 있는 인원들의 여러 서명이 필요한데, 이는 멀티시그라고 불리는 표준 보안 절차입니다.

서명자들이 거래를 승인하기 위해 Safe{Wallet}을 열었을 때, 인터페이스에는 올바른 목적지 주소가 표시되었습니다. 하지만 악성 코드는 이미 내부 명령을 다른 것으로 바꿔치기한 상태였습니다. 직원들은 자신도 모르게 바이비트의 콜드 월렛 전체를 비우는 거래를 승인하게 되었습니다.

불과 몇 분 만에 약 15억 달러 상당의 500,000 ETH가 공격자들이 관리하는 주소로 흘러 들어갔습니다.

기술적 취약점 악용: Delegatecall​

핵심 취약점은 이더리움의 delegatecall 함수였습니다. 이 함수는 스마트 컨트랙트가 자신의 저장소 컨텍스트 내에서 다른 컨트랙트의 코드를 실행할 수 있게 합니다. 공격자들은 바이비트의 서명자들을 속여 지갑의 컨트랙트 로직을 악성 버전으로 변경하게 만들었고, 결과적으로 해커들에게 전권을 부여하게 되었습니다.

이것은 이더리움 자체나 Safe{Wallet}의 핵심 프로토콜에 있는 버그가 아니었습니다. 신뢰받는 직원이 거래를 확인하고 승인하는 순간인 '인적 계층(human layer)'에 대한 공격이었습니다.

북한 라자루스 그룹: 세계에서 가장 많은 수익을 올리는 해커들​

공격 후 24시간 이내에 블록체인 조사관 ZachXBT는 이번 해킹이 북한의 라자루스 그룹과 확실히 연결되어 있다는 증거를 Arkham Intelligence에 제출했습니다. FBI는 2025년 2월 26일에 이 사실을 공식 확인했습니다.

TraderTraitor 및 APT38로도 알려진 라자루스 그룹은 북한 정찰총국 산하에서 활동합니다. 이들은 개인적인 부를 축적하려는 범죄 조직이 아닙니다. 이들의 수익금은 북한의 핵무기 및 탄도 미사일 프로그램의 자금으로 사용되는 국가 차원의 작전 부대입니다.

수치는 놀라운 수준입니다:

• 2025년 한 해만: 북한 해커들이 탈취한 암호화폐는 20억 2,000만 달러에 달함
• 바이비트 비중: 15억 달러 (2025년 북한이 단일 공격으로 벌어들인 수익의 74%)
• 2017년 이후: 북한은 67억 5,000만 달러 이상의 암호화폐 자산을 탈취함
• 2024년 대비 2025년: 탈취 자산 가치 51% 증가

북한은 2025년 전 세계에서 도난당한 모든 암호화폐의 59%, 전체 거래소 해킹 사건의 76%를 차지했습니다. 다른 어떤 위협 행위자도 이 수치에 근접하지 못합니다.

암호화폐 절도의 산업화​

북한이 다른 점은 단순히 규모뿐만이 아닙니다. 그들의 작전은 매우 정교합니다.

기술적 취약점보다 사회 공학적 기법 우선​

2025년 주요 해킹 사건의 대부분은 기술적 취약점이 아닌 사회 공학적 기법을 통해 자행되었습니다. 이는 근본적인 변화를 의미합니다. 해커들은 더 이상 스마트 컨트랙트의 버그나 암호학적 약점만을 찾지 않습니다. 그들은 사람을 노립니다.

라자루스 그룹 요원들은 암호화폐 기업 내부에 IT 직원으로 위장 취업하기도 했습니다. 임원을 사칭하거나 개발자들에게 악성코드가 포함된 채용 제안을 보내기도 했습니다. 바이비트 공격은 개발자가 가짜 주식 거래 시뮬레이터를 다운로드하는 것에서 시작되었으며, 이는 전형적인 사회 공학적 공격 경로입니다.

중국의 돈세탁 조직 (The Chinese Laundromat)​

암호화폐를 훔치는 것은 도전의 절반에 불과합니다. 발각되지 않고 이를 사용할 수 있는 자금으로 전환하는 과정 또한 그만큼 복잡합니다.

북한은 직접 현금화하는 대신, 조사관들이 "중국의 돈세탁 조직(Chinese Laundromat)"이라 부르는 조직에 돈세탁을 외주화했습니다. 이들은 지하 뱅커, OTC(장외거래) 브로커, 무역 기반 세탁 중개인들로 구성된 광범위한 네트워크입니다. 이들은 여러 체인, 관할권 및 결제망을 가로질러 도난당한 자산을 세탁합니다.

Bybit 해킹 발생 후 한 달도 채 되지 않은 2025년 3월 20일, CEO 벤 저우(Ben Zhou)는 해커들이 이미 여러 중간 지갑, 탈중앙화 거래소(DEX) 및 크로스체인 브리지를 통해 도난당한 ETH 의 86.29% 를 비트코인(Bitcoin)으로 전환했다고 보고했습니다. 대규모 탈취 이후 45일간 이어지는 세탁 주기는 이제 예측 가능한 패턴이 되었습니다.

이러한 노력에도 불구하고, 저우는 도난당한 자산의 88.87% 가 추적 가능하다고 언급했습니다. 하지만 "추적 가능"이 곧 "회수 가능"을 의미하지는 않습니다. 자금은 미국이나 국제 법 집행 기관과 협력 관계가 없는 관할권으로 흘러 들어갑니다.

Bybit의 대응: 위기 속의 위기 관리​

침해 사실을 발견한 지 30분 만에 CEO 벤 저우는 지휘권을 잡고 X (구 트위터)를 통해 실시간 업데이트를 제공하기 시작했습니다. 그의 메시지는 직설적이었습니다. "이 해킹 피해가 복구되지 않더라도 Bybit 은 지급 능력이 있으며 (Solvent), 모든 고객 자산은 1 : 1 로 담보되어 있으므로 우리가 손실을 감당할 수 있습니다."

거래소는 12시간 이내에 35만 건 이상의 출금 요청을 처리했습니다. 이는 치명적인 손실에도 불구하고 운영이 정상적으로 계속될 것이라는 신호를 사용자들에게 보낸 것입니다.

긴급 자금 조달​

72시간 이내에 Bybit 은 Galaxy Digital, FalconX, Wintermute를 포함한 파트너들로부터 긴급 자금을 확보하여 447,000 ETH 를 보충했습니다. Bitget 은 출금이 중단 없이 이어질 수 있도록 40,000 ETH 를 대여해 주었으며, Bybit 은 이를 3일 이내에 상환했습니다.

사이버 보안 기업 해큰 (Hacken)은 Bybit 의 주요 자산이 100% 이상의 담보로 뒷받침되고 있음을 확인하는 보유 자산 증명 (PoR) 감사를 실시했습니다. 이러한 투명성은 이 정도 규모의 위기 상황에서 전례 없는 일이었습니다.

바운티 프로그램 (The Bounty Program)​

저우는 "라자루스와의 전쟁"을 선포하고, 동결된 자산으로 이어지는 정보에 대해 최대 10% 의 보상을 제공하는 글로벌 바운티 프로그램을 시작했습니다. 연말까지 Bybit 은 자금 추적이나 회수를 도운 기여자들에게 218만 달러 상당의 USDT 를 지급했습니다.

시장의 판결​

2025년 말까지 Bybit 은 전 세계 사용자 8,000만 명을 돌파했고, 일일 거래대금 71억 달러를 기록하며 암호화폐 현물 거래소 중 5위를 차지했습니다. 이들의 위기 대응은 치명적인 해킹에서 살아남는 방법에 대한 사례 연구 (Case Study)가 되었습니다.

2025년: 암호화폐 도난액이 34억 달러에 달한 해​

Bybit 해킹이 헤드라인을 장식했지만, 이는 더 큰 패턴의 일부였습니다. 2025년 전체 암호화폐 도난액은 34억 달러에 달하며 새로운 기록을 세웠고, 3년 연속 증가세를 보였습니다.

주요 통계:

• 2023년: 20억 달러 도난
• 2024년: 22억 달러 도난
• 2025년: 34억 달러 도난

전체 암호화폐 도난에서 북한이 차지하는 비중은 약 절반에서 거의 60% 로 늘어났습니다. 북한 (DPRK)은 더 적은 사건으로 더 큰 규모의 탈취를 달성하며 점차 효율성과 정교함이 증가하고 있음을 입증했습니다.

교훈: 보안이 실패한 지점​

Bybit 해킹은 단일 거래소를 넘어선 치명적인 취약점들을 노출했습니다.

제3자 리스크는 실존적 위협이다​

Bybit 자체의 보안 실패가 아니었습니다. Safe{Wallet} 의 문제였습니다. 하지만 그 결과는 Bybit 이 짊어져야 했습니다.

암호화폐 산업은 거래소가 지갑 제공업체에 의존하고, 지갑 제공업체는 클라우드 인프라에 의존하며, 클라우드 인프라는 개별 개발자의 워크스테이션에 의존하는 복잡한 종속성 체인을 구축해 왔습니다. 이 체인의 어느 한 곳이라도 침해되면 치명적인 연쇄 반응을 일으킬 수 있습니다.

콜드 스토리지만으로는 충분하지 않다​

업계는 오랫동안 콜드 월렛을 보안의 황금 표준으로 여겨왔습니다. 하지만 Bybit 의 자금은 도난당할 당시 콜드 스토리지에 있었습니다. 취약점은 자금을 이동시키는 과정, 즉 멀티시그 (Multisig)가 보호하도록 설계된 '인간의 승인 단계'에 있었습니다.

이체가 일상화되면 서명자들은 승인을 비판적인 보안 결정이 아닌 형식적인 절차로 취급하며 거짓 보안 실감에 빠지게 됩니다. Bybit 공격은 바로 이러한 행동 패턴을 악용했습니다.

UI는 단일 장애점 (SPOF)이다​

멀티시그 보안은 서명자가 자신이 승인하는 내용을 확인할 수 있다는 점을 전제로 합니다. 하지만 트랜잭션 세부 정보를 표시하는 인터페이스가 침해되면 확인은 무의미해집니다. 공격자들은 서명자들에게는 한 가지를 보여주면서 실제로는 다른 명령을 실행했습니다.

직원들이 승인 전 트랜잭션의 실제 목적지를 미리 볼 수 있게 하는 '서명 전 시뮬레이션 (Pre-signing simulations)'이 있었다면 이 공격을 방지할 수 있었을 것입니다. 대규모 출금에 대한 지연 시간을 두어 추가 검토 시간을 확보하는 것도 방법이 될 수 있었습니다.

사회 공학적 기법은 기술적 보안을 능가한다​

세계에서 가장 정교한 암호화 보안을 갖추고 있더라도, 단 한 명의 직원이 잘못된 파일을 다운로드하는 것만으로 모든 보안을 우회할 수 있습니다. 암호화폐 보안의 취약점은 점차 기술적인 문제가 아닌 인간의 문제가 되고 있습니다.

규제 및 업계에 미치는 영향​

Bybit 해킹은 이미 규제 환경을 재편하고 있습니다.

다음과 같은 항목들에 대한 의무 요구 사항이 예상됩니다:

• 키 관리를 위한 하드웨어 보안 모듈 (HSM) 도입
• 실시간 트랜잭션 모니터링 및 이상 징후 탐지
• 정기적인 제3자 보안 감사
• 강화된 AML 프레임워크 및 대규모 이체에 대한 트랜잭션 지연

보안과 컴플라이언스는 이제 시장 진입을 위한 필수 조건이 되고 있습니다. 강력한 키 관리, 권한 설계 및 신뢰할 수 있는 보안 프레임워크를 입증하지 못하는 프로젝트는 뱅킹 파트너 및 기관 사용자로부터 고립될 것입니다.

업계에 시사하는 점​

바이비트 (Bybit) 해킹은 불편한 진실을 드러냅니다. 암호화폐의 보안 모델은 가장 취약한 운영 링크만큼만 강력할 뿐이라는 점입니다.

업계는 영지식 증명 (zero-knowledge proofs), 임계값 서명 (threshold signatures), 보안 인클레이브 (secure enclaves) 와 같은 암호학적 보안에 막대한 투자를 해왔습니다. 하지만 공격자가 사람을 속여 악성 트랜잭션을 승인하게 만들 수 있다면, 아무리 정교한 암호화 기술도 무용지물입니다.

거래소들에게 주는 메시지는 분명합니다. 보안 혁신은 기술을 넘어 운영 프로세스, 제3자 위험 관리, 지속적인 직원 교육까지 확장되어야 합니다. 정기적인 감사, 협력적인 위협 인텔리전스 공유, 사고 대응 계획 수립은 더 이상 선택 사항이 아닙니다.

사용자들에게 주는 교훈 또한 냉혹합니다. 가장 정교한 보안 시스템을 갖춘 최대 규모의 거래소라도 침해될 수 있다는 것입니다. 셀프 커스터디 (Self-custody), 하드웨어 월렛, 분산된 자산 보관은 다소 불편하더라도 여전히 가장 안전한 장기 전략입니다.

결론​

북한의 라자루스 그룹 (Lazarus Group) 은 암호화폐 절도를 산업화했습니다. 이들은 2017년 이후 67억 5천만 달러 이상을 탈취했으며, 2025년은 그들에게 역대 최고의 성과를 거둔 해로 기록되었습니다. 단 한 번의 작전으로 15억 달러를 탈취한 바이비트 해킹은 어떤 정보 기관도 부러워할 만한 능력을 보여줍니다.

암호화폐 업계는 무한한 인내심과 정교한 기술력을 갖추고 결과에 대한 두려움이 없는 국가 지원 해커들과 군비 경쟁을 벌이고 있습니다. 바이비트 공격이 성공한 이유는 새로운 익스플로잇 덕분이 아니라, 공격자들이 코드가 아닌 사람이 가장 취약한 고리라는 점을 이해했기 때문입니다.

업계가 암호학적 보안에 적용하는 것과 동일한 엄격함으로 운영 보안을 다루지 않는 한, 이러한 공격은 계속될 것입니다. 문제는 또 다른 10억 달러 규모의 해킹이 발생할지 여부가 아니라, 언제 발생할 것인가, 그리고 대상이 바이비트만큼 효과적으로 대응할 수 있는가 하는 점입니다.

---

본 기사는 교육적인 목적으로만 제공되며 재무적 조언으로 간주되어서는 안 됩니다. 암호화폐 거래소 및 지갑을 사용할 때는 항상 스스로 조사하고 보안을 최우선으로 하십시오.

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

형식 검증은 수학적 및 논리 기반 기술을 사용하여 스마트 계약의 정확성과 보안을 증명하는 것을 의미합니다. 실제로 이는 속성 기반 퍼즈 테스트와 심볼릭 실행부터 엄격한 정리 증명 및 모델 체킹에 이르기까지 다양한 방법론을 포함합니다. 목표는 계약이 명세를 충족하고 모든 가능한 입력과 상태에 걸쳐 악용 가능한 버그가 없음을 보장하는 것입니다. 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)

수년간 블록체인 분야에서 일반적인 상식은 “클수록 좋다”는 것이었습니다. 이더리움 글로벌 네트워크(EGN)는 이더리움 메인넷부터 수많은 다른 프로젝트에 이르기까지 수천 개의 서비스를 지원하는 방대한 피어‑투‑피어(P2P) 레이어로, 바로 이 생각에 기반해 구축되었습니다[cite: 4, 25]. 이론은 간단했습니다: 모두가 같은 공간을 공유하는 거대하고 혼합된 네트워크가 노드 탐색을 촉진하고 생태계를 공격에 더 탄력적으로 만든다는 것이었습니다[cite: 34, 35].

하지만 “A Place for Everyone vs Everyone in its Place: Measuring and Attacking the Ethereum Global Network”라는 중요한 연구 논문은 이 근본적인 믿음에 도전합니다. 연구 결과는 “모두를 위한 장소” 아키텍처가 강점이 아니라 심각한 비효율성과 위험한 보안 취약성을 초래하며, 총 시장 가치가 5천억 달러가 넘는 서비스에 영향을 미칠 수 있음을 보여줍니다[cite: 6, 24].

효율성 악몽: 군중 속에 외치기​

EGN의 약속은 노드가 동일한 서비스를 제공하는 피어를 쉽게 찾고 연결할 수 있다는 것이었습니다[cite: 34]. 현실은 정반대였습니다. 연구에 따르면 노드들은 방대한 EGN의 소음 속에서 동료를 찾기 위해 필사적으로 고군분투하고 있습니다[cite: 8].

비효율성은 충격적입니다:

• 낭비된 연결: 노드의 연결 시도 중 75% 이상이 전혀 다른 서비스의 피어에게 향합니다[cite: 8].
• 극단적인 연결 비용: 놀라운 사례에서, 한 노드는 단 하나의 유효한 이웃을 찾기 위해 평균 45,908번의 연결 시도를 해야 했습니다[cite: 9]. 이는 비트코인의 성공률이 4분의 1이라는 추정치와 크게 대조됩니다[cite: 54].
• 뒤로 물러나는 한 걸음: 개선을 목표로 만든 최신 탐색 프로토콜 Discv5는 오히려 더 나쁜 성능을 보였습니다. 12시간 테스트에서 Discv5를 사용한 노드들은 세 개 이하의 연결만을 수립했으며, 이는 서비스 광고를 위한 핵심 “주제 탐색 메커니즘”이 모든 주요 클라이언트에서 구현되지 않았기 때문입니다[cite: 57, 59].

핵심 문제는 EGN의 대부분 노드가 라우팅 테이블(‘주소록’)에 관련 없는 피어들로 가득 차 있다는 점입니다. 연구에 따르면 대부분의 Discv4 노드는 DHT(분산 해시 테이블)에서 동일 서비스 피어를 5% 미만만 유지하고 있습니다[cite: 44].

보안 환상: 취약한 거인​

“클수록 안전하다”는 논리의 두 번째 기둥은 보안이었습니다— EGN의 거대한 규모가 공격자의 영향력을 희석시킬 것이라는 주장[cite: 35]. 논문은 악성 노드가 네트워크 주소록을 자체 엔트리로 가득 채우는 DHT 오염 공격을 시뮬레이션함으로써 이 가정을 무너뜨립니다[cite: 61, 62].

결과는 EGN의 혼합 특성이 방어가 아니라 치명적인 취약점임을 보여줍니다[cite: 10, 65]:

• 압도적으로 효과적: 전체 네트워크의 0.3% 미만에 해당하는 300개의 악성 노드만으로도 대부분 서비스의 연결 성공률을 1% 이하로 떨어뜨릴 수 있습니다[cite: 11, 63].
• 대규모 격리: 24시간 만에 이 소규모 공격은 네트워크를 성공적으로 분할시켜 수천 개의 정직한 노드가 자신의 서비스를 이용하지 못하도록 만들었습니다[cite: 11, 64].
• 설계상의 문제: 이 취약점은 버그가 아니라 혼합 아키텍처의 내재된 결과입니다[cite: 65]. 동일한 공격을 서비스별로 분리된 전용 네트워크에 적용했을 때는 라우팅 테이블이 깨끗하고 관련 피어만 포함하고 있어 “대체로 효과가 없었다”는 결과가 나왔습니다[cite: 66].

앞으로의 길: “제자리에 있는 모두”​

연구는 EGN의 혼합 아키텍처가 특히 비효율적이고 불안정한 환경에서 작은 서비스들을 부수적으로 피해를 입히는 구조라고 결론짓습니다[cite: 37]. 해결책은 글로벌 네트워크를 포기하는 것이 아니라, “모두를 위한 장소”에서 “모두가 제자리에 있는” 구조로 전환하는 것입니다[cite: 522].

논문이 제시하는 두 가지 핵심 해결책:

1. 서비스별 DHT: 모든 노드가 자신의 서비스 정보를 Ethereum Node Record(ENR)에 직접 포함하도록 의무화합니다[cite: 490, 491]. 이 간단한 변경만으로도 노드가 동일 서비스 피어를 필터링하고 우선순위를 두게 되어, 탈중앙성을 해치지 않으면서도 탐색 효율성과 보안을 크게 향상시킬 수 있습니다[cite: 495].
2. 보다 신뢰할 수 있는 부트노드: 시뮬레이션은 부트노드가 네트워크 분할에 대한 최후 방어선 역할을 한다는 점을 강조했습니다[cite: 496]. 논문은 각 서비스가 부트노드 수를 늘리고, 동일 서비스 피어를 저장하도록 구성해 네트워크 복구를 위한 탄탄한 백본을 구축할 것을 권고합니다[cite: 499].

개발자와 전체 생태계의 건강을 위해, 이 발견은 중요한 경각심을 일깨워 줍니다. 견고하고 효율적인 P2P 레이어는 모든 탈중앙화 서비스의 기반입니다. 제안된 수정 사항을 구현함으로써, 커뮤니티는 모두에게 작동하는 보다 조직적이고 안전하며 진정한 글로벌 네트워크를 향해 나아갈 수 있습니다.