정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 대신 더 유용한 것을 증명할 수 있습니다.

답은 “아니오”입니다. 진짜 질문은 그 대신 무엇을 증명할 수 있느냐는 것입니다.

정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 하지만 고도계 제어 루프가 0으로 나누기를 절대 하지 않고, 배열 범위를 벗어나는 인덱싱을 절대 하지 않으며, 고정 소수점 누산기에서 오버플로우가 절대 발생하지 않음은 증명할 수 있습니다. 이 둘의 차이가 중요한 이유는, 하나는 물리학, 공기역학, 그리고 응력을 받는 알루미늄에 대한 주장이고, 다른 하나는 비행기가 이륙하기 전에 검증할 수 있는 코드에 대한 주장이기 때문입니다.

이것이 추상 해석이 약속하는 바입니다. 전지전능함이 아닙니다. 특정 범주의 재앙적인 소프트웨어 결함이 모든 가능한 실행에서 불가능함을 엄밀하게 증명하는 것입니다.

수백만 개의 시나리오를 테스트해도 여전히 추측에 의존해야 하는 이유

일반적인 비행 제어 시스템은 수십만 줄의 C 코드로 이루어져 있습니다. 입력 공간은 센서 판독값, 조종사 명령, 환경 조건, 내부 상태 변수들의 교차 곱입니다. 시뮬레이터에서 우주의 열 죽음이 올 때까지 시스템을 실행해도 여전히 모든 경로를 커버할 수 없습니다.

테스트는 버그를 찾습니다. 버그가 없음을 증명하지는 않습니다. 통과하는 모든 테스트는 하나의 데이터 포인트일 뿐입니다. 그것은 보장이 아닙니다.

추상 해석은 이 접근법을 뒤집습니다. 특정 입력으로 프로그램을 실행하는 대신, 가능한 값의 집합을 표현하는 추상 도메인 위에서 프로그램을 실행합니다. 추상 분석이 특정 오류 상태에 도달할 수 없다고 말한다면, 그 오류는 모든 구체적 입력에 대해 도달할 수 없는 것입니다. 이 증명은 처음부터 끝까지 포괄적인데, 단 한 번의 통과로 전체 입력 공간을 커버하기 때문입니다.

구체적 값은 너무 비쌉니다. 대신 형태를 사용하세요.

간단한 변수 x를 생각해 보세요. 구체적 실행에서 x는 42일 수 있습니다. 추상 해석에서 x는 “0에서 255 사이의 임의의 정수”일 수 있습니다. 이를 구간 추상화(interval abstraction)라고 합니다.

분석기는 이러한 구간을 모든 연산을 통해 추적합니다. x가 [0, 100]이고 y가 [1, 10]이라면, x / y는 [0, 100]입니다. 분석기는 나눗셈이 안전한 것을 알고 있는데, 그 이유는 나누는 수의 구간에 0이 포함되지 않기 때문입니다.

하지만 y가 [-5, 5]라면, 분석기는 잠재적인 0으로 나누기를 표시할 것입니다. 구체적 실행에서 0에 실제로 도달하는지는 알 수 없습니다. 단지 0이 가능한 범위 안에 있다는 것을 알 뿐입니다. 그것만으로도 경고를 발생시키기에는 충분합니다.

1976년 Patrick Cousot과 Radhia Cousot이 제시한 핵심 통찰은, 추상 도메인이 구체적 의미론의 건전한 과대 근사(sound over-approximation)여야 한다는 것입니다. 모든 구체적 동작은 추상화 안에서 표현 가능해야 합니다. 추상화가 안전하다면, 구체적 프로그램도 안전합니다. 추상화가 경고한다면, 구체적 프로그램은 괜찮을 수도 있습니다. 하지만 그렇지 않을 수도 있습니다.

Python으로 간단한 구간 분석기 만들기

다음은 동작하는 구간 추상 도메인입니다. 단순하지만, 그 메커니즘을 보여줍니다.

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class Interval:
    lo: int
    hi: int

    def __post_init__(self):
        if self.lo > self.hi:
            raise ValueError("Empty interval")

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lo + other.lo, self.hi + other.hi)

    def div(self, other: "Interval") -> Optional["Interval"]:
        if other.lo <= 0 <= other.hi:
            return None  # Potential division by zero
        # Simplified: assumes positive divisor for demo
        return Interval(self.lo // other.hi, self.hi // other.lo)

    def intersect(self, other: "Interval") -> Optional["Interval"]:
        lo = max(self.lo, other.lo)
        hi = min(self.hi, other.hi)
        if lo > hi:
            return None
        return Interval(lo, hi)

    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"


def analyze_division(a: Interval, b: Interval) -> None:
    result = a.div(b)
    if result is None:
        print(f"ALERT: {a} / {b} may divide by zero")
    else:
        print(f"SAFE: {a} / {b} = {result}")

몇 가지 경우를 실행해 보겠습니다:

analyze_division(Interval(10, 20), Interval(2, 5))   # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1))  # ALERT
analyze_division(Interval(10, 20), Interval(0, 5))   # ALERT

첫 번째 경우는 모든 나누는 수가 양수이므로 안전합니다. 두 번째는 [-1, 1] 안에 0이 포함되어 있어 표시되었습니다. 세 번째는 [0, 5] 안에 0이 포함되어 있어 표시되었습니다.

세 번째 경우에서 무슨 일이 일어났는지 주목하세요. 구체적 프로그램은 실제로 b = 0으로 실행되지 않을 수도 있습니다. 분석기는 그것을 알지 못합니다. 분석기는 설계상 보수적입니다. 이것이 근본적인 트레이드오프입니다.

오탐의 대가

건전한 정적 분석기는 버그를 놓치지 않습니다. 충돌이 가능하다면, 그것을 보고할 것입니다. 하지만 불가능한 충돌도 보고할 것입니다. 이러한 오탐(false positive)이 건전성의 대가입니다.

실제로 이 대가는 큽니다. for (i = 0; i < n; i++)와 같은 루프에 대한 단순한 구간 분석은, n이 유한하더라도 i가 [0, +∞]라고 종종 결론 내립니다. 분석기는 두 개의 제어 흐름 경로가 합쳐지고 그 추상 상태들을 결합해야 하는 병합 지점에서 정밀도를 잃습니다.

실제 도구들은 더 정교한 도메인을 사용합니다. 다면체(polyhedra), 팔면체(octagons), 그리고 술어 추상화(predicate abstractions)는 변수 간의 관계를 추적합니다. x < y는 구간에게 보이지 않지만, 다면체 도메인은 이를 기억합니다. 이러한 도메인들은 더 정밀합니다. 하지만 더 비쌉니다. 다면체 도메인은 최악의 경우 지수 시간 복잡도를 가집니다. 30만 줄의 C 코드를 가진 비행 제어 시스템에 대해 단순한 구현을 한다면, 비행기가 퇴역하기 전에 종료되지 않을 것입니다.

Astrée가 A380에서 실제로 증명한 것

Astrée는 추상 해석을 항공 분야에서 유명하게 만든 정적 분석기입니다. 2003년, Astrée는 에어버스 A380의 주 비행 제어 소프트웨어에 대해 실행되었습니다. 그것은 어떤 런타임 오류도 없음을 증명했습니다. 0으로 나누기 없음. 배열 범위를 벗어난 접근 없음. 산술 오버플로우 없음. 중요 경로에서 도달할 수 없는 코드 없음.

그것은 비행기가 추락하지 않음을 증명하지는 않았습니다. 제어 법칙이 올바르다는 것도 증명하지 않았습니다. 공격각(angle-of-attack) 계산이 비행기의 물리학과 일치한다는 것도 증명하지 않았습니다. 이들은 다른 문제이며, 다른 도구로 해결됩니다.

Astrée는 소프트웨어가 스스로 충돌하지 않음을 증명했습니다. 그것은 들리는 것보다 더 좁은 주장이지만, 대부분의 사람들이 인식하는 것보다 더 가치 있는 주장입니다. 소프트웨어 자기 파괴는 항공 사고의 흔한 원인입니다. 그것이 발생할 수 없음을 증명하는 것은 그 노력의 가치가 있습니다.

이 도구는 여러 도메인별 기법을 결합하여 이를 달성했습니다. 속도를 위해 비관계형 도메인을 사용하고, 정밀도를 위해 관계형 도메인을 사용합니다. 반올림 오차를 고려하는 모델로 부동 소수점 연산을 처리합니다. 항공 전자 공학에서 사용되는 특정 C 하위 집합을 이해하고, 정의되지 않은 동작을 오류로 취급합니다. 엔지니어들이 결과를 신뢰할 만큼 오탐률을 낮추기까지 수년의 튜닝이 필요했습니다.

건전성은 선택이지 기본값이 아니다

모든 정적 분석기가 건전성을 목표로 하는 것은 아닙니다. Coverity, CodeQL, Infer와 같은 도구들은 부재를 증명하는 것보다 실제 버그를 찾는 것을 우선시합니다. 이들은 상태 공간을 과소 근사합니다. 0으로 나누기를 놓칠 수도 있지만, 찾아낸 것들은 보통 실제 버그입니다.

이것은 합당한 엔지니어링 선택입니다. 웹 애플리케이션의 경우, 몇 분 안에 실행되는 90% 정확도의 버그 탐지기가 오탐으로 넘쳐나는 건전한 분석기보다 낫습니다. 비행 제어 시스템의 경우는 그 반대입니다. 노이즈를 필터링해야 하더라도 증명을 원합니다.

추상 해석은 그 증명을 가능하게 하는 기술입니다. 유일한 형식적 방법은 아닙니다. SPIN과 TLA+와 같은 모델 검사기는 상태 기계를 검증합니다. Coq와 Isabelle과 같은 정리 증명기는 기능적 정확성을 검증합니다. 추상 해석은 황금분할점에 위치합니다: 완전히 자동화되며, 대규모 codebases로 확장되고, 런타임 동작에 대한 수학적 보장을 제공합니다.

추상 해석이 한계에 부딪히는 곳

이 방법에는 확실한 한계가 있습니다. 복잡한 포인터 연산을 통해 할당된 메모리에 대해 추론할 수 없습니다. 알고리즘이 올바른 값을 계산하는지는 검증할 수 없고, 계산하는 동안 충돌하지 않음만 검증할 수 있습니다. 동시성, 동적 디스패치, 그리고 의도적으로 정의되지 않은 동작에 의존하는 코드에 대해서는 어려움을 겪습니다.

또한 코드가 검증 가능한 스타일로 작성되어야 합니다. A380 비행 소프트웨어는 재귀를 피하고, 동적 메모리 할당을 제한하며, 제어 흐름을 단순하게 유지합니다. 이러한 제약들은 분석기의 한계가 아닙니다. 증명을 위한 전제 조건입니다. 모델링하기에 너무 혼란스러운 코드의 속성은 증명할 수 없습니다.

실제 함수에서 구간으로 시작하기

이러한 아이디어를 적용하기 위해 Astrée가 필요한 것은 아닙니다. codebase에서 하나의 순수 함수를 고르세요. 범위 내에 있어야 하는 변수 하나를 확인하세요. 간단한 구간 전파 스크립트를 작성하세요. 모든 분기와 연산을 통해 그 변수를 추적하세요.

사용 지점에서의 구간이 안전 범위 내에 있다면, 해당 변수에 대한 수동적인 안전성 증명을 갖게 된 것입니다. 그렇지 않다면, 버그나 추론이 불완전한 곳을 발견한 것입니다. 어느 쪽이든, 단위 테스트가 놓칠 수 있는 무언가를 배운 것입니다.

추상 해석은 비행기가 추락하지 않음을 증명하지는 못합니다. 아무것도 그것을 증명할 수 없습니다. 하지만 소프트웨어가 그 원인이 되지 않음은 증명할 수 있습니다.

자주 묻는 질문

추상 해석이란 무엇인가요?

추상 해석은 구체적 프로그램 값을 구간이나 형태와 같은 추상적 표현으로 대체하는 정적 프로그램 분석을 위한 형식적 방법입니다. 분석기는 이러한 추상 값 위에서 프로그램 실행을 시뮬레이션합니다. 추상 도메인에서 오류에 도달할 수 없다면, 모든 가능한 입력에 대해 구체적 프로그램에서도 도달할 수 없습니다.

추상 해석은 모든 버그를 찾을 수 있나요?

아니요. 추상 해석은 0으로 나누기, 버퍼 오버플로우, 산술 오버플로우와 같은 특정 런타임 오류의 부재를 증명합니다. 알고리즘이 올바른 결과를 생성하는지는 검증할 수 없으며, 충돌하지 않음만 검증할 수 있습니다. 또한 하드웨어 결함이나 물리적 시스템 동작과 같은 코드 외부의 속성에 대해서는 추론할 수 없습니다.

건전한 정적 분석과 건전하지 않은 정적 분석의 차이는 무엇인가요?

건전한 분석기는 가능한 프로그램 동작의 집합을 과대 근사합니다. 설계된 유형의 버그를 절대 놓치지 않지만, 오탐을 보고할 수 있습니다. 건전하지 않은 분석기는 과소 근사합니다. 버그를 놓칠 수도 있지만, 보고된 버그들은 실제일 가능성이 더 높습니다. 건전성은 안전 필수 시스템에 필수적입니다. 건전하지 않은 분석은 일반적인 소프트웨어 개발에서 더 빠른 피드백을 위해 종종 선호됩니다.

추상 해석은 안전 필수 소프트웨어에만 사용되나요?

아니요, 비록 가장 많이 사용되는 분야는 그곳이지만. 추상 해석 뒤에 있는 아이디어는 많은 컴파일러와 최적화기에 나타납니다. 예를 들어 LLVM의 범위 분석은 불필요한 경계 검사를 제거하기 위해 구간 추상화를 사용합니다. 경계를 증명하는 것이 중요한 모든 코드에 동일한 구간 추론을 적용할 수 있습니다. 임베디드 펌웨어부터 고성능 수치 커널까지.