Meta는 프로그램을 실행하지 않는 정적 분석기로 프로덕션 코드에서 10만 개의 버그를 찾아냈다

Meta는 코드가 사용자에게 도달하기 전에 정적 분석기가 포착한 10만 건 이상의 버그 수정을 배포했다. 이 도구의 이름은 Infer이며 오픈 소스이고 코드를 실행하지 않는다. 코드를 읽어 코드가 할 수 있는 동작의 수학적 모델을 구축하고, 특정한 나쁜 일이 일어날 수 없음을 증명한다. 아니면 그런 일이 일어날 수 있는 경로를 찾아낸다.

이 기법은 abstract interpretation이다. 학문적으로 들리는 이유는 그것이 학문이기 때문이다. 패트릭 쿠소와 라디아 쿠소는 1970년대에 프로그램을 실행하지 않고 추론하는 방법으로 이를 발명했다. 피터 오헌이 이끄는 Meta 팀은 이 이론을 받아들여 수백만 줄의 모바일 및 서버 코드를 몇 분 만에 분석할 수 있을 만큼 빠르게 만들었다. 그 결과는 null pointer, memory leak, resource leak, 그리고 race condition을 diff 시점에 찾아내는 도구다.

문제: 동적 테스트는 실행해 보려 하지 않은 경로를 커버할 수 없다

단위 테스트는 코드의 한 경로를 검사한다. 통합 테스트는 몇 개 더 검사한다. 하지만 조건문이 다섯 개, 반복문이 두 개인 함수는 수백 개의 경로를 가지며, 그 대부분은 테스트 스위트에서 결코 실행되지 않는다.

동적 테스트, 즉 코드를 실행하는 방식은 실제로 실행한 경로에서만 버그를 찾을 수 있다. 정적 분석은 한 번도 생각해 보지 않은 경로에서 버그를 찾는다. 이는 손전등을 들고 방을 돌아다니며 침입자를 확인하는 것과, 모든 문과 창문이 잠겨 있음을 증명하여 확인하는 것의 차이와 같다.

도전은 실제 프로그램에 대해 무언가를 증명하는 것이 어렵다는 점이다. 실제 프로그램에는 반복문, 재귀, 힙 할당, 그리고 동시성이 있다. 모든 상태를 열거할 수는 없다. abstract interpretation은 이를 근사화하여 해결한다.

abstract interpretation의 실제 의미

abstract interpretation은 구체적인 값 대신 추상적인 값을 사용해 프로그램을 실행하는 방식으로 작동한다.

일반적인 실행에서 변수 x는 정수 42를 가질 수 있다. abstract interpretation에서는 x가 “양수”라는 추상 값을 가질 수 있다. 분석기는 x가 42라는 사실을 모른다. x가 0보다 크다는 사실만 안다. 이는 y도 양수라면 x / y가 0으로 나누지 않음을 증명하기에 충분하다. 하지만 x == 42임을 증명하기에는 부족하다. abstract interpretation은 계산 가능성을 얻기 위해 정확성을 희생한다.

추상 값의 집합을 추상 도메인(abstract domain)이라고 한다. 가장 단순한 도메인은 부호 도메인으로, 각 변수는 음수, 영, 양수, 또는 알 수 없음 중 하나다. 더 복잡한 도메인은 범위, 포인터, 또는 메모리 위치가 해제되었는지를 추적한다. 분석기는 프로그램을 반복하며 각 연산의 추상 버전을 적용하고, 추상 상태가 변하지 않을 때까지 계속한다. 그 시점에서 고정점(fixed point)을 찾았으며, 이는 각 프로그램 지점에서 가능한 모든 구체적 상태의 근사치다.

반복문이 어려운 부분이다. 반복문은 0번, 1번, 또는 10억 번 실행될 수 있다. 분석기가 10억 번이나 펼칠 수는 없다. 대신 과대 근사(over-approximation)로 점프하는 확대 연산자(widening operator)를 적용한다. 변수가 매 반복마다 1씩 증가한다면, 분석기는 그 추상 값을 “양수”에서 “비음수”로 확대하고 거기서 멈출 수 있다. 정확한 상한은 잃지만, 증명에 필요한 속성은 유지한다.

Infer가 양방향 추론을 사용해 절차를 모듈식으로 분석하는 방법

전통적인 abstract interpretation은 전체 프로그램을 하나로 분석한다. 이는 수백만 줄의 모바일 앱에는 확장되지 않는다. Infer는 양방향 추론(bi-abduction)이라는 기법으로 이 문제를 해결한다.

양방향 추론을 통해 Infer는 한 번에 하나의 함수를 분석할 수 있다. Infer가 함수를 분석할 때 두 가지를 발견한다: 함수가 안전하려면 반드시 성립해야 하는 전조건(precondition), 그리고 함수가 보장하는 후조건(postcondition)이다. 이들은 프로그래머가 작성하는 것이 아니라 자동으로 추론된다.

구체적인 예를 보자. Infer가 다음 C 함수를 본다고 가정하자:

void greet(struct Person* p) {
    printf("Hello, %s\n", p->name);
}

Infer는 greet가 p가 널이 아닐 것을 요구한다고 추론한다. 이것이 전조건이다. 또한 greet가 p를 해제하지 않고 가시적인 상태를 변경하지 않는다고도 추론한다. 이것이 후조건이다. 다른 함수가 greet를 호출하면 Infer는 호출자를 추론된 전조건에 대해 검사한다. 호출자가 널을 전달할 가능성이 있으면 Infer는 버그를 보고한다.

양방향 추론 엔진은 분리 논리(separation logic) 위의 기호 실행(symbolic execution)으로 작동한다. 분리 논리를 통해 Infer는 힙 소유권에 대해 추론할 수 있다: 어떤 함수가 어떤 메모리를 소유하고, 그 메모리가 해제되었는지. 이것이 Infer가 C, C++, Objective-C, Java에서 null reference과 memory leak을 찾는 데 뛰어난 이유다.

Infer가 잡아내는 것과 놓치는 것

Infer는 범용 린터가 아니다. 동적으로 발견하기 비싸고 프로덕션에서 위험한 특정 버그 클래스를 대상으로 한다.

null pointer. Infer는 각 포인터가 확실히 널인지, 확실히 널이 아닌지, 아니면 널일 가능성이 있는지를 추적한다. 널일 가능성이 있는 포인터의 참조는 보고를 유발한다. Java와 Objective-C에서 이것은 가장 흔한 크래시 유형을 잡아낸다.

memory leak. Infer는 분리 논리를 사용해 힙 소유권을 추적한다. 함수가 메모리를 할당하고 해제하거나 호출자에게 반환하지 않으면 Infer는 누수를 보고한다. 이는 가동 시간이 길어질수록 누수가 누적되는 C 및 C++ 코드베이스에서 특히 가치 있다.

resource leak. 파일 디스크립터, 소켓, 그리고 락도 비슷하게 추적된다. 함수가 파일을 열고 모든 경로에서 닫지 않고 복귀하면 Infer는 누수를 보고한다.

race condition. Infer의 RacerD 모듈은 Java 동시성을 분석한다. 어떤 스레드가 어떤 필드에 접근하고 그 접근이 락으로 보호되는지를 추적한다. 동기화 없이 같은 필드에 접근하는 두 스레드는 경쟁이다.

Infer는 모든 것을 잡아내지는 않는다. 수치 정밀도, 문자열 내용, 또는 복잡한 에일리어싱 패턴에 대한 추론이 필요한 버그는 놓친다. 설계상 unsound(불완전)하기도 하다: false positive을 낮게 유지하기 위해 버그를 놓칠 수 있다. diff마다 거짓 경보를 울리는 정적 분석기는 비활성화된다. Meta의 내부 배포는 Infer의 false positive률을 10% 미만으로 유지했기 때문에 개발자는 실제로 그 보고에 대응한다.

자체 코드에서 Infer 실행하기

Infer는 오픈 소스이며 C, C++, Objective-C, Java, 그리고 (실험적으로) Rust와 Swift를 지원한다. 가장 쉽게 시도해 볼 방법은 Java나 C 프로젝트에서 사용하는 것이다.

Homebrew나 Docker를 통해 Infer를 설치한다:

# macOS
brew install infer

# Or via Docker
docker run --rm -v $(pwd):/repo infer/infer infer run -- make -C /repo

Maven을 사용하는 Java 프로젝트의 경우:

infer run -- mvn compile

Make를 사용하는 C 프로젝트의 경우:

infer run -- make

Infer는 코드를 컴파일하고, 제어 흐름 그래프를 구축하고, 분석을 실행한다. 출력은 파일명, 줄 번호, 그리고 위반된 추론된 전조건이 포함된 일련의 버그 보고서다.

Infer가 플래그를 세울 최소한의 C 예제는 다음과 같다:

// leak.c
#include <stdlib.h>

int* allocate_but_leak(void) {
    int* p = malloc(sizeof(int));
    *p = 42;
    // forgot to return p or free it
    return NULL;
}

infer run -- cc leak.c를 실행하면 다음이 출력된다:

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

Infer는 다음 예제의 null reference도 잡아낸다:

// null.c
#include <stdio.h>

void print_length(const char* s) {
    if (s != NULL) {
        printf("%zu\n", strlen(s));
    }
}

void unsafe_call(void) {
    print_length(NULL);  // Infer reports this
}

사실 Infer는 위 예제를 보고하지 않는다. print_length 함수는 널 인수를 안전하게 처리한다. Infer는 널일 가능성이 있는 포인터에서 검사 없이 참조가 일어날 때만 보고한다. 다음은 트리거되는 예제다:

// null_bad.c
#include <stdio.h>

void unsafe_print(const char* s) {
    // No null check before dereference
    printf("first char: %c\n", s[0]);
}

void call_unsafe(void) {
    unsafe_print(NULL);  // Infer reports this
}

Infer는 call_unsafe에서 unsafe_print를 거쳐가는 경로를 추적하고, s[0]이 평가될 때 s가 널임을 보고한다.

트레이드오프: 속도 대 정확도

Infer의 모듈형 설계는 Meta에서 각 풀 리퀘스트마다 실행할 만큼 충분히 빠르다. 하지만 모듈성은 근사화를 도입한다. Infer가 함수를 분석할 때 정확한 호출 맥락은 알지 못한다. Infer는 보수적인 전조건을 추론하는데, 이는 필요 이상으로 강할 수 있다. 더 강한 전조건은 호출 지점에서 보고되는 버그가 줄어들지만, false positive도 줄어든다.

이것이 정적 분석의 핵심적인 긴장 관계다. sound(완전한) 분석기는 모든 버그를 보고하지만 거짓 긍의에 잠긴다. Infer와 같은 unsound 분석기는 확신을 가진 버그만 보고함으로써 개발자를 만족시킨다. 놓치는 버그는 도입의 대가다.

Infer의 양방향 추론 엔진은 전역 상태와 복잡한 콜백에서도 어려움을 겪는다. Java 코드가 익명 내부 클래스를 실행기에 전달하면 Infer는 어떤 스레드가 어떤 메서드를 실행하는지 추적을 잃을 수 있다. RacerD는 일반적인 패턴을 처리하지만 조건 변수나 원자적 필드를 포함하는 미묘한 경쟁은 놓친다.

정적 분석을 도입해야 할 때와 피해야 할 때

네이티브 코드, 모바일 앱, 또는 C 계열이나 Java로 된 서버 코드를 배포한다면 Infer를 고려해야 한다. Infer가 찾는 버그, 즉 null reference, 누수, 경쟁은 바로 프로덕션 크래시와 보안 취약점을 일으키는 것들이다.

Infer가 테스트 스위트를 대체할 것으로 기대해서는 안 된다. 정적 분석과 동적 테스트는 상호 보완적이다. 테스트는 선택한 입력에 대해 코드가 의도한 대로 작동하는지 검증한다. 정적 분석은 어떤 입력에 대해서도 코드가 금지된 동작을 하지 않는지 검증한다.

코드베이스가 Python, Ruby, 또는 JavaScript라면 Infer는 적절한 도구가 아니다. 이러한 언어는 Infer가 추상 모델을 구축하는 데 사용하는 정적 타입 정보가 부족하다. 동적 언어의 경우 mypy나 pyright 같은 타입 검사기가 다른 클래스의 오류를 잡아낸다.

핵심 요약

Meta의 10만 건의 버그 수정은 마케팅 숫자가 아니다. 이는 diff마다 실행되어 코드를 실행하지 않고 분석하고, 어떤 테스트도 포착하지 못했을 버그를 보고하는 도구의 산출물이다. 근간이 되는 기법인 abstract interpretation은 수십 년의 역사를 가진다. 공학적 성과는 이를 개발자가 끄지 않을 만큼 빠르고 정확하게 만든 것이다.

Meta의 인프라가 없어도 혜택을 받을 수 있다. Infer를 설치하고 빌드 시스템을 가리킨 다음, 무서워하는 모듈에서 실행하라. 메모리 관리 모듈, 동시성 레이어, C 상호운용 경계. 발견된 누수와 null reference을 수정하라. 그런 다음 CI에 추가하고 버그 수가 늘어나지 않도록 하라.

abstract interpretation은 마법이 아니다. 이는 근사와 트레이드오프를 수반하는, 코드에 적용된 수학이다. 하지만 이는 실제 코드베이스에서 실제 버그를 찾아내는 수학이며, 그것을 알 가치가 있다.