스파스 분석 틀 (Sparse Analysis Framework)

정확하고 안전한 프로그램 전체 분석을 초대형 프로그램에까지

오학주, 허기홍, 이원찬, 이우석, 이광근
서울대학교 프로그래밍 연구실, 소프트웨어 무결점 연구센터

소개

스파스 분석 틀 (sparse analysis framework) 은 실행상황을 정확하게(precise) 모두 포섭하면서(sound) 프로그램을 한꺼번에 정적 분석(global static analysis) 할 때, 이를 초대형 프로그램에까지 확장 가능하게끔 (scalable) 만들어 주는 일반적인 방법입니다. 어떤 언어로 작성된 프로그램을 분석하든, 또는 어떤 성질 (관계 분석이든 비관계 분석이든)을 분석하든 관계 없이, 요약해석 (abstract interpretation) 이론에 기반하여 설계된 분석이면 적용이 가능합니다. 분석기를 설계하는 사람은 우선 성능을 생각하지 않은 채 요약해석 이론을 이용해서 올바른 정적 분석기를 설계합니다. 그리고 이 틀이 제시하는대로 스파스 분석을 유도해내면 기존 분석의 정확도를 잃지 않은채 초대형 프로그램까지 분석해 낼 수 있습니다. 이 틀이 기존 분석의 정확도를 잃지 않기 위해서 꼭 지켜야 할 사항들을 제시해 주기 때문에 가능합니다.

스파스 분석이란?

아래 슬라이드는 스파스 분석의 핵심 아이디어를 기존 프로그램 분석과 대비해서 설명합니다.

논문

Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi. Design and Implementation of Sparse Global Analyses for C-like Languages. PLDI 2012 [pdf] [bib]
Hakjoo Oh and Kwangkeun Yi. Access-based Localization with Bypassing. APLAS 2012. [pdf] [bib]
Hakjoo Oh, Lucas Brutschy, and Kwangkeun Yi. Access Analysis-based Tight Localization of Abstract Memories. VMCAI 2011. [pdf] [bib]