불변식을 처음 작성하는 개발자는 코드를 보기 전에 자산 보존·권한·상태 전이 규칙을 자연어 문장으로 정리한 뒤 이를 형식 명세로 옮기는 순서로 진행하는 것이 바람직합니다. 처음부터 모든 함수를 증명하기보다 자금이 오가는 핵심 경로의 불변식 몇 개를 정해 증명이 성립하는지 확인하고, 실패한 증명은 반례를 분석해 코드와 명세 중 어느 쪽이 틀렸는지 판정합니다. 이렇게 정리한 명세와 증명 결과는 이후 스마트컨트랙트감사와 블록체인보안감사에서 감사인이 검토 범위를 정하는 근거 자료로 쓰입니다.
검증 명세는 왜 코드보다 먼저 정리해야 합니까?
정형 기법은 소프트웨어와 시스템 개발에 쓰이는 수학적 접근법입니다(수학적으로 확인하는 기법 관련 문헌 참고). 포멀검증은 이러한 접근을 활용해 코드가 미리 정한 명세를 모든 입력과 상태에서 만족하는지 확인하는 작업입니다. 따라서 검증 결과의 가치는 명세의 품질을 넘지 못합니다. 명세가 잘못되었거나 지나치게 약하면 증명이 통과해도 실제 취약점은 그대로 남습니다. 미국 국립표준기술연구소(NIST)의 용어집은 정형 정책 모델을, 정형 언어로 특정 동작이나 보안 정책을 기술해 그 정확성을 정형적으로 증명할 수 있게 하는 것으로 정의합니다. 이 정의처럼 무엇을 증명할지는 먼저 정형 언어로 기술한 동작과 정책이 정하므로, 검증의 출발점은 코드가 아니라 명세입니다.
코드를 먼저 읽고 명세를 쓰면 구현의 동작을 그대로 옮겨 적는 경우가 많습니다. 이렇게 쓴 명세는 구현에 있는 버그까지 정상 동작으로 받아들이므로 검증하는 의미가 사라집니다. 백서, 토크노믹스 문서, 기능 요구사항처럼 설계 의도를 담은 자료에서 규칙을 먼저 뽑아내고, 코드는 그 규칙을 어기는지 확인하는 대상으로 다루어야 합니다.
불변식은 어떤 순서로 찾아 적어야 합니까?
처음 작성하는 개발자에게는 다음 순서가 실무에서 무리가 적습니다. 단계마다 산출물을 문서로 남기면 감사인과 소통할 때도 그대로 쓸 수 있습니다.
1단계: 자산 흐름을 나열합니다
컨트랙트가 보관하거나 이동시키는 자산(토큰 잔액, 예치금, 담보, 수수료 적립금)을 모두 나열하고, 각 자산이 들어오고 나가는 함수를 표시합니다. 이 목록이 보존 불변식의 후보가 됩니다. 예를 들어 "모든 사용자 잔액의 합은 총발행량과 같다", "컨트랙트가 보유한 토큰은 사용자 예치금 합계 이상이다" 같은 문장입니다.
2단계: 권한 주체와 행위를 표로 만듭니다
소유자, 관리자, 일반 사용자, 외부 컨트랙트처럼 호출 주체별로 실행할 수 있는 함수를 정리합니다. "관리자가 아닌 주소는 수수료율을 바꿀 수 없다", "일시 정지 상태에서는 출금 외의 상태 변경이 불가능하다" 같은 접근통제 속성이 여기서 나옵니다.
3단계: 상태 전이 규칙을 정합니다
경매, 베스팅, 대출 청산처럼 단계가 있는 로직은 허용되는 전이와 금지되는 전이를 구분합니다. "종료된 경매는 다시 시작될 수 없다", "베스팅 해제량은 시간이 지나도 줄어들지 않는다"처럼 단조성이나 비가역성을 표현하는 속성이 대표적입니다.
4단계: 자연어 문장을 형식 명세로 옮깁니다
앞 단계의 문장을 사용하는 도구의 명세 언어로 바꿉니다. 이때 한 속성에는 한 가지 주장만 담아야 실패 원인을 추적하기 쉽습니다. 문장 하나를 여러 조건으로 쪼개야 한다면 쪼개는 쪽이 낫습니다.
5단계: 일부러 틀린 코드로 명세를 시험합니다
명세가 지나치게 약하지 않은지 확인하려면 잔액 차감을 빼거나 권한 검사를 지우는 식으로 코드를 일부러 바꾸어 봅니다. 이런 변형을 넣었는데도 증명이 통과한다면 그 명세는 보강해야 합니다.
명세 유형별로 무엇을 증명할 수 있습니까?
속성의 종류에 따라 증명 난이도와 효과가 다릅니다. 아래 표는 처음 작성하는 단계에서 우선순위를 정할 때 참고할 수 있는 기준입니다.
| 명세 유형 | 예시 속성 | 막을 수 있는 취약점 | 작성 우선순위 |
|---|---|---|---|
| 자산 보존 불변식 | 잔액 합계와 총발행량이 같다 | 무단 발행, 회계 불일치, 반올림 오류 누적 | 가장 먼저 작성 |
| 접근통제 속성 | 관리자만 파라미터를 변경할 수 있다 | 권한 누락, 초기화 함수 재호출 | 보존 불변식 다음 |
| 상태 전이 규칙 | 종료 상태에서 되돌아갈 수 없다 | 중복 청구, 단계 우회 | 단계형 로직이 있을 때 |
| 함수 단위 사전·사후 조건 | 출금 뒤 사용자 잔액이 요청액만큼 줄어든다 | 계산 오류, 경계값 처리 실패 | 핵심 함수부터 점진 확대 |
| 외부 호출 관련 속성 | 재진입 중 잔액이 이중 차감되지 않는다 | 재진입, 콜백 악용 | 외부 호출이 많은 경우 필수 |
표의 순서는 절대적인 규칙이 아니고, 프로젝트가 보관하는 자산 규모와 구조에 따라 조정합니다. 다만 자산 보존 불변식은 거의 모든 디파이와 토큰 컨트랙트에서 효과가 크므로 첫 작업으로 권합니다.
증명이 실패하거나 시간이 초과되면 어떻게 대응합니까?
증명 실패는 정상적인 과정의 일부입니다. 도구가 반례를 내놓으면 다음 세 가지 중 어디에 원인이 있는지 판정합니다.
- 코드 결함: 반례가 실제로 일어날 수 있는 호출 순서라면 구현을 고치고 다시 검증합니다.
- 명세 오류: 설계 의도상 허용되는 동작인데 명세가 금지하고 있다면 명세를 고칩니다. 이때 수정 이유를 기록으로 남깁니다.
- 비현실적 초기 상태: 도구가 실제로 도달할 수 없는 상태에서 출발한 반례라면, 그 상태가 도달 불가능하다는 보조 불변식을 추가합니다.
시간 초과는 비선형 연산(곱셈·나눗셈이 섞인 이자 계산), 큰 반복문, 복잡한 외부 호출에서 자주 생깁니다. 이때는 함수를 작은 단위로 나누어 따로 증명하거나, 외부 컨트랙트 동작을 요약 명세로 대체하거나, 검증 범위를 핵심 경로로 좁히는 방법을 씁니다. 범위를 좁혔다면 증명하지 않은 부분을 반드시 문서에 적어야 합니다. 증명된 속성과 가정의 경계를 명시하지 않은 결과물은 외부 검토자에게 과대 해석될 수 있습니다.
정형 기법으로 얻은 보증 근거는 그 근거가 어떤 가정 위에서 성립하는지와 함께 제시하는 것이 바람직합니다. 컨트랙트 검증에서도 컴파일러 동작, 체인 실행 환경, 오라클 값처럼 증명 밖에 둔 가정을 목록으로 남겨 두는 것이 좋습니다.
스마트컨트랙트감사와 블록체인보안감사에서 검증 결과는 어떻게 활용됩니까?
사내에서 작성한 명세와 증명 기록은 외부 스마트컨트랙트감사의 대체물이 아니라 입력 자료입니다. 감사인은 명세를 보고 설계 의도를 빠르게 파악하고, 증명되지 않은 영역이나 가정이 약한 부분에 수동 검토를 집중할 수 있습니다. 체인 구조, 노드, 브릿지, 운영 키 관리까지 포함하는 블록체인보안감사에서는 컨트랙트 검증 결과가 전체 위협 모델의 한 구성요소로 다루어집니다.
높은 보증이 필요한 분야에서는 정형 기법을 요구하거나 활용해 온 사례가 있습니다. 국제 보안 평가 기준인 공통평가기준(CC)에서 EAL7은 정형적으로 검증된 설계와 시험(Formally verified design and tested)을 요구하는 등급입니다. 미국 국방고등연구계획국(DARPA)의 HACMS 프로그램은 정형 기법에 기반해 고신뢰 차량(vehicle) 시스템을 처음부터 새로 구축하는 접근을 추진했습니다. 되돌릴 수 없는 거래가 자산을 직접 움직이는 스마트컨트랙트도 같은 이유로 정형 기법의 효용이 큰 영역입니다.
외부 감사로 넘길 때는 다음 자료를 함께 제출하면 검토 효율이 높아집니다.
- 자연어로 정리한 속성 목록과 각 속성의 설계 근거
- 형식 명세 파일과 사용한 도구·버전 정보
- 통과·실패·시간 초과 결과와 실패 항목의 판정 기록
- 증명 범위에서 제외한 함수와 가정 목록
외부 서비스의 검증 범위와 방식을 미리 살펴보려면 써틱이 공개한 포멀검증 서비스 설명을 참고해 사내 명세의 수준과 형식을 맞추어 볼 수 있습니다. 서비스마다 다루는 속성의 범위와 산출물 형식이 다르므로, 계약 전에 증명 대상과 제외 범위를 서면으로 확인하는 것이 좋습니다.
자주 묻는 질문
포멀검증을 통과하면 별도의 감사가 필요 없습니까?
그렇지 않습니다. 증명은 작성한 명세에 대해서만 성립하므로 명세에 없는 위험, 경제적 공격, 운영 키 관리 문제는 따로 검토해야 합니다. 수동 감사와 함께 진행할 때 가장 효과가 큽니다.
불변식은 몇 개부터 시작하는 것이 적당합니까?
정해진 개수는 없지만, 자금이 오가는 핵심 경로의 보존 불변식과 주요 접근통제 속성부터 시작해 점차 넓히는 방식이 일반적입니다. 개수보다 각 속성이 실제 위험을 막는지와 변형 코드로 시험했을 때 실패하는지가 더 중요합니다.
업그레이드 가능한 컨트랙트도 명세를 다시 써야 합니까?
구현이 바뀌면 기존 증명은 새 코드에 자동으로 이어지지 않으므로 재검증이 필요합니다. 저장소 배치가 바뀌거나 새 함수가 추가된 경우에는 기존 불변식이 여전히 성립하는지 확인하고, 써틱 같은 외부 감사 기관이나 보안 전문가와 재검증 범위를 상의하는 것이 바람직합니다.