형식 검증

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 형식 검증의 접근법
3. 소프트웨어 형식 검증
- 3.1. 의존 타입 프로그래밍
- 3.2. 프로그램 파생
4. 검증 및 유효성 검사 (Verification and Validation)
5. 자동 프로그램 복구 (Automated Program Repair)
6. 산업 응용
7. 같이 보기
참조

1. 개요

형식 검증은 시스템이 요구 사항을 충족하는지 확인하는 기술로, 모델 검증, 논리적 추론, 정적 분석 등의 접근 방식을 사용한다. 모델 검증은 시스템의 유한 상태 모델을 검사하고, 논리적 추론은 정리 증명 소프트웨어를 활용하며, 정적 분석은 코드나 바이너리 코드를 분석한다. 소프트웨어 형식 검증은 프로그램이 명세를 만족하는지 증명하는 것을 목표로 하며, 연역적 검증, 추상 해석, 자동 정리 증명, 타입 시스템 등을 포함한다. 형식 검증은 하드웨어 및 소프트웨어 산업에서 사용되며, 특히 하드웨어 산업에서 중요성이 커지고 있다.

더 읽어볼만한 페이지

정형 기법 - 자동 정리 증명
자동 정리 증명은 논리적 진술의 타당성을 자동으로 확인하는 기술로서, 형식 논리 발전과 컴퓨터 등장 이후 다양한 논리를 지원하며 여러 분야에 응용되고, 관련 연구와 시스템 개발이 활발히 진행되고 있다.
정형 기법 - 튜링 기계
튜링 기계는 앨런 튜링이 제시한 계산 모델로, 테이프 위에서 기계적으로 작동하며, 유한한 상태, 테이프, 헤드, 명령 표를 통해 작동하고, 계산 가능성과 알고리즘의 한계를 연구하는 데 사용된다.
컴퓨터 과학 내 논리 - 자동화된 추론
자동화된 추론은 컴퓨터 프로그램을 사용하여 논리적 추론을 수행하는 인공지능 분야로, 수리 논리학의 발전과 초기 연구를 통해 자동 정리 증명 분야의 기틀을 마련했으며, AI 겨울을 겪었지만 소프트웨어 검증 등 다양한 분야에 활용되며 Coq, HOL Light 등의 증명 보조기가 개발되어 난제들의 형식적 증명에 기여했다.
컴퓨터 과학 내 논리 - 혼 절
혼 절은 하나의 긍정 리터럴만을 포함하는 분리절이며, 논리 프로그래밍, 자동 정리 증명, 데이터베이스 이론 등 여러 분야에 응용된다.
이론 컴퓨터 과학 - 알고리즘
알고리즘은 문제 해결을 위한 명확하고 순서화된 유한 개의 규칙 집합으로, 알콰리즈미의 이름에서 유래되었으며, 수학 문제 해결 절차로 사용되다가 컴퓨터 과학에서 중요한 역할을 하며 다양한 방식으로 표현되고 효율성 분석을 통해 평가된다.
이론 컴퓨터 과학 - 자동화된 추론
자동화된 추론은 컴퓨터 프로그램을 사용하여 논리적 추론을 수행하는 인공지능 분야로, 수리 논리학의 발전과 초기 연구를 통해 자동 정리 증명 분야의 기틀을 마련했으며, AI 겨울을 겪었지만 소프트웨어 검증 등 다양한 분야에 활용되며 Coq, HOL Light 등의 증명 보조기가 개발되어 난제들의 형식적 증명에 기여했다.

형식 검증

2. 형식 검증의 접근법

형식 검증은 크게 모델 검증, 연역적 검증, 그리고 정적 분석 등의 방법으로 나뉜다.

형식 검증의 기법은 크게 두 가지로 분류할 수 있다.

모델 검사: 수리 모델을 체계적이고 철저하게 검증하는 기법이다. (\[\[유한 모델 이론|유한 모델]]에서만 가능하지만, 무한한 상태를 가진 모델이라도 추상화를 통해 유한한 표현이 가능하다면 검증이 가능하다). 일반적으로 모델 내의 모든 상태와 모든 전이를 검증하며, 연산 시간을 줄이기 위해 영역 고유의 추상화 기법 등을 활용하여 효율을 높인다.
논리적 추론: \[\[자동 정리 증명|정리 증명]] 소프트웨어를 사용하여 시스템에 관해 형식적인 추론을 수행하는 기법이다. 이 기법은 완전 자동화되어 있지 않은 것이 일반적이며, 사용자의 대상 시스템에 대한 이해에 따라 진행된다.

\[\[선형 논리]]나 \[\[시상 논리]] 등의 \[\[비고전 논리]]는 모델 검사뿐만 아니라 논리적 추론에서도 사용된다.

프로그램의 형식 검증은 프로그램이 동작에 대한 형식적인 명세를 만족하는지 증명하는 것을 포함한다. 형식 검증의 하위 분야에는 연역적 검증(위 참조), \[\[추상 해석]], \[\[자동 정리 증명]], \[\[타입 시스템]], 그리고 \[\[형식 방법#경량 형식 방법|경량 형식 방법]]이 있다. 유망한 타입 기반 검증 접근 방식은 \[\[의존 타입|의존적으로 타입이 지정된 프로그래밍]]인데, 여기서 함수의 타입에는 해당 함수의 명세의 (적어도 일부)가 포함되며, 코드의 타입 검사는 해당 명세에 대한 정확성을 확립한다. 완전한 기능을 갖춘 의존적으로 타입이 지정된 언어는 연역적 검증을 특별한 경우로 지원한다.

또 다른 보완적인 접근 방식은 \[\[프로그램 파생]]인데, 여기서 효율적인 코드는 일련의 정확성 보존 단계를 거쳐 \[\[함수형 프로그래밍|함수형]] 명세에서 생성된다. 이러한 접근 방식의 예는 \[\[버드-미어텐스 형식주의]]이며, 이 접근 방식은 또 다른 형태의 \[\[프로그램 합성]]으로 볼 수 있다.

이러한 기술은 ''\[\[soundness|건전성]]''을 가질 수 있는데, 이는 검증된 속성이 의미론으로부터 논리적으로 추론될 수 있음을 의미하며, 또는 ''비건전성''을 가질 수 있는데, 이는 그러한 보장이 없음을 의미한다. 건전한 기술은 모든 가능성의 공간을 완전히 다루었을 때만 결과를 생성한다. 비건전한 기술의 예는 예를 들어 특정 숫자까지의 정수와 같은 가능성의 하위 집합만 다루고 "적절한" 결과를 제공하는 것이다. 기술은 또한 ''\[\[decidability (logic)|결정 가능성]]''을 가질 수 있는데, 이는 알고리즘 구현이 답변으로 \[\[종료 분석|종료가 보장]]됨을 의미하거나, 결정 불가능할 수 있는데, 이는 종료되지 않을 수 있음을 의미한다. 가능성의 범위를 제한함으로써, 결정 가능한 건전한 기술을 사용할 수 없을 때 결정 가능한 비건전한 기술을 구성할 수 있다. 형식 검증의 적용 예로는 내부에 메모리를 가진 암호 회로, 조합 회로, \[\[디지털 회로]] 등의 시스템, \[\[소스 코드]]로 표현되는 \[\[소프트웨어]]가 있다.

이러한 시스템의 검증은 시스템을 추상화한 \[\[수리 모델]]상에서 수행되며, 그 수리 모델과 실제 시스템의 성질은 일치한다. 사용되는 수리 모델로는 \[\[유한 상태 기계]], \[\[상태 전이 시스템|레이블이 붙은 전이 시스템]], \[\[페트리 네트]], \[\[:en:timed automaton|시간 오토마타]], \[\[:en:hybrid automata|하이브리드 오토마타]], \[\[프로세스 계산]], \[\[프로그램 의미론|프로그래밍 언어의 형식 의미론]] (\[\[조작적 의미론]], \[\[표시적 의미론]], \[\[공리적 의미론]]), \[\[호어 논리]] 등이 있다.

2. 1. 모델 검증

모델 검증은 시스템의 유한 상태 모델을 생성하고, 해당 모델이 특정 속성을 만족하는지 자동으로 검사하는 방법이다.^[4] 검증할 속성은 시간 논리를 사용하여 기술하는데, 예를 들어 선형 시간 논리(LTL), 속성 명세 언어(PSL), SystemVerilog 단언(SVA),^[4] 또는 계산 트리 논리(CTL) 등을 사용한다.

모델 검증은 주로 다음 기술을 사용하여 구현한다.

기술
상태 공간 열거
기호 상태 공간 열거
추상 해석
기호 시뮬레이션
추상화 개선

모델 검증의 가장 큰 장점은 완전 자동화가 가능하다는 것이지만, 대규모 시스템에는 적용하기 어렵다는 단점이 있다. 기호 모델은 수백 비트 상태로 제한되며, 명시적 상태 열거는 탐색하는 상태 공간이 작아야 한다.

2. 2. 연역적 검증

연역적 검증은 시스템의 동작을 수학적으로 기술하고, 정리 증명기를 사용하여 시스템이 요구사항을 만족함을 증명하는 방법이다.^[5]^[6] HOL, ACL2, Isabelle, Coq, PVS와 같은 증명 보조 도구 (Interactive Theorem Prover) 또는 만족성 모듈로 이론 (SMT) 솔버를 포함하는 자동 정리 증명기를 사용하여 증명 의무를 해결한다. 이 접근 방식은 사용자가 시스템이 정확히 작동하는 이유를 자세히 이해하고, 검증 시스템에 증명해야 할 일련의 정리 또는 시스템 구성 요소(예: 함수, 프로시저) 및 하위 구성 요소(예: 루프, 데이터 구조)의 명세(불변성, 사전 조건, 사후 조건) 형태로 이 정보를 전달해야 할 수 있다는 단점이 있다.

2. 3. 정적 분석

정적 분석은 프로그램을 실행하지 않고 소스 코드나 바이너리 코드를 분석하여 잠재적인 오류나 취약점을 찾는 방법이다. 타입 시스템, 추상 해석 등의 기술을 활용한다.

3. 소프트웨어 형식 검증

소프트웨어 형식 검증은 프로그램이 형식적인 명세(Specification)를 만족하는지 증명하는 것을 목표로 한다. 형식 검증의 하위 분야에는 연역적 검증, 추상 해석, 자동 정리 증명, 타입 시스템, 경량 형식 방법 등이 있다.

이러한 기술은 ''건전성''(검증된 속성이 의미론으로부터 논리적으로 추론될 수 있음) 혹은 ''비건전성''(그러한 보장이 없음)을 가질 수 있다. 건전한 기술은 모든 가능성의 공간을 완전히 다루었을 때만 결과를 생성하며, 비건전한 기술은 특정 범위(예: 특정 숫자까지의 정수)의 가능성만 다루고 "적절한" 결과를 제공한다. 또한, 기술은 ''결정 가능성''(알고리즘 구현이 답변으로 종료가 보장됨) 혹은 결정 불가능성(종료되지 않을 수 있음)을 가질 수 있다. 결정 가능한 건전한 기술을 사용할 수 없을 때는 가능성의 범위를 제한하여 결정 가능한 비건전한 기술을 구성할 수 있다.

소프트웨어 형식 검증을 위한 논리 추론 방법은 다음과 같이 분류된다.

1970년대의 고전적인 방법: 먼저 코드를 일반적인 방식으로 작성하고, 이후 단계에서 정확성을 검증한다.

3. 1. 의존 타입 프로그래밍

의존 타입 프로그래밍에서는 함수의 타입에 해당 함수의 명세(일부)가 포함되며, 코드의 타입 검사를 통해 명세에 대한 정확성이 보장된다. 완전한 의존 타입 프로그래밍 언어는 1970년대의 고전적인 방법(먼저 코드를 작성하고 나중에 검증하는 방식)을 특수한 경우로 지원한다.

3. 2. 프로그램 파생

프로그램 파생은 일련의 정확성 보존 단계를 거쳐 함수형 명세에서 효율적인 코드를 생성하는 방법이다. 이 접근 방식의 예로는 버드-미어텐스 형식주의가 있으며, 이는 또 다른 형태의 프로그램 합성으로 볼 수 있다.

4. 검증 및 유효성 검사 (Verification and Validation)

형식 검증은 시스템이 요구사항을 만족하는지 확인하는 과정인 검증(Verification)과, 시스템이 실제 사용자의 요구를 충족하는지 확인하는 과정인 유효성 검사(Validation)의 중요한 부분이다.

'''검증(Verification):''' "우리가 제품을 올바르게 만들고 있는가?" - 시스템이 명세대로 만들어졌는지 확인한다.
'''유효성 검사(Validation):''' "우리가 올바른 제품을 만들고 있는가?" - 시스템이 사용자의 실제 요구사항에 맞게 지정되었는지 확인한다.^[4]

검증 프로세스는 정적/구조적 측면과 동적/행동적 측면으로 구성된다. 예를 들어, 소프트웨어 제품의 경우 소스 코드를 검사(정적)하고 특정 테스트 케이스에 대해 실행(동적)할 수 있다. 유효성 검사는 일반적으로 동적으로만 수행할 수 있는데, 이는 제품을 전형적인 사용과 비전형적인 사용을 거치면서 테스트하는 것이다. ("모든 유스케이스를 만족스럽게 충족하는가?").

5. 자동 프로그램 복구 (Automated Program Repair)

자동 프로그램 복구는 프로그램의 원하는 기능을 설명하는 오라클을 기반으로 프로그램의 버그를 자동으로 수정하는 기술이다. 간단한 예로 테스트 슈트를 들 수 있는데, 입력/출력 쌍은 프로그램의 기능을 지정한다. 이 과정에서 다양한 기술이 사용되며, 특히 만족성 모듈로 이론(SMT) 솔버와 유전자 프로그래밍이 활용된다.^[7]

진화 컴퓨팅은 수정 후보를 생성하고 평가하는 데 사용된다. 만족성 모듈로 이론 솔버는 결정론적 방법인 반면, 유전 프로그래밍은 무작위적 방법이다.

자동 프로그램 복구는 형식 검증 및 프로그램 합성 기술을 결합한다. 형식 검증의 오류 위치 확인 기술은 합성 모듈의 대상이 될 수 있는, 즉 버그가 있을 가능성이 있는 프로그램 지점을 계산하는 데 사용된다. 자동 프로그램 복구 시스템은 검색 공간을 줄이기 위해 종종 작고 미리 정의된 버그 클래스에 중점을 둔다. 그러나 기존 기술은 계산 비용이 크기 때문에 산업적 사용은 제한적이다.

6. 산업 응용

설계 복잡성이 증가함에 따라 하드웨어 산업에서 형식 검증 기술의 중요성이 커지고 있다.^[8]^[9] 현재 형식 검증은 대부분 또는 모든 주요 하드웨어 회사에서 사용하고 있지만,^[10] 소프트웨어 산업에서의 사용은 여전히 부진하다. 이는 하드웨어 산업에서 오류가 더 큰 상업적 중요성을 갖기 때문에 더 큰 필요성 때문일 수 있다. 구성 요소 간의 잠재적인 미묘한 상호 작용으로 인해 시뮬레이션을 통해 현실적인 가능성 집합을 실행하기가 점점 더 어려워지고 있다. 하드웨어 설계의 중요한 측면은 자동화된 증명 방법에 적합하여 형식 검증을 도입하고 생산성을 높이기 쉽다.^[11]

형식 검증이 적용된 운영 체제는 다음과 같다.

NICTA의 보안 임베디드 L4 마이크로커널(OK Labs에서 seL4로 상업적으로 판매)^[12]
화동사범대학교의 OSEK/VDX 기반 실시간 운영 체제 ORIENTAIS
Green Hills Software의 Integrity 운영 체제^[13]
SYSGO의 PikeOS^[13]^[14]

2016년 예일 대학교의 Zhong Shao가 이끄는 팀은 CertiKOS라는 형식적으로 검증된 운영 체제 커널을 개발했다.^[15]^[16]

2017년 현재 형식 검증은 네트워크의 수학적 모델을 통해 대규모 컴퓨터 네트워크 설계에 적용되었으며,^[17] 새로운 네트워크 기술 범주인 의도 기반 네트워킹의 일부로 적용되었다.^[18] 형식 검증 솔루션을 제공하는 네트워크 소프트웨어 공급업체는 시스코(Cisco)^[19], Forward Networks^[20]^[21] 및 Veriflow Systems^[22]가 있다.

SPARK 프로그래밍 언어는 형식 검증을 통한 소프트웨어 개발을 가능하게 하는 도구 세트를 제공하며, 여러 고 무결성 시스템에서 사용된다.

CompCert C 컴파일러는 ISO C의 대부분을 구현하는 형식적으로 검증된 C 컴파일러이다.^[23]^[24]

7. 같이 보기

모델 검증
정적 분석
정리 증명

참조

_[1] 학술지 What is formal verification? 2010-05-21
_[2] 서적 Handbook of Model Checking https://doi.org/10.1[...] Springer 2018
_[3] 웹사이트 Introduction to Formal Verification http://embedded.eecs[...] Berkeley University of California 2013-11-06
_[4] 서적 SystemVerilog Assertions Handbook CreateSpace Independent Publishing Platform
_[5] 서적 Deductive Software Verification - The KeY Book: From Theory to Practice Springer International Publishing : Imprint: Springer 2016
_[6] 서적 Engineering secure and dependable software systems IOS Press 2019
_[7] 학술지 GenProg: A Generic Method for Automatic Software Repair https://www.proquest[...] 2012-01
_[8] 서적 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings
_[9] 웹사이트 Formal verification of a real-time hardware design http://portal.acm.or[...] Portal.acm.org 1983-06-27
_[10] 웹사이트 Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar http://formalverific[...]
_[11] 웹사이트 Formal Verification in Industry http://www.cl.cam.ac[...] 2012-09-20
_[12] 웹사이트 Abstract Formal Specification of the seL4/ARMv6 API https://sel4.systems[...] 2015-05-19
_[13] 간행물 Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS http://www-wjp.cs.un[...]
_[14] 웹사이트 Getting it Right http://www.ganssle.c[...]
_[15] 웹사이트 Unhackable OS? CertiKOS enables creation of secure system kernels https://www.zdnet.co[...] 2019-06-10
_[16] 웹사이트 CertiKOS: Yale develops world's first hacker-resistant operating system https://www.ibtimes.[...] 2019-06-10
_[17] 웹사이트 For Cisco, intent-based networking heralds future tech demands http://www.computerw[...] Computer Weekly 2018-02-12
_[18] 웹사이트 Intent-based networking https://blogs.gartne[...] Gartner 2018-02-12
_[19] 웹사이트 Cisco brings intent based networks to the data center https://www.networkw[...] NetworkWorld 2018-02-12
_[20] 웹사이트 Forward Networks: Accelerating and De-risking Network Operations http://www.insightss[...] Insights Success 2018-02-12
_[21] 웹사이트 Getting Grounded in Intent=based Networking https://images.idges[...] NetworkWorld 2018-02-12
_[22] 웹사이트 Veriflow Systems https://www.bloomber[...] Bloomberg 2018-02-12
_[23] 웹사이트 CompCert - The CompCert C compiler https://compcert.org[...] 2023-02-22
_[24] 학술지 Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler 2023-01-09
_[25] 웹사이트 seL4: Formal Verification of an OS Kernel (paper submitted to 22nd ACM Symposium on Operating Systems Principles, October 2009) http://www.sigops.or[...] 2011-11-07
_[26] 학술지 Formal verification at Intel
_[27] 웹사이트 Formal verification of a real-time hardware design http://portal.acm.or[...] Portal.acm.org 1983-06-27
_[28] 웹사이트 Formal Verification in Industry http://www.cl.cam.ac[...]
_[29] 뉴스 A new OS has been proven to be correct using mathematical proofs. The cost: astronomical. http://www.embedded.[...]
_[30] 간행물 Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS http://www-wjp.cs.un[...]
_[31] 학술지 What is formal verification? 2010-05-21
_[32] 서적 Handbook of Model Checking https://doi.org/10.1[...] Springer 2018
_[33] 웹사이트 Introduction to Formal Verification http://embedded.eecs[...] Berkeley University of California 2013-11-06

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com