대출 프로토콜 개발팀은 모든 코드를 포멀검증 대상으로 삼기보다, 자금 이동·청산·이자 계산처럼 오류가 곧바로 손실로 이어지는 핵심 불변식부터 범위를 정하는 것이 현실적입니다. 범위는 「명세로 정확히 쓸 수 있는 속성인가」, 「검증 도구가 다룰 수 있는 코드 구조인가」, 「업그레이드 뒤에 다시 검증할 수 있는가」의 세 기준으로 좁히고, 나머지 영역은 수동 리뷰·퍼징·단위 테스트로 보완합니다. 이렇게 정한 범위를 견적 요청서에 함께 적어야 여러 감사 업체의 제안을 같은 기준으로 비교할 수 있습니다.
포멀검증은 일반적인 스마트컨트랙트검증과 무엇이 다릅니까?
NIST 알고리즘·자료구조 사전은 포멀검증을 논리를 사용해 하드웨어나 소프트웨어 설계의 속성을 입증하는 것으로 정의합니다. 테스트는 개발자가 고른 입력에서 오류가 나지 않는다는 것을 보여 줄 뿐이지만, 포멀검증은 명세에 적은 속성을 테스트나 비형식적 논증만이 아니라 논리를 사용해 입증한다는 점에서 다릅니다.
현업에서 말하는 스마트컨트랙트검증은 의미가 넓습니다. 블록 탐색기에 소스코드를 공개하고 배포된 바이트코드와 일치하는지 확인하는 절차도 「검증」이라고 부르기 때문에, 견적을 요청할 때는 어떤 검증을 원하는지 구체적으로 적어야 합니다. 대표적인 방법은 다음과 같습니다.
- 수동 코드 리뷰: 감사인이 비즈니스 로직과 권한 구조를 직접 읽고 설계 결함을 찾습니다.
- 정적 분석: 재진입, 검사하지 않은 외부 호출처럼 잘 알려진 패턴을 자동으로 탐지합니다.
- 퍼징·속성 기반 테스트: 무작위 또는 유도된 입력을 대량으로 넣어 불변식이 깨지는 경우를 찾습니다.
- 심볼릭 실행·모델 검사: 입력을 기호로 다뤄 경로 전체를 탐색하고, 속성이 깨지면 반례를 내놓습니다.
- 정리 증명: 증명 보조기를 써서 속성을 단계별로 증명하며, 가장 강한 보증을 주지만 비용도 가장 큽니다.
다만 증명의 강도는 명세의 품질을 넘지 못합니다. 중요한 속성이 명세에서 빠졌다면 검증을 통과해도 취약점이 남을 수 있고, 가격 오라클 조작이나 거버넌스 공격, 시장 유동성 같은 외부 조건은 보통 검증 범위 밖의 「가정」으로 처리됩니다.
대출 프로토콜에서는 어떤 속성부터 검증해야 합니까?
대출 프로토콜은 예치·차입·상환·청산이 하나의 회계 장부를 공유하기 때문에 상태 간 관계가 복잡합니다. 우선 검증 후보로 삼을 만한 불변식은 다음과 같습니다.
- 프로토콜이 실제로 보유한 자산이 장부상 예치 총액에서 대출 총액을 뺀 값과 준비금의 합보다 작아지지 않아야 합니다.
- 담보 비율이 청산 기준 아래로 떨어진 계정만 청산할 수 있고, 청산 뒤 해당 계정의 건전성이 나빠지지 않아야 합니다.
- 이자 누적 지수는 시간이 지나면서 줄어들지 않아야 하며, 반올림은 항상 프로토콜에 불리하지 않은 방향으로 처리되어야 합니다.
- 파라미터 변경·일시 정지·업그레이드 함수는 지정된 권한 주소만 호출할 수 있어야 합니다.
- 외부 토큰 호출 중 재진입이 일어나도 장부 상태가 일관되게 유지되어야 합니다.
우선순위는 세 가지로 매깁니다. 첫째, 속성이 깨졌을 때 자금 손실로 바로 이어지는지 봅니다. 둘째, 상태 조합이 많아 테스트만으로는 다 확인하기 어려운지 봅니다. 셋째, 반올림 오차 누적이나 여러 거래를 이어 붙인 시나리오처럼 수동 리뷰에서 놓치기 쉬운 성격인지 봅니다. 세 항목에 모두 해당하는 속성을 첫 번째 검증 대상으로 둡니다.
검증 범위는 어떤 절차로 정합니까?
높은 보증 수준을 시스템 전체가 아니라 핵심부에 집중하는 방식은 기존 보안 평가 체계에서도 볼 수 있습니다. 국제표준 ISO/IEC 15408(공통평가기준)은 평가보증등급의 가장 높은 단계인 EAL7을 「정형적으로 검증된 설계 및 시험」 수준으로 규정하며, 이 단계는 위험이 매우 크고 대상 범위가 비교적 좁은 제품에 적용하는 것이 일반적입니다.
공공 연구 분야에서도 같은 접근을 확인할 수 있습니다. 미국 국방고등연구계획국(DARPA)은 HACMS 프로그램에서 포멀 메서드 기반으로 고신뢰 차량 소프트웨어를 새로 설계하는 연구를 진행했습니다. 컨트랙트에서는 금고·회계 모듈처럼 신뢰의 기반이 되는 핵심부에 이런 접근을 적용할 수 있습니다. 실무 절차는 다음 순서로 정리할 수 있습니다.
- 자금을 직접 옮기거나 장부를 바꾸는 함수 목록을 뽑고, 호출 관계도를 그립니다.
- 함수별 사전·사후 조건과 전역 불변식을 자연어로 먼저 적고, 팀 안에서 합의합니다.
- 외부 토큰 동작, 오라클 값의 범위, 관리자 행위 등 검증이 전제로 삼을 가정을 따로 문서화합니다.
- 반복문 길이, 인라인 어셈블리, 외부 호출 깊이처럼 도구가 다루기 어려운 구조를 미리 표시합니다.
- 속성마다 포멀검증, 퍼징, 수동 리뷰 가운데 어떤 방법을 쓸지 배정합니다.
- 검증 대상 커밋을 고정하고, 범위 밖 항목과 그 이유를 요청서에 명시합니다.
| 방법 | 확인할 수 있는 것 | 주요 한계 | 대출 프로토콜에서 적합한 대상 |
|---|---|---|---|
| 수동 코드 리뷰 | 설계 의도와 구현의 불일치, 경제적 공격 시나리오 | 감사인 역량에 따라 결과가 달라짐 | 청산 인센티브 설계, 거버넌스 흐름 |
| 퍼징·속성 기반 테스트 | 여러 거래를 이어 붙였을 때 불변식이 깨지는 반례 | 찾지 못한 경로에 대해서는 보증하지 못함 | 이자 누적, 반올림 오차, 다중 사용자 시나리오 |
| 심볼릭 실행·모델 검사 | 정해진 범위 안의 모든 경로에서 속성 성립 여부 | 상태 폭발, 반복문·외부 호출 처리의 제약 | 권한 검사, 단일 함수의 사전·사후 조건 |
| 정리 증명 | 모든 입력과 상태에서 성립하는 수학적 증명 | 명세 작성과 증명 비용이 큼 | 금고 회계 불변식, 핵심 수학 라이브러리 |
블록체인감사 견적과 결과물은 어떻게 비교해야 합니까?
블록체인감사를 개발 생애주기의 한 단계로 보는 관점은 공공 지침과도 맞닿아 있습니다. NIST의 보안 소프트웨어 개발 프레임워크(SSDF, SP 800-218)는 기존 개발 생애주기 모델 대부분이 소프트웨어 보안을 구체적으로 다루지 않는다고 지적하며, 보안 실천 항목을 개발 과정에 넣도록 제시합니다. 감사를 출시 직전 한 번의 행사로 끝내지 않고, 명세 작성 단계부터 일정에 넣어야 하는 이유가 여기에 있습니다.
미국 사이버보안·인프라보안청(CISA)도 「설계 단계부터 보안(Secure by Design)」 원칙에서 소프트웨어 제조사가 고객의 보안 결과에 책임을 지도록 권고합니다. 이 관점에서 보면 감사 업체를 고를 때는 가격보다 결과물의 구성을 먼저 비교하는 것이 합리적입니다. 견적 단계에서 다음 항목이 결과물에 들어가는지 확인합니다.
- 자연어 명세와 형식 명세가 함께 제공되고, 둘의 대응 관계가 표시되어 있는지
- 검증이 전제로 삼은 가정 목록과 범위 밖 항목이 명시되어 있는지
- 증명에 성공한 속성, 실패한 속성, 시간 초과로 결론이 나지 않은 속성이 구분되어 있는지
- 실패한 속성마다 반례와 재현 방법이 첨부되어 있는지
- 도구 이름과 버전, 검증 대상 커밋 해시, 실행 설정이 기록되어 있는지
- 코드 수정 뒤 팀이 직접 다시 돌려 볼 수 있는 검증 스크립트가 넘겨지는지
특히 「결론 없음」으로 끝난 속성을 통과로 표기하는 보고서는 주의해야 합니다. 업그레이드 가능한 구조라면 다음 버전을 배포할 때 같은 명세로 재검증하는 비용과 절차도 견적 단계에서 함께 합의해 두는 것이 좋습니다.
자주 묻는 질문
포멀검증을 받으면 수동 감사는 생략해도 됩니까?
권장하지 않습니다. 포멀검증은 명세에 적힌 속성만 보증하므로, 명세가 놓친 설계 결함이나 경제적 공격 시나리오는 수동 리뷰로 찾아야 합니다. 두 방법은 서로 대체하는 관계가 아니라 보완하는 관계로 보는 것이 적절합니다.
업그레이드 가능한 프록시 구조도 포멀검증할 수 있습니까?
가능하지만 구현 컨트랙트의 로직과 함께 스토리지 배치 충돌, 초기화 함수의 1회 실행, 업그레이드 권한 같은 속성을 별도로 명세해야 합니다. 또 새 구현을 배포할 때마다 같은 명세로 다시 검증해야 의미가 있으므로, 검증 스크립트를 저장소에 두고 배포 절차에 포함하는 것이 좋습니다.
소규모 팀도 자체적으로 포멀검증을 시작할 수 있습니까?
Solidity 컴파일러에 내장된 SMTChecker나 오픈소스 심볼릭 실행 도구로 단순한 사전·사후 조건부터 확인하는 방식으로 시작할 수 있습니다. 다만 자체 검증 결과는 외부 감사를 대신하지 못하며, 사용자 자금을 다루는 서비스라면 출시 전 전문 감사 기관과 법률·규제 전문가의 검토를 함께 받을 것을 권합니다.