정형검증 기법은 소프트웨어 품질에 어떻게 기여할 수 있을까?

** 본 글은 차성덕 교수님의 소프트웨어공학이야기 책을 정리한 글입니다. **

정형검증 기법

• 소프트웨어 품질보증에서 테스팅의 한계를 보완해줄 수 있음 (모든 입력 확인 불가능)
  - equivalent partition: 입력값을 그룹으로 묶어서 임의의 값으로 테스팅
  - boundary value analysis: 경계값을 테스트케이스로 사용하는 테스팅
• 정형기법: 정형명세 + 정형검증
• symbolic execution, program proof/verification, model checking, program synthesis
• 높은 신뢰도를 요구하는 safety-critical 시스템, 보안이 중요한 시스템에서 사용
  DAL의 catastrophic, EAL7에서는 정형기법의 적용이 필수이다.

+ EAL: evaluation assurance level

• EAL1: 보안기능에 대한 기능 검사 Functionally Tested
             입력값과 출력값을 포함하는 테스트케이스를 만들어 시험
• EAL4: 개발 전 과정에 걸쳐 보안 기능에 대한 분석이 적절히 이루어짐 (디자인, 리뷰, 테스팅)
• EAL7: Formal Verification of Design
              보안 기능에 대한 정형명세 + security policy도 formal notation으로 기술 + 수학 증명
• 보안시스템 중 카드 관련 제품이 절반 이상, EAL4~5등급이 다수, EAL1은 별로 없음
  EAL6은 UML을 사용하여 기술하고 설득할 수 있지만, EAL7은 수학적 증명이 필수 (자연어 기술 X) 

Symbolic execution

• 입력을 기호 symbolic value로 나타내서 수행
• 파이: path condition 초기값은 true, 지날수록 정보가 추가됨.
• 어려운 점 → 쓰일 수 있는 수준으로 발전되는데 오래 걸림 (KLEE, PathFinder, SAGE, CUTE)
  • index의 값이 변수로 표시되거나 포인터가 사용된 경우 + index나 포인터가 함수 호출 시 parameter로 쓰이는 경우
  • 반복문의 경우, loop invariant를 알기 전까지 symbolic으로 표현할 수 없다
    * loop invariant란 반복문을 몇 번 수행하든 항상 만족하는 조건문 (NP-complete 문제)

Program Verification / Program correctness proof

• {P} C {Q}: precondition P, postcondition Q 
• ex) x를 y로 나누는 나눗셈의 경우. Loop invariant: x = y*q + r   
  
• 배열이나 포인터 등은 고려하지 않았으며, parameter passing 과정의 변수 aliasing 문제도 다루지 않은 예제임

 

---