정적 프로그램 분석

정적 프로그램 분석은 소스 코드나 중간 코드를 실행하지 않고 검사하여 변수가 가질 수 있는 값이나 오류 발생 가능성 등의 속성을 추론합니다.

Definition

정적 프로그램 분석은 프로그램을 실행하지 않고 코드로부터 직접 프로그램의 가능한 동작에 대한 근사적이지만 건전한 정보를 계산하는 것으로, 일반적으로 추상 상태의 래티스(lattice of abstract states)에 대한 데이터 흐름 방정식(dataflow equations)을 해결함으로써 이루어집니다.

Scope

이 주제는 제어 흐름 그래프(control-flow graph)를 통한 데이터 흐름 분석(dataflow analysis), 래티스(lattice) 기반 고정점 계산(fixpoint computation), 프로시저 간 분석(interprocedural analysis), 포인터 및 별칭 분석(pointer and alias analysis), 호출 그래프(call-graph) 및 제어 흐름 분석을 다룹니다. 또한 정밀도 차원(흐름 민감도, 문맥 민감도, 경로 민감도), 분석의 건전성(soundness), 그리고 최적화 및 버그 탐지에서의 활용에 대해 다룹니다.

Core questions

• 제어 흐름 그래프를 통해 사실(fact)을 전파함으로써 프로그램 속성은 어떻게 계산됩니까?
• 흐름 민감도, 문맥 민감도, 경로 민감도가 정밀도와 비용에 어떻게 영향을 미칩니까?
• 프로시저 호출을 통해 건전한 분석이 어떻게 수행됩니까?
• 포인터 분석은 별칭(aliasing)과 간접 참조(indirection)를 어떻게 처리합니까?

Key theories

Dataflow analysis as fixpoint over a lattice

Kildall unified global program optimizations as the computation of a fixpoint of dataflow equations over a lattice, providing the general framework for static analyses.

Interprocedural analysis via graph reachability

Reps, Horwitz, and Sagiv reduced a large class of precise interprocedural dataflow problems to graph reachability, enabling efficient context-sensitive analysis across procedure boundaries.

Principles and dimensions of analysis

Nielson, Nielson, and Hankin systematize dataflow, constraint-based, and type-based analyses and the precision-versus-cost trade-offs that govern their design.

Clinical relevance

정적 분석은 컴파일러 최적화, 버그 및 취약점 탐지 도구, 린터(linter), 통합 개발 환경(IDE) 기능의 핵심입니다. 건전한 분석은 특정 오류의 부재를 보증할 수 있으며, 확장 가능한 휴리스틱 분석은 개발 초기 단계에서 결함을 포착하기 위해 널리 사용됩니다.

History

데이터 흐름 분석은 최적화 컴파일러에서 발전했으며, Kildall의 1973년 래티스 프레임워크와 Allen-Cocke 분석이 이론적 기반을 제공했습니다. 프로시저 간 분석과 포인터 분석은 1980년대와 1990년대에 Reps-Horwitz-Sagiv의 도달 가능성(reachability) 공식화를 포함하여 발전했으며, 이후 정적 분석은 매우 큰 코드베이스에 대한 산업적 버그 탐지로 확장되었습니다.

Debates

정밀도 대 확장성

분석 설계자들은 문맥 민감도 및 경로 민감도와 같은 정밀도 차원(오탐을 줄이는)과 분석할 수 있는 프로그램의 크기를 제한하는 계산 비용 사이에서 지속적으로 균형을 맞춥니다.

Key figures

• Gary Kildall
• Thomas Reps
• Susan Horwitz
• Flemming Nielson
• Hanne Riis Nielson

Seminal works

• kildall1973
• reps1995
• nielson1999

Frequently asked questions

정적 분석이 '건전하다(sound)'는 것은 무엇을 의미합니까?

건전한 분석은 확인하는 속성의 실제 발생을 절대 놓치지 않습니다. 즉, 특정 종류의 오류가 없다고 보고하면 해당 종류의 오류는 실제로 발생할 수 없지만, 오탐(false alarm)을 발생시킬 수도 있습니다.

포인터 분석이 어려운 이유는 무엇입니까?

포인터와 참조는 여러 이름이 동일한 메모리를 참조하는 별칭(aliasing)을 도입하므로, 분석은 각 포인터가 어떤 위치를 대상으로 할 수 있는지 근사해야 하며, 이는 정밀도와 확장성 사이의 균형을 요구하는 문제입니다.