효율적인 포인터 오류 검증 이욱세 한양대학교 컴퓨터공학과 2008. 2. 5

포인터 오류 Java 덕에 포인터 오류가 줄었지만, C/C++로 여전히 많은 프로그램, 특히 OS 및 디바이스 드라이버가 작성되고 있고 오류를 생산하고 있음 디바이스 드라이버: OS 개발자가 아닌 비전문가가 개발, 포인터를 과도하게 사용 프로그램 분석기에서 포인터 연산은 종종 무시됨 포인터가 있으면 분석의 안전성이 보장 안됨

포인터 오류 검증 도구의 덕목 빠르고 정확 현재까지의 결과 [이욱세 2006, 프로그래밍언어논문지 20(1)] 셀 식별 느린 검증 도구는 실제 현장에서 불편 정확 거짓 보고(false alarm)가 많은 도구는 불편 현재까지의 결과 [이욱세 2006, 프로그래밍언어논문지 20(1)] 셀 식별 접근오류 메모리 누수 성능 포인터분석  X O 출생지기반분석 모양분석

모양 분석 (Shape Analysis) [Sagiv et al. 2002, TOPLAS 20(1)] 포인터 오류 검증의 새로운 가능성 제시 정확한 포인터 추적 가능 완전한 변경(strong update) 재귀적 자료구조를 적절히 요약 속도가 현재까지도 문제

완전한 변경 (Strong Update) 포인터 저장문에 대해 제대로 분석하는지 여부 *x가 0일 때, *x = 1; 이후의 분석 결과는? x 가 가리키는 셀이 확실할 때는 *x = { 1 } (완전) x 가 가리키는 셀이 확실치 않을 때는 *x = { 0, 1 } (불완전) 게다가 다른 셀의 내용 변경까지 가능 이것이 안된다면 정확한 포인터 분석은 NO! {0,1} {0} y y x x {0,1} {0}

모양 분석에서 완전한 변경: 가상 주소 포인터 분석 (alias analysis) 출생지 기반 분석 모양 분석 셀을 식별할 때, 경로 사용 x, y, z->next x가 가리키는 셀, y가 가리키는 셀간에 혼동 출생지 기반 분석 셀을 식별할 때, 출생지 사용 출생지가 같은 녀석끼리 혼동: 예, 서울 출생은 모두 100 원을 가지고 있다. 나는 서울 출생 중 한 명에게 100 원을 주었다. 영범이는 서울 출생이다. 영범이는 얼마를 가지고 있지? 모양 분석 셀을 식별할 때, 가상 주소 (symbolic address) 사용 가상 주소는 분석 도중 필요에 따라 부여

모양 분석에서 완전한 변경: 집합 {0} {0}  {1} {0} {0} {0} 다양한 경우를 집합으로 관리하여 따로따로 분석 y y x x {0} {0} {0} 다양한 경우를 집합으로 관리하여 따로따로 분석 y x {0}  {1}

재귀적 자료 구조의 적절한 요약 x y x x y y 공유된 리스트 ns, rx list ns,rx,ry list ns, ry 객체의 속성으로 요약 [Lee et al. 2005, ESOP] [Berdine et al. 2007, CAV] 셀의 속성으로 요약 [Sagiv et al. 2002, TOPLAS] x ns, rx x list s,rx,ry ns,rx,ry list y ns, ry y list

모양 분석에서 완전한 변경: 꺼내기, 넣기 l=x=list0; while(x!=NULL) { x->elm = 1; 요약 노드: 여러 셀을 요약한 것 l=x=list0; while(x!=NULL) { x->elm = 1; x=x->next; } x list elm={1} list elm={0} l elm={0} x list elm={1} list elm={0} l elm={1} x list elm={1} list elm={0} l elm={1} elm={0} 꺼내기! x list elm={1} list elm={0} l elm={1} elm={0} x list elm={1} list elm={0} l 넣기! elm={0}

모양 분석 정리 포인터 오류 검증의 해답에 가까운 유력 후보! 메모리 집합을 표현하는 모양 그래프가 기본 단위 모양 그래프의 멱집합(powerset)을 요약 도메인(abstract domain)으로 하는 프로그램 분석기 특별한 연산 꺼내기 (focusing): 포인터 연산 대상 셀에 대해 수행 넣기 (abstraction 또는 summarization) 합치기 (join)

오늘의 주제는 모양 분석(shape analysis)의 효율적인 수행 CASE 1: [Yang et al. 2008, TR, Queen Mary U. of London] 복잡한 모양 분석 도메인: 중첩 양방향 순환 리스트 (nested cyclic doubly-linked list) 문맥 민감 프로시저 간 분석 (context-sensitive interprocedural analysis) CASE 2: [이욱세 외 6인, ETRI] 단순 모양 분석 도메인: 트리 (tree) 문맥 둔감 프로시저 간 분석 (context-insensitive interprocedural analysis)

CASE I Yang et al. 2008

Peter O’Hearn 그룹의 모양 분석 구성원 분리 논리 (separation logic) 기반 모양 분석 Queen Mary University at London, Imperial College, Microsoft Research at Cambridge 분리 논리 (separation logic) 기반 모양 분석 리스트 [Distefano et al. 2006, TACAS] 중첩 순환 양방향 리스트 [Berdine et al. 2007, CAV] Footprint analysis [Calcagno et al. 2007, SAS]

프로시저 간 분석 (Interprocedural Analysis) 프로시저 호출을 통한 상호작용을 고려한 분석 int f(int x) { return x; } int main() { printf(“%d\n”, f(1)+f(2)); } 문맥 둔감 (context insensitive) 여러 호출을 하나로 묶어서 분석 위 예제에서 f(1), f(2) 두 경우를 합쳐 x는 {1, 2} 이므로, 프로시저 f의 결과는 {1, 2}, 그러므로 f(1)+f(2)는 {2, 3, 4}. 문맥 민감 (context sensitive) 여러 호출을 별도로 분석 위 예제에서 f(1)의 경우 x는 1이므로 결과는 1, f(2)의 경우 x는 2이므로 결과는 2, 그러므로 f(1)+f(2)=3

테이블 기반 문맥 민감 프로시저 간 분석 각 프로시저 별로 입력, 결과 요약 상태를 표에 저장하고, 같은 입력에 대해서는 다시 분석하지 않는 방법 [Reps et al. 2005, POPL] f(1)  1 f(2)  2 모양 분석에서는 모양 그래프 개별 단위로 표에 저장 입력 결과 1 2

정말로 실제적인 분석이 될 수 있을까? 악재 접근 방법 복잡한 모양 분석 도메인 테이블 기반 문맥 민감 프로시저 분석 경우 줄이기: 최적화, 요약 정도를 높임, 지역성 활용 (localization) 메모리 줄이기: 유지하는 표의 크기 감소 및 중간 결과 버리기

BEFORE & AFTER No false alarm!

경우 줄이기 #1. 무효 변수 제거 프로그램 일부분에서 잠깐 사용되고 더 이상 사용되지 않는 변수가 경우의 수를 증가시킴 프로시저 내 생존 분석(liveness analysis)을 통해 더 이상 사용되지 않는 변수를 제거 수작업한 코드의 분석 속도를 향상 List* t, h=0; /* t=0; */ while (nondet) { t = h; h = malloc(); h->next=t; } t=? h=0 t=0 h h list h list t

경우 줄이기 #2. 과감한 경우 결합 (Join) 예전의 분석은 여러 경우로 나누어진 것을 다시 결합하는 연산(join)이 비효율적 거의 합집합 수준: 다음 두 경우를 합치지 못함 확장 연산 (widening) 수준의 과감한 결합 무한루프가 발생할 수 있는 프로시저의 출입구, 반복문에서만 사용 non-empty list non-empty list h h h non-empty list t t t non-empty list

속도 향상 실험 결과: 결합 프로그램 결합 없이 경우의 수 결합 사용시 onelist.c 3 2 twolist.c 9 4 firewire.c 3,969 37 프로그램 줄 결합 없이 결합 사용 속도 (s) 메모리 (MB) 속도(s) t1394Diag.c (일부) 973 184.87 575.82 0.36 2.70 1,825 > 90 min - 1.21 5.16 pci-driver.c 2,532 0.55 4.42 cdrom.c 6,218 107.91 357.58

경우 줄이기 #3: 빈 리스트 처리 빈 리스트 예제: IEEE1394 드라이버 리스트의 요약 노드에 빈 리스트 포함 여부 표기 요약 노드가 빈 리스트(empty list)를 포함하는지 여부가 버그 찾는데 중요 일반적으로 모양분석에서는 빈 리스트와 비지 않은 리스트를 구분하여 분석 결과는 경우 폭발 예제: IEEE1394 드라이버 한 구조체(structure)에는 다섯 개의 리스트 필드 존재 각 필드 별로 빈 리스트, 비지 않은 리스트, 2 가지 경우가 나오므로 최소 25 = 32 가지 경우가 발생 리스트의 요약 노드에 빈 리스트 포함 여부 표기 NE (non-empty), PE (possibly empty) NE < PE 순서에 따라 합쳐 주면 (join) 경우의 수가 감소

속도 향상 실험 결과: PE 프로그램 PE 없이 경우의 수 PE 사용시 onelist.c 2 1 twolist.c 4 firewire.c 37 프로그램 줄 NE NE & PE 속도 (s) 메모리 (MB) 속도(s) t1394Diag.c 10,240 > 90 min - 119.40 425.16 pci-driver.c 2,532 0.55 4.42 cdrom.c 6,218 107.91 357.58

경우 줄이기 #4: 프로시저 분석시 지역성 활용 프로시저 입력 상태에 프로시저와 상관 없는 것이 포함되면 경우의 수가 증가 프로시저와 상관 있는 것 프로시저에서 사용하는 변수에서 도달 가능한 (reachable) 셀 들 y=0,z=0 x=0,y=0,z=0 int f(int x) { return x+z; } x=0,z=0 y=0,z=0 y=1,z=0 x=0,y=1,z=0 y=1,z=0 f(z) f(z) y=0,z=0,$=0 y=0,z=0,$=0 y=0,z=0,$=0 y=1,z=0,$=0 y=1,z=0,$=0 z=0,$=0 y=1,z=0,$=0

속도 향상 실험 결과: 지역성 프로그램 줄 지역성 없이 지역성 사용 속도 (s) 메모리 (MB) 속도(s) t1394Diag.c (일부) 973 0.64 3.69 0.36 2.70 1,825 9.58 1.21 5.16 pci-driver.c 2,532 1.75 9.09 0.55 4.42 cdrom.c 6,218 > 90 min - 107.91 357.58

메모리 줄이기 #1. 듬성 듬성 분석 표 모든 프로그램 지점의 중간 결과를 저장할 필요는 없음 반복문, 결합지점 등 중요한 고정점에 도달했다는 것을 확인하기 위해 필요 반복문, 결합지점 등 중요한 부분에서만 중간 결과 저장 및 고정점 확인 기본 블록 (basic block) 개념 int f(int x) { …. return x+z; } x=0,z=0 x=1,z=0 x=2,z=0 x=8,z=0 x=3,z=0 x=2,z=0 z=0,$=0

메모리 줄이기 #2. 중간 결과 버리기 프로시저 분석이 끝나고 나서 중간 결과들에 대한 표를 저장하고 있을 필요가 없음 중간 결과를 버림으로써 분석 도중 메모리 피크를 낮춤 고정점 계산시 순서를 조정하여야만 버리는 시점을 알 수 있음 int f(int x) { …. return x+z; } x=0,z=0 y=0,z=0 x=0,z=0 y=1,z=0 x=0,z=0 f(z) …. x=0,z=0 y=0,z=0,$=0 z=0,$=0 y=1,z=0,$=0

메모리 절약 실험 결과 프로그램 줄 유지 버리기 속도 (s) 메모리 (MB) 속도(s) pci-driver.c 2,532 0.55 4.42 0.75 3.19 cdrom.c 6,218 107.91 357.58 91.45 84.79 t1394Diag.c 10,240 119.40 425.16 137.78 73.24 md.c 6,635 > 90 min - 1,819.53 1,010.81 ll_rw_blk.c 5,469 947.20 511.43

CASE II Lee et al. 2008

디바이스 드라이버 검증 (ETRI 위탁과제) 목표 디바이스 드라이버 소스 코드를 입력 받아, 입력 코드가 API 규칙을 제대로 지키는지 메모리 오류 및 누수가 없는지 정적으로 검증하는 효과적인 도구를 구현한다. 접근 방법 2005 년: BLAST 기술 정수에 대해 자세히 분석, 경로 민감 분석 포인터는 대강 처리 2006 년~2007 년: 모양 분석 엔진 + 프로그램 분석 포인터에 관한 정교한 분석 + 정수는 필요한 만큼만 분석

API 검증에 포인터 분석이 필요한 이유 d, *e 가 같은 구조체를 의미 혼동 분석(alias analysis) 변수 두 개가 같은 객체를 가리키는 경우만 값싸게 분석 그러나 재귀적 자료구조에는 효과가 없음 SLAM, BLAST 채용 typedef struct { ... int state; } device; device d; device *e = &d; d.state = 0; ... if(e->state!=0) error; open(e); e->state = 1; if(d.state!=1) error; close(&d); if(d.state!=0) error;

APROV 0.92 개요

사용된 모양 분석 엔진 트리 구조만 요약 가능한 단순 요약 노드 문맥 둔감 프로시저 간 분석 정수 필드 포함 스택 주소, 필드 주소 표현 가능 요약은 반복문, 함수 호출에서만 문맥 둔감 프로시저 간 분석 조금 민감: 절단면 (cut-point) 민감 분석 정수는 P({less, -1, 0, …, 5, more}) 효율성은 단순 최적화된 도메인과 정확성을 조금 포기하는 알고리즘에서!

요약 노드 들어오는 엣지로부터 도달가능한 여러 셀을 의미 들어오는 엣지는 하나 나가는 엣지는 없거나 반드시 존재하는 하나 셀이 없을 수도 있음 (PE) 내부 셀: 입구 셀: 바깥에서 들어오는 엣지 하나 중간 셀들: 내부 셀로부터 들어오는 엣지 하나 (공유 없음) 출구 셀: 바깥으로 나가는 엣지 하나

예제: 초점맞추기 x x x x

예제: 요약 Note: 요약은 여러 셀이 있다고 요약되는 것이 아니라 여러 가능성이 있을 때만 요약된다! x x y y z z

구현 최적화: 가상 주소의 수 최소화 x 1 y 2 x z 3 y 1 1 z 2 3 3

프로시저 호출 프로시저에서 사용할 부분만 떼어 내서 프로시저 분석 분석 후 나머지와 결합 메모리 분리 메모리 결합 프로시저 g 프로시저 호출 x y 프로시저에서 사용할 부분만 떼어 내서 프로시저 분석 분석 후 나머지와 결합 x 메모리 분리 g y 메모리 결합 g g y x y 프로시저 분석

기본적으로 문맥 둔감 분석 just_id(x) { return x; } x = non-empty list just_id (x) x = NULL + NULL just_id

절단면 (Cut-Point) 민감 분석 + NULL NULL NULL just_id(x) { return x; } x = non-empty list y points to the last cell of x just_id (x) x = NULL + NULL NULL just_id y NULL

정리 APROV 0.92 Yang et al. 2008과의 비교 성능 테스트는 아직 미완 정확도에 대한 분석도 아직 미완 요약할 수 있는 자료 구조? 리스트 vs 중첩 순환 양방향 리스트 정확도? 문맥 둔감 vs 문맥 민감

결론 무거운 포인터 분석? 여전히 걸림돌 No, 10k lines / 100 seconds 개선의 여지는 아직도 많음 현재 방법론, 최악의 경우 처리 미흡 배열에 대한 적절한 처리 필요 파일 별 분석을 위해 진정한 지역성 필요: footprint analysis