길리랩blog

스마트 컨트랙트 신뢰성을 높이는 감사·형식 검증·퍼징

스마트 컨트랙트 감사, 형식 검증, 퍼징을 하나의 검증 파이프라인으로 묶어 배포 게이트와 운영 리스크를 관리하는 방법을 다룬다.

2026-08-14 · 최초 발행 2025-10-31

배포 전 검증은 서로 다른 맹점을 다뤄야 한다

퍼블릭·엔터프라이즈 블록체인에서 스마트 컨트랙트의 무결성은 Test & Verification 파이프라인에 달려 있다. 코드 리뷰만으로는 경제적 인센티브와 상태 전이를 충분히 다루기 어렵고, 자동 테스트만으로는 명세 자체의 누락을 보장할 수 없다.

감사(Audit), 형식 검증(Formal Verification), 퍼징(Fuzzing)은 역할이 다르다. 함께 운영할 때 보안 취약점, 경제적 설계 문제, 런타임 오류와 회귀 결함을 각기 다른 방식으로 확인할 수 있다.

감사가 확인하는 범위

감사는 수동 코드 리뷰에 자동 정적·동적 분석을 결합해 결함을 찾는 활동이다. 보안 취약점뿐 아니라 경제적 인센티브의 취약성, 설계상 불변식 위반도 대상에 들어간다.

검토 범위에는 명세와의 일치 여부, ERC·EIP 같은 업계 표준 준수, 권한 체계와 업그레이드 경로가 포함된다.

형식 검증이 다루는 속성

형식 검증은 불변식과 전역 속성을 논리식으로 모델링한 뒤 모델 체커, SMT, 도메인 전용 프로버로 증명하거나 반예시를 찾는 방법이다. 재진입 방지, 보유 자산 보전, 권한 제약, 금액 보존 같은 안전 속성을 수학적으로 보장하는 데 쓰인다.

퍼징이 찾는 실행 경로

퍼징은 자동 생성한 입력으로 경계값과 에지 케이스를 대량 탐색해 런타임 오류와 논리 취약점을 발견한다. 커버리지 지향·속성 지향 퍼징을 CI에서 상시 실행하면 회귀 결함을 일찍 찾을 수 있다.

명세부터 배포 게이트까지 연결하는 방법

검증은 도구를 나열하는 일보다, 어떤 속성을 배포 판단에 사용할지 결정하는 일에 가깝다. 시스템 요구사항은 상태 불변식, 전이 규칙, 권한 매트릭스로 정식화하고 코드 주석·애노테이션을 바탕으로 속성을 추출할 수 있다. 우선순위는 자산 보전, 접근 제어, 수수료·슬리피지 경계, 가스 상한 순으로 둘 수 있다.

도구 체인은 정적·심볼릭 분석에 Slither, Mythril, Manticore, Solc SMTChecker를 사용하고, 퍼징·테스트에는 Echidna, Foundry(forge fuzz), Hardhat, Tenderly를 둘 수 있다. 형식 검증 영역에는 Certora Prover, Securify, KEVM/K, VerX, Move Prover가 있다.

테스트 오라클은 가격 조작, MEV, 리밸런싱처럼 경제적 시나리오를 판정할 수 있어야 한다. 이벤트와 상태 다이제스트로 판정을 자동화하고, 시드 트랜잭션과 에이전트 기반 멀티액터 상호작용 케이스도 확보한다. 브랜치마다 정적 분석, 단위·퍼징, 형식 검증의 요약 리포트를 만들고 커버리지·증명 성공률·취약점 임계치로 배포를 게이팅한다. 아티팩트 보존과 변경 영향 분석도 자동화 대상이다.

⤢✕예예예아니오아니오아니오예아니오요구사항/명세불변식·권한·경제 모델정적/심볼릭 분석Slither/Mythril/SMTChecker테스트/퍼징Foundry Fuzz/Echidna형식 검증Certora/KEVM이슈 발견?속성 위반?증명 실패/반예시?치명도 분류SWC/CWE 매핑수정 패치커버리지/증명 요약배포 게이트 통과?테스트넷→메인넷 배포

문제가 확인되면 CWE/SWC에 매핑하고 Critical/High/Medium/Low 심각도를 부여한다. 재현 절차와 PoC를 남긴 뒤 패치를 검증하고 재감사하는 루프를 운영한다.

검증 기법은 운영 특성이 다르다

접근법 성능(속도/스루풋) 확장성(대형 코드베이스) 일관성(결과 재현) 안정성(오탐/미탐) 운영 편의
감사(Audit) 중간, 인력 병목 중간, 팀 스케일 필요 중간, 리뷰어 편차 존재 낮은 오탐, 미탐 위험 중간, 경험 의존
형식 검증 낮음~중간, 계산 비용 큼 낮음, 모델 단순화 필요 높음, 증명/반예시 결정적 매우 낮은 오탐, 미탐 낮음(모델 품질 영향) 낮음, 전문 지식 요구
퍼징 높음, 대량 탐색 가능 높음, 분산 실행 용이 높음, 시드/설정 고정 시 중간, 오라클 품질 의존 높음, CI 통합 용이

감사는 리뷰어의 경험이 결과에 영향을 주지만 낮은 오탐으로 설계와 구현을 함께 살필 수 있다. 형식 검증은 결정적인 증명이나 반예시를 제공하지만 모델 단순화와 전문 지식이 필요하다. 퍼징은 CI 통합과 분산 실행에 유리하지만 테스트 오라클의 품질에 좌우된다.

계약 유형별로 검증 대상을 좁힌다

DeFi 금고 전략 컨트랙트에서는 총 예치금 보존, 수수료 상한, 관리자 권한을 불변식으로 정한다. Slither로 재진입·정수 오버플로우·권한 분기를 점검하고, Foundry로 단위·퍼징 테스트를 실행한다. Echidna는 속성 지향 퍼징에, Certora는 자산 보전 증명에 사용한다. 커버리지 ≥ 85%, Critical/High 0건, 핵심 불변식 증명이 성공한 경우 배포를 승인한다. 반예시의 재현 트랜잭션은 자동으로 캡처하고, 포크 테스트로 회귀를 검증한 뒤 패치 후 같은 시나리오를 다시 실행한다.

브리지의 록-민트 패턴은 잠금→검증→발행→상환 상태 기계를 모델링하고 리플레이와 중복 처리 방지 속성을 명세화한다. 멀티체인 포크 퍼징에서는 타이밍과 Finality 지연 시나리오를 주입해 서명 검증 실패에 대한 반응을 점검한다. 형식 검증은 금액 보존과 단조성(monotonicity) 속성 증명에 사용한다.

NFT 민팅과 화이트리스트에서는 가격 단계, 총량 상한, 서명 기반 허용목록의 검증 속성이 대상이다. 퍼징으로 시계 조작, 프런트런, 동시 민팅을 스트레스 테스트하고 가스 상한을 확인한다. 감사에서는 로열티와 수익 분배의 정확성, 취약한 권한 경로를 검토한다.

Foundry와 Echidna로 속성을 실행한다

전제조건은 다음과 같다.

  • Solidity 0.8.27, Foundry forge 0.2.x, Node 18+, echidna 2.x
  • EVM 체인 로컬(Anvil) 또는 포크 환경

Foundry에서는 불변식과 퍼즈 테스트를 다음처럼 작성할 수 있다.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.27;

contract Vault {
    mapping(address => uint256) public balance;
    uint256 public total;

    function deposit() external payable {
        balance[msg.sender] += msg.value;
        total += msg.value;
    }

    function withdraw(uint256 amt) external {
        require(balance[msg.sender] >= amt, "insufficient");
        balance[msg.sender] -= amt;
        total -= amt;
        (bool ok, ) = msg.sender.call{value: amt}("");
        require(ok, "xfer");
    }
}

import "forge-std/Test.sol";

contract VaultInvariantTest is Test {
    Vault v;

    function setUp() public {
        v = new Vault();
    }

    // 퍼저가 임의 주소/금액으로 deposit/withdraw 호출
    function invariant_TotalIsSumOfBalances() public {
        // 단순 합산 체크: total은 0 이상이어야 함
        assertGe(v.total(), 0);
    }

    function testFuzz_DepositWithdraw(address user, uint64 amt) public {
        vm.deal(user, amt);
        vm.prank(user);
        v.deposit{value: amt}();
        vm.prank(user);
        v.withdraw(amt);
        assertEq(v.balance(user), 0);
    }
}

실행 명령은 아래와 같다.

  • forge test -vvv
  • 포크 테스트 예: forge test --fork-url $RPC_URL -vv

Echidna에서는 속성 함수가 true를 유지하도록 작성한다.

// echidna: test 함수는 true 유지 필요
contract VaultProp is Vault {
    function echidna_total_nonnegative() public view returns (bool) {
        return total >= 0;
    }
}

실행 명령은 아래와 같다.

  • echidna . --contract VaultProp

실전에서는 재진입 보호(Checks-Effects-Interactions, ReentrancyGuard)와 pull-payment 패턴 적용을 권장한다.

검증 체계를 운영할 때의 선택지

기능 요구사항을 속성으로 명문화한 뒤 개발과 테스트를 병행하면 스펙 중심으로 검증할 수 있다. 다만 초기 비용이 늘고 문서와 코드의 동기화 부담이 생긴다.

감사, 퍼징, 형식 검증을 병렬로 적용하면 기법별 맹점을 보완할 수 있지만, 도구 운영은 복잡해지고 CI 시간도 증가한다. 경제 시뮬레이션, MEV 시나리오, 멀티액터 상호작용을 테스트 데이터와 오라클에 반영해야 하며, 모델을 과도하게 단순화하면 미탐이 생기고 지나치게 복잡하게 만들면 비용이 올라간다.

업그레이더블·프록시 컨트랙트는 UUPS/Transparent Proxy의 스토리지 레이아웃 잠금(Storage layout check)과 권한 이행 테스트까지 포함한다. 이 경우 형식 검증 모델링 난이도와 마이그레이션 리스크가 커진다. 세이프티 스위치, 파우즈블(pausable), 타임락, 멀티시그를 적용하면 운영 통제를 강화할 수 있지만 응답 지연과 운영 복잡성도 감수해야 한다.

파이프라인이 만드는 운영상 효과

사전 발견율은 +30~60%p로 높아지고 치명적 취약점 유출 위험과 메인넷 사고 확률은 대폭 감소한다. 자동 퍼징과 심볼릭 실행을 상시화하면 탐지 시간은 70% 이상 단축되고, 패치 검증 반복 시간은 50% 이상 단축된다.

라인·분기 커버리지는 8090%에 도달할 수 있으며, 핵심 불변식의 증명을 완료하면 회귀 안정성을 확보할 수 있다. 사고 대응·보상·포크 비용을 피하고 감사 재작업은 2040% 절감할 수 있다. 정적 분석으로 불필요한 연산을 제거하면 부수적으로 5~15%의 가스 절감도 가능하다.

초기에는 Foundry+Slither+Echidna 조합으로 자동화 기반을 만들고, 고가치 자산 영역에 Certora·KEVM 등의 형식 검증 단계를 점진적으로 확장하는 방식이 적합하다.

블록체인스마트 컨트랙트형식 검증퍼징보안 감사