Frama-C 프로그램검증시스템소개 박종현 @ POSTECH PL
Frama-C? C 프로그램대상정적분석도구 플러그인구조 JESSIE Wp Aorai Frama-C 커널 2 ROSAEC 2011 동계워크샵 @ 통영
JESSIE? Frama-C 연역검증플러그인 프로그램분석 검증조건추출 증명 Hoare 논리에기초한프로그램검증도구 사용법 $ frama-c jessie < 검증대상 C 파일 > 특징 다양한자동정리증명기및증명보조기지원 함수단위로안전성검증및기능검증수행 3 ROSAEC 2011 동계워크샵 @ 통영
안전성검증? 프로그램이안전하게동작하는가? 4 ROSAEC 2011 동계워크샵 @ 통영
안전성검증? 프로그램이안전하게동작하는가? 32비트정수표현범위안에서만계산? 할당된메모리영역만참조? 프로그램이유한시갂안에종료? 예제 int mean(int p, int q) { return (p + q) / 2; int mean(int p, int q) { return p / 2 + q / 2 + (p % 2 + q % 2) / 2; 5 ROSAEC 2011 동계워크샵 @ 통영
기능검증? 프로그램이의도한기능을수행하는가? sort 함수가주어진입력을실제로정렬하는가? 각프로그램마다의도하는기능이다름 void mean(int* p, int* q) ; void sort(int* arr, int len); 사용자가의도하는기능에대한정보필요 6 ROSAEC 2011 동계워크샵 @ 통영
명세? 프로그램이의도하는기능에대한논리적기술 /*@ 명세 */ int mean(int* p, int* q) { 종류? requires ensures assigns 7 ROSAEC 2011 동계워크샵 @ 통영
requires & ensures requires P 함수가호출될때만족해야하는조건 \valid ensures P 함수가종료된후만족되어야하는조건 \result 예제 /*@ requires \valid(p) && \valid(q) ensures \result == (*p + *q) / 2; */ int mean(int* p, int* q) { return *p / 2 + *q / 2 + (*p % 2 + *q % 2) / 2; 8 ROSAEC 2011 동계워크샵 @ 통영
requires & ensures ensures 는함수가종료된후상태를기술 /*@ requires \valid(p) && \valid(q); ensures \result == (*p + *q) / 2; */ int mean(int* p, int* q) { *p = 0; *q = 0; return 0; \old /*@ requires \valid(p) && \valid(q); ensures \result == (\old(*p) + \old (*q)) / 2; */ int mean(int p, int q) { *p = 0; *q = 0; return 0; 9 ROSAEC 2011 동계워크샵 @ 통영
requires & ensures ensures 는함수가종료된후상태만을기술 예제 /*@ requires \valid(p) && \valid(q); ensures \result == (\old(*p) + \old(*q)) / 2; */ int mean(int* p, int* q) { int i = 0; while( i >= 0 ); return 0; 10 ROSAEC 2011 동계워크샵 @ 통영
requires 와 ensures 만으로도충분하다! 11 ROSAEC 2011 동계워크샵 @ 통영
assigns 하지만 int M; /*@ requires \valid(p) && \valid(q); ensures \result == (\old(*p) + \old (*q)) / 2; */ int mean(int* p, int* q) { M = 0; return *p / 2 + *q / 2 + (*p % 2 + *q % 2) / 2; assigns L 함수가종료된후변경될수있는외부메모리영역한정기술되지않은메모리영역은변경되지않음 \nothing 12 ROSAEC 2011 동계워크샵 @ 통영
assigns 하지만 int M; /*@ requires \valid(p) && \valid(q); ensures \result == (\old(*p) + \old (*q)) / 2; assigns \nothing; */ int mean(int* p, int* q) { M = 0; return *p / 2 + *q / 2 + (*p % 2 + *q % 2) / 2; assigns L 함수가종료된후변경될수있는외부메모리영역한정기술되지않은메모리영역은변경되지않음 \nothing 13 ROSAEC 2011 동계워크샵 @ 통영
시연! /*@ requires \valid(p) && \valid(q); ensures \valid == (\old(*p) + \old(*q)) / 2; assigns \nothing; */ int mean(int* p, int* q) { return *p / 2 + *q / 2 + (*p % 2 + *q % 2) / 2; 14 ROSAEC 2011 동계워크샵 @ 통영
반복문!? /*@ requires len >= 1 && \valid_range(arr, 0, len 1); ensures 0 <= \result < len; ensures \forall int i; 0 <= i < len ==> arr[i] <= arr[\result]; assigns \nothing; */ int find_max(int* arr, int len) { int idx = 0; for(int i = 1; i < len; i++) if( arr[i] > arr[idx] ) idx = i; return idx; 15 ROSAEC 2011 동계워크샵 @ 통영
loop variant & loop invariant loop variant e 반복문실행시값이줄어드는정수계산식 loop invariant P 반복문시작점에서항상만족되는조건 16 ROSAEC 2011 동계워크샵 @ 통영
시연! /*@ requires len >= 1 && \valid_range(arr, 0, len 1); ensures 0 <= \result < len; ensures \forall int i; 0 <= i < len ==> arr[i] <= arr[\result]; assigns \nothing; */ int find_max(int* arr, int len) { int idx = 0; idx i len-1 /*@ loop variant len i; loop invariant 0 <= i <= len; loop invariant 0 <= idx < i; loop invariant \forall int n; 0 <= n < i ==> arr[n] <= arr[idx]; */ for(int i = 1; i < len; i++) if( arr[i] > arr[idx] ) idx = i; return idx; 17 ROSAEC 2011 동계워크샵 @ 통영
포인터!? typedef struct _list { int element; struct _list *next; list; /*@ requires \valid(root) &&???; ensures???; assigns \nothing; */ list *find_max(list *root) { list *ptr = root; while(root->next) { root = root->next; if( root->element > ptr->element ) ptr = root; return ptr; 18 ROSAEC 2011 동계워크샵 @ 통영
inductive & predicate inductive & predicate 대상에대한논리적성질정의 예제 /*@ inductive reachable{l(list *root, list *node) { case reachable_root {L: \forall list* root; reachable(root, root); case reachable_next {L: \forall list* root, *node; \valid(root) ==> reachable(root->next, node) ==> reachable(root, node); */ //@ predicate finite_list{l(list *l) = reachable(l, \null); 19 ROSAEC 2011 동계워크샵 @ 통영
inductive & predicate 예제 ( 계속 ) /*@ predicate connected_list{l(list *root) = \forall list *node; reachable(root, node) ==> node == \null (\valid(node->next) && reachable(root, node->next)); */ //@ predicate linked_list{l(list *l) = finite_list(l) && connected_list(l); 20 ROSAEC 2011 동계워크샵 @ 통영
명세 /*@ requires \valid(root) && linked_list(root); ensures \valid(\result) && reachable(root, \result); ensures \forall list *node; \valid(node) ==> reachable(root, node) ==> assigns \nothing; */ list *find_max(list *root) { node->element <= \result->element; /*@ requires len >= 1 && \valid_range(arr, 0, len 1); ensures 0 <= \result < len; ensures \forall int i; 0 <= i < len ==> arr[i] <= arr[\result]; assigns \nothing; */ 21 ROSAEC 2011 동계워크샵 @ 통영
명세 ( 계속 ) list *ptr = root; loop variant??? /*@ loop invariant \valid(root) && \valid(ptr); loop invariant reachable(\at(root, Pre), root); loop invariant reachable(\at(root, Pre), ptr); loop invariant \forall list *node; \valid(node) ==> reachable(\at(root, Pre), node) &&!reachable(root->next, node) ==> node->element <= ptr->element; */ while(root->next) { /*@ loop variant len i; root = root->next; loop invariant 0 <= i <= len; if( root->element loop > invariant ptr->element 0 <= idx ) ptr < = i; root; loop invariant \forall int n; 0 <= n < i ==> arr[n] <= arr[idx]; */ return ptr; 22 ROSAEC 2011 동계워크샵 @ 통영
logic logic 입력에따라결과를반환하는논리함수정의 프로그램상의값을이용해야할경우? 예제 선언적정의를이용해서함수정의 /*@ axiomatic Length { logic integer length{l(list *root); axiom length_nil{l : length(\null) == 0; axiom length_cons(l : \forall list *l; \valid(l) ==> length(l) == length(l->next) + 1; */ /*@ predicate finite_list{l(list *l) = reachable(l, \null) && \forall list *node; reachable(l, node) ==> length(node) >= 0; */ 23 ROSAEC 2011 동계워크샵 @ 통영
명세 ( 계속 ) list *ptr = root; /*@ loop variant length(root); loop invariant \valid(root) && \valid(ptr); loop invariant reachable(\at(root, Pre), ptr); loop invariant reachable(\at(root, Pre), root); loop invariant \forall list *node; \valid(node) ==> reachable(\at(root, Pre), node) &&!reachable(root->next, node) ==> node->element <= ptr->element; */ while(root->next) { root = root->next; if( root->element > ptr->element ) ptr = root; return ptr; 24 ROSAEC 2011 동계워크샵 @ 통영
시연! 25 ROSAEC 2011 동계워크샵 @ 통영
감사합니다! 26 ROSAEC 2011 동계워크샵 @ 통영
27 ROSAEC 2011 동계워크샵 @ 통영