함수 요약에 기반한 메모리 누수 정적 탐지기 = A Static Analyzer for Detecting Memory Leaks based on Procedural Summary

국문 초록 (Abstract)

C프로그램에서 발생할 수 있는 메모리 누수(memory leaks)를 실행 전에 찾아 주는 분석기를 제안한다. 이 분석기는 SPEC2000 벤치마크 프로그램과 여러 오픈 소스 프로그램들에 적용시킨 결과 다른 분석기에 비해 상대적으로 뛰어난 성능을 보여준다. 총 1,777 KLOC의 프로그램에서 332개의 메모리 누수 오류를 찾아냈으며 이 때 발생한 허위 경보(false positive)는 47개에 불과하다(12.4%의 허위 경보율). 이 분석기는 초당 720 LOC를 분석한다. 각각의 함수들이 하는 일을 요약하여 그 함수들이 불려지는 곳에서 사용함으로써 모든 함수에 대해 단 한번의 분석만을 실행한다. 각각의 함수 요약(procedural summary)은 잘 매개화 되어 함수가 불려질 때의 상황에 맞게 적용할 수 있다. 실제 프로그램들에 적용하고 피드백 받는 방법을 통해 함수가 하는 일중에 메모리 누수를 찾는데 효과적인 정보들만으로 추리는 과정을 거쳤다. 분석은 요약 해석(abstract interpretation)에 기반하였기 때문에 C의 여러 문법 구조와 순환 호출(recursive call), 루프(loop)등은 고정점 연산(fixpoint iteration)을 통해 자연스럽게 해결한다.

다국어 초록 (Multilingual Abstract)

We present a static analyzer that detects memory leaks in C programs. It achieves relatively high accuracy at a relatively low cost on SPEC2000 benchmarks and several open-source software packages, demonstrating its practicality and competitive edge against other reported analyzers: for a set of benchmarks totaling 1,777 KLOCs, it found 332 bugs with 47 additional false positives (a 12.4% false-positive ratio), and the average analysis speed was 720 LOC/sec. We separately analyze each procedure's memory behavior into a summary that is used in analyzing its call sites. Each procedural summary is parameterized by the procedure's call context so that it can be instantiated at different call sites. What information to capture in each procedural summary has been carefully tuned so that the summary should not lose any common memory-leak-related behaviors in real-world C program. Because each procedure is summarized by conventional fixpoint iteration over the abstract semantics (`a la abstract interpretation), the analyzer naturally handles arbitrary call cycles from direct or indirect recursive calls.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. 함수 요약
• 3. 성능 향상을 위한 여러 가지 기술들
• 4. 메모리 변화로부터 함수 요약기
• 5. 실험 결과
• 6. 관련 연구
• 7. 경로고려(Path-sensitive) 분석기로의 확장
• 8. 결론
• 참고문헌

참고문헌 (Reference)

• 1 David L. Heine, "Static Detection of Leaks in Polymorphic Containers" ACM Press 252-261, 2006
• 2 David Evans, "Static Detection of Dynamic Memory Errors" 44-53, 1996
• 3 J. Reynolds, "Separation Logic: A Logic for Shared Mutable Data Structures" 2002
• 4 Yichen Xie, "Scalable Error Detection Using Boolean Satisfiability" ACM 351-363, 2005
• 5 Sigmund Cherem, "Practical Memory Leak Detection Using Guarded Value-flow Analysis" 2007
• 6 M. Orlovich, "Memory Leak Analysis by Contradiction" Springer 2006
• 7 Cristiano Calcagno, "Footprint Analysis: A Shape Analysis That Discovers Preconditions" Springer 2007
• 8 Manuvir Das, "ESP: Path-sensitive Program Verification in Polynomial Time" 57-68, 2002
• 9 M. Das, "ESP: Path- sensitive program verification in polynomial time" 57-68, 2002
• 10 Yichen Xie, "Context- and Path- sensitive Memory Leak Detection" ACM 115-125, 2005
• 11 John Whaley, "Compositional Pointer and Escape Analysis for Java Programs" 187-206, 1999
• 12 Erick M. Nystrom, "Bottom-up and Top-down Context-sensitive Summary-based Pointer Analysis" Springer 2006
• 13 Patrick Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints" 238-252, 1977
• 14 Bruno Blanchet, "A static analyzer for large safety-critical software" ACM Press 196-207, 2003
• 15 David, L. Heine, "A Practical Flow-sensitive and Context-sensitive C and C++ Memory Leak Detector" 161-181, 2003