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값을 알 수 있는 것이 나오는 것)

  1) 적용

  -program analysis (pessimistic inaccuracy)

  -Test data generation(optimistic inaccuracy)

  -프로그램 correctness에 대한 Formal Verification(공식 검증)

  • critical 하위 시스템에 대한 철저한 검증

    ex) safety kernel of a medical device

  • dynamic testing이 불가한 critical property 검증

    ex) 보안

  • 알고리즘 description(설명) 및 logical design 검증

    → 실행시키는 것 보다 덜 복잡하다.

• Program Execution > Symbolic Execution하기

  → static analysis, model checking에서 assertion(precondition, roop invariant, post condition)을 제공 해줌

2) Summary information

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

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

• W → pre-condition, post-condition, loop invariant

3) Weaker Precondition

• 기계적으로 선택되지 않고 사람이 선택해야 한다. (코드 이해도와, 이 것이 맞을 것이라는 믿음의 비율에 의존함)
• Assertion : 특정 포인트에서 true여야 한다는 것을 나타낸다.
• 한계 (시험)

  • Weakening the predicate 은 테스팅에 cost를 요구한다.

    → predicate을 만족하는 것은 program execution이 길 따라 잘 작동하는 데이터를 찾기에 충분하지 않다

    ⇒ W를 만족하는 test data는 path를 정상적으로 execute하긴 하지만, 충분하지 않음

    ⇒ W를 만족하지 않는 다는 것은 path가 infeasibility(실현가능하지않다) 라는 것을 보여줌

  • 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

Top을 증명한다면, 아래를 추론할 수 있다.

새로운 프로그래밍 언어를 만들었을 때 정상 동작을 증명하기 위해 위를 밝히면 아래를 추론할 수 있다.

2) Reasoning Style

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

• ex) binary search

• Data Structure module

  : Procedure(method) 의 모음 (specification이 강하게 연결된)

• Contracts

  : Procedure를 inner state의 abstract model(추상 모델)과 관련시킨다.

  ex) Dictionary는 {<key,value>}로 abstract된다.

  Dictionary는 독립적으로 list, tree, hash table 등에 사용된다.

• Structural invariants

  : maintain되어야 하는 structural 특징 (loop invariant와 비슷)

  ex) tree class 내의 모든 method들은 key를 정렬해야 한다.

• Abstract function

  : concrete > abstract model states

  

Summary

• Symbolic execution은 program execution과 logical&mathmatical statement의 다리 역할을 한다.

• loops, procedure calls, data structures의 Symbolic execution은 계층적으로 동작한다.

  (작은 부분을 큰 부분으로 구성)

• Fundamental techniques for

  -Test Data 만들기

  -Verifying systems

  -Performing or checking program transformations(변형)