Frama-C/JESSIS 사용법 소개

Size: px

Start display at page:

Download "Frama-C/JESSIS 사용법 소개"

희본 양
5 years ago
Views:

1 Frama-C 프로그램검증시스템소개 POSTECH PL

2 Frama-C? C 프로그램대상정적분석도구 플러그인구조 JESSIE Wp Aorai Frama-C 커널 2 ROSAEC 2011 통영

3 JESSIE? Frama-C 연역검증플러그인 프로그램분석 검증조건추출 증명 Hoare 논리에기초한프로그램검증도구 사용법 $ frama-c jessie < 검증대상 C 파일 > 특징 다양한자동정리증명기및증명보조기지원 함수단위로안전성검증및기능검증수행 3 ROSAEC 2011 통영

4 안전성검증? 프로그램이안전하게동작하는가? 4 ROSAEC 2011 통영

5 안전성검증? 프로그램이안전하게동작하는가? 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 통영

6 기능검증? 프로그램이의도한기능을수행하는가? sort 함수가주어진입력을실제로정렬하는가? 각프로그램마다의도하는기능이다름 void mean(int* p, int* q) ; void sort(int* arr, int len); 사용자가의도하는기능에대한정보필요 6 ROSAEC 2011 통영

7 명세? 프로그램이의도하는기능에대한논리적기술 명세 */ int mean(int* p, int* q) { 종류? requires ensures assigns 7 ROSAEC 2011 통영

8 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 통영

9 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 통영

10 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 통영

11 requires 와 ensures 만으로도충분하다! 11 ROSAEC 2011 통영

12 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 통영

13 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 통영

14 시연! 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 통영

15 반복문!? 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 통영

16 loop variant & loop invariant loop variant e 반복문실행시값이줄어드는정수계산식 loop invariant P 반복문시작점에서항상만족되는조건 16 ROSAEC 2011 통영

17 시연! 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 통영

18 포인터!? 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 통영

19 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 통영

20 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 통영

21 명세 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 통영

22 명세 ( 계속 ) 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 통영

23 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 통영

24 명세 ( 계속 ) 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 시연! 25 ROSAEC 2011 통영

26 감사합니다! 26 ROSAEC 2011 통영

27 27 ROSAEC 2011 통영

11장 포인터

11장 포인터 Dynamic Memory and Linked List 1 동적할당메모리의개념 프로그램이메모리를할당받는방법 정적 (static) 동적 (dynamic) 정적메모리할당 프로그램이시작되기전에미리정해진크기의메모리를할당받는것 메모리의크기는프로그램이시작하기전에결정 int i, j; int buffer[80]; char name[] = data structure"; 처음에결정된크기보다더큰입력이들어온다면처리하지못함