정적분석기술을 이용한 sw오류 자동 검증 Airac의 예를통해서 이광근 프로그래밍 연구실 서울대 컴퓨터공학부 4/21/2005 @ Netsec’05

차례 프로그램 정적분석 기술 소개 Airac 소개

소프트웨어 오류의 비용 소프트웨어 오류를 일반사람들이 점점 접한다: 일상=컴퓨터 오류로 인한 불편이 사회적 문제가 된다. 소프트웨어 오류에 대한 책임소재 입법화. 소프트웨어 개발업체의 대응: 보험을 든다. 소프트웨어 가격의 상승. 모든 제품의 경쟁력 = 무결점/고품질 저비용 소프트웨어

소프트웨어의 오류 잡는 기술 만족스럽지못한 현재 새로운 기술 sw tests runtime monitoring field manual 새로운 기술 프로그램 분석기술 static program analysis 30-40년간 연구된 기술 산업체에서 관심가지기 시작

아이락 = 소프트웨어 MRI Airac Parsing and transformation done: 25 ast nodes Option: the unrolling depth 3 the unrolling bound 0 Analysis begins Fixpoint iterations with widening Fixpoint iterations with narrowing Result: array index out of bound at (file: a.c, line: 13) Overflow (array index: [24, 24], array size: [10, 10])

아이락 Airac static analyzer for automatic verification of array index ranges in C programs 소프트웨어의 오류 (메모리접근오류) 자동 검출기 무결점 소프트웨어의 저렴한 개발을 위한 첨단 기반기술 전세계적으로 2003년 이후에야 실용화되고있는 기술 소프트웨어를 테스트하지 않고 자동으로 모든 오류를 찾아줌: 저비용 무결점 달성 기술 (정적프로그램분석기술static program analysis) 2004년 스탠포드대학의 도슨 앵글러 교수가 상용화한 검증기 성능을 능가.

프로그래밍 연구실 + 프로그램 분석 시스템 연구단 프로그래밍 연구실 + 프로그램 분석 시스템 연구단 1995-2003 KAIST, 2003-now SNU 1998-2003 과기부 창의적연구 진흥사업 지정 프로그램분석 시스템 연구단 목표: 무결점 소프트웨어를 만들고 확인할 수 있는 원천 기술 연구 “The Open Problem in Computer Science”

static program analysis 원천 기술 프로그램 분석기술 static program analysis 실행전에 실행성질을 자동으로 안전하게 어림잡는 일반적인 방법

프로그램 분석 static program analysis “실행전”: 프로그램을 돌리기 전에 “실행성질”: 실행중의 프로그램 성질 “자동으로”: 프로그램이 프로그램을 분석 “안전하게”: 모든 실제상황을 포섭 “어림잡는”: 군더더기가없을 순 없다 “일반적인”: 대상 소스 언어와 실행성질이 무제한

프로그램 분석기술의 쓰임새 프로그램의 오류 자동 검증 프로그램 최적화를 위한 정보제공 프로그램 이해/관리를 위한 정보제공 실행중에 이러이러하면 안되는 데, 혹시? “오류”의 정의에 따라서 다양하게: “보안 오류” 프로그램 최적화를 위한 정보제공 이 부분은 중복되는 일을 하는군 이 부분은 자원을 필요이상으로 소모하는군 프로그램 이해/관리를 위한 정보제공 이 변수와 관계되는 프로그램 부분들만 프로그램이 어느 테이블을 건드리는지

프로그램 분석 기술들 프로그램 분석(static program analysis) 20-30년 동안 학교에서 무르익은 기술 요약해석(abstract interpretation) 타입시스템(type system) 자료흐름분석(data flow analysis) 자동증명(theorem proving) 모델검증(model checking) 20-30년 동안 학교에서 무르익은 기술 위의 기술의 조합이 이제 비로소 실용적인 모습으로 현장으로 퍼지고 있슴

프로그램분석 기술이 실제에 적용된 예 Microsoft (2002년-현재) AirBus (2002년-현재) 프로그램분석 기술이 실제에 적용된 예 Microsoft (2002년-현재) device driver sw 검증에 적용 안전한, 오류없는 sw개발에 집중: 요즘 Bill Gates 연설의 기초 AirBus (2002년-현재) aviation controller모듈 sw 검증에 적용 AirBus sw개발 프로세스의 표준으로 프로그램분석 과정을 포함 삼성전자 소프트웨어 센터 (2004년-현재) Airac: 다양한 sw 검증에 적용 이기술에 특화된 회사들 등장: AbsInt, Coverity, PolySpace technologies, Trusted Logic, GrammaTech, Esterel Technologies, etc.

Value = Int U Real U Addr U Tree U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U Exception val(x) val(*p) val(p) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 요약실행 V = I U R U A U T U E v(x) v(*p) v(p) pgm point 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

Value = Int U Real U Addr U Tree U List U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U List U Exception v(x) v(y) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 오류 검증 V = I U R U A U T U E v(x) v(*p) v(y) pgm point 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

Value = Int U Real U Addr U Tree U List U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U List U Exception val(x) val(y) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 허위경보 V = I U R U A U T U E v(x) v(y) 프로그램 분석의 정확도 문제 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

Value = Int U Real U Addr U Tree U List U Exception 프로그램의 실행 Value = Int U Real U Addr U Tree U List U Exception val(x-y) 1 2 11 3 4 5 11 3 4 5 11 3 4 5 22 8 9 8 9 8 9 2 3 4 99 2 3 4 99 2 3 4 time

프로그램의 분석: 관계형분석 V = I U R U A U T U E v(x-y) pgm point 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 pgm point

프로그램 분석의 3-스텝 입력: 프로그램 step1: “연립방정식”을 세운다 step2: 그 방정식을 푼다 모든것이 요약된 세계에서 (abstract domain) 모든 프로그램의 상태가 어떻게 변화되 가는지 (abstract execution flow) step2: 그 방정식을 푼다 step3: 그 해를 가지고 결론을 내린다 있는가 없는가? 같은가 다른가?

Airac Static Analyzer for Automatic Verification of Array Index Ranges in C Programs

Airac int *c = (int *)malloc(sizeof(int)*10); C 프로그램의 메모리접근 오류 자동 검출 c[i] = 1; c[i + f()] = 1; c[*k + (*g)()] = 1; x = c; x[1] = 1; y = c + f(); y[*(y+1)] = 1; z->a = c; (z->a)[i] = 1; foo(c+2); int foo(int *d) {… d[i] = 1; …}

Airac keywords C: analyzes ANSI C + (GNU) program pointers(array, procedure) controls(procedure, return, break, goto) intra- and inter-procedural statically: no test runs all: complete, no un-noticed bug automatic: a software always stops: for infinite-loop programs modular: for large programs correct: solid theoretical foundation

Airac: performance (1/3) (commercial softwares) X Softwares Alarms Real Errors LOC Time (min) 검증용 Code 46 34 4,688 306 A1 18 9 280,379 8 A2 196 56 3,584,664 789 A3 78 15 119,211 82 A4 435 7 806,829 112 A5 197 517,314

Airac: performance (2/3) Linux kernel 2.6.4 Alarms Real Errors LOC Time (sec) vmax302.c 1 246 0.28 xfrm_user.c 2 1,201 45.07 usb-midi.c 10 4 2,206 91.32 atkbd.c 811 1.99 keyboard.c 1,256 3.36 af_inet.c 1,273 1.17 eata_pio.c 3 984 7.50 cdc_acm.c 849 3.98 ip6_output.c 1,110 1.53 mptbase.c 6,158 0.79 aty128fb.c 2,466 0.32

Airac: performance (3/3) GNU Softwares Alarms Real Errors LOC Time (sec) tar-1.13 66 1 20,258 577 bison-1.875 50 15,907 809 sed-4.0.8 29 6,053 1154 gzip-1.2.4a 17 7,327 794 grep-2.5.1 2 9,297 604

Airac: scalability

Airac vs Swat (1/3) (국제경쟁력) Linux kernel 2.6.4 SWAT (Stanford) AIRAC (서울대) Found Errors /drivers/mtd/maps/vmax301.c 1 /net/xfrm/xfrm_user.c /drivers/usb/class/usb-midi.c 2 /drivers/input/keyboard/atkbd.c /drivers/char/keyboard.c /net/ipv4/af_inet.c /drivers/scsi/eata_pio.c /drivers/usb/class/cdc-acm.c (*) 3 /net/ipv6/ip6_output.c (**) /drivers/message/fusion/mptbase.c /drivers/video/aty/aty128fb.c

Airac vs Swat (2/3) Airac Bugs Coverity

Airac vs Swat (3/3) 구분 SWAT (Coverity社) AIRAC (서울대) 에러 검출력 62% detect율 (8/13) 100% detect율 (13/13) A 적용결과 #Alarms: 19 buffers #Real Errors: 2 buffers #False Alarms: 17 buffers Time: 7 min #Alarms: 78 #Real Errors: 15 access (5 buffers) #False Alarms: 63 access (18 buffers) Time: 82 min B 적용결과 #Alarms: 2 buffers #False Alarms: 0 buffers Time: 4 min #Alarms: 18 #Real Errors: 9 access (2 buffers) #False Alarms: 9 access (6 buffers) Time: 8 min

cdc_acm.c (Linux device driver)

rmt.c (GNU software – tar)

hardtoswat.c (homemade sample)

감사합니다 ropas.snu.ac.kr/airac