작성한 모든 테스트를 통과하는 두 프로그램을 생각해 보세요. 하나는 올바르게 실행되고, 다른 하나는 특정 입력값 조합이 동시에 들어올 때만 발생하는 0으로 나누기 오류가 있습니다. 그런데 테스트에서는 그런 조합이 절대 발생하지 않습니다. 전통적인 테스트 방식으로는 어느 프로그램이 올바르게 실행되고 어느 프로그램이 올바르게 실행되는지 구분할 수 없습니다. 하지만 추상적인 해석을 통해서는 가능합니다.
추상적 해석은 정적 분석 도구가 프로그램을 실행하지 않고도 프로그램의 모든 가능한 동작을 추론할 수 있도록 하는 수학적 틀입니다. 이는 페이스북의 Infer가 대규모로 널 포인터 버그를 찾아내는 데 사용된 기술이며, Astrée 분석기가 에어버스 항공기 제어 소프트웨어를 형식적으로 검증하는 데 사용된 기술이기도 합니다. 또한 건전성을 보장하는 모든 정적 분석 도구의 기반이 되기도 하는데, 건전성 보장이란 프로그램이 분석을 통과하면 검사 대상 오류 유형에서 실제로 자유롭다는 것을 의미합니다. 추상적 해석의 작동 방식을 이해하면 어떤 도구는 버그를 찾아내는 반면 다른 도구는 놓치는 이유와 이러한 보장이 특정한 장단점을 수반하는 이유를 알 수 있습니다.
추상해석이란 무엇인가?
추상 해석은 패트릭 쿠소와 라디아 쿠소가 1977년에 개발한 프로그램 근사 이론입니다. 핵심 아이디어는 일반적으로 결정 불가능한 모든 가능한 프로그램 상태의 정확한 집합을 계산하는 대신, 분석하기 쉬운 단순화된 수학적 영역을 사용하여 안전한 과대 근사를 계산하는 것입니다.
여기서 "추상적"이라는 단어는 모호하거나 개념적이라는 의미가 아닙니다. 구체적인 수학적 연산을 가리키는데, 이는 구체적인 값들의 집합을 불필요한 세부 사항을 제거하면서 중요한 속성은 유지하는 더 간단한 표현으로 추상화하는 것을 의미합니다. 예를 들어, 구체적인 정수 값(예: ...)은 다음과 같습니다. 42 부호 분석이라는 추상화 과정을 거치면 단순히 "양수"가 됩니다. 이러한 추상화는 정보 손실(정확한 값을 알 수 없음)을 가져오지만, 다루기 쉬워집니다(모든 정수의 부호는 양수, 음수 또는 0의 세 가지 가능성 중 하나입니다).
프로그램 분석에 있어 이러한 방식이 유용한 이유는 다음과 같은 보장이 있기 때문입니다. 추상화된 영역에서 오류가 발견되지 않으면 실제 실행에서도 오류가 존재하지 않습니다. 잠재적 오류가 발견되더라도, 그 오류가 실제로 발생할 수도 있고 발생하지 않을 수도 있지만, 실제 오류는 숨길 수 없습니다. 이것이 바로 건전성입니다.
추상 해석 vs. AST 분석 vs. 동적 분석
이 용어들은 자주 혼동되며, "AST 코드 분석"이라는 용어가 이 기사의 검색 데이터에 나타나기도 하는데, 이 두 용어는 서로 다른 것을 의미합니다.
추상 구문 트리(AST) 는 소스 코드의 문법적 구조를 나타내는 데이터 구조입니다. 모든 컴파일러와 린터는 AST를 생성합니다. AST는 구문 분석, 리팩토링 도구, 패턴 기반 정적 분석의 기초가 됩니다. AST 기반 분석은 패턴을 찾습니다. 규칙(매개변수가 너무 많은 함수, 문자열 연결로 만들어진 SQL 문자열 등)과 일치하는 코드는 플래그가 지정됩니다. AST 기반 분석은 값이나 런타임 동작에 대해서는 분석하지 않습니다.
추상 해석은 프로그램을 실행하지 않고 런타임 동작을 추론합니다. AST(추상 구문 트리)를 입력으로 사용하지만, AST를 훨씬 뛰어넘어 프로그램 내에서 값의 흐름, 변수의 범위, 특정 함수 호출 지점에서 포인터가 null일 수 있는지 여부, 루프 종료 여부 등을 모델링합니다. AST 분석은 패턴 매칭이고, 추상 해석은 동작 추론입니다.
대부분의 린터(ESLint, Checkstyle, Pylint)는 주로 추상 구문 트리(AST) 기반입니다. 대부분의 형식 검증 도구(Infer, Astrée, Polyspace)는 추상 해석을 사용합니다. 동적 분석(프로그램을 실행하고 실제 동작을 관찰하는 방식)은 특정 입력에 의해 발생하는 버그만 찾아냅니다. 반면 추상 해석은 프로그램을 실행하지 않고도 모든 가능한 입력에 대한 버그를 찾아냅니다.
정적 해석의 수학적 원리
"정적 분석 도구의 수학적 원리는 무엇인가?"라는 질문이 검색 데이터에 직접적으로 나타납니다. 이에 대한 명확한 답변은 다음과 같습니다.
추상적 해석은 세 가지 수학적 구조에 기반을 두고 있다.
격자(Lattice). 격자는 모든 쌍의 요소가 최소 상한(결합)과 최대 하한(만남)을 갖는 부분 순서 집합입니다. 정적 분석에서 격자는 추상 영역, 즉 가능한 추상 값들의 집합을 나타내며, 각 값이 지닌 정보의 양에 따라 순서가 정해집니다. 부호 분석에서 격자는 다음과 같습니다.
⊤ (unknown -- could be anything)
/ \
pos neg
\ /
0
|
⊥ (unreachable -- no possible value)격자 위로 올라갈수록 정확도가 떨어지고(알 수 있는 것이 적어지고), 아래로 내려갈수록 정확도가 높아집니다(알 수 있는 것이 많아지고). 맨 위쪽 요소 ⊤는 "우리는 유용한 정보를 전혀 알지 못한다"는 의미이고, 맨 아래쪽 요소 ⊥는 "이 상태에는 도달할 수 없다"는 의미입니다.
갈루아 연결. 갈루아 연결은 구체적인 영역(실제 프로그램 값)과 추상적인 영역(단순화된 표현) 사이의 형식적인 관계입니다. 이는 두 가지 함수로 구성됩니다. 구체적인 값을 추상적인 표현으로 매핑하는 추상화 함수 α와, 추상적인 값을 다시 그것들이 나타내는 구체적인 값들의 집합으로 매핑하는 구체화 함수 γ입니다.
핵심 속성: 추상 영역은 안전한 과대 근사치여야 합니다. γ(α(S)) ⊇ S 모든 구체적인 집합 S에 대해. 추상화는 실제로 존재하는 값보다 더 많은 값을 포함할 수 있으며, 이것이 오탐을 발생시키는 원인이지만, 실제로 존재하는 값을 절대 배제해서는 안 됩니다. 실제 값을 배제하면 실제 버그를 놓치게 되기 때문입니다.
고정점 반복법. 반복문이 있는 프로그램의 경우, 분석은 안정적인 상태에 도달할 때까지 반복해야 합니다. 예를 들어 다음과 같은 반복문이 있습니다.
c
int x = 0;
while (condition) {
x = x + 1;
}첫 번째 반복에서는, x is {0}한 번의 루프 본문 후에, x 될 수 {0, 1}2년 후, {0, 1, 2}이 집합은 계속 증가하며, 저절로 안정화되지 않습니다. 해결책은 다음과 같습니다. 확장: 더 넓은 범위의 근사값(일반적으로)으로 이동하여 수렴을 강제하는 연산자 [0, +∞) 간격 분석의 경우). 그런 다음 분석은 다음을 사용합니다. 좁히기 정확도를 어느 정도 회복하기 위해.
이 고정 소수점 계산 때문에 추상 해석은 루프를 포함한 모든 실행 경로에서 완전하게 이루어지며, 단순 패턴 매칭보다 계산 비용이 더 많이 드는 것입니다.
추상 영역: 근사할 대상을 선택하기
추상 영역은 분석을 통해 무엇을 찾을 수 있고 무엇을 찾을 수 없는지를 결정합니다. 각기 다른 영역은 프로그램 동작에 대한 서로 다른 질문에 답합니다.
| 추상 도메인 | 무엇을 추적하는가 | 사용 예 | 이 작품이 놓친 점 |
|---|---|---|---|
| 신호 분석 | 값이 양수, 음수 또는 0인지 여부 | 0으로 나누기 감지 | 정확한 값, 오버플로 조건 |
| 구간 분석 | 수치 값의 상한 및 하한 | 버퍼 오버플로, 어레이 접근 안전성 | 변수 간의 관계 |
| 팔각형 영역 | 두 변수 사이의 선형 관계 | 보다 정확한 오버플로우 감지 | 비선형 관계 |
| 포인터 분석 | 포인터가 null일 수 있는지 또는 서로 별칭이 될 수 있는지 여부 | 널 역참조, 해제 후 사용 | 객체 수명, 힙 형태 |
| 오염 분석 | 값이 신뢰할 수 없는 출처에서 비롯되었는지 여부 | SQL 인젝션, XSS 탐지 | 제어를 통한 암묵적 흐름 |
| 다면체 영역 | 임의의 선형 산술 제약 조건 | 루프 경계 검증 | 성능 비용은 기하급수적으로 증가합니다. |
도메인 선택 시 항상 정밀도와 성능 간의 절충점이 존재합니다. 구간 도메인은 속도가 빠르고 대부분의 수치적 오류를 잡아냅니다. 다면체 도메인은 훨씬 더 정밀하지만 변수 개수에 따라 계산 복잡성이 기하급수적으로 증가합니다. 실용적인 정적 분석 도구는 대상 애플리케이션에 맞춰 이러한 절충점의 균형을 고려하여 도메인을 선택합니다. 안전에 중요한 임베디드 시스템은 속도는 느리지만 정밀도가 높은 분석을 감당할 수 있지만, CI/CD에 통합된 린터는 몇 초 내에 분석을 완료해야 합니다.
세 가지 실제 도구가 추상적 해석을 활용하는 방법
이론을 개별적으로 설명하기보다는 구체적인 도구를 통해 이론의 적용을 명확히 보여준다.
Facebook Infer는 양방향 귀납적 추론이라는 추상적 해석 방식을 사용하여 Java, C, C++, Objective-C 코드에서 널 포인터 역참조, 리소스 누수, 경쟁 조건을 분석합니다. 양방향 귀납적 추론은 함수의 사전 조건과 사후 조건을 자동으로 찾아내어 수동 지정 없이도 프로시저 간 분석을 가능하게 합니다. Infer는 Facebook, Spotify, Mozilla를 비롯한 수십 개의 대규모 조직에서 CI(지속적 통합) 환경에서 사용되고 있는데, 이는 수백만 줄에 달하는 코드베이스에서도 뛰어난 확장성을 유지하면서 검사하는 오류 유형에 대해 건전성을 보장하기 때문입니다.
Astrée는 수치 추상 도메인을 사용한 추상 해석을 통해 C 프로그램의 런타임 오류가 없음을 증명합니다. 에어버스는 Astrée를 사용하여 A380의 주요 비행 제어 소프트웨어를 형식적으로 검증했으며, 전체 제어 시스템에서 런타임 오류가 없음을 입증했습니다. 이는 어떤 테스트 프로그램도 보장할 수 없었던 결과입니다. Astrée는 검사하는 오류 유형에 대해 오탐(false negative)이 전혀 발생하지 않지만, 수동 검토가 필요한 오양성(false positive)이 발생할 수 있습니다.
Polyspace (MathWorks)는 안전에 중요한 애플리케이션에 내장된 C 및 C++ 코드에 대해 추상 해석을 적용합니다. 모든 연산을 "녹색"(오류 없음이 확실히 증명됨), "빨간색"(확실히 오류 있음), "주황색"(검토가 필요한 잠재적 오류 있음)으로 분류합니다. 녹색 분류는 형식적인 증명으로, 해당 연산에서 런타임 오류가 발생할 수 없음을 의미합니다.
건전성-정밀성-성능의 삼각형
추상 해석 도구는 서로 상충하는 세 가지 기본 속성을 탐색합니다. 어떤 도구도 이 세 가지 속성을 동시에 극대화할 수는 없습니다.
건전성 이란 오탐이 없다는 것을 의미합니다. 즉, 분석 대상 클래스의 모든 실제 버그를 탐지해야 합니다. 건전한 도구는 확실한 보장을 제공하지만, 건전하지 않은 도구는 버그를 놓칠 수 있습니다.
정확성은 오탐이 적다는 것을 의미합니다. 즉, 발견된 결과가 발생할 수 없는 이론적인 문제가 아니라 실제 문제와 일치한다는 뜻입니다. 높은 정확성을 위해서는 더욱 정교한 추상적 영역과 절차 간 분석이 필요합니다.
성능이란 분석이 유용한 시간 내에 완료되는 것을 의미합니다. 더 정확한 분석일수록 비용이 더 많이 듭니다. 수백만 줄에 달하는 코드베이스에서 모든 런타임 오류가 없음을 증명하는 데는 몇 시간이 걸리지만, 린터 검사는 몇 초밖에 걸리지 않습니다.
다양한 응용 분야에는 이 삼각형의 서로 다른 지점이 필요합니다.
- IDE 린팅 및 CI/CD성능이 최우선이고, 정밀도는 그다음이며, 건전성은 선택 사항입니다.
- 보안 스캐닝정확성 우선 (개발자 알림 피로도 감소), 심각도가 높은 클래스의 경우 건전성도 중요
- 안전 필수 인증: 건전성 최우선 (실제 버그를 놓쳐서는 안 됨), 성능은 차선책, 수동 검토 과정을 통해 오탐은 허용 가능
임베디드 및 안전 필수 개발에서의 추상적 해석
"임베디드 개발에서 정적 분석의 이점"이라는 질문은 추상 해석의 가장 중요한 응용 분야 중 하나를 가리킵니다. 임베디드 시스템, 자동차 제어 장치, 의료 기기 펌웨어, 항공우주 비행 제어 소프트웨어는 추상 해석이 특히 유용한 제약 조건을 가지고 있습니다.
모든 상태를 테스트할 수 있는 테스트 시스템은 없습니다. 자동차 ECU는 수천 가지 센서 조합에 실시간으로 반응합니다. 모든 조합에 대한 테스트를 구축하는 것은 불가능합니다. 추상적인 해석을 통해 모든 상태를 동시에 파악할 수 있습니다.
인증 요건. DO-178C(항공우주), ISO 26262(자동차), IEC 62443(산업 제어)은 소프트웨어가 모든 조건에서 올바르게 동작함을 입증할 것을 요구합니다. 추상적 해석을 이용한 형식 검증은 테스트 커버리지 보고서로는 충족할 수 없는 이러한 요건을 해결할 수 있습니다.
자원 제약. 임베디드 소프트웨어는 종종 메모리 할당자, 예외 처리, 운영 체제 대체 기능이 없습니다. 런타임 오류, 널 포인터 역참조, 배열 범위 초과는 심각한 시스템 오류로 이어집니다. 이러한 버그를 놓치는 데 드는 비용은 단순히 크래시 보고서와 핫픽스에 그치지 않습니다. 이는 안전 사고로 이어질 수 있습니다.
Astrée 및 Polyspace 분석기는 바로 이러한 맥락을 위해 개발되었습니다. 이 분석기들은 높은 오탐률과 느린 분석 속도를 감수하는 대신, 오분류가 발생하지 않도록 보장합니다.
오탐지와 그 심각해지는 문제
추상 해석 도구에 대한 가장 일반적인 비판은 오탐, 즉 실제 실행에서는 발생할 수 없는 잠재적 오류에 대한 경고입니다. 오탐이 품질 결함이 아니라 본질적인 문제라는 것을 이해하면 이를 관리하기가 더 쉬워집니다.
오탐은 두 가지 원인에서 발생합니다.
추상 영역에서의 과대 근사. 간격 영역이 추적하는 경우 x ∈ [0, 100]그것은 어떤 경우와 어떤 경우를 구분할 수 없습니다. x 실제로는 항상 50보다 작습니다. 로 나누면 x 프로그램 로직이 0으로 나누기를 보장하더라도 0으로 나누기 오류가 발생할 가능성이 있다고 표시될 수 있습니다. x > 0보다 정밀한 도메인(정확한 값을 추적하거나 제약 조건을 연결하는 방식) x 다른 변수로 변환하면 오탐을 제거할 수 있지만 계산 비용이 더 많이 듭니다.
넓어지고 있습니다. 루프 분석을 용이하게 만드는 수렴 연산자는 필연적으로 정보 손실을 수반합니다. 확장 후 x 에 [0, 5] 에 [0, +∞)분석기는 더 이상 그것을 알지 못합니다. x 제한된 범위를 유지합니다. 코드가 확인하는 경우 assert(x < 1000) 반복문 이후에는 실제로 그렇더라도 이 주장을 더 이상 증명할 수 없습니다. x 항상 1000보다 훨씬 낮은 수준을 유지합니다.
오탐을 관리하기 위한 실용적인 전략: 중요 모듈에 대해 더 정확한 도메인을 사용하도록 분석을 구성하고(분석 속도 저하 감수), 표적 주석을 사용하여 확인된 오탐을 억제하고, 도구의 주황색/알 수 없음 표시를 확정된 버그가 아닌 우선순위 검토 대기열로 처리합니다.
방법 SMART TS XL 엔터프라이즈 규모에 정적 분석을 적용합니다.
SMART TS XL 이 시스템은 추상적 해석 이론과 기업 현실이 만나는 영역, 즉 여러 언어에 걸쳐 있는 코드베이스, 수십 년에 걸친 개발, 그리고 프로그램별 형식적 검증을 비현실적으로 만드는 조직적 경계가 존재하는 영역에서 작동합니다.
모든 프로그램에 단일 추상 도메인을 적용하는 대신, SMART TS XL의 정적 코드 분석 이 도구는 COBOL, JCL, Java, Python, RPG, PL/I, SQL 및 최신 스택을 포함한 환경 내 각 언어에 적합한 구조 분석 기법을 결합하여 전체 포트폴리오에 걸쳐 품질 지표, 종속성 데이터 및 보안 결과를 동시에 생성합니다.
애플리케이션 종속성 매핑 기능은 그래프 이론적 분석을 언어 간 호출 그래프에 적용하여 프로그램, 데이터 세트 및 작업 스트림이 언어 경계를 넘어 어떻게 연결되는지 식별합니다. 이는 단일 언어 도구로는 수행할 수 없는 전체 시스템 분석입니다. 즉, 시스템 수준에서의 구조적 추론으로, 개별 프로그램의 속성을 증명하는 것이 아니라 프로그램 간의 연결 방식에 대한 속성을 증명하는 것입니다.
영향 분석 기능은 종속성 그래프에 대한 도달 가능성 분석을 적용합니다. 즉, 한 노드에서 변경이 제안되면 해당 노드에서 도달 가능한 모든 노드의 집합을 계산합니다. 이는 정적 분석에서 묻는 "무엇이 영향을 받을 것인가?"라는 질문에 대한 답을 런타임 관찰이나 사람의 예측이 아닌 코드 구조 자체에서 도출하는 것입니다.
진행하는 팀의 경우 레거시 현대화 프로그램 SMART TS XL구조 분석은 언어별로 다르며 구성에 도메인 전문 지식이 필요한 형식적 추상 해석 도구와, 대규모의 문서화되지 않은 다국어 레거시 시스템이 실제로 어떻게 작동하는지 이해해야 하는 실질적인 필요성 사이의 간극을 메워줍니다. 이는 실행 도중 가장 값비싼 문제점을 발견하고 싶지 않은 모든 현대화 프로그램의 필수 조건입니다.
자주 묻는 질문
추상 해석과 모델 검증의 차이점은 무엇일까요? 둘 다 프로그램 검증을 위한 형식적 방법입니다. 추상 해석은 가능한 상태 집합을 과대 근사화합니다(건전하지만 잠재적으로 부정확할 수 있음). 모델 검증은 상태 공간을 철저하게 탐색합니다(완전하지만 유한하고 경계가 있는 시스템에서만 실행 가능). 추상 해석은 대규모 프로그램에 적용 가능하며, 모델 검증은 소규모 모델의 복잡한 속성에 적용 가능합니다. 이 둘은 상호 보완적이며 경쟁 관계가 아닙니다.
추상 해석은 안전에 중요한 소프트웨어에만 적용되는 것일까요? 그렇지 않습니다. 물론 그곳에서 가장 명확한 가치를 발휘하긴 하지만요. Infer는 대형 기술 기업의 표준 CI/CD 파이프라인에서 실행되어 일상적인 Java 및 C 코드에서 널 포인터 역참조와 리소스 누수를 찾아냅니다. 적용되는 엄격성의 정도는 선택 사항입니다. 한쪽 끝에는 형식적 보장을 통한 완전한 건전성이 있고, 다른 쪽 끝에는 가벼운 휴리스틱 분석이 있으며, 대부분의 실용적인 도구는 그 중간 어딘가에 있습니다.
추상 해석으로 COBOL을 분석할 수 있을까요? 추상 해석은 이론적으로 언어에 구애받지 않습니다. 하지만 COBOL에 적용하려면 COBOL 연산, PIC 필드 연산, REDEFINES 절, 레벨 88 조건 이름 등에 대한 추상 전달 함수를 구현해야 합니다. 일반적인 추상 해석 도구(Infer, Astrée)는 COBOL을 지원하지 않습니다. COBOL을 기본적으로 이해하는 엔터프라이즈 구조 분석 플랫폼은 관련 정적 분석 기법을 적용하여 COBOL 코드베이스에서 품질 문제, 사용되지 않는 코드, 아키텍처 문제를 찾아냅니다.
