형식 검증(Formal Verification)

Introduction

형식 검증(Formal verification)은 형식 정의를 사용하여 프로그램이 특정 Specification을 따르는지 확인하는 프로세스입니다. 다시 말하면, 수학을 사용하여 "우리가 만들려고 했던 것을 만들었습니까?" 라는 질문에 답합니다.

반대로 프로그래머는 현재 프로그램이 특정 Specification을 준수하는지 확인하기 위해 단위 테스트(unit test)를 작성합니다. 가능한 한 많은 입력값으로 프로그램을 테스트하고 Specification에 언급 된 내용과 출력값이 일치 하는지 각각 확인합니다. 예를 들어, 프로그램이 숫자 목록을 정확하게 오름차순으로 정렬하는지 테스트하려면[2, 3, 1]입력으로 테스트합니다. 테스트의 결과는[1, 2, 3]이어야 하며 그렇지 않으면 프로그램이 잘못된 것입니다.

그러나 단위 테스트 방법은 가능한 모든 입력 과 극단적인 경우를 처리 할 수 ​​없으며 이로 인해 프로그램이 실패 할 수 있습니다. 이에 대한 해결책은 형식 검증(formal verification)입니다. 형식 검증(formal verification)는 프로그램의 수학적인 정의에 대해서 작성하는 것과 관련이 있습니다. 위에서 주어진 동일한 예를 표현하기 위해 "모든 항목 j에 대해 리스트의 요소들은 j ≤ j + 1 이다 "이라는 정의를 작성할 수 있습니다. 이것은 프로그램의 정확성이 수학적으로 보편적라는 것을 보여주기 때문에 단위 테스트에서 엄청난 발전입니다.

Michelson 과 GADT

GADT는 일반화된 대수 데이터 타입(Generalized Algebraic Data Type)을 나타냅니다. OCaml 개발자는 GADT를 통해 데이터 생성자(constructor)와 타입 간의 풍부한 관계를 설명 할 수 있습니다. 현재 Michelson 은 타입의 형식 검증을 위해 GADT (Generalized Algebraic Data Types)를 사용합니다.

Michelson 과 Coq

2019년 1월, Coq를 사용한 Michelson의 형식 검증의 구현체는 아직 완료되지 않았습니다. 그러나 Coq 인터렉티브 이론 검증자(interactive theorem prover)를 사용하면 (프로그래밍)언어의 다음과 같은 부분이 형삭화됩니다.

  • 타입 system
  • 문법(Syntax)
  • 시맨틱(semantics)

Coq는 Gallina라는 프로그램 Specification 및 고급 수학 언어를 구현합니다. 이 언어는 고차원 논리와 풍부한 타입(richly-typed)의 함수형 프로그래밍을 모두 결합한 귀납적 구성의 미적분학 이라는 표현 형식 언어(expressive formal language)를 기반으로 합니다. 커맨드의 특정 형식(vernacular) 을 통해 Coq는 다음을 수행 할 수 있습니다.

  • 효율적으로 평가할 수있는 함수 또는 술어 정의;
  • 상태에 대한 수학적 정리(state mathematical theorems) 및 소프트웨어 Specification;
  • 이러한 정리에 대한 공식적인 증명을 인터렉티브하게 개발함.
  • 상대적으로 작은 인증 "커널(Kernel)"을 통해 이러한 증명을 기계가 검사함.
  • 인증된 프로그램을 Objective Caml, Haskell 또는 Scheme과 같은 언어로 추출(extract).

증명 개발 시스템(proof development system) 인 Coq는 인터렉티브 증명 방법(interactive proof method), 의사 결정과 준-의사결정 알고리즘, 그리고 사용자가 자체적으로 증명 방법을 정의 할 수있는 전술적(tactic) 언어를 제공합니다. 외부의 컴퓨터 대수 시스템과 가설 증명기(theorem prover)와의 연결도 가능합니다.

Coq는 수학의 형식화(formalization of mathematics) 및 프로그램 개발을 위한 플랫폼으로서 Coq는 고급 표기법(high-level notation), 압축적인 콘텐츠(implicit content) 와 다른 유용한 매크로를 지원합니다. 이 repository는 Coq 인터렉티브 이론 증명기 (interactive theorem prover)를 사용하여 Michelson을 형식화(formalization) 한 것입니다.

왜 이런것들이 금융계약에서 중요할까요?

Smart Contract는 금액을 가지고 있는 프로그램입니다. 따라서 오류가 없고 정확한 것이 결정적인 요소입니다. 단위 테스트는 모든 극단적인 케이스와 외부에서 발생할 수있는 모든 에러를 처리하기에 충분하지 않습니다.

복잡한 금융 계약은 관련 당사자의 신뢰와 연관된 단게와 프로세스가 관련되어 있고 계약이 구축 된 시스템의 신뢰성에 지분을 가진 다른 당사자도 관련이 있습니다.

잘못 구성된 계약은 시스템에 대한 신뢰를 깰 수 있습니다. 최악의 경우 의도하지 않은 프로그램 효과로 인해 Ethereum의 여러 사례에서 보았던 것처럼 돈을 잃을 수 있습니다.

형식 검증을 통해 컴퓨터 과학자와 개발자는 특정 프로그램에 오류가 없다는 것을 반론의 여지 없이 증명할 수 있습니다. 정리를 증명하길 원하는 수학자에게 요구되는 확실성과 같은 정도로 (Smart contract 에 대한) 증명이 가능합니다. 이러한 진보는 무인 드론에서부터 인터넷까지 모든 것을 보호하기 위해 사용되고 있습니다.