스마트 계약의 형식 검증
페이지 마지막 업데이트됨: 2026년 2월 23일
스마트 계약은 새로운 사용 사례를 제시하고 사용자에게 가치를 창출하는 탈중앙화되고 신뢰가 필요 없으며 견고한 애플리케이션을 만들 수 있도록 합니다. 스마트 계약은 막대한 가치를 다루기 때문에 보안은 개발자에게 매우 중요한 고려 사항입니다.
형식 검증은 스마트 계약 보안을 향상시키기 위해 권장되는 기술 중 하나입니다. 프로그램을 명시하고, 설계하고, 검증하기 위해 형식적 방법 (opens in a new tab)을 사용하는 형식 검증은 수년 동안 중요한 하드웨어 및 소프트웨어 시스템의 정확성을 보장하는 데 사용되어 왔습니다.
스마트 계약에 구현될 때, 형식 검증은 계약의 비즈니스 로직이 사전에 정의된 사양을 충족함을 증명할 수 있습니다. 테스트와 같이 계약 코드의 정확성을 평가하는 다른 방법에 비해 형식 검증은 스마트 계약이 기능적으로 올바르다는 것을 더 강력하게 보장합니다.
형식 검증이란 무엇인가요?
형식 검증은 형식 사양에 대한 시스템의 정확성을 평가하는 과정을 의미합니다. 간단히 말해 형식 검증을 통해 시스템의 동작이 일부 요구 사항을 충족하는지(즉, 원하는 대로 작동하는지) 확인할 수 있습니다.
시스템(이 경우 스마트 계약)의 예상 동작은 형식 모델링을 사용하여 설명되는 반면, 사양 언어는 형식적 속성을 생성할 수 있도록 합니다. 형식 검증 기술은 계약의 구현이 해당 사양을 준수하는지 검증하고 전자의 정확성에 대한 수학적 증명을 도출할 수 있습니다. 계약이 사양을 충족하면 '기능적으로 올바름', '설계에 따라 올바름' 또는 '구성에 따라 올바름'으로 설명됩니다.
형식 모델이란 무엇인가요?
컴퓨터 과학에서 형식 모델 (opens in a new tab)은 계산 과정에 대한 수학적 설명입니다. 프로그램은 수학적 함수(방정식)로 추상화되며, 모델은 입력이 주어졌을 때 함수에 대한 출력이 어떻게 계산되는지를 설명합니다.
형식 모델은 프로그램의 동작 분석을 평가할 수 있는 추상화 수준을 제공합니다. 형식 모델의 존재는 해당 모델의 바람직한 속성을 설명하는 형식 사양을 생성할 수 있게 합니다.
형식 검증을 위해 스마트 계약을 모델링하는 데는 여러 기술이 사용됩니다. 예를 들어, 일부 모델은 스마트 계약의 상위 수준 동작에 대해 추론하는 데 사용됩니다. 이러한 모델링 기술은 스마트 계약에 블랙박스 관점을 적용하여, 입력을 수락하고 해당 입력을 기반으로 계산을 실행하는 시스템으로 봅니다.
상위 수준 모델은 스마트 계약과 외부 소유 계정(EOA), 계약 계정, 블록체인 환경과 같은 외부 에이전트 간의 관계에 중점을 둡니다. 이러한 모델은 특정 사용자 상호 작용에 대한 계약의 동작 방식을 지정하는 속성을 정의하는 데 유용합니다.
반대로, 다른 형식 모델은 스마트 계약의 하위 수준 동작에 중점을 둡니다. 상위 수준 모델은 계약의 기능에 대한 추론에 도움이 될 수 있지만, 구현의 내부 작동에 대한 세부 정보를 포착하지 못할 수 있습니다. 하위 수준 모델은 프로그램 분석에 화이트박스 관점을 적용하고 프로그램 추적 및 제어 흐름 그래프 (opens in a new tab)와 같은 스마트 계약 애플리케이션의 하위 수준 표현에 의존하여 계약 실행과 관련된 속성을 추론합니다.
하위 수준 모델은 이더리움의 실행 환경(즉, EVM)에서 스마트 계약의 실제 실행을 나타내므로 이상적인 것으로 간주됩니다. 하위 수준 모델링 기술은 스마트 계약에서 중요한 안전 속성을 설정하고 잠재적인 취약점을 감지하는 데 특히 유용합니다.
형식 사양이란 무엇인가요?
사양은 특정 시스템이 충족해야 하는 기술적 요구 사항입니다. 프로그래밍에서 사양은 프로그램 실행에 대한 일반적인 아이디어(즉, 프로그램이 무엇을 해야 하는지)를 나타냅니다.
스마트 계약의 맥락에서 형식 사양은 계약이 충족해야 하는 요구 사항에 대한 형식적 설명인 속성을 의미합니다. 이러한 속성은 '불변성'으로 설명되며 예외 없이 모든 가능한 상황에서 참으로 유지되어야 하는 계약 실행에 대한 논리적 주장을 나타냅니다.
따라서 형식 사양을 스마트 계약의 의도된 실행을 설명하는 형식 언어로 작성된 문장의 모음으로 생각할 수 있습니다. 사양은 계약의 속성을 다루고 다양한 상황에서 계약이 어떻게 작동해야 하는지 정의합니다. 형식 검증의 목적은 스마트 계약이 이러한 속성(불변성)을 소유하고 있는지, 그리고 이러한 속성이 실행 중에 위반되지 않는지를 확인하는 것입니다.
형식 사양은 스마트 계약의 보안 구현을 개발하는 데 중요합니다. 불변성을 구현하지 못하거나 실행 중에 속성이 위반된 계약은 기능을 손상시키거나 악의적인 익스플로잇을 유발할 수 있는 취약점에 노출되기 쉽습니다.
스마트 계약의 형식 사양 유형
형식 사양을 통해 프로그램 실행의 정확성에 대한 수학적 추론이 가능합니다. 형식 모델과 마찬가지로 형식 사양은 계약 구현의 상위 수준 속성이나 하위 수준 동작을 포착할 수 있습니다.
형식 사양은 프로그램의 속성에 대한 형식적 추론을 허용하는 프로그램 논리 (opens in a new tab)의 요소를 사용하여 파생됩니다. 프로그램 논리에는 프로그램의 예상 동작을 (수학적 언어로) 표현하는 형식 규칙이 있습니다. 도달 가능성 논리 (opens in a new tab), 시간 논리 (opens in a new tab), 호어 논리 (opens in a new tab)를 포함하여 형식 사양을 만드는 데 다양한 프로그램 논리가 사용됩니다.
스마트 계약에 대한 형식 사양은 크게 상위 수준 또는 하위 수준 사양으로 분류할 수 있습니다. 사양이 속한 범주에 관계없이 분석 중인 시스템의 속성을 적절하고 명확하게 설명해야 합니다.
상위 수준 사양
이름에서 알 수 있듯이 상위 수준 사양('모델 지향 사양'이라고도 함)은 프로그램의 상위 수준 동작을 설명합니다. 상위 수준 사양은 스마트 계약을 작업을 수행하여 상태 간에 전환할 수 있는 유한 상태 머신 (opens in a new tab)(FSM)으로 모델링하며, 시간 논리를 사용하여 FSM 모델의 형식적 속성을 정의합니다.
시간 논리 (opens in a new tab)는 '시간의 관점에서 한정된 명제에 대해 추론하기 위한 규칙(예: '나는 항상 배고프다' 또는 '나는 결국 배고플 것이다')'입니다. 형식 검증에 적용될 때, 시간 논리는 상태 머신으로 모델링된 시스템의 올바른 동작에 대한 주장을 진술하는 데 사용됩니다. 특히, 시간 논리는 스마트 계약이 있을 수 있는 미래 상태와 상태 간 전환 방법을 설명합니다.
상위 수준 사양은 일반적으로 스마트 계약에 대한 두 가지 중요한 시간적 속성인 안전성과 활성을 포착합니다. 안전성 속성은 '나쁜 일은 절대 일어나지 않는다'는 아이디어를 나타내며 일반적으로 불변성을 표현합니다. 안전성 속성은 교착 상태 (opens in a new tab)로부터의 자유와 같은 일반적인 소프트웨어 요구 사항을 정의하거나 계약에 대한 도메인별 속성(예: 함수에 대한 접근 제어의 불변성, 상태 변수의 허용 값 또는 토큰 전송 조건)을 표현할 수 있습니다.
예를 들어, ERC-20 토큰 계약에서 transfer() 또는 transferFrom() 사용 조건을 다루는 다음과 같은 안전성 요구 사항을 살펴보겠습니다. '전송자의 잔액은 전송 요청된 토큰의 양보다 결코 낮아서는 안 된다.' 계약 불변성에 대한 이 자연어 설명은 형식(수학적) 사양으로 변환될 수 있으며, 그 후 유효성을 엄격하게 확인할 수 있습니다.
활성 속성은 '결국 좋은 일이 일어난다'고 주장하며, 계약이 여러 상태를 거쳐 진행할 수 있는 능력과 관련이 있습니다. 활성 속성의 예로는 '유동성'이 있으며, 이는 요청 시 사용자에게 잔액을 전송하는 계약의 능력을 의미합니다. Parity 지갑 사건 (opens in a new tab)에서 발생했던 것처럼 이 속성이 위반되면 사용자는 계약에 저장된 자산을 인출할 수 없게 됩니다.
하위 수준 사양
상위 수준 사양은 계약의 유한 상태 모델을 시작점으로 삼고 이 모델의 바람직한 속성을 정의합니다. 이와 대조적으로 하위 수준 사양('속성 지향 사양'이라고도 함)은 종종 프로그램(스마트 계약)을 수학적 함수 모음으로 구성된 시스템으로 모델링하고 이러한 시스템의 올바른 동작을 설명합니다.
간단히 말해, 하위 수준 사양은 프로그램 추적을 분석하고 이러한 추적을 통해 스마트 계약의 속성을 정의하려고 시도합니다. 추적은 스마트 계약의 상태를 변경하는 함수 실행 시퀀스를 의미합니다. 따라서 하위 수준 사양은 계약의 내부 실행에 대한 요구 사항을 지정하는 데 도움이 됩니다.
하위 수준 형식 사양은 호어 스타일 속성 또는 실행 경로에 대한 불변성으로 주어질 수 있습니다.
호어 스타일 속성
호어 논리 (opens in a new tab)는 스마트 계약을 포함한 프로그램의 정확성에 대해 추론하기 위한 일련의 형식 규칙을 제공합니다. 호어 스타일 속성은 호어 삼중항 {P}c{Q}로 표시됩니다. 여기서 c는 프로그램이고 P와 Q는 c의 상태(즉, 프로그램)에 대한 술어이며, 각각 공식적으로 사전 조건과 사후 조건으로 설명됩니다.
사전 조건은 함수의 올바른 실행에 필요한 조건을 설명하는 술어입니다. 계약을 호출하는 사용자는 이 요구 사항을 충족해야 합니다. 사후 조건은 함수가 올바르게 실행될 경우 함수가 설정하는 조건을 설명하는 술어입니다. 사용자는 함수를 호출한 후 이 조건이 참일 것으로 기대할 수 있습니다. 호어 논리에서 불변성은 함수 실행에 의해 보존되는(즉, 변경되지 않는) 술어입니다.
호어 스타일 사양은 부분적 정확성 또는 전체 정확성을 보장할 수 있습니다. 계약 함수의 구현은 함수가 실행되기 전에 사전 조건이 참이고 실행이 종료되면 사후 조건도 참인 경우 '부분적으로 올바름'입니다. 함수가 실행되기 전에 사전 조건이 참이고, 실행이 종료되는 것이 보장되며, 종료될 때 사후 조건이 참이면 전체 정확성의 증명이 얻어집니다.
일부 실행은 종료되기 전에 지연되거나 전혀 종료되지 않을 수 있으므로 전체 정확성의 증명을 얻는 것은 어렵습니다. 즉, 이더리움의 가스 메커니즘이 무한 프로그램 루프를 방지하므로(실행이 성공적으로 종료되거나 '가스 부족' 오류로 인해 종료됨) 실행이 종료되는지 여부는 논란의 여지가 있는 문제입니다.
호어 논리를 사용하여 생성된 스마트 계약 사양에는 계약의 함수 및 루프 실행에 대해 정의된 사전 조건, 사후 조건 및 불변성이 포함됩니다. 사전 조건에는 종종 함수에 대한 잘못된 입력 가능성이 포함되며, 사후 조건은 이러한 입력에 대한 예상 응답(예: 특정 예외 발생)을 설명합니다. 이러한 방식으로 호어 스타일 속성은 계약 구현의 정확성을 보장하는 데 효과적입니다.
많은 형식 검증 프레임워크는 함수의 의미론적 정확성을 증명하기 위해 호어 스타일 사양을 사용합니다. 또한 솔리디티의 require 및 assert 문을 사용하여 호어 스타일 속성(어설션으로)을 계약 코드에 직접 추가할 수도 있습니다.
require 문은 사전 조건 또는 불변성을 표현하며 종종 사용자 입력을 검증하는 데 사용되는 반면, assert는 안전에 필요한 사후 조건을 포착합니다. 예를 들어, 호출하는 계정의 ID에 대한 사전 조건 확인으로 require를 사용하여 함수에 대한 적절한 접근 제어(안전성 속성의 예)를 달성할 수 있습니다. 마찬가지로, 계약의 상태 변수 허용 값에 대한 불변성(예: 유통 중인 총 토큰 수)은 함수 실행 후 계약의 상태를 확인하기 위해 assert를 사용하여 위반으로부터 보호될 수 있습니다.
추적 수준 속성
추적 기반 사양은 계약을 여러 상태 간에 전환하는 작업과 이러한 작업 간의 관계를 설명합니다. 앞서 설명했듯이 추적은 특정 방식으로 계약의 상태를 변경하는 작업의 시퀀스입니다.
이 접근 방식은 미리 정의된 전환 집합(계약 함수에 의해 설명됨)과 함께 일부 미리 정의된 상태(상태 변수에 의해 설명됨)를 가진 상태 전환 시스템으로서의 스마트 계약 모델에 의존합니다. 또한, 프로그램의 실행 흐름을 그래픽으로 표현한 제어 흐름 그래프 (opens in a new tab)(CFG)가 계약의 운영 의미론을 설명하는 데 자주 사용됩니다. 여기서 각 추적은 제어 흐름 그래프의 경로로 표시됩니다.
주로 추적 수준 사양은 스마트 계약의 내부 실행 패턴에 대해 추론하는 데 사용됩니다. 추적 수준 사양을 생성함으로써 스마트 계약에 대한 허용 가능한 실행 경로(즉, 상태 전환)를 주장합니다. 기호 실행과 같은 기술을 사용하여 형식 모델에 정의되지 않은 경로를 실행이 따르지 않음을 형식적으로 검증할 수 있습니다.
DAO 계약의 예를 사용하여 추적 수준 속성을 설명해 보겠습니다. 이 계약에는 공개적으로 접근 가능한 몇 가지 기능이 있습니다. 여기서는 DAO 계약이 사용자가 다음 작업을 수행할 수 있도록 허용한다고 가정합니다.
-
자금 예치
-
자금 예치 후 제안에 투표
-
제안에 투표하지 않으면 환불 요청
추적 수준 속성의 예로는 '자금을 예치하지 않은 사용자는 제안에 투표할 수 없음' 또는 '제안에 투표하지 않은 사용자는 항상 환불을 요청할 수 있어야 함'이 있습니다. 두 속성 모두 선호되는 실행 순서를 주장합니다(투표는 자금을 예치하기 전에 발생할 수 없으며 환불 요청은 제안에 투표한 후에 발생할 수 없습니다).
스마트 계약의 형식 검증 기술
모델 체킹
모델 체킹은 알고리즘이 스마트 계약의 형식 모델을 해당 사양과 대조하여 확인하는 형식 검증 기술입니다. 모델 체킹에서 스마트 계약은 종종 상태 전환 시스템으로 표현되며, 허용 가능한 계약 상태에 대한 속성은 시간 논리를 사용하여 정의됩니다.
모델 체킹은 시스템(즉, 계약)의 추상적인 수학적 표현을 생성하고 명제 논리 (opens in a new tab)에 기반한 공식을 사용하여 이 시스템의 속성을 표현해야 합니다. 이는 모델 체킹 알고리즘의 작업, 즉 수학적 모델이 주어진 논리 공식을 만족함을 증명하는 작업을 단순화합니다.
형식 검증에서의 모델 체킹은 주로 시간 경과에 따른 계약의 동작을 설명하는 시간적 속성을 평가하는 데 사용됩니다. 스마트 계약의 시간적 속성에는 이전에 설명한 안전성과 활성이 포함됩니다.
예를 들어, 접근 제어와 관련된 보안 속성(예: 계약 소유자만 selfdestruct를 호출할 수 있음)은 형식 논리로 작성할 수 있습니다. 그 후, 모델 체킹 알고리즘은 계약이 이 형식 사양을 만족하는지 검증할 수 있습니다.
모델 체킹은 상태 공간 탐색을 사용하며, 이는 스마트 계약의 모든 가능한 상태를 구성하고 속성 위반을 초래하는 도달 가능한 상태를 찾으려고 시도하는 것을 포함합니다. 그러나 이는 무한한 수의 상태( '상태 폭발 문제'로 알려짐)로 이어질 수 있으므로, 모델 체커는 스마트 계약의 효율적인 분석을 가능하게 하기 위해 추상화 기술에 의존합니다.
정리 증명
정리 증명은 스마트 계약을 포함한 프로그램의 정확성에 대해 수학적으로 추론하는 방법입니다. 계약 시스템의 모델과 해당 사양을 수학 공식(논리 문)으로 변환하는 과정이 포함됩니다.
정리 증명의 목표는 이러한 문장 간의 논리적 동등성을 검증하는 것입니다. '논리적 동등성'('논리적 쌍방함의'라고도 함)은 첫 번째 문장이 참일 경우에만 두 번째 문장이 참이 되는 두 문장 사이의 관계 유형입니다.
계약 모델과 그 속성에 대한 문장 간의 필요한 관계(논리적 동등성)는 증명 가능한 문장(정리라고 함)으로 공식화됩니다. 형식적 추론 시스템을 사용하여 자동 정리 증명기는 정리의 유효성을 검증할 수 있습니다. 즉, 정리 증명기는 스마트 계약의 모델이 해당 사양과 정확히 일치함을 결정적으로 증명할 수 있습니다.
모델 체킹은 계약을 유한 상태를 가진 전환 시스템으로 모델링하는 반면, 정리 증명은 무한 상태 시스템의 분석을 처리할 수 있습니다. 그러나 이는 자동 정리 증명기가 논리 문제가 '결정 가능'한지 여부를 항상 알 수 없다는 것을 의미합니다.
결과적으로, 정리 증명기가 정확성 증명을 도출하도록 안내하기 위해 종종 인간의 도움이 필요합니다. 정리 증명에 인간의 노력을 사용하는 것은 완전히 자동화된 모델 체킹보다 사용 비용이 더 비쌉니다.
기호 실행
기호 실행은 구체적인 값(예: x == 5) 대신 기호 값(예: x > 5)을 사용하여 함수를 실행함으로써 스마트 계약을 분석하는 방법입니다. 형식 검증 기술로서 기호 실행은 계약 코드의 추적 수준 속성에 대해 형식적으로 추론하는 데 사용됩니다.
기호 실행은 실행 추적을 기호 입력 값에 대한 수학 공식으로 나타내며, 이를 경로 술어라고도 합니다. SMT 솔버 (opens in a new tab)는 경로 술어가 '만족 가능'한지(즉, 공식을 만족할 수 있는 값이 존재하는지) 확인하는 데 사용됩니다. 취약한 경로가 만족 가능하면, SMT 솔버는 실행을 해당 경로로 유도하는 구체적인 값을 생성합니다.
스마트 계약의 함수가 uint 값(x)을 입력으로 받고 x가 5보다 크고 10보다 작을 때 되돌린다고 가정해 보겠습니다. 일반적인 테스트 절차를 사용하여 오류를 유발하는 x 값을 찾는 것은 오류를 유발하는 입력을 실제로 찾을 수 있다는 보장 없이 수십 개(또는 그 이상)의 테스트 사례를 실행해야 합니다.
반대로, 기호 실행 도구는 기호 값 X > 5 ∧ X < 10 (즉, x가 5보다 크고 10보다 작음)으로 함수를 실행합니다. 연관된 경로 술어 x = X > 5 ∧ X < 10은 해결을 위해 SMT 솔버에 주어집니다. 특정 값이 x = X > 5 ∧ X < 10 공식을 만족하면 SMT 솔버가 이를 계산합니다. 예를 들어, 솔버는 x의 값으로 7을 생성할 수 있습니다.
기호 실행은 프로그램에 대한 입력에 의존하고, 도달 가능한 모든 상태를 탐색하기 위한 입력 집합은 잠재적으로 무한하므로 여전히 테스트의 한 형태입니다. 그러나 예에서 보듯이, 기호 실행은 속성 위반을 유발하는 입력을 찾는 데 있어 일반적인 테스트보다 더 효율적입니다.
또한, 기호 실행은 함수에 대한 입력을 무작위로 생성하는 다른 속성 기반 기술(예: 퍼징)보다 거짓 양성이 적습니다. 기호 실행 중에 오류 상태가 트리거되면, 오류를 트리거하는 구체적인 값을 생성하고 문제를 재현하는 것이 가능합니다.
기호 실행은 또한 어느 정도의 수학적 정확성 증명을 제공할 수 있습니다. 오버플로 방지 기능이 있는 계약 함수의 다음 예를 고려해 보십시오.
1function safe_add(uint x, uint y) returns(uint z){23 z = x + y;4 require(z>=x);5 require(z>=y);67 return z;8}정수 오버플로를 초래하는 실행 추적은 z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) 공식을 만족해야 합니다. 이러한 공식은 해결될 가능성이 거의 없으므로, safe_add 함수가 절대 오버플로되지 않는다는 수학적 증거 역할을 합니다.
스마트 계약에 형식 검증을 사용하는 이유는 무엇인가요?
신뢰성의 필요성
형식 검증은 실패 시 사망, 부상 또는 재정적 파탄과 같은 파괴적인 결과를 초래할 수 있는 안전이 중요한 시스템의 정확성을 평가하는 데 사용됩니다. 스마트 계약은 막대한 가치를 제어하는 고부가가치 애플리케이션이며, 설계상의 사소한 오류는 사용자에게 복구 불가능한 손실 (opens in a new tab)을 초래할 수 있습니다. 그러나 배포 전에 계약을 형식적으로 검증하면 블록체인에서 실행될 때 예상대로 작동할 것이라는 보장을 높일 수 있습니다.
신뢰성은 모든 스마트 계약에서 매우 바람직한 품질이며, 특히 이더리움 가상 머신(EVM)에 배포된 코드는 일반적으로 불변이기 때문입니다. 출시 후 업그레이드에 쉽게 접근할 수 없기 때문에 계약의 신뢰성을 보장해야 하므로 형식 검증이 필요합니다. 형식 검증은 감사자 및 테스터가 놓칠 수 있는 정수 언더플로 및 오버플로, 재진입성, 부실한 가스 최적화와 같은 까다로운 문제를 감지할 수 있습니다.
기능적 정확성 증명
프로그램 테스트는 스마트 계약이 일부 요구 사항을 충족함을 증명하는 가장 일반적인 방법입니다. 이는 계약이 처리할 것으로 예상되는 데이터 샘플로 계약을 실행하고 그 동작을 분석하는 것을 포함합니다. 계약이 샘플 데이터에 대해 예상 결과를 반환하면 개발자는 그 정확성에 대한 객관적인 증거를 갖게 됩니다.
그러나 이 접근 방식은 샘플에 포함되지 않은 입력 값에 대한 올바른 실행을 증명할 수 없습니다. 따라서 계약을 테스트하면 버그를 감지하는 데 도움이 될 수 있지만(즉, 일부 코드 경로가 실행 중에 원하는 결과를 반환하지 못하는 경우), 버그가 없음을 결정적으로 증명할 수는 없습니다.
반대로 형식 검증은 계약을 전혀 실행하지 않고도 스마트 계약이 무한한 실행 범위에 대한 요구 사항을 만족함을 형식적으로 증명할 수 있습니다. 이를 위해서는 올바른 계약 동작을 정확하게 설명하는 형식 사양을 만들고 계약 시스템의 형식(수학적) 모델을 개발해야 합니다. 그런 다음 형식 증명 절차에 따라 계약 모델과 해당 사양 간의 일관성을 확인할 수 있습니다.
형식 검증을 통해 계약의 비즈니스 로직이 요구 사항을 만족하는지 검증하는 문제는 증명되거나 반증될 수 있는 수학적 명제입니다. 명제를 형식적으로 증명함으로써 유한한 단계로 무한한 수의 테스트 사례를 검증할 수 있습니다. 이러한 방식으로 형식 검증은 계약이 사양에 대해 기능적으로 올바르다는 것을 증명할 더 나은 가능성을 가집니다.
이상적인 검증 대상
검증 대상은 형식적으로 검증될 시스템을 설명합니다. 형식 검증은 '임베디드 시스템'(더 큰 시스템의 일부를 형성하는 작고 간단한 소프트웨어 조각)에 가장 잘 사용됩니다. 또한 규칙이 거의 없는 전문화된 도메인에도 이상적입니다. 이는 도메인별 속성을 검증하기 위한 도구를 수정하기 쉽게 만들기 때문입니다.
스마트 계약은 어느 정도까지는 두 요구 사항을 모두 충족합니다. 예를 들어, 이더리움 계약의 작은 크기는 형식 검증에 적합하게 만듭니다. 마찬가지로, EVM은 간단한 규칙을 따르므로 EVM에서 실행되는 프로그램의 의미론적 속성을 지정하고 검증하기가 더 쉽습니다.
더 빠른 개발 주기
모델 체킹 및 기호 실행과 같은 형식 검증 기술은 일반적으로 스마트 계약 코드의 일반적인 분석(테스트 또는 감사 중에 수행됨)보다 더 효율적입니다. 이는 형식 검증이 주장을 테스트하기 위해 기호 값에 의존하기 때문입니다('사용자가 n 이더를 인출하려고 하면 어떻게 될까?') 구체적인 값을 사용하는 테스트와는 다릅니다('사용자가 5 이더를 인출하려고 하면 어떻게 될까?').
기호 입력 변수는 여러 클래스의 구체적인 값을 포함할 수 있으므로, 형식 검증 접근 방식은 더 짧은 시간 내에 더 많은 코드 범위를 약속합니다. 효과적으로 사용하면 형식 검증은 개발자의 개발 주기를 가속화할 수 있습니다.
형식 검증은 또한 비용이 많이 드는 설계 오류를 줄여 탈중앙화 애플리케이션(탈중앙화앱) 구축 과정을 개선합니다. 취약점을 수정하기 위해 (가능한 경우) 계약을 업그레이드하려면 코드베이스를 광범위하게 다시 작성하고 개발에 더 많은 노력을 기울여야 합니다. 형식 검증은 테스터와 감사자가 놓칠 수 있는 계약 구현의 많은 오류를 감지하고 계약을 배포하기 전에 이러한 문제를 해결할 충분한 기회를 제공합니다.
형식 검증의 단점
수작업 비용
형식 검증, 특히 인간이 증명기가 정확성 증명을 도출하도록 안내하는 반자동 검증은 상당한 수작업을 필요로 합니다. 또한, 형식 사양을 만드는 것은 높은 수준의 기술을 요구하는 복잡한 활동입니다.
이러한 요인(노력과 기술)은 형식 검증을 테스트 및 감사와 같은 계약의 정확성을 평가하는 일반적인 방법에 비해 더 까다롭고 비용이 많이 들게 만듭니다. 그럼에도 불구하고, 스마트 계약 구현의 오류 비용을 감안할 때 전체 검증 감사 비용을 지불하는 것은 실용적입니다.
거짓 음성
형식 검증은 스마트 계약의 실행이 형식 사양과 일치하는지 여부만 확인할 수 있습니다. 따라서 사양이 스마트 계약의 예상 동작을 올바르게 설명하는지 확인하는 것이 중요합니다.
사양이 잘못 작성되면, 속성 위반(취약한 실행을 가리킴)이 형식 검증 감사에 의해 감지될 수 없습니다. 이 경우 개발자는 계약에 버그가 없다고 잘못 가정할 수 있습니다.
성능 문제
형식 검증은 여러 성능 문제에 부딪힙니다. 예를 들어, 모델 체킹 및 기호 체킹 중에 각각 발생하는 상태 및 경로 폭발 문제는 검증 절차에 영향을 미칠 수 있습니다. 또한 형식 검증 도구는 종종 기본 레이어에서 SMT 솔버 및 기타 제약 조건 솔버를 사용하며, 이러한 솔버는 계산 집약적인 절차에 의존합니다.
또한 프로그램이 절대 종료되지 않을 수 있기 때문에 프로그램 검증기가 속성(논리 공식으로 설명됨)이 만족될 수 있는지 여부를 항상 결정할 수 있는 것은 아닙니다('결정 문제 (opens in a new tab)'). 따라서 잘 명시되어 있더라도 계약에 대한 일부 속성을 증명하는 것이 불가능할 수 있습니다.
이더리움 스마트 계약을 위한 형식 검증 도구
형식 사양 생성을 위한 사양 언어
Act: Act는 저장소 업데이트, 사전/사후 조건 및 계약 불변성의 사양을 허용합니다. 해당 도구 제품군에는 Coq, SMT 솔버 또는 hevm을 통해 많은 속성을 증명할 수 있는 증명 백엔드도 있습니다.
Scribble - Scribble은 Scribble 사양 언어의 코드 주석을 사양을 확인하는 구체적인 주장으로 변환합니다.
Dafny - Dafny는 코드의 정확성을 추론하고 증명하기 위해 상위 수준 주석에 의존하는 검증 준비 프로그래밍 언어입니다.
정확성 확인을 위한 프로그램 검증기
Certora Prover - Certora Prover는 스마트 계약의 코드 정확성을 확인하기 위한 자동 형식 검증 도구입니다. 사양은 CVL(Certora Verification Language)로 작성되며, 속성 위반은 정적 분석과 제약 조건 해결의 조합을 사용하여 감지됩니다.
Solidity SMTChecker - Solidity의 SMTChecker는 SMT(Satisfiability Modulo Theories) 및 Horn 해결을 기반으로 하는 내장 모델 체커입니다. 컴파일 중에 계약의 소스 코드가 사양과 일치하는지 확인하고 안전 속성 위반을 정적으로 확인합니다.
solc-verify - solc-verify는 주석 및 모듈식 프로그램 검증을 사용하여 Solidity 코드에 대한 자동 형식 검증을 수행할 수 있는 Solidity 컴파일러의 확장 버전입니다.
KEVM - KEVM은 K 프레임워크로 작성된 이더리움 가상 머신(EVM)의 형식 의미론입니다. KEVM은 실행 가능하며 도달 가능성 논리를 사용하여 특정 속성 관련 주장을 증명할 수 있습니다.
정리 증명을 위한 논리적 프레임워크
Isabelle - Isabelle/HOL은 수학 공식을 형식 언어로 표현하고 해당 공식을 증명하기 위한 도구를 제공하는 증명 보조 도구입니다. 주요 애플리케이션은 수학적 증명의 형식화, 특히 컴퓨터 하드웨어 또는 소프트웨어의 정확성을 증명하고 컴퓨터 언어 및 프로토콜의 속성을 증명하는 것을 포함하는 형식 검증입니다.
Rocq - Rocq는 정리를 사용하여 프로그램을 정의하고 기계 검사된 정확성 증명을 대화형으로 생성할 수 있는 대화형 정리 증명기입니다.
스마트 계약의 취약한 패턴을 감지하기 위한 기호 실행 기반 도구
Manticore - 기호 실행을 기반으로 하는 EVM 바이트코드 분석 도구.
hevm - hevm은 EVM 바이트코드에 대한 기호 실행 엔진 및 등가성 검사기입니다.
Mythril - 이더리움 스마트 계약의 취약점을 감지하기 위한 기호 실행 도구