프로그램 증명을 위한 중간 증명 언어—Why3와 Boogie

Intermediate Verification Languages for Program Verification—Why3 and Boogie

저자
김익순 / 인터랙티브입체영상연구실
권호
30권 4호 (통권 154)
논문구분
SW·콘텐츠 기술동향 특집
페이지
54-58
발행일자
2015.08.01
DOI
10.22648/ETRI.2015.J.300406
초록
수리 논리 기반의 프로그램 증명방법은 매우 유용한 프로그램 분석방법이지만, 수리 논리식에 대한 증명을 사람이 직접 수행하는 것은 매우 힘들고 고된 작업이다. 본고에서는 이러한 수리 논리 기반의 프로그램 증명을 자동화하기 위하여 개발된 중간 증명 언어(Intermediate Verification Language)에 대하여 살펴보고자 한다.
   2227 Downloaded 2045 Viewed
목록

I. 서론

프로그램이 어떤 특성(Property)을 만족하는지 보여주기 위한 프로그램 증명은 고품질의 프로그램 개발을 위해 필수적인 기술이다. 이러한 프로그램 증명 기술은 프로그램이 어떤 특성을 만족함으로써 프로그램 실행 중에 특정 오류가 발생하지 않음을 보이는 데에 사용하거나, 반대로 어떤 특성을 만족하지 않는 반례(또는 프로그램 오류)를 찾는 데에도 사용할 수 있다. 이러한 프로그램 증명 기술은 프로그램 안전성 향상, 프로그램 보안 강화 등을 위하여 널리 활용되고 있다.

Ⅱ. 프로그램 분석방법 분류

프로그램이 어떤 특성을 만족하는지 보여주기 위한 많은 방법이 연구되어 왔는데, 이들은 다음과 같이 크게 3가지로 구분할 수 있다.

1. 프로그램 테스팅 기법

프로그램 실행시간에 프로그램의 특성을 조사하는 프로그램 테스팅 기법은 프로그램이 주어진 특성을 만족하지 않는 반례를 찾음으로써 프로그램에 특정 오류가 있음을 보이는 데에 효과적이다. 하지만 테스팅 기법은 프로그램에 특정 오류가 없음을 보이기에는 비효율적이라는 단점이 있다.

2. 프로그램 자동분석 기법

프로그램을 분석하여 어떤 특성을 만족하는지 여부를 보여주는 프로그램 자동분석 기법은 프로그램이 어떤 특성을 만족함으로써 특정 오류가 발생하지 않음을 보여줄 수 있지만, 분석방법에 따라서 오류가 아님에도 오류라고 보고하거나, 오류임에도 오류가 아니라고 간주하는 잘못된 오류(False Alarm)가 발생할 수 있다. 프로그램을 실행하지 않고 분석을 시도하는 정적분석 기법과 프로그램 실행시간에 분석을 시도하는 동적분석 기법이 활발히 연구되고 있다.

3. 수리 논리 기반 프로그램 증명기법

수리 논리를 이용하여 프로그램이 어떤 특성을 만족하는지 여부를 보여주는 프로그램 증명기법은 정리 증명기(Theorem Prover)를 이용하여 수리 논리의 증명(Proof)을 시도한다. 증명하려는 특성을 수리 논리를 이용한 수리 논리식으로 표현한 후, 이 논리식을 수리 논리에 기반하여 증명한다.

수리 논리에 기반한 증명방법은 특성을 표현할 수 있는 표현력이 매우 우수하며 옳고 그름을 판단할 수 있는 잘 정의된 수학적 증명방법이 있다는 점에서 매우 강력한 증명방법이다. 또한, 최근 정리 증명기는 사람이 제시한 수리 논리식의 증명이 올바른지 여부를 자동으로 체크해줄 수 있다. 하지만 일반적으로 수리 논리 표현식에 대한 증명은 기계에 의하여 자동으로 수행되기보다는 사람이 직접 수행해야 한다는 어려움이 있다.

Ⅲ. 정리 증명기(Theorem Prover)

수리 논리를 증명하기 위한 많은 정리 증명기가 연구되고 있다. 수리 논리 증명은 정리에 대한 증명을 기계가 자동으로 수행해주는 자동정리 증명기(Automatic Theorem Prover)에 대한 연구와 정리에 대한 증명을 사람이 수행하고 이 증명이 올바른지를 자동으로 체크해주는 상호대화식 정리 증명기(Interactive Theorem Prover)에 대한 연구가 이루어지고 있다.

자동정리 증명기는 증명할 수 있는 수리 논리의 표현력이 Propositional Logic이나 First-Order Logic인 경우가 대부분이어서 상대적으로 표현력에 제약이 있다. 최근에는 특히 SAT[1] 및 SMT[2]Solver 관련 기술들이 많이 발전하여서 자동정리 증명기의 성능과 표현력도 빠르게 향상되고 있다.

상호대화식 정리 증명기는 증명의 일부분을 자동으로 해주거나 사람이 제공한 증명이 맞는지 틀리는지 체크해주는 정리 증명기이다. 상호대화식 정리 증명기에서 사용하는 수리 논리는 Higher-Order/Dependent Logic까지 확장되어서 자동정리 증명기보다 표현력에서 매우 우수하다. 상호대화식 정리 증명기로 Coq[3], Isa-belle/HOL[4], PVS[5] 등이 있다.

Ⅳ. 반자동 프로그램 증명기법

최근 프로그램의 프로그램 증명기법은 앞에서 소개한 수리 논리 기반 프로그램 증명기법의 많은 증명과정을 자동으로 처리함으로써 사람이 수행하는 정리 증명 과정을 대폭 줄이는 수리 논리 기반 반자동 프로그램 증명기법을 시도한다.

프로그램의 분석하고자 하는 특성을 컴파일러 기술을 활용하여 보다 간단한 중간 증명 언어(Intermediate Verification Language)로 번역하고, 이렇게 번역된 중간 증명 언어로 작성된 수리 논리식들을 자동정리 증명기(가령, SMT[2] Solver)를 활용하여 자동증명을 시도한다. 자동정리 증명기로 증명되지 않은 수리 논리식들은 사람이 직접 증명을 작성하고, 정리 증명기는 이 증명이 올바른지 체크해준다.

수리 논리에 기반한 반자동 프로그램 증명기법은 기존의 수리 논리 프로그램 증명기법의 증명과정을 자동화 시키려는 시도로서, 사용되는 수리 논리의 표현력을 자동증명이 가능한 수준으로 제한하지만, 기존의 프로그램 자동분석 기법에서 다루기 어려운 특성들을 증명하려고 시도한다.

수리 논리 기반 반자동 프로그램 증명기법에서 사용되는 대표적인 중간 증명 언어(Intermediate Verification Language)로는 미국 Microsoft사의 Boogie와 프랑스 Paris-Sud 대학과 Inria 연구소가 개발한 Why3 (WhyML) 등이 있다.

V. Why3(WhyML)

Why3[6]는 프랑스 Paris-Sud 대학과 Inria 대학에서 개발한 프로그램 증명 플랫폼으로 다양한 도구들을 제공하고 있다. Why3는 Frama-C와 같은 오픈 소스 기반 C, Java 프로그램 분석 도구와 연계되어 널리 사용되고 있다.

Why3는 First-Order Logic의 수리 논리를 표현하고 증명할 수 있도록 지원한다. Why3의 증명과정은 크게 기계에 의한 자동증명 단계와 사람에 의한 증명단계로 나뉘어 진행된다. Why3의 자동증명 단계는 기존의 많은 자동정리 증명기를 이용하여 자동증명을 시도하며, 하나의 자동정리 증명기가 실패할 경우 다른 자동정리 증명기를 이용하여 새로운 자동증명을 시도할 수 있다. Why3의 사용화면이 (그림 1)에 있으며, Simplify, Alt-Ergo 등과 같은 자동정리 증명기를 선택하여 사용할 수 있다.

(그림 1)

Why3 GUI 사용 화면[6]

images_1/2015/v30n4/ETRI_J003_2015_v30n4_54_f001.jpg

Why3의 사람에 의한 증명단계는 자동정리 증명기로 증명되지 않은 정리들에 대해서 Coq, Isabelle/HOL, PVS와 같은 상호작용식 정리 증명기들(Interactive Theorem Provers) 중 하나를 선택하여 사람이 직접 증명을 할 수 있도록 지원한다.

Why3는 WhyML이라는 계산(Computation)과 명세(Specification)을 동시에 할 수 있는 언어를 제공한다. (그림 2)는 WhyML로 작성한 프로그램의 예를 보여준다. WhyML 언어는 First-Order 언어라는 제약을 제외하고는, 다형(Polymorphic) 타입 지원, 레코드 타입 지원, 할당문(Assignment) 지원, 루프(Loop) 지원, Ex-ception 지원, First-Order Logic에 기반을 둔 Pre/Post Condition 지원, Assertion 지원, 루프 Invariant 지원 등과 같이 풍부한 기능을 제공한다. 또한, WhyML로 작성한 프로그램은 Why3 증명기를 통하여 자동증명을 시도하여서 사람이 작성해야 하는 증명을 많이 줄여준다.

(그림 2)

WhyML로 작성한 sort 함수[7]

images_1/2015/v30n4/ETRI_J003_2015_v30n4_54_f002.jpg

Why3의 장점은 여러 개의 자동정리 증명기를 편리하게 사용할 수 있도록 해준다는 점이다. 사용자가 다른 자동정리 증명기의 사용법을 몰라도 Why3는 다른 정리 증명기를 활용하여 증명 시도 과정을 자동으로 처리해준다. 실제로 자동정리 증명기들은 각각의 특징들이 달라서 자동증명 가능한 수리 논리 표현식들이 서로 다를 수 있다. Why3는 여러 개의 자동정리 증명기를 사용하여 자동증명을 시도함으로써 보다 많은 수리 논리 표현식들이 자동증명될 수 있도록 시도한다.

한편, Why3의 단점은 Why3가 자동증명 기능이 강화되어 사람에 의한 증명과정을 많이 줄일 수 있게 되었지만, 수리 논리 표현식이 First-Order Logic으로 Coq, Isabelle/HOL, PVS 등의 정리 증명기와 비교하여 제한적이라는 점이다.

이와 같은 Why3의 장단점으로 Why3 또는 WhyML은 다른 증명 시스템의 증명을 위한 중간언어 (Intermediate Verification Language)로서 사용되고 있다. 오픈 소스인 Frama-C 분석 도구는 C나 Java 프로그램의 특성을 증명하기 위하여 Why3를 증명을 위한 중간언어로 사용하고 있다.

Ⅵ. Boogie

Boogie[8]는 미국 Microsoft사가 개발한 중간 증명 언어로 프로그램 증명기를 제작하는 데에 중간언어로 사용할 목적으로 개발되었다. (그림 3)과 같이 Boogie를 기반으로 Havoc[9], Symdiff[10], VCC[11] 등과 같이 여러 가지 프로그램 증명기가 개발되었다.

Boogie 중간언어를 증명하는 시스템 역시 Boogie라고 불리는데, Boogie 증명 시스템은 Boogie로 작성된 프로그램을 입력으로 받아서 증명이 필요한 VC(Verification Condition)을 추출한 후 SMT[2] solver 등을 이용하여 자동증명을 시도한다.

(그림 3)

Boogie 시스템 개념도[8]

images_1/2015/v30n4/ETRI_J003_2015_v30n4_54_f003.jpg

Boogie 언어는 기본적으로 First-Order Logic에 기반을 두고 있으며 자동정리 증명은 SMT[2] Solver에 크게 의존하고 있다. Boogie 언어는 Procedure, Mutable 변수, Pre/Post Condition을 지원하지만, Side Effect가 있는 표현식이나, 동적 메모리 지원, Class 지원, Call-By-Reference 매개변수 전송, 구조화된 Control-flow 등은 지원하지 않는다. 또한 SMT[2] Solver 등에서 지원하는 Constants, Function Symbols, Axioms 등을 지원한다.

Boogie 언어의 증명은 최근 Why3와 유사하게 SMT Solver기반의 자동정리 증명기를 통하여 증명을 시도하며 자동증명 되지 않는 경우 Isabelle/HOL[4]등을 통하여 증명할 수 있도록 확장되고 있다.

Ⅶ. 결론

기존의 많은 연구들이 프로그램 성능을 향상시키기 위하여 많은 연구가 진행되어온 반면, 향후에는 복잡하고 거대한 소프트웨어를 오류없이 잘 작성하는 방법에 대하여 많은 연구가 필요하다.

수리 논리에 기반한 프로그램 증명기법은 최근 프로그래밍 언어 분야를 중심으로 활발히 연구되고 있다. 아직은 수리 논리를 프로그램에 접목시켜 프로그램을 증명하는 것은 일부 관련 기술 전문가들 위주로 행해지고 있으나 최근 운영체제, 하이퍼바이저, 시스템 프로그램 개발 등에 빠르게 적용되고 있다.

[1] 

SAT(Boolean Satisfiability Problem), https://en.wikipe dia.org/wiki/Boolean_satisfiability_problem

[2] 

Satisfiability Modulo Theories, http://en.wikipedia.org /wiki/Satisfiability_modulo_theories

[3] 

The Coq Proof Assistant, http://coq.inria.fr/

[4] 

Isabelle, https://isabelle.in.tum.de/

[5] 

A. Koprowski, “Introduction to PVS: Proving with Computer Assistance,” Lecture Material in Radboud University Nijmegen, May 2008.

[6] 

Why3, http://why3.lri.fr/

[7] 

F. Bobot et al., “Let’s Verify This with Why3,” Int. J. Softw. Tools for Technol. Transfer, Apr. 19th, 2014.

[8] 

Boogie: An Intermediate Verification Language, http: //research.microsoft.com/en-us/projects/boogie/

[9] 

Havoc: a Tool for Checking Systems Software Written in C, http://research.microsoft.com/en-us/projects/havoc

[10] 

SymDiff: Differential Program Verifier, http://researc h.microsoft.com/en-us/projects/symdiff

[11] 

VCC: a Verifier for Concurrent C, http://research.mic rosoft.com/en-us/projects/vcc

(그림 1)

Why3 GUI 사용 화면[6]

images_1/2015/v30n4/ETRI_J003_2015_v30n4_54_f001.jpg
(그림 2)

WhyML로 작성한 sort 함수[7]

images_1/2015/v30n4/ETRI_J003_2015_v30n4_54_f002.jpg
(그림 3)

Boogie 시스템 개념도[8]

images_1/2015/v30n4/ETRI_J003_2015_v30n4_54_f003.jpg
Sign Up
전자통신동향분석 이메일 전자저널 구독을 원하시는 경우 정확한 이메일 주소를 입력하시기 바랍니다.