프로그램분석. SW오류검증. 산과골. 미개한. 08/29/2011 @ 학부교수점심발표
문제 작성한 SW 의오류를자동으로미리모두찾아주거나, 없으면없다고확인해주는기술들은있는가? 그래서, SW 의오류때문에발생하는 개인 / 기업 / 국가 / 사회적비용을 절감시켜주는기술들은있는가?
목표 소프트웨어 MRI 소프트웨어 fmri 소프트웨어 PET
기반기술 정적프로그램분석 (static program analysis) 프로그램의실행성질을실행전에자동으로안전하게어림잡는일반적인방법엄밀히예측테스팅의단점을보완실용성확산 ( 국내외성과 ) 우리예 ) 산업화한 Sparrow
기반기술실용성예시 : Sparrow 대상 : C, memory leak/buffer overrun/etc, 오류검출률 6/KLOC, 속도 100Loc/sec
기술위치
오늘내용 구체적인예 : Sparrow 기술한계진행연구
Sparrow (as of 2008) static analyzer fully automatic and scalable detects common bugs buffer overrun, memory leak, null dereference, uninitialized access, divide by zero, etc. for non domain-specific C code From the elusive three (deep property, scalability, automation) deep property + domain-independence
Steps of Sparrow One-button solution with four steps:
Our motivation (as of 2004) to prove that static analysis is useful in real world curious about extra miles from academia to industry Of course, the reality has been challenging us a lot, and we ve been struggling to respond to.
Sparrow-detected Overrun Errors (1/3) in Linux Kernel 2.6.4 625 for (minor = 0; minor < 32 && acm_table[minor]; minor++);...... 713 acm_table[minor] = acm; in a proprietary code if (length >= NET_MAX_LEN)... return API_SET_ERR_NET_INVALID_LENGTH; buff[length] = (num << 4); in a proprietary code index = memmgr_get_bucket_index(block_size);... mem_stats.pool_ptr[index] = prt in a proprietary code imi_send_to_daemon(pm_eap, CONFIG_MODE, set_str, sizeof(set_str));... imi_send_to_daemon(int module, int mode, char *cmd, int len) {... strncpy(cmd, reply.str, len); cmd[len] = 0;
Sparrow-detected Leak Errors (2/3) in sed-4.0.8/regexp internal.c 948: new_nexts = re_realloc (dfa->nexts, int, dfa->nodes_alloc); 949: new_indices = re_realloc (dfa->org_indices, int, dfa->nodes_alloc); 950: new_edests = re_realloc (dfa->edests, re_node_set, dfa->nodes_alloc); 951: new_eclosures = re_realloc (dfa->eclosures, re_node_set, 952: dfa->nodes_alloc); 953: new_inveclosures = re_realloc (dfa->inveclosures, re_node_set, 954: dfa->nodes_alloc); 955: if (BE (new_nexts == NULL new_indices == NULL 956: new_edests == NULL new_eclosures == NULL 957: new_inveclosures == NULL, 0)) 958: return -1; in proprietary code line = read_config_read_data(asn_integer, line, &StorageTmp->traceRouteProbeHistoryHAddrType, &tmpint);... line = read_config_read_data(asn_octet_str, line, &StorageTmp->traceRouteProbeHistoryHAddr, &StorageTmp->traceRouteProbeHistoryHAddrLen);... if (StorageTmp->traceRouteProbeHistoryHAddr == NULL) { config_perror ( invalid specification for tracerouteprobehistoryhaddr ); return SNMPERR_GENERR; }
Sparrow-detected Leak Errors (3/3) in mesa/osmesa.c(in SPEC 2000) 276: osmesa->gl_ctx = gl_create_context( osmesa->gl_visual );... 287: gl_destroy_context( osmesa->gl_ctx ); ------------------ 1164: GLcontext *gl_create_context( GLvisual *visual,... GLcontext *share_list, void *driver_ctx ) { 1183: ctx = (GLcontext *) calloc( 1, sizeof(glcontext) );... 1211: ctx->shared = alloc_shared_state(); --------------------- 476: static struct gl_shared_state *alloc_shared_state( void ) 477: {... 489: ss->default1d = gl_alloc_texture_object(ss, 0, 1); 490: ss->default2d = gl_alloc_texture_object(ss, 0, 2); 491: ss->default3d = gl_alloc_texture_object(ss, 0, 3); ---------------------- 1257: void gl_destroy_context( GLcontext *ctx ) 1258: {... 1274: free_shared_state( ctx, ctx->shared );
기술소개
정적프로그램분석 (static program analysis) 프로그램의실행성질을실행전에자동으로안전하게어림잡는일반적인방법 응용 : sw 오류검증, sw 관리, sw 테스트, sw 최적화, 등등 다양한레벨 / 목적 / 이름으로존재 : theory pl, se, veri. cmplr 요약해석 abstract interpretation type system, model checking, theorem proving data-flow analysis, etc.
기술위치 ( 우물안 )
기술단계 ( 우물밖 )
현수준
아직은아닌
( 여담 ) 정적분석은가까이에늘 대학입학시험궁합점, 손금, 관상나이트클럽기도무이론 + 대충. 틀리는것이문제. 다른공학분야의정적분석기계설계분석검증후제작전기설계분석검증후제작공정설계분석검증후설비건축설계분석검증후건설
정적프로그램분석 실행전 : 프로그램을실행시키지않고 자동으로 : 프로그램이프로그램을분석 안전하게 : 모든가능성을포섭 어림잡는 : 실제이외의것들이포함됨어림잡지않으면불가능 일반적 : 소스언어와성질에무제한 C, Java, ML, Bluespec, Dalvik, x86, binary, etc. buffer overrun?, memory leak?, unhandled exn? x=y at line 2?, memory use 2K?, terminate?, race? etc. One-on-One : 분석기1개당, 1언어 1성질.
정적프로그램분석비유 128 22 + (1920 10) + 4는어떤값을계산합니까? 정적분석 : 정수입니다. 정적분석 : 짝수입니다. 정적분석 : 10, 0000과 1, 0000 사이의수입니다. 정적분석 : 음수입니다.
정적프로그램분석예 x = readint; while (x 99) x++; 실행중 / 후에변수 x가가질값은?
정적분석기개발싸이클 1. 분석할소스언어결정 : C, Java, ML, Bluespec, Dalvik, JVM, x86, binary 2. 분석할실행성질결정 : buffer overrun? memory leak? race? uncaught exn? time/power/memory/wire consumption? equivalent? terminate? etc. 3. ( 디자인 ; 구현 ; 테스트 ) +
모든정적분석은 3 스텝 1. 연립방정식 을세운다요약된세계에서 (abstract semantic domains) 프로그램의실행다이나믹스에관한 (abstract execution flows) 2. 그방정식을푼다 3. 그해를가지고결론을내린다있는가없는가? 같은가다른가?
프로그램분석이론 PL 이론과어휘를사용 올바른연립방정식을어떻게유도하는가? 방정식이실제실행의모든것을포착하는가? 유도한연립방정식의해는항상있는가? 그해를어떻게계산하는가? 유한시간내에해를구할수있는가?
다른분야와다르지않은 프로그램 기계디자인 실행 = 컴퓨터 ( 언어정의 ) 작동 = 자연 ( 자연법칙 ) 실행에대한방정식 작동에대한방정식 방정식풀기 방정식풀기 생각대로돌것이다 생각대로작동할것이다 무인비행기에심자 만들어팔자 PL & Logic 이론 물리-화학법칙, XX방정식
정적프로그램분석기술의한계 I (SW 오류분석에서 ) 마의삼각형 단둘만가능
정적프로그램분석기술의한계 II (SW 오류분석에서 ) 허위경보 (false alarm) 오류가아닌것을오류라고판별 이론적으로불가능 : 허위경보가항상 0
우리가보는틈새 (SW 오류분석에서 ) 오류검출과무결점검증오류검출 (bug-finding) 허위경보가항상적음 ( 20%, non domain-specific) 오류를모두찾지못함무결점검증 (verification) 허위경보가거의 0 오류를모두찾는것이보장특정 SW에대해서만 (domain-specific)
오류검출기 (bug-finder) 있는오류대부분을검출 not exhaustive a few false-alarm domain-independent 허위경보율 20%
무결점검증기 (verifier) 오류가없으면없다고확인 exhaustive zero false-alarm domain-specific 허위경보율 1%
정적분석기술제품상황 전세계적으로 무결점검증기 (verification-level analyzer) 개발업체는아직. 오류검출기 (bug-finder) 들이시장에있슴경쟁잣대 : 오류검출력 vs 허위경보율 vs 센스있는 오류들 vs UI+UX
진행연구들 이론 실제 multi-staged programming language (e.g. web pgm): 분석 어떻게? implicit programming (e.g. 분석어떻게? Sparrow 개선 : Android app 분석기 : semantic clone detector binary malware detector Bluespec analyzers Haskell, Scala, C++ Concept): more scalable, alarm clustering, etc. privacy leak detector Hypervisor Xen core verification by Coq 논문들 : POPL 06, POPL 11, ICSE 11, VMCAI 11, TACAS 11, TOPLAS, SPE, TCS, Acta Info. etc.
SW Clinic Service 대상 : C 프로그램실습학생, C 프로그램개발자등 http://rosaec.snu.ac.kr/clinic