[SoftwareV&V] 07. Symbolic Execution and Proof of Properties

[원문링크]

https://adorable-aspen-d23.notion.site/SoftwareV-V_07_Symbolic-Execution-and-Proof-of-Properties-a74f42ccdcc64adca0234c8ebbbb9577

SoftwareV&V_07_Symbolic Execution and Proof of Properties

[2021 - 1학기 수강한 Software V&V 강의 정리본입니다.]

(Software Verification & Validation)

 

Symbolic Execution and Proof of Properties

Learning Objectives

• Symbolically executing program의 Goal, 함축의미 이해하기
• 무한한 execution을 요약하기 위해 assertion 사용하기
• 프로그램 correctness에 대해 추론하는 방법 알아보기
• symbolic execution을 통해 프로그램 property 추론하는 방법 알아보기
• symbolic execution의 한계와 문제점 이해하기

1. Symbolic Execution

: program behavior(execution) 과 logic(predicate) 사이의 다리 역할

https://www.lazenca.net/pages/viewpage.action?pageId=6324534

• predicate을 만든다. (symbol에 값을 넣었을 때 T/F값을 알 수 있는 것이 나오는 것)-program analysis (pessimistic inaccuracy)-프로그램 correctness에 대한 Formal Verification(공식 검증)
  • critical 하위 시스템에 대한 철저한 검증
  • ex) safety kernel of a medical device
  • dynamic testing이 불가한 critical property 검증
  • ex) 보안
  • 알고리즘 description(설명) 및 logical design 검증
  • → 실행시키는 것 보다 덜 복잡하다.
• -Test data generation(optimistic inaccuracy)
• 1) 적용
• Program Execution > Symbolic Execution하기
• → static analysis, model checking에서 assertion(precondition, roop invariant, post condition)을 제공 해줌

2) Summary information

• 복잡한 조건 P ⇒ Weaker 조건 W로

정보를 덜 가지고 있지만 correctness를 추론하는 데에는 충분하다.

3) Weaker Precondition

• 기계적으로 선택되지 않고 사람이 선택해야 한다. (코드 이해도와, 이 것이 맞을 것이라는 믿음의 비율에 의존함)
• Assertion : 특정 포인트에서 true여야 한다는 것을 나타낸다.
• 한계 (시험)
  • Weakening the predicate 은 테스팅에 cost를 요구한다.⇒ W를 만족하는 test data는 path를 정상적으로 execute하긴 하지만, 충분하지 않음
  • ⇒ W를 만족하지 않는 다는 것은 path가 infeasibility(실현가능하지않다) 라는 것을 보여줌
  • → predicate을 만족하는 것은 program execution이 길 따라 잘 작동하는 데이터를 찾기에 충분하지 않다
  • program이 static한 상태에서 판단하기 때문에(pessimistic) false alarm이 30%정도 존재한다. (correctness 판단 불가)

4) Loops and Assertions

• loop로 인한 execution path는 무한하다.
• 이를 추론하기 위해 loop를 Invariant(불변) 하게 만든다.
• → Assertion : 해당 지점에 도달할 때마다 true가 될 것이라고 예상되는 predicate 을 말함
• invariant assertion에 도달할 때마다, weaken 할 수 있다.

5) Precondition and Postcondition

: 사람이 제공한다.

2. Verification of Program Correctness (#109-#111)

: precondition이 주어지고, invariant한 loop를 다 실행한 후 postCondition을 만족한다면

⇒ pre&post condition에 대해 correct하다고 할 수 있다.

1) Hoare triple : inference

: precondition을 만족하고 block에 들어가서 postCondition을 만족하는 상태로 간다.

https://ropas.snu.ac.kr/~dreameye/PL/slide/PL10.pdf

2) Reasoning Style

: contract = precondition + postcondition을 만들어 놓고 필요한 곳에서 불러서 씀

• ex) binary search

• Data Structure module
• : Procedure(method) 의 모음 (specification이 강하게 연결된)
• Contractsex) Dictionary는 {<key,value>}로 abstract된다.
• Dictionary는 독립적으로 list, tree, hash table 등에 사용된다.
• : Procedure를 inner state의 abstract model(추상 모델)과 관련시킨다.
• Structural invariantsex) tree class 내의 모든 method들은 key를 정렬해야 한다.
• : maintain되어야 하는 structural 특징 (loop invariant와 비슷)

Summary

• Symbolic execution은 program execution과 logical&mathmatical statement의 다리 역할을 한다.
• loops, procedure calls, data structures의 Symbolic execution은 계층적으로 동작한다.
• (작은 부분을 큰 부분으로 구성)
• Fundamental techniques for-Verifying systems
• -Performing or checking program transformations(변형)
• -Test Data 만들기