[IT보안] SW정형검증

1. SW정형 검증 개요

1) SW정형기법(Formal Method)의 정의
- 논리학이나 이산 수학을 이용하여 요구 사항 명세, 설계 및 구현 과정에서 사용하는 기법 입니다.
- 정형 기법에는 정형 명세(Formal Specification), Formal Synthesis, 정형 검증(Formal Verification) 등이 있습니다.
2) SW정형 검증(Formal Specification)의 정의
- 논리학과 이산 수학을 기반으로 하여 시스템의 동작을 표현하는 정형 명세[Formal Specification]가 시스템이 만족해야 할 특성[Property]을 만족시킴을 논리적으로 검증하는 소프트웨어 검증 기법입니다.
- 회로디자인과 같은 HW분석, 요구 명세와 같은 정적인 SW 분석에 주로 사용되어온 기법으로써 분석대상 시스템의 기능을 논리식과 같은 정형 언어로 기술하여 수학적 증명 기법을 적용하고 검증하는 분석기법입니다.
3) 필요성
- 안정성과 보안이 중요시되는 높은 완전한 시스템에서 신뢰성과 탄탄한 디자인 검증 필요합니다.
- 기존 테스팅의 행위 적합성 테스트의 한계(버튼 A가 눌려지면 문이 열린다)에서 행위의 부재시 검증 필요합니다. (문이 열린 상태에서 전자레인지 작동되면 안됨)

 

2. SW정형 기법의 구성 및 적용 수준

1) 구성

(1) 정형 명세(Specification)

- 개발 시스템에 대해 원하는 어떠한 수준의 레벨로도 명세 가능합니다.
- 시스템의 요구사항이 완전하게 정확하게 명시되었는지 검증합니다.
- ALGOL 60에서 John Backus가 만든 BNF(Backus–Naur Form)로 표현
(2) 정형 개발(Development)

- 정형 명세를 통해 만든 명세는 개발의 기준이 됩니다.
(3) 정형 검증(Verification)

- 만들어진 명세는 명세의 특성을 증명하는 기초입니다.
- 사람 주도적인 증명: 시스템의 정확성을 자연 언어로 수학적 증명을 함. 자연 언어의 태생적 모호함으로 인해 문제점을 검출하지 못할 수도 있으며, 좋은 증명은 높은 수학 지식과 전문 지식을 요합니다.
- 자동화 증명: 자동화 기법을 효율적으로 사용하기 위해서는 중요 state을 정의해줄 수 있는 사람의 도움이 필요함. 검증한 것은 모두 수학적으로 증명된 것으로 정확도가 더 높다고 인지하고, 고급인력이 제한되지 않습니다.

2) 적용 수준

(1) Level 0 : Formal Specification을 시행하고, 이를 비공식적인 토대로 개발을 하는 방식으로 Formal Methods Lite라고도 부르며, 많은 경우 비용 효율적인 옵션입니다.
(2) Level 1 : Formal Specification을 통해 만들어진 것을 공식적으로 Formal development와 formal verification으로 제품을 완성하는 방식으로 안정성과 보안성이 필요한 완전한 시스템에 적절합니다.
(3) Level 2 : 수학적 정리 증명가를 전 과정에 활용되며, 이 방식은 고비용이기 때문에 문제시 극도로 높은 비용이 발생할 경우에만 사용하는 것이 실용적입니다.

 

3. SW정형 검증 종류

1) Model Checking

- 시스템(H/W, SW)을 유한 상태 머신으로 모델링(SW화)하고, 시제 논리식을 입력값으로 하며 모델이 논리식을 만족하는지 점검하는 기법입니다.
- 특정 속성이 시스템 실행 중에 일어날 수 있는 모든 상태를 검색하는 방식 입니다.
- 입력값 불만족시 반례(counterexample) 제시 합니다.
- 초기 상태에서 최종 상태까지 도달할 수 있는지 검사 : 도달성 분석
- 문제점 : 상태 폭발 (모델 체킹 수행 시 고려해야 할 상태의 수는 보델의 크기에 따라 지수적으로 증가하는 문제)
2) 자동화된 정리 증명 (theorem proving)

- 주어진 시스템의 설명(description), 논리적 원리, 추론 법칙을 통해 증명
- 툴은 주로 부분적으로 자동화된 것으로, 사용자의 시스템 이해를 통해 확인(validate) 함
3) Equivalence Checking

- EDA (Electronic Design Automation)의 일부로 주로 디지털 직접회로 개발에 사용하며, 회로 디자인의 두 표현이 동일한 처리를 하는지 증명
4) SAT

- 불린 함수 이용. 기 정의한 함수 결과가 성공이면 1, 증명하지 못하면 0 상태를 유지하는 방법

 

※ SW 정형 검증 비교

구분	정리 증명	모델 체킹
사용기법	- 수학/논리학적 공리[Axiom], 규칙[Rule]을 활용하여 시스템명세/특성 도출	- 정형 명세 언어를 통한 시스템 명세 (유한상태기계) - 시스템 요구사항에 기반하여 시스템 특성 도출
검증확인	시스템 명세와 특성의 논리학적 정합성	시스템 모델의 시스템 특성 만족 여부
장점	무한상태기계도 명세 및 증명 가능	모델 증명 도구를 통한 자동화 가능
단점	시스템 명세 도출 및 증명이 매우 어려움	유한상태기계만 명세 및 증명 가능
활용 예	- SPEAR(II), PVS	CMU’s SMV, Bell/s SPIN, Berkeley’s VIS

 

4. SW정형 검증을 방해하는 상태 폭발 문제 및 해결방안

1) 상태 폭발 문제 
- 정형 검증에서는 일어날 수 있는 모든 상황/상태를 체크하여 분석해야 합니다.
- 정형 검증은 다양한 알고리즘에 의해 자동 수행되며 여러 프로세스가 추가되면 상태의 숫자는 지수적으로 증가합니다.
- 지수적으로 증가한 상태는 결과적으로 상태 폭발 문제를 야기하여 정확한 정형검증 분석이 불가능하게 합니다.
2) 상태폭발 문제를 야기하는 구조적 문제 해결방안
(1) 기호적 모델 체킹 : 상태들을 직접 검사하지 않고, 특성들을 상태를 의미하는 BDD (Binary Decision Diagram)과 상태 전이를 의미하는 BDD로 표현하고, BDD연산을 통해 도달성을 너비 우선 탐색 방식으로 검사 합니다.
(2) 추상화 기법 : 원래 시스템이 도달 가능한 경로를 포함하고 있는 좀 더 작은 크기 모델 생성하며, 상위 근사 추상화 모델 > 원 모델 > 하위 근사 추상화 모델
(3) 릴레이 모델 체킹 : 한 번에 모든 도달 가능상태 검사를 나누어 검사 합니다.
(4) 프로그램의 효율적 구현 : 슈퍼컴퓨터, 그리드 컴퓨팅, 분산/병렬 처리하며, 기존 도구들이 도달 가능한 상태들의 집합을 메인 메모리에 저장하고, 중첩된 탐색을 수행하는 것을 HDD 저장하여 탐색 횟수 줄이는 기법을 적용 합니다.
(5) 컴포넌트 기반 정형 검증 : 시스템이 여러 컴포넌트 프로세스들의 유기적 결합으로 작동하는 경우, 각각의 컴포넌트 프로세스를 먼저 검증한 후 시스템 조합 규칙에 따라 전체 시스템의 성질을 유추해내는 방식 입니다.

 

5. SW정형 검증의 모델 체킹 기법 적용 시 고려사항

- 상태 폭발(State Explosion) : SW의 상태 수가 HW 대비하여 매우 많습니다. (구성요소 증가 시, 상태 수는 지수적 증가)
- 모델 구현의 어려움 : SW의 소스코드를 모델 명세 언어로 재작성 또는 변형 필요합니다.
- 요구 명세 적용의 어려움 :정형 명세 언어는 HW의 정적 상태 묘사에 적합하며 SW의 동적 상태 변화 묘사에 어려움 존재 합니다. (예) 객체/스레드의 생성 및 소멸 묘사
- 검증 결과 해석의 모호성 : 오류에 대한 소스 코드로의 역추적이 곤란합니다. (현재는 대략의 위치가 추정 가능)