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은 홀수라서 참을 보장하지만, 추상적 해석은 이를 보장할 수 없기 때문에 경고를 발생시킴
'전공 > 프로그래밍 언어 및 컴파일러' 카테고리의 다른 글
[Lec.Halting] Undecidability, Halting Problem - 11주차 2강 (0) | 2024.12.09 |
---|---|
Lec11. Semantic Analysis (2) - 11주차 2강, 12주차 2강 (0) | 2024.12.09 |
Lec09. Lexer & Parser Generators - 10주차 2강 (0) | 2024.12.08 |
[컴파일러] 과제 환경 세팅 - WSL을 VSCODE로 열기 (0) | 2024.11.07 |
Lec08. Syntax Analysis (4) - 10주차 1강 (5) | 2024.11.05 |