본문 바로가기

전공/프로그래밍 언어 및 컴파일러

Lec10. Semantic Analysis (1) - 11주차 1강

11월 11일, 11주차 1강


* 개인 공부를 위해 정리한 것입니다. 정확한 내용은 꼭 본인이 공부하는 교재를 참고하시기 바랍니다.

 

 

  • soundness: 정확성
    • 분석기가 p가 안전하다고 생각하면, 실제로 p는 안전해야 한다
    • 만약 p가 안전하지 않다면, 분석기는 반드시 unsafe로 판단해야 한다
    • 분석기가 error를 놓치지 않아야 한다. no false negative
  • completeness: 완전성
    • p가 실제로 안전하다면, 분석기는 반드시 p의 안전성을 증명해야 하낟
    • 분석기가 p를 unsafe로 판단했다면, p는 실제로 안전하지 않음
    • 분석기가 안전한 프로그램을 위험하다고 판단하지 않아야 한다. no false positive
  • 이상적인 분석기: no false negative, no false positive

  • hard limit: undecidability 결정 불가능성 - 이상적인 분석기를 만들 수 없는 이유
    • 만약 정확한 분석이 가능하다면 halting problem 을 해결할 수 있어야 함
    • halting problem은 프로그램 P가 멈추는지 여부를 결정할 수 있는 문제
    • halting problem은 이미 증명된 결정 불가능 문제이므로, 이를 해결하는 분석기를 만들 수 없음
  • proof by contradiction: 모순을 통한 증명, 정확한 분석기가 존재한다고 가정
    • 프로그램 p에 assert(false) 추가해 p가 멈추는지(halts) 판단
    • 분석기가 p를 safe로 판단하면 p는 멈추지 않음, unsafe로 판단하면 p는 멈춤 -> halting pb 풀 수 있음
    • 모순: 그러나, halting problem은 결정 불가능하므로, 정확한 분석기가 존재할 수 없음
  • rice theorem
      • 이 튜링 완전한 언어라고 가정합니다.
        비자명한 의미론적 속성(nontrivial semantic property)이라고 할 때:
      • L에 있는 일부 프로그램은 를 만족하며, 일부는 를 만족하지 않음
        • 이런 에 대해, 모든 프로그램에 대해 를 판단하는 알고리즘 는 존재하지 않음
      • 프로그램의 비자명한 속성(예: 정지 여부, 안전성)을 정확히 분석하는 것은 불가능함

  • under-approxiamtion(과소 근사)
    • completeness(완전성) 유지, soundness(정확성) 희생
    • 모든 발견된 오류는 실제 오류지만, 놓친 오류 false negative가 있을 수 있다
    • 실제로 존재하는 오류만 탐지 - true positive, 일부 오류를 놓칠 수 있음 - false negative
    • 오류는 프로그램의 부분집합으로 표시
  • over-approximation(과대 근사)
    • soundness(정확성) 유지, completeness(완전성) 희생
    • 탐지된 오류는 정확하지만, 실제 오류가 아닌 것도 탐지될 수 있음 - false positive
    • 탐지된 오류는 항상 실제 오류 - true positive, 오류가 아닌 것을 탐지할 수 있음 - false positive
    • 오류와 프로그램 영역이 겹치며, 실제 오류 외에 탐지된 오류가 있을 수 있음

  • line5에서 오류를 유발하는 입력값 찾기, x=2*y를 만족하면서,  y>10인 값을 찾아야 함
    • y는 y>10와 y<=100조건에 의해 11~100 사이 값이 가능하고, x=2*y 조건에 의해 11~50값이 가능함 ->40개
    • 따라서 y가 유효범위에 있을 확률은 P(y) = 40/100 = 0.4%

  • 프로그램에서 입력값을 구체적인 값 대신 symbolic variables로 나타냄
  • SMT 솔버로 논리적 제약 조건을 만족하는 값을 찾음

  • formal verification: 형식적 검증
    • precondition: 프로그램이 실행되기 전에 참이라고 가정하는 조건, n은 0 이상이다
    • postcondition: 프로그램 실행이 끝난 후 참이어야 하는 조건, j=n이 성립해야 한다
  • fuzzing과 symbolic execution은 postcondition을 증명할 수 없다
    • fuzzing: 다양한 입력 값으로 테스트하지만, 모든 경우를 방증할 수느 없음
    • symbolic execution: 프로그램의 경로를 따라가며 조건식을 생성하지만, loop의 무한한 경우를 정확히 처리는 x
  • loop invariant: 루프 불변 조건
    • 반복문이 시작될 때, 반복되는 과정 중, 종료될 때 항상 참인 조건을 정의해 반복문이 올바르게 동작함을 증명
    • 반복문이 실행되는 동안 i=j 유지
    • 초기 조건: i=0, j=0이므로 i=j
    • 반복 유지: i와 j가 동시에 1씩 증가해 i=j
    • 종료조건: 종료 시 i=n, 불변조건 i=j에 의해 j=n도 성립
    • 정확히 n번 실행되고, 종료시 j=n임을 증명할 수 있음

  • 버블 정렬
    • 알고리즘에 대한 불변조건을 사용해 형식적 검증을 수행
    • 불변 조건을 추론해 정렬이 올바르게 동작하는지 증명하는 과정
    • sorted(a,l,u) 배열의 a의 인덱스 l부터 u까지 정렬되어 있음을 나타냄
    • paritioned(a,l1,u1,l2,u2) 배열 a의 두 구간의 모든 값에 대해 우측 구간이 더 큰값을 가짐을 나타냄
  • L1: 외부 반복문 불변 조건, 배열의 오른쪽 끝부터 정렬해나감
    • partitioned에서 우측 구간이 정렬된 부분. 배열의 오른쪽 끝 부분은 항상 정렬되어 있음을 나타냄
  • L2: 내부 반복문 불변 조건, i까지의 배열을 한번씩 확인하며 정렬함
    • 0부터 i까지 요소에 대해 정렬 구간, 미정렬 구간으로 나눈다. 배열이, 오른쪽 끝부분은 정렬된 상태
  • 외부 반복문이 종료되는 조건: i=-1, sorted(a,0,|a|--1)이 성립함

 

추상적 해석을 사용해 프로그램의 안정성을 증명하는 과정

  • 코드에서 항상 assert(y%2==1)임을 증명해야 함, y가 항상 홀수임
  • 입력값 대신 입력값의 추상적 특성인 짝수, 홀수로 분석함
  • x: 정수, x*12: 짝수, 9*11: 홀수 -> 짝수+홀수 = 홀수, 따라서 y는 항상 홀수
  • 모든 가능한 입력에 대해 간결하고 추상적인 방식으로 증명할 수 있음

추상적 해석의 한계

  • x를 모든 가능한 정수로 두고, y도 모든 가능한 정수로 둠. 임의의수+홀수 = 임의의 수는 항상 홀수가 아닐 수 있음
  • 실제로 오류가 없는 경우에도 경고 false alarm을 발생시킬 수 있음.
  • 수학적으로 2x+1은 홀수라서 참을 보장하지만, 추상적 해석은 이를 보장할 수 없기 때문에 경고를 발생시킴