본문으로 건너뛰기
Change page

스마트 컨트랙트 정형 검증

페이지 편집 (opens in a new tab)

스마트 컨트랙트는 새로운 사용 사례를 도입하고 사용자를 위한 가치를 창출하는 탈중앙화된 무신뢰 기반의 강력한 애플리케이션을 만들 수 있게 해줍니다. 스마트 컨트랙트는 막대한 가치를 다루기 때문에, 보안은 개발자에게 매우 중요한 고려 사항입니다.

정형 검증은 스마트 컨트랙트 보안을 향상시키기 위해 권장되는 기법 중 하나입니다. 프로그램을 명세, 설계 및 검증하기 위해 정형 기법(formal methods) (opens in a new tab)을 사용하는 정형 검증은 중요한 하드웨어 및 소프트웨어 시스템의 정확성을 보장하기 위해 수년 동안 사용되어 왔습니다.

스마트 컨트랙트에 구현될 때, 정형 검증은 컨트랙트의 비즈니스 로직이 사전 정의된 명세를 충족함을 증명할 수 있습니다. 테스트와 같이 컨트랙트 코드의 정확성을 평가하는 다른 방법과 비교할 때, 정형 검증은 스마트 컨트랙트가 기능적으로 정확하다는 더 강력한 보장을 제공합니다.

정형 검증이란 무엇인가요?

정형 검증은 정형 명세(formal specification)를 기준으로 시스템의 정확성을 평가하는 과정을 의미합니다. 간단히 말해, 정형 검증을 통해 시스템의 동작이 특정 요구 사항을 충족하는지(즉, 우리가 원하는 대로 작동하는지) 확인할 수 있습니다.

시스템(이 경우 스마트 컨트랙트)의 예상되는 동작은 정형 모델링을 사용하여 설명되며, 명세 언어(specification language)를 통해 정형 속성(formal properties)을 생성할 수 있습니다. 그런 다음 정형 검증 기법은 컨트랙트의 구현이 명세를 준수하는지 확인하고 구현의 정확성에 대한 수학적 증명을 도출할 수 있습니다. 컨트랙트가 명세를 충족할 때, 이를 "기능적으로 정확하다(functionally correct)", "설계상 정확하다(correct by design)" 또는 "구조적으로 정확하다(correct by construction)"고 설명합니다.

정형 모델이란 무엇인가요?

컴퓨터 과학에서 정형 모델 (opens in a new tab)은 연산 과정을 수학적으로 설명한 것입니다. 프로그램은 수학적 함수(방정식)로 추상화되며, 모델은 입력이 주어졌을 때 함수의 출력이 어떻게 계산되는지 설명합니다.

정형 모델은 프로그램 동작에 대한 분석을 평가할 수 있는 추상화 수준을 제공합니다. 정형 모델이 존재함으로써 해당 모델의 원하는 속성을 설명하는 정형 명세를 생성할 수 있습니다.

정형 검증을 위해 스마트 컨트랙트를 모델링하는 데 다양한 기법이 사용됩니다. 예를 들어, 일부 모델은 스마트 컨트랙트의 고수준(high-level) 동작을 추론하는 데 사용됩니다. 이러한 모델링 기법은 스마트 컨트랙트에 블랙박스 관점을 적용하여, 입력을 받아들이고 해당 입력을 기반으로 연산을 실행하는 시스템으로 간주합니다.

고수준 모델은 스마트 컨트랙트와 외부 소유 계정(EOA), 컨트랙트 계정 및 블록체인 환경과 같은 외부 에이전트 간의 관계에 중점을 둡니다. 이러한 모델은 특정 사용자 상호 작용에 대한 응답으로 컨트랙트가 어떻게 동작해야 하는지 지정하는 속성을 정의하는 데 유용합니다.

반대로, 다른 정형 모델은 스마트 컨트랙트의 저수준(low-level) 동작에 중점을 둡니다. 고수준 모델은 컨트랙트의 기능을 추론하는 데 도움이 될 수 있지만, 구현의 내부 작동에 대한 세부 정보를 포착하지 못할 수 있습니다. 저수준 모델은 프로그램 분석에 화이트박스 관점을 적용하며, 프로그램 트레이스(traces) 및 제어 흐름 그래프(control flow graphs) (opens in a new tab)와 같은 스마트 컨트랙트 애플리케이션의 저수준 표현에 의존하여 컨트랙트 실행과 관련된 속성을 추론합니다.

저수준 모델은 이더리움의 실행 환경(즉, EVM)에서 스마트 컨트랙트의 실제 실행을 나타내기 때문에 이상적인 것으로 간주됩니다. 저수준 모델링 기법은 스마트 컨트랙트에서 중요한 안전성 속성을 확립하고 잠재적인 취약점을 탐지하는 데 특히 유용합니다.

정형 명세란 무엇인가요?

명세는 단순히 특정 시스템이 충족해야 하는 기술적 요구 사항입니다. 프로그래밍에서 명세는 프로그램 실행에 대한 일반적인 아이디어(즉, 프로그램이 수행해야 하는 작업)를 나타냅니다.

스마트 컨트랙트의 맥락에서 정형 명세는 속성(properties)을 의미하며, 이는 컨트랙트가 충족해야 하는 요구 사항에 대한 정형적인 설명입니다. 이러한 속성은 "불변성(invariants)"으로 설명되며, 예외 없이 모든 가능한 상황에서 항상 참이어야 하는 컨트랙트 실행에 대한 논리적 단언(assertions)을 나타냅니다.

따라서 정형 명세는 스마트 컨트랙트의 의도된 실행을 설명하는 정형 언어로 작성된 명령문 모음이라고 생각할 수 있습니다. 명세는 컨트랙트의 속성을 다루며 다양한 상황에서 컨트랙트가 어떻게 동작해야 하는지 정의합니다. 정형 검증의 목적은 스마트 컨트랙트가 이러한 속성(불변성)을 가지고 있는지, 그리고 실행 중에 이러한 속성이 위반되지 않는지 확인하는 것입니다.

정형 명세는 스마트 컨트랙트의 안전한 구현을 개발하는 데 매우 중요합니다. 불변성을 구현하지 못하거나 실행 중에 속성이 위반되는 컨트랙트는 기능을 손상시키거나 악의적인 익스플로잇을 유발할 수 있는 취약점에 노출되기 쉽습니다.

스마트 컨트랙트를 위한 정형 명세의 유형

정형 명세는 프로그램 실행의 정확성에 대한 수학적 추론을 가능하게 합니다. 정형 모델과 마찬가지로 정형 명세는 고수준 속성이나 컨트랙트 구현의 저수준 동작을 포착할 수 있습니다.

정형 명세는 프로그램의 속성에 대한 정형적 추론을 허용하는 프로그램 논리(program logic) (opens in a new tab)의 요소를 사용하여 도출됩니다. 프로그램 논리에는 프로그램의 예상되는 동작을 (수학적 언어로) 표현하는 정형 규칙이 있습니다. 정형 명세를 생성하는 데에는 도달 가능성 논리(reachability logic) (opens in a new tab), 시제 논리(temporal logic) (opens in a new tab) 및 호어 논리(Hoare logic) (opens in a new tab)를 포함한 다양한 프로그램 논리가 사용됩니다.

스마트 컨트랙트에 대한 정형 명세는 크게 고수준 또는 저수준 명세로 분류할 수 있습니다. 명세가 어떤 범주에 속하든 분석 중인 시스템의 속성을 적절하고 명확하게 설명해야 합니다.

고수준 명세

이름에서 알 수 있듯이 고수준 명세("모델 지향 명세"라고도 함)는 프로그램의 고수준 동작을 설명합니다. 고수준 명세는 스마트 컨트랙트를 연산을 수행하여 상태 간에 전환할 수 있는 유한 상태 기계(finite state machine, FSM) (opens in a new tab)로 모델링하며, FSM 모델의 정형 속성을 정의하는 데 시제 논리가 사용됩니다.

시제 논리 (opens in a new tab)는 "시간의 관점에서 한정된 명제를 추론하기 위한 규칙(예: "나는 항상 배가 고프다" 또는 "나는 결국 배가 고플 것이다")"입니다. 정형 검증에 적용될 때 시제 논리는 상태 기계로 모델링된 시스템의 올바른 동작에 대한 단언을 명시하는 데 사용됩니다. 구체적으로, 시제 논리는 스마트 컨트랙트가 가질 수 있는 미래 상태와 상태 간의 전환 방법을 설명합니다.

고수준 명세는 일반적으로 스마트 컨트랙트에 대한 두 가지 중요한 시제 속성인 안전성(safety)과 활성(liveness)을 포착합니다. 안전성 속성은 "나쁜 일은 절대 일어나지 않는다"는 개념을 나타내며 주로 불변성을 표현합니다. 안전성 속성은 교착 상태(deadlock) (opens in a new tab)가 없는 것과 같은 일반적인 소프트웨어 요구 사항을 정의하거나 컨트랙트에 대한 도메인별 속성(예: 함수에 대한 접근 제어의 불변성, 상태 변수의 허용 가능한 값 또는 토큰 전송 조건)을 표현할 수 있습니다.

ERC-20 토큰 컨트랙트에서 transfer() 또는 transferFrom() 사용 조건을 다루는 다음 안전성 요구 사항을 예로 들어 보겠습니다. "발신자의 잔액은 전송하도록 요청된 토큰 양보다 절대 적을 수 없습니다." 컨트랙트 불변성에 대한 이러한 자연어 설명은 정형(수학적) 명세로 변환될 수 있으며, 그런 다음 유효성을 엄격하게 확인할 수 있습니다.

활성 속성은 "결국 좋은 일이 일어난다"고 단언하며 컨트랙트가 다른 상태로 진행할 수 있는 능력과 관련이 있습니다. 활성 속성의 예로는 "유동성"이 있으며, 이는 요청 시 컨트랙트가 잔액을 사용자에게 전송할 수 있는 능력을 의미합니다. 이 속성이 위반되면 Parity 지갑 사건 (opens in a new tab)에서 발생한 것처럼 사용자는 컨트랙트에 저장된 자산을 인출할 수 없게 됩니다.

저수준 명세

고수준 명세는 컨트랙트의 유한 상태 모델을 출발점으로 삼고 이 모델의 원하는 속성을 정의합니다. 대조적으로, 저수준 명세("속성 지향 명세"라고도 함)는 종종 프로그램(스마트 컨트랙트)을 수학적 함수 모음으로 구성된 시스템으로 모델링하고 이러한 시스템의 올바른 동작을 설명합니다.

간단히 말해, 저수준 명세는 프로그램 트레이스를 분석하고 이러한 트레이스에 대한 스마트 컨트랙트의 속성을 정의하려고 시도합니다. 트레이스는 스마트 컨트랙트의 상태를 변경하는 함수 실행의 시퀀스를 의미합니다. 따라서 저수준 명세는 컨트랙트의 내부 실행에 대한 요구 사항을 지정하는 데 도움이 됩니다.

저수준 정형 명세는 호어(Hoare) 스타일 속성 또는 실행 경로의 불변성으로 주어질 수 있습니다.

호어 스타일 속성

호어 논리 (opens in a new tab)는 스마트 컨트랙트를 포함한 프로그램의 정확성을 추론하기 위한 일련의 정형 규칙을 제공합니다. 호어 스타일 속성은 호어 트리플(Hoare triple) {P}c{Q}로 표현되며, 여기서 c는 프로그램이고 P와 Q는 c(즉, 프로그램)의 상태에 대한 술어(predicates)로서 각각 사전 조건(preconditions)과 사후 조건(postconditions)으로 정형적으로 설명됩니다.

사전 조건은 함수의 올바른 실행에 필요한 조건을 설명하는 술어입니다. 컨트랙트를 호출하는 사용자는 이 요구 사항을 충족해야 합니다. 사후 조건은 함수가 올바르게 실행될 경우 확립되는 조건을 설명하는 술어입니다. 사용자는 함수를 호출한 후 이 조건이 참일 것으로 예상할 수 있습니다. 호어 논리에서 불변성은 함수의 실행에 의해 보존되는(즉, 변경되지 않는) 술어입니다.

호어 스타일 명세는 부분적 정확성(partial correctness) 또는 전체적 정확성(total correctness)을 보장할 수 있습니다. 함수가 실행되기 전에 사전 조건이 참이고 실행이 종료될 때 사후 조건도 참이라면 컨트랙트 함수의 구현은 "부분적으로 정확"합니다. 함수가 실행되기 전에 사전 조건이 참이고 실행이 종료됨이 보장되며 종료 시 사후 조건이 참이라면 전체적 정확성에 대한 증명을 얻게 됩니다.

일부 실행은 종료되기 전에 지연되거나 전혀 종료되지 않을 수 있으므로 전체적 정확성에 대한 증명을 얻는 것은 어렵습니다. 그렇긴 하지만, 이더리움의 가스 메커니즘이 무한 프로그램 루프를 방지하기 때문에(실행이 성공적으로 종료되거나 '가스 부족(out-of-gas)' 오류로 인해 종료됨) 실행이 종료되는지 여부에 대한 질문은 사실상 무의미한 논쟁일 수 있습니다.

호어 논리를 사용하여 생성된 스마트 컨트랙트 명세에는 컨트랙트의 함수 및 루프 실행에 대해 정의된 사전 조건, 사후 조건 및 불변성이 있습니다. 사전 조건에는 종종 함수에 대한 잘못된 입력의 가능성이 포함되며, 사후 조건은 이러한 입력에 대한 예상 응답(예: 특정 예외 발생)을 설명합니다. 이러한 방식으로 호어 스타일 속성은 컨트랙트 구현의 정확성을 보장하는 데 효과적입니다.

많은 정형 검증 프레임워크는 함수의 의미론적 정확성을 증명하기 위해 호어 스타일 명세를 사용합니다. 또한 Solidity에서 require 및 assert 문을 사용하여 호어 스타일 속성을 (단언으로서) 컨트랙트 코드에 직접 추가할 수도 있습니다.

require문은 사전 조건 또는 불변성을 표현하며 종종 사용자 입력을 검증하는 데 사용되는 반면, assert는 안전성에 필요한 사후 조건을 포착합니다. 예를 들어, 함수에 대한 적절한 접근 제어(안전성 속성의 예)는 호출 계정의 신원에 대한 사전 조건 검사로 require문을 사용하여 달성할 수 있습니다. 유사하게, 컨트랙트의 상태 변수의 허용 가능한 값(예: 유통되는 총 토큰 수)에 대한 불변성은 함수 실행 후 컨트랙트의 상태를 확인하기 위해 assert를 사용하여 위반으로부터 보호될 수 있습니다.

트레이스 수준 속성

트레이스 기반 명세는 컨트랙트를 다른 상태로 전환하는 연산과 이러한 연산 간의 관계를 설명합니다. 앞서 설명했듯이 트레이스는 특정 방식으로 컨트랙트의 상태를 변경하는 연산의 시퀀스입니다.

이 접근 방식은 스마트 컨트랙트를 사전 정의된 전환 세트(컨트랙트 함수로 설명됨)와 함께 일부 사전 정의된 상태(상태 변수로 설명됨)를 갖는 상태 전환 시스템으로 모델링하는 것에 의존합니다. 또한 프로그램의 실행 흐름을 그래픽으로 표현한 제어 흐름 그래프 (opens in a new tab)(CFG)가 컨트랙트의 연산 의미론을 설명하는 데 종종 사용됩니다. 여기서 각 트레이스는 제어 흐름 그래프의 경로로 표현됩니다.

주로 트레이스 수준 명세는 스마트 컨트랙트의 내부 실행 패턴을 추론하는 데 사용됩니다. 트레이스 수준 명세를 생성함으로써 스마트 컨트랙트에 허용되는 실행 경로(즉, 상태 전환)를 단언합니다. 기호 실행(symbolic execution)과 같은 기법을 사용하여 실행이 정형 모델에 정의되지 않은 경로를 절대 따르지 않음을 정형적으로 검증할 수 있습니다.

트레이스 수준 속성을 설명하기 위해 공개적으로 접근 가능한 일부 함수가 있는 DAO 컨트랙트의 예를 사용해 보겠습니다. 여기서 DAO 컨트랙트는 사용자가 다음 연산을 수행할 수 있도록 허용한다고 가정합니다.

  • 자금 예치

  • 자금 예치 후 제안에 투표

  • 제안에 투표하지 않은 경우 환불 청구

트레이스 수준 속성의 예로는 "자금을 예치하지 않은 사용자는 제안에 투표할 수 없다" 또는 "제안에 투표하지 않은 사용자는 항상 환불을 청구할 수 있어야 한다"가 있을 수 있습니다. 두 속성 모두 선호되는 실행 시퀀스를 단언합니다(투표는 자금을 예치하기 전에 발생할 수 없으며 환불 청구는 제안에 투표한 후에 발생할 수 없습니다).

스마트 컨트랙트의 정형 검증 기법

모델 검사

모델 검사(Model checking)는 알고리즘이 스마트 컨트랙트의 정형 모델을 명세와 대조하여 확인하는 정형 검증 기법입니다. 모델 검사에서 스마트 컨트랙트는 종종 상태 전환 시스템으로 표현되는 반면, 허용 가능한 컨트랙트 상태에 대한 속성은 시제 논리를 사용하여 정의됩니다.

모델 검사에는 시스템(즉, 컨트랙트)의 추상적인 수학적 표현을 생성하고 명제 논리(propositional logic) (opens in a new tab)에 뿌리를 둔 공식을 사용하여 이 시스템의 속성을 표현하는 작업이 필요합니다. 이는 수학적 모델이 주어진 논리 공식을 충족함을 증명하는 모델 검사 알고리즘의 작업을 단순화합니다.

정형 검증의 모델 검사는 주로 시간에 따른 컨트랙트의 동작을 설명하는 시제 속성을 평가하는 데 사용됩니다. 스마트 컨트랙트의 시제 속성에는 앞서 설명한 안전성과 활성이 포함됩니다.

예를 들어, 접근 제어와 관련된 보안 속성(예: 컨트랙트의 소유자만 selfdestruct를 호출할 수 있음)은 정형 논리로 작성될 수 있습니다. 그 후 모델 검사 알고리즘은 컨트랙트가 이 정형 명세를 충족하는지 검증할 수 있습니다.

모델 검사는 상태 공간 탐색(state space exploration)을 사용하는데, 이는 스마트 컨트랙트의 모든 가능한 상태를 구성하고 속성 위반을 초래하는 도달 가능한 상태를 찾으려고 시도하는 것을 포함합니다. 그러나 이는 무한한 수의 상태("상태 폭발 문제"로 알려짐)로 이어질 수 있으므로 모델 검사기는 스마트 컨트랙트의 효율적인 분석을 가능하게 하기 위해 추상화 기법에 의존합니다.

정리 증명

정리 증명(Theorem proving)은 스마트 컨트랙트를 포함한 프로그램의 정확성에 대해 수학적으로 추론하는 방법입니다. 여기에는 컨트랙트 시스템의 모델과 그 명세를 수학적 공식(논리 명령문)으로 변환하는 작업이 포함됩니다.

정리 증명의 목적은 이러한 명령문 간의 논리적 동치(logical equivalence)를 검증하는 것입니다. "논리적 동치"("논리적 쌍조건문"이라고도 함)는 첫 번째 명령문이 참일 때 그리고 오직 그때만 두 번째 명령문이 참이 되는 두 명령문 간의 관계 유형입니다.

컨트랙트의 모델과 그 속성에 대한 명령문 간의 필수 관계(논리적 동치)는 증명 가능한 명령문(정리라고 함)으로 공식화됩니다. 정형 추론 시스템을 사용하여 자동화된 정리 증명자(theorem prover)는 정리의 유효성을 검증할 수 있습니다. 즉, 정리 증명자는 스마트 컨트랙트의 모델이 명세와 정확히 일치함을 결정적으로 증명할 수 있습니다.

모델 검사가 컨트랙트를 유한 상태를 가진 전환 시스템으로 모델링하는 반면, 정리 증명은 무한 상태 시스템의 분석을 처리할 수 있습니다. 그러나 이는 자동화된 정리 증명자가 논리 문제가 "결정 가능(decidable)"한지 여부를 항상 알 수는 없음을 의미합니다.

결과적으로 정리 증명자가 정확성 증명을 도출하도록 안내하기 위해 종종 사람의 지원이 필요합니다. 정리 증명에 사람의 노력을 사용하면 완전히 자동화된 모델 검사보다 사용하는 데 비용이 더 많이 듭니다.

기호 실행

기호 실행(Symbolic execution)은 구체적인 값(예: x == 5) 대신 기호 값(예: x > 5)을 사용하여 함수를 실행함으로써 스마트 컨트랙트를 분석하는 방법입니다. 정형 검증 기법으로서 기호 실행은 컨트랙트 코드의 트레이스 수준 속성에 대해 정형적으로 추론하는 데 사용됩니다.

기호 실행은 실행 트레이스를 기호 입력 값에 대한 수학적 공식으로 나타내며, 이를 경로 술어(path predicate)라고도 합니다. SMT 솔버 (opens in a new tab)는 경로 술어가 "충족 가능한지"(즉, 공식을 충족할 수 있는 값이 존재하는지) 확인하는 데 사용됩니다. 취약한 경로가 충족 가능하면 SMT 솔버는 실행을 해당 경로로 유도하는 구체적인 값을 생성합니다.

스마트 컨트랙트의 함수가 uint 값(x)을 입력으로 사용하고 x가 5보다 크고 10보다 작을 때 되돌린다(revert)고 가정해 보겠습니다. 일반적인 테스트 절차를 사용하여 오류를 트리거하는 x 값을 찾으려면 실제로 오류를 트리거하는 입력을 찾는다는 보장 없이 수십 개(또는 그 이상)의 테스트 케이스를 실행해야 합니다.

반대로 기호 실행 도구는 기호 값 X > 5 ∧ X < 10(즉, x가 5보다 크고 AND x가 10보다 작음)를 사용하여 함수를 실행합니다. 그런 다음 연관된 경로 술어 x = X > 5 ∧ X < 10가 SMT 솔버에 주어져 해결됩니다. 특정 값이 공식 x = X > 5 ∧ X < 10를 충족하면 SMT 솔버가 이를 계산합니다. 예를 들어 솔버는 x의 값으로 7을 생성할 수 있습니다.

기호 실행은 프로그램에 대한 입력에 의존하고 도달 가능한 모든 상태를 탐색하기 위한 입력 세트가 잠재적으로 무한하기 때문에 여전히 테스트의 한 형태입니다. 그러나 예제에서 볼 수 있듯이 기호 실행은 속성 위반을 트리거하는 입력을 찾는 데 일반 테스트보다 더 효율적입니다.

또한 기호 실행은 함수에 대한 입력을 무작위로 생성하는 다른 속성 기반 기법(예: 퍼징)보다 오탐(false positives)을 덜 생성합니다. 기호 실행 중에 오류 상태가 트리거되면 오류를 트리거하는 구체적인 값을 생성하고 문제를 재현할 수 있습니다.

기호 실행은 또한 어느 정도의 수학적 정확성 증명을 제공할 수 있습니다. 오버플로 보호 기능이 있는 컨트랙트 함수의 다음 예를 고려해 보세요.

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

정수 오버플로를 초래하는 실행 트레이스는 다음 공식을 충족해야 합니다. z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) 이러한 공식은 해결될 가능성이 낮으므로 safe_add 함수가 절대 오버플로되지 않는다는 수학적 증명 역할을 합니다.

스마트 컨트랙트에 정형 검증을 사용하는 이유는 무엇인가요?

신뢰성의 필요성

정형 검증은 실패할 경우 사망, 부상 또는 재정적 파탄과 같은 파괴적인 결과를 초래할 수 있는 안전 필수 시스템의 정확성을 평가하는 데 사용됩니다. 스마트 컨트랙트는 막대한 양의 가치를 제어하는 고가치 애플리케이션이며, 설계상의 단순한 오류로 인해 사용자에게 돌이킬 수 없는 손실 (opens in a new tab)이 발생할 수 있습니다. 그러나 배포 전에 컨트랙트를 정형적으로 검증하면 블록체인에서 실행될 때 예상대로 수행될 것이라는 보장을 높일 수 있습니다.

신뢰성은 모든 스마트 컨트랙트에서 매우 요구되는 품질이며, 특히 이더리움 가상 머신(EVM)에 배포된 코드는 일반적으로 불변이기 때문입니다. 출시 후 업그레이드에 쉽게 접근할 수 없기 때문에 컨트랙트의 신뢰성을 보장해야 할 필요성으로 인해 정형 검증이 필수적입니다. 정형 검증은 감사자(auditors)와 테스터가 놓칠 수 있는 정수 언더플로 및 오버플로, 재진입(re-entrancy), 열악한 가스 최적화와 같은 까다로운 문제를 탐지할 수 있습니다.

기능적 정확성 증명

프로그램 테스트는 스마트 컨트랙트가 일부 요구 사항을 충족함을 증명하는 가장 일반적인 방법입니다. 여기에는 처리할 것으로 예상되는 데이터 샘플로 컨트랙트를 실행하고 그 동작을 분석하는 작업이 포함됩니다. 컨트랙트가 샘플 데이터에 대해 예상된 결과를 반환하면 개발자는 정확성에 대한 객관적인 증거를 갖게 됩니다.

그러나 이 접근 방식은 샘플의 일부가 아닌 입력 값에 대한 올바른 실행을 증명할 수 없습니다. 따라서 컨트랙트를 테스트하면 버그를 탐지하는 데 도움이 될 수 있지만(즉, 일부 코드 경로가 실행 중에 원하는 결과를 반환하지 못하는 경우), 버그가 없음을 결정적으로 증명할 수는 없습니다.

반대로 정형 검증은 컨트랙트를 전혀 실행하지 않고도 스마트 컨트랙트가 무한한 범위의 실행에 대한 요구 사항을 충족함을 정형적으로 증명할 수 있습니다. 이를 위해서는 올바른 컨트랙트 동작을 정확하게 설명하는 정형 명세를 생성하고 컨트랙트 시스템의 정형(수학적) 모델을 개발해야 합니다. 그런 다음 정형 증명 절차를 따라 컨트랙트의 모델과 명세 간의 일관성을 확인할 수 있습니다.

정형 검증을 사용하면 컨트랙트의 비즈니스 로직이 요구 사항을 충족하는지 검증하는 문제는 증명하거나 반증할 수 있는 수학적 명제가 됩니다. 명제를 정형적으로 증명함으로써 유한한 수의 단계로 무한한 수의 테스트 케이스를 검증할 수 있습니다. 이러한 방식으로 정형 검증은 명세와 관련하여 컨트랙트가 기능적으로 정확함을 증명할 더 나은 전망을 가지고 있습니다.

이상적인 검증 대상

검증 대상은 정형적으로 검증할 시스템을 설명합니다. 정형 검증은 "임베디드 시스템"(더 큰 시스템의 일부를 구성하는 작고 단순한 소프트웨어 조각)에서 가장 잘 사용됩니다. 또한 규칙이 거의 없는 특수 도메인에 이상적인데, 이는 도메인별 속성을 검증하기 위한 도구를 수정하기 더 쉽게 만들기 때문입니다.

스마트 컨트랙트는 적어도 어느 정도는 두 가지 요구 사항을 모두 충족합니다. 예를 들어, 이더리움 컨트랙트의 작은 크기는 정형 검증을 용이하게 합니다. 유사하게, EVM은 간단한 규칙을 따르므로 EVM에서 실행되는 프로그램의 의미론적 속성을 지정하고 검증하기가 더 쉽습니다.

더 빠른 개발 주기

모델 검사 및 기호 실행과 같은 정형 검증 기법은 일반적으로 (테스트 또는 감사 중에 수행되는) 스마트 컨트랙트 코드의 일반적인 분석보다 더 효율적입니다. 이는 구체적인 값을 사용하는 테스트("사용자가 5 이더를 인출하려고 하면 어떻게 될까?")와 달리 정형 검증은 기호 값을 사용하여 단언을 테스트("사용자가 n 이더를 인출하려고 하면 어떻게 될까?")하기 때문입니다.

기호 입력 변수는 여러 클래스의 구체적인 값을 포괄할 수 있으므로 정형 검증 접근 방식은 더 짧은 시간 내에 더 많은 코드 커버리지를 약속합니다. 효과적으로 사용될 때 정형 검증은 개발자의 개발 주기를 가속화할 수 있습니다.

정형 검증은 또한 비용이 많이 드는 설계 오류를 줄임으로써 탈중앙화 애플리케이션 (dapp)을 구축하는 프로세스를 개선합니다. 취약점을 수정하기 위해 컨트랙트를 업그레이드하는 것(가능한 경우)은 코드베이스의 광범위한 재작성과 개발에 더 많은 노력을 필요로 합니다. 정형 검증은 테스터와 감사자가 놓칠 수 있는 컨트랙트 구현의 많은 오류를 탐지할 수 있으며 컨트랙트를 배포하기 전에 이러한 문제를 수정할 수 있는 충분한 기회를 제공합니다.

정형 검증의 단점

수작업 비용

정형 검증, 특히 사람이 증명자를 안내하여 정확성 증명을 도출하는 반자동 검증은 상당한 수작업을 필요로 합니다. 더욱이 정형 명세를 생성하는 것은 높은 수준의 기술을 요구하는 복잡한 활동입니다.

이러한 요소(노력과 기술)는 테스트 및 감사와 같이 컨트랙트의 정확성을 평가하는 일반적인 방법에 비해 정형 검증을 더 까다롭고 비용이 많이 들게 만듭니다. 그럼에도 불구하고 스마트 컨트랙트 구현의 오류 비용을 고려할 때 전체 검증 감사에 대한 비용을 지불하는 것은 실용적입니다.

미탐(False negatives)

정형 검증은 스마트 컨트랙트의 실행이 정형 명세와 일치하는지 여부만 확인할 수 있습니다. 따라서 명세가 스마트 컨트랙트의 예상되는 동작을 제대로 설명하는지 확인하는 것이 중요합니다.

명세가 잘못 작성된 경우, 취약한 실행을 가리키는 속성 위반은 정형 검증 감사에서 탐지할 수 없습니다. 이 경우 개발자는 컨트랙트에 버그가 없다고 잘못 가정할 수 있습니다.

성능 문제

정형 검증은 여러 가지 성능 문제에 부딪힙니다. 예를 들어, 모델 검사 및 기호 검사 중에 각각 발생하는 상태 및 경로 폭발 문제는 검증 절차에 영향을 미칠 수 있습니다. 또한 정형 검증 도구는 종종 기본 계층에서 SMT 솔버 및 기타 제약 조건 솔버를 사용하며, 이러한 솔버는 계산 집약적인 절차에 의존합니다.

또한 프로그램이 절대 종료되지 않을 수 있기 때문에 프로그램 검증자가 (논리 공식으로 설명된) 속성이 충족될 수 있는지 여부를 항상 결정할 수 있는 것은 아닙니다("결정 가능성 문제(decidability problem) (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는 정리를 사용하여 프로그램을 정의하고 기계가 확인한 정확성 증명을 대화형으로 생성할 수 있게 해주는 대화형 정리 증명자입니다.

스마트 컨트랙트의 취약한 패턴 탐지를 위한 기호 실행 기반 도구

맨티코어 - 기호 실행을 기반으로 하는 EVM 바이트코드 분석 도구입니다.

hevm - hevm은 EVM 바이트코드를 위한 기호 실행 엔진 및 동치 검사기입니다.

Mythril - 이더리움 스마트 컨트랙트의 취약점을 탐지하기 위한 기호 실행 도구

더 읽어보기

페이지 최근 업데이트: 2026년 4월 28일

shalom-ezekiels (opens in a new tab)
corwintinesc (opens in a new tab)
MOSHKA-GOTM (opens in a new tab)
+12