Formal Verification of Smart Contracts

신건우(Thomas Shin)
Nov 4 · 9 min read

이번에 참석한 devcon5에서 다양한 주제의 발표를 들을 수 있었습니다. 그 중 저는 Formal Verification에 대한 내용이 인상적이였고 이에 대한 내용을 정리해 소개하고자 합니다. Formal Verification은 스마트 컨트랙트의 보안성을 한층 업그레이드 시킬 수 있는 기술로 활발히 연구, 개발되고 있습니다.

Correctness of Smart Contract

Solidity 언어로 작성된 컨트랙트는 컴파일된 후 bytecode로 블록체인에 저장됩니다. 배포된 Contract는 누구든 실행할 수 있기 때문에 컨트랙트에 취약점이 발견된다면 그에 따른 문제가 발생할 수 있습니다. 또한 한번 배포된 컨트랙트 코드는 수정할 수 없기 때문에, 컨트랙트를 배포하기 전에 항상 컨트랙트의 Correctness를 검증해야만 합니다.

“Correctness를 검증한다”라는 의미는 컨트랙트의 소스 코드(또는 알고리즘)가 Specification에 맞게 정확하고(Precisely)도 완전하게(Totally) 동작함을 의미합니다.

보통 컨트랙트의 Correctness를 검증하기 위해서는 테스트 코드를 작성하고 추가로 오딧팅 작업까지 수행을 합니다. 하지만 여기서 의문은 테스트 코드를 작성하고 오딧팅을 했다고 해서 스마트 컨트랙트의 Correctness를 100%로 보장할 수 있는가”입니다.

이에 따른 대안으로 나온 개념이 Formal Verification이고 오사카에서 열린 devcon5에서도 이에 대한 발표가 있었습니다. 그렇다면 Formal Verification이 어떻게 스마트 컨트랙트의 Correctness를 완전히 보장할 수 있을까요?

Formal Verification

Formal Verification이란, 예를 들어, Program인 P와 Property인 S가 Input 값으로 주어졌을 때, P가 어떻게 동작을 하든 항상 PS라는 Property를 만족함을 증명하는 것을 말합니다.

이를 위해서는 수학적인 모델링이 필요합니다. 즉 기존의 Solidity Specification으로부터 수학적인 모델링을 통해 Formal Specification을 만듭니다. 예를 들어 `A`라는 기능을 테스트할 때 보통 특정 데이터의 Single set만을 이용합니다. 그러나 Specification는 “모든 Set에 대해서 `A`라는 기능이 정상적으로 동작함.”을 가정하고 있습니다. 그렇기 때문에 Formal Specification는 `A`라는 기능이 모든 Set에 대해 정상적으로 동작함을 검증하기 위해 모든 상태/조건 등을 고려한 수학적 모델링으로 재탄생하게 됩니다.

이렇게 작성된 Refined Specification(Formal Specification)은 Solidity-level에서 작성되지 않고 bytecode-level에서 작성됩니다. 그 이유는 다음과 같습니다.

  1. bytecode로 작성된 Specification이 있다면, EVM을 다루는 모든 high-level 언어에서도 이를 이용할 수 있다는 장점이 있습니다.
  2. Solidity-level에서 작성된 Specification 같은 경우, EVM 내에서 발생하는 stack size limit 문제나 gas calculation과 같은 문제를 커버할 수 없습니다.
  3. Correctness가 입증된 Solidity 코드라 할지라도 Solidity 컴파일러 자체 버그로 인해 잘못된 bytecode가 생성될 수 있습니다.

Formal Specification은 Dapphub/klab에서 개발한 specification language(eg. eDSL)를 사용해 만들 수 있습니다.

Formal Specification은 4가지 섹션으로 구분해 작성합니다.

  • Preamble: behaviour와 interface의 헤더를 가집니다. 이는 어떤 Contract으로부터 어떤 function의 기능을 검증할 것인가에 대해 작성합니다.
  • Types: 타입을 선언합니다.
  • Statements of our semantic claim: storage 헤더를 가집니다. 이 섹션에서는 <X> |-> <Y> => <Z>의 표현식이 사용됩니다. 이 표현식은 “Storage Slot, X에 있는 Y라는 값이 execution 이후에 Z가 됨”을 나타냅니다.
  • Assumption of our semantic claim: iffif 절을 가집니다. iff는 해당 조건이 만족하지 않았을 때 revert를 시키게 되고, if는 단순 if절의 기능을 담당합니다.

Time to Verify

Formal Specification을 만든 뒤에는 컨트랙트의 bytecode와 Formal Specification이 매칭되는지 검증해야 합니다. 이 과정이 바로 Formal Verification입니다. 하지만 Formal Verification을 하기 위해서는 추가로 필요한 것이 있는데 바로 EVM의 semantic입니다. EVM의 semantic 또한 수학적 모델링을 통해 만들어집니다. EVM의 semantic은 K-framework에서 만든 KEVM이 있습니다.

Ethereum Virtual Machine Semantics에 따라 컨트랙트의 bytecode와 Formal Specification의 매칭을 검증합니다. 이러한 검증을 도와주는 프레임워크가 있는데 바로 K-framework입니다. K-framework에서는 Formal Verification을 위한 specification language 및 여러 툴들을 제공합니다.

K-framework

K-framework에서 제공해주는 툴은 다음과 같습니다.

  • K language: Semantic을 작성하는 언어입니다.
  • Z3: Semantic을 검증하는 툴입니다. 이 툴은 automatic proving을 위한 것으로 Microsoft Research로부터 개발되었습니다.
  • KEVM: EVM의 Semantics을 작성한 것입니다. KEVM은 Everett Hildenbrandt에 의해 작성되었습니다.
  • EDSL: Formal Specification과 같이 high-level semantic을 작성하기 위한 specification language입니다.

K-framework에서는 위에서 소개한 툴을 이용해 Formal Verification을 수행합니다.

우선 Solidity 코드로부터 컴파일된 bytecode와 EDSL로 작성된 Formal Specification을 컴파일 합니다. 컴파일 이후, KEVM semantic을 사용해서 bytecode와 Formal Specification의 매칭을 검증하게 됩니다. 이 검증은 Z3가 수행하고 검증 결과를 도출합니다.


Formal Verification을 하기 위한 절차는 매우 복잡해보입니다. 하지만 이미 Formal Verification을 위한 여러 툴들이 제공되고 있으며, 단순히 우리가 추가로 만들어야 하는 것은 Formal Specification입니다. Formal Specification을 만드는 일 역시 쉬운 일은 아니지만 컨트랙트의 요구사항을 잘 분석하고 specification language에 익숙해진다면 누구나 Formal Verification을 할 수 있다고 생각합니다.

앞으로 블록체인이 더 발전함에 따라 컨트랙트의 보안성 역시 더욱 중요해질 것입니다. 그렇기 때문에 Formal Verfication이라는 기술은 매우 Practical해보이고 컨트랙트 개발자라면 한번쯤 분석해보고 사용해보시는 것을 권해드립니다.

Reference

Onther-Tech

Building an Ethereum Blockchain ECO system to Change the World

신건우(Thomas Shin)

Written by

Onther-Tech

Building an Ethereum Blockchain ECO system to Change the World

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade