Rust borrow checker 버그: 건전성(soundness)의 진짜 의미

Rust의 타입 시스템은 확실한 약속을 합니다. 안전한 코드가 컴파일되면 댕글링 포인터, 데이터 레이스, use-after-free가 있을 수 없다는 것입니다. 그런데 GitHub 이슈에 완벽하게 안전해 보이는 Rust 코드 조각이 올라왔습니다. 이 코드는 죽은 스택 프레임에서 가져온 쓰레기 값을 출력합니다. 그리고 이 구멍이 Rust borrow checker에 11년 동안 숨어 있었다는 사실이 드러나면서 많은 사람들이 충격을 받았습니다. 이 버그는 공변적(covariant) 필드 할당을 통해 구조체의 라이프타임 요구사항이 빠져나가게 만듭니다. 악의적인 Drop 구현과 함께 쓰면 지역 변수를 가리키는 참조를 전역 변수에 숨겨 두었다가, 그 변수가 사라진 뒤에도 읽을 수 있습니다. AddressSanitizer는 이를 stack-use-after-scope라고 부릅니다. 하지만 컴파일러는 문제없다고 판단했습니다.

반응은 예상대로였습니다. 어떤 사람들은 Rust의 안전성 이야기가 끝났다고 선언했습니다. 다른 사람들은 버그는 원래 생긴다며 어깨를 으쓱했습니다. 둘 다 이 사건에서 정말 흥미로운 부분을 놓치고 있습니다. 이 버그는 정적 보장이 실제로 무엇을 의미하는지, 비공식적 추론이 어디서 무너지는지, 그리고 "타입 시스템은 건전하다"와 "컴파일러가 건전한 타입 시스템을 강제한다" 사이의 간극에 왜 가장 흥미로운 버그가 숨어 있는지를 보여 주는 깔끔한 자연 실험입니다. 그래서 이 사건에서 떠오른 흔한 믿음들을 하나씩 검증해 보겠습니다.

오해 1: 건전성 버그는 Rust의 안전성 모델이 실패했다는 뜻이다

처음 드는 생각은 이것을 이론에 난 균열로 보는 것입니다. 하지만 그렇지 않습니다. 라이프타임 규칙이 다시 쓰인 것도 아니고, 소유권과 빌림이 근본적으로 깨졌다는 것이 발견된 것도 아닙니다. 화이트보드와 RFC에서 설계된 Rust 타입 시스템은 이 프로그램을 거부해야 한다고 말합니다. 컴파일러가 거부하지 못했을 뿐입니다.

명세와 구현의 차이는 우리 분야에서 가장 오래된 단층선 중 하나입니다. Tony Hoare는 통신하는 순차 프로세스(CSP)라는 아름다운 이론을 내놓았지만, 수십 년 동안 C 컴파일러들은 표준상 완벽히 유효한 코드를 잘못 컴파일해 왔습니다. 이론은 맞지만 실제 결과물은 새고 있는 것입니다. 우리는 이전에 명세와 구현의 간극이 버그가 사는 곳이라는 글을 쓴 적이 있는데, 이번 사건이 바로 그 교과서적인 사례입니다. 라이프타임 규칙이 틀린 것은 아니었습니다. 문제는 rustc의 변성(variance) 추론 코드에 있었습니다. 이 코드는 &'a T를 &'static T가 필요한 자리에 대체해도 되는지 판단하는데, 할당이 공변적 필드를 타고 흐를 때 구멍이 있었습니다.

간단히 줄여 본 익스플로잇의 형태는 이렇습니다. 먼저 Drop 구현이 자신의 페이로드를 전역 'static 저장소에 복사하는 래퍼를 만듭니다. 원래 컴파일러는 페이로드가 'static이어야 한다고 강제하므로, 지역 변수에 대한 참조는 들어갈 수 없습니다. 하지만 이 버그를 이용하면 수명이 짧은 참조를 공변적 할당을 통해 세탁할 수 있고, 결과적으로 래퍼는 지역 String인 l에 대한 &l을 보관하게 됩니다:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

각 줄은 따로 보면 모두 무해해 보입니다. 건전성 문제는 조합에서만 나타납니다. 공변적 필드, 라이프타임 경계를 느슨하게 만드는 할당, 그리고 페이로드를 참조 대상보다 오래 살아남는 곳으로 옮기는 Drop이 함께 있을 때 생깁니다. 이것은 검사기 구현 버그의 전형적인 특징입니다. 불변식은 전역적인데 강제는 국소적으로 이루어지고, 한 코드 경로가 검사를 빠뜨린 것입니다.

그러니까 안전성 모델이 실패한 것은 아닙니다. 안전성 모델을 강제하는 부분이 실패한 것입니다. 더 작은 실패처럼 보이지만, 뒤에서 보겠듯이 사소한 문제는 아닙니다.

오해 2: 11년 동안 발견되지 않았으니 버그는 무해하다

Rust 팀의 자체 트리아지 논리는 대략 이랬습니다. 사람들이 실제로 겪고 있었다면 P-critical이었을 텐데, 11년 동안 한 번도 보고되지 않았다면 쉽게 트리거될 수 없다는 뜻이니 P-high라는 것입니다. 일리가 있습니다. 실제로 메모리 안전성을 깨뜨리려면 데이터를 'static 위치로 옮기는, 일부러 고약하게 짠 Drop 구현이 필요합니다. 그런 코드를 쓰는 사람은 거의 없습니다. 우발적 노출 범위는 아주 작습니다.

하지만 이 문장에서 "우발적으로는 거의 트리거되지 않는다"는 말이 많은 역할을 하고 있습니다. 안전성 보장은 우발적 사고에 관한 것만이 아닙니다. 주변 코드가 우호적이지 않을 때 무엇을 믿을 수 있는지에 관한 것입니다. 건전한 타입 시스템의 핵심은 모듈 단위로 추론할 수 있다는 점입니다. 여러분의 Drop 구현을 감사할 필요가 없는 이유는, 컴파일러가 특정 나쁜 조합은 표현 자체가 불가능하다는 것을 이미 증명했기 때문입니다. 구멍이 생기면 이런 모듈성도 사라집니다. 악의적인 의존성이나, 선의를 가졌지만 실수한 작성자의 의존성도 언어가 불가능하다고 약속했던 일을 할 수 있게 됩니다.

역사에는 적절한 가젯이 나타나자 아주 쉽게 악용된 "악용 불가능한" 버그가 가득합니다. 한 댓글러가 말했듯이 실제로 중요한 질문은 이 수정이 생태계의 실제 크레이트를 깨뜨리는지 여부인데, 답은 아마 "거의 없거나 전혀 없다"일 것이고 이는 좋은 소식입니다. 하지만 11년의 조용한 세월에서 얻어야 할 올바른 교훈은 "버그가 무해했다"가 아닙니다. 증거가 없다는 것이 부재의 증거는 아니라는 점, 특히 우연이 아니라 의도를 요구하는 실패 모드에서는 더욱 그렇다는 점입니다.

오해 3: 눈이 많으면 모든 버그는 얕아진다

이것은 우리를 가장 부끄럽게 만들어야 할 오해입니다. rustc는 지금까지 작성된 컴파일러 중 가장 많은 검토를 받은 것 중 하나입니다. 오픈 소스이고, 전담 타입 팀이 있으며, 활발한 학계 커뮤니티가 있고(RustBelt는 몇 년 전 Rust 핵심부의 형식 모델을 내놓았습니다), 매일 수많은 사용자가 두드리고 있습니다. 그런데도 건전성 구멍이 라이프타임 추론에 10년 넘게 숨어 있었고, 그 사이 주변 구조가 완전히 다시 쓰이기도 했습니다.

Linus의 법칙은 눈들이 올바른 곳을, 올바른 모델을 머릿속에 담고 본다고 가정합니다. 타입 시스템의 건전성 문제는 이 두 가정을 모두 무너뜨립니다. 이런 문제는 변성, drop 순서, 강제 변환(coercion), 트레이트 경계 같은 여러 기능이 교차하는 지점에 살고, 각 기능은 지역적으로는 모두 올바릅니다. 리뷰어들은 코드를 읽으면서 의도된 불변식을 보는데, 코드를 쓴 사람들도 같은 의도된 불변식을 보고 작성했기 때문입니다. 확증 편향이 프로세스에 내장되어 있는 셈입니다. 반례를 찾으려면 적대적인 사고방식이 필요한데, 자신이 만든 추상화에 대해 적대적으로 생각하는 것은 정말 어렵습니다.

counterexamples.org라는 사이트에는 그럴듯해 보이는 타입 규칙이 어떻게 깨지는지를 정리한 자료가 있습니다. 공통점은 가변성이 다른 까다로운 무언가와 조합될 때 문제가 생긴다는 것인데, 바로 이 버그의 형태입니다. 이것들은 새로운 교훈이 아닙니다. ML의 타입 시스템에는 가변 참조와 다형성 주변에 유명한 건전성 문제가 있었고, 이는 값 제한(value restriction)으로 고쳐졌습니다. Java의 배열은 공변적이어서 런타임에 ArrayStoreException을 던질 수 있는데, 언어 설계자들이 건전성 대신 편의성을 택했기 때문입니다. 세월이 흘러도 서브타이핑, 변경(mutation), 제네릭이라는 같은 세 가지 기능이 결합해 누군가를 물곤 합니다. 이런 고고학을 좋아한다면 Lisp의 60년 역사가 이 아이디어들이 얼마나 오랫동안 발전해 왔는지 보여 주고, Rob Pike의 오래된 규칙들은 복잡성이 건전성 구멍이 자라나는 곳이라는 사실을 깨달으면 다르게 읽힙니다.

눈은 도움이 됩니다. 하지만 충분하지는 않습니다. 직접 언어를 만들고 있는 한 사람에게서 들은 정직한 입장은 대략 이렇습니다. 어떤 검토도 모든 문제를 해결하지 못하므로, 지치지 않고 여러분의 가정을 공유하지 않는 기계적 방법이 필요하다는 것입니다.

오해 4: 비공식적 추론은 사실상 증명이다

Rust의 라이프타임 규칙이 설계될 때, 똑똑한 사람들이 많은 예제를 가지고 신중하게 논증했습니다. 이것은 비공식적 추론이고, 사실상 모든 상용 컴파일러가 이런 방식으로 만들어집니다. 그 결과 시스템은 누구나 확인할 수 있는 한에서 건전합니다. 그런데 우리가 두 번이나 겪으며 알게 됐듯이, 이것은 건전하다는 것과 같지 않습니다.

그 둘 사이의 간극을 메우는 것이 RustBelt 같은 프로젝트와 차세대 트레이트 솔버에 대한 진행 중인 작업입니다. Iris 분리 논리 프레임워크 위에 Coq(지금은 Rocq)로 만들어진 RustBelt는 unsafe 추상화 경계 같은 까다로운 부분을 포함해 Rust 핵심 타이핑 규칙의 모델을 기계로 검증했습니다. 이것은 획기적인 성과였습니다. 하지만 무엇을 증명했는지 주목해야 합니다. rustc가 아니라 Rust의 모델을 증명한 것입니다. 증명은 λRust 계산법을 다루고, 실제 컴파일러는 그동안 표류하며 기능이 늘고 누구도 다시 검증하지 않은 구현 결정들이 쌓여 왔습니다. 이번 문제는 그 표류에 대한 청구서가 도착한 것입니다.

프로덕션 컴파일러 전체를 형식화하는 일은 엄청나게 비쌉니다. 형식 검증된 C 컴파일러인 CompCert는 Rust보다 훨씬 작은 언어를 위해 수년간 전문가의 노력이 들어갔고, 그마저도 컴파일 패스를 검증할 뿐 원본 타입 시스템이 모든 잘못된 프로그램을 잡는다는 것을 증명하지는 않습니다. rustc의 200만 줄을 Coq로 증명하려는 사람은 없을 겁니다. 현실적인 길은 다음과 같은 다중 방어선에 가깝습니다.

• 핵심 규칙의 기계 검증 모델(RustBelt 스타일)로, 이론 자체에 구멍이 없도록 합니다.
• 체계적인 퍼징과 사례 분석 도구로, 사람이 테스트할 생각을 하지 못하는 기능 상호작용의 모서리를 공격적인 프로그램으로 생성합니다.
• 검사기의 뮤테이션 테스트와 속성 기반 테스트: 경계 하나를 뒤집었을 때 프로그램이 실패해야 한다면, 실제로 실패하는지 확인합니다. SQLite의 테스트 문화가 여기서 모범이 됩니다.
• 유지 관리되는 알려진 건전성 문제 목록을 두세요. Rust에는 100개가 넘는 태그가 붙어 있는데, 이를 민간 지식이 아니라 엔지니어링 우선순위가 있는 백로그로 다뤄야 합니다.

흥미롭게도 LLM 기반 검색이 결국 순이익이 될 수도 있습니다. 기능을 삐딱한 방식으로 끈질기게 조합하는 도구야말로 비공식적 추론에 부족한 적대자이기 때문입니다. 많은 사람들이 바라는 최종 목표는 형식적으로 명세된 Rust와, 그 명세에 대해 증명된 검사기입니다. 하지만 지금과 그 목표 사이에는 지루하고 화려하지 않은 제약 해결 작업이 계속 필요합니다.

오해 5: 건전성이 절대적이지 않다면 정적 안전성은 사기다

냉소적인 해석은 이렇습니다. Rust는 안전성을 약속했는데 그 약속에 허점이 있었으니, 그 약속은 마케팅이었고 우리는 다시 C에서 포인터를 마구 다뤄도 된다는 것입니다. 이것은 정확히 거꾸로이며, 몇 가지를 정밀하게 짚어 볼 가치가 있습니다.

타입 시스템의 건전성은 수학적 대상에 대한 정리입니다. 반면 실무 언어가 주는 것은 통계적이고 경제적인 보장입니다. use-after-free, 데이터 레이스, 이터레이터 무효화 같은 버그 전체 클래스가 "코드베이스의 상시 배경 복사선"에서 "11년 뒤에야 발견되어 메인 페이지에 오를 만큼 드문 사건"으로 바뀝니다. 기저율을 비교해 보세요. 대규모 C와 C++ 코드베이스의 메모리 안전성 버그는 해마다 심각한 CVE의 대부분을 차지하고, 이제는 개별 사례에 아무도 놀라지 않습니다. 반면 Rust의 건전성 버그는 너무 드물어서 하나하나가 자체 GitHub 이슈, 토론 스레드, 사후 분석 문화를 얻습니다. 열거 가능한 희소성은 열거할 수 없는 희소성과는 전혀 다른 세계입니다.

실패가 어떻게 누적되는지에도 차이가 있습니다. C에서는 모든 줄이 잠재적 메모리 안전성 위험이므로, 경계심의 비용이 코드 크기에 비례해 영원히 늘어납니다. Rust에서는 경계심이 가장자리에 집중됩니다. 즉 unsafe 블록, FFI, 그리고 (지금 알게 된 것처럼) 컴파일러 자체의 검사기가 그곳입니다. 이런 집중 덕분에 감사, Miri 같은 도구, 형식 기법이 애초에 실용적으로 가능해집니다. 보장은 이진적이지 않습니다. 위험이 어디에 있는지를 극적으로 재배치하는 것입니다.

알려진 버그가 있더라도 11년 동안 운영 트래픽이 한 번도 건드리지 않은 타입 시스템은, 그 버그가 설계 자체인 언어보다 여전히 무한히 강합니다.

실제로 가져갈 교훈

Rust를 작성한다면 아무것도 바꿀 필요가 없습니다. 이 이슈가 제기되기 전에도 여러분의 코드가 조용히 안전하지 않았던 것은 아닙니다. 실질적인 악용 경로에는 의도가 필요했습니다. 라이브러리를 유지 관리한다면 정직한 대응은 예전과 같습니다. unsafe 표면을 작게 유지하고, 까다로운 부분에서는 Miri를 돌리고, borrow checker를 다른 사람의 악의적인 코드에 대한 신탁처럼 취급하지 마십시오. 대신 여러분 자신의 실수를 잡아내는 매우 신뢰할 만한 도구로 다루면 됩니다.

언어나 컴파일러를 만든다면 이 버그는 선물입니다. 프로덕션에서 건전성이 실제로 어떻게 무너지는지를 보여 주는 드물고 잘 문서화된 표본입니다. 이론에서가 아니라 강제 과정에서, 하나의 기능이 아니라 기능들이 교차하는 지점에서, 리뷰가 아니라 적대적 구성으로 발견되었습니다. 이를 진지하게 받아들이고 트레이트 솔버 재작성, 리전 제약 재설계, 검증 관련 도구에 투자하는 팀들이 10년 뒤에도 의미 있는 보장을 제공하는 팀이 될 것입니다.

그리고 모든 사람에게 보장이 무엇인지 다시 짚어 보자는 이야기입니다. 우리는 수십 년 동안 "증명됨"과 "설득력 있게 논증되었고 아직 반박되지 않음"을 혼동해 왔습니다. 타입 시스템, 암호 프로토콜, 분산 합의 전반에서 그랬습니다. 성숙한 신뢰는 다리가 완벽하다고 가정하는 것이 아닙니다. 다리에 검사관이 있고, 그들이 발견한 내용을 공개하며, 고친 것과 아직 고치지 못한 균열의 공개 목록을 유지한다는 것을 아는 것입니다. 그런 면에서 구멍을 찾는 데 11년이 걸렸다는 것은 비난거리가 아닙니다. 컴파일러 주변의 인간 시스템이 대체로 기대한 대로 작동하고 있다는 증거입니다.