요약
Rust 컴파일러가 수명 규칙을 어기는 코드를 11년 동안 통과시켜 왔습니다.
10월 13일 Rust 저장소에 올라온 이슈입니다. 구조체 필드에 참조를 대입하는 짧은 코드만으로 이미 사라진 스택 메모리를 읽을 수 있었고, Rust 타입 팀은 이를 건전성(타입 검사를 통과한 코드는 메모리 오류를 내지 않는다는 보장) 버그로 분류했습니다.
왜 중요한가
- 컴파일러가 허락한 코드가 해제된 메모리를 읽었습니다. Rust가 약속하는 메모리 안전에 구멍이 있었다는 뜻입니다.
- 다만 악용하려면 일부러 악의적인 Drop 구현을 짜야 합니다. 그래서 기존 코드가 실수로 이 버그를 밟았을 가능성은 낮다고 타입 팀은 봤습니다.
핵심 내용
- 구조체에 'static(프로그램 끝까지 유효한 데이터) 제약을 걸어도, 필드에 지역 변수의 참조를 넣는 대입이 통과됐습니다.
- 값이 사라질 때 도는 Drop 코드가 그 참조를 계속 유효한 것으로 다뤄, 해제된 메모리 내용을 출력했습니다.
- 스레드나 클로저로 같은 구멍을 여는 변형도 잇달아 나왔고, 그중 하나는 2015년의 Rust 1.4부터 통했습니다.
- 타입 팀의 lcnr은 11년간 아무도 찾지 못한 만큼 밟기 쉬운 버그는 아니라며 최고 등급 바로 아래인 P-high로 분류했습니다.
- 수정 PR(#164277)이 올라와 있지만 아직 병합되지는 않았습니다.
HN 반응
- 타입 체계가 아니라 컴파일러가 검사를 빠뜨린 버그라서 규칙을 바꾸지 않고 고칠 수 있다는 의견이 많았습니다.
- Rust가 안전을 과장했다는 비판에는, C 컴파일러에도 이런 버그가 흔하고 Rust의 안전성은 실제로 효과가 있었다는 반박이 맞섰습니다.
이 버그가 그렇게 오래 눈에 띄지 않았다니 놀랍지만, 그래도 고치기는 쉽습니다. 타입 시스템 자체의 버그가 아니라 컴파일러의 버그일 뿐이니까요. 러스트 타입 시스템의 라이프타임 규칙대로라면 컴파일러는 처음부터 그 코드를 거부했어야 합니다. 그러니 라이프타임의 근본 규칙을 바꿀 필요 없이, 그 코드를 거부하도록 고치기만 하면 됩니다.
러스트가 막아 주기로 되어 있는데도 이런 버그는 결국 피할 수 없다는 게 흥미롭습니다. 러스트는 실무에서 이 문제를 크게 줄여 주었지만, 이런 이슈 때문에 완전히 확신할 수는 없습니다. 동료 평가를 거쳐 참으로 인정받은 수학 증명도 틀렸을 가능성이 있는 것과 비슷합니다. 확률은 아주 작아도 0은 아니고, 복잡도가 높아질수록 더 그렇습니다.
재미있네요. 핵심 논거는 C는 문제를 피하려면 프로그래머에게 너무 많은 숙련도를 요구한다는 것이었잖아요.
그런데 안전하다고 홍보하고, C를 비난하면서 인기를 얻은 언어가 이제는 거짓 안전감을 줬다고 말할 수 있게 됐어요. 컴파일러와 화해하려고 프로젝트에 새 기능을 넣을 때마다 끝없이 리팩터링하게 만드는 에러 메시지 덕에, 프로그래머가 진짜 문제에서 눈을 돌리게 된 거죠. 프로그래머를 프로그래밍하는 언어, 역할이 뒤집힌 언어예요.
아니요, 그렇게 해석할 일이 아닙니다. 러스트는 단지 더 안전해 보이는 데 그치지 않고 C보다 실제로 안전하다는 것을 보여 주며 크게 성공했습니다. 그 안전감은 거의 전적으로 실체가 있는 것이었습니다. 다만 일부 상황을 다루지 못했을 뿐입니다.
C 컴파일러에는 이런 버그가 산더미처럼 많지 않은 것처럼 이야기하는 사람들이 이해가 안 돼요. 무슨 판타지 세계에 사는 것도 아니고요. 게다가 이건 버그만 센 거고, 공식적으로 인정된 UB는 따지지도 않았잖아요.
다른 컴파일러 버그와 뭐가 다른가요?
얼마 전에 리눅스 커널에서도 중요한 null 체크를 잘못 제거해 버린 버그가 있었잖아요.
이게 다른 건가요?
아니요, 러스트를 실제로 써 보지 않은 사람들이 이걸 실제보다 거창한 일인 것처럼 포장하길 좋아하는 겁니다. 보여 주기식 분노겠죠.
러스트에서 지금 열려 있는, 비슷한(unsoundness를 일으키는) 컴파일러 버그 목록은 다음과 같습니다.
https://github.com/rust-lang/rust/issues?q=state%3Aopen%20label%3A%22I-unsound%22
이론적으로는 borrow checker의 건전성(soundness)을 형식 검증하는 것이 가능합니다. AI가 발전하면 가까운 미래에 가능해질지도 모르죠. 아니, 나비에-스토크스 방정식을 증명하는 것보다 얼마나 더 복잡하겠어요?
참고로 Lean 커널 자체도 형식 검증되어 있지 않습니다.
본질적으로 하드웨어 구현에 의존하는 것의 건전성은 형식 검증할 수 없습니다. 그 하드웨어 자체에 결함이 있을 수 있으니까요.
하드웨어의 속성은 공리로 받아들이면 됩니다. 예를 들어 ARMv6의 캐시 일관성은 방대한 사양서에 상세히 규정되어 있지만, 실제 하드웨어가 그 사양을 충실히 따른다는 보장은 없잖습니까.
내가 통제할 수 있는 범위, 즉 컴파일러 코드의 건전성은 얼마든지 검증할 수 있습니다. 위에서 제안한 것도 바로 그거고요.
그래도 알고리즘이 원하는 속성을 갖는다는 것은 형식 검증할 수 있습니다. 건전성을 위해 하드웨어에 추가 속성이 필요하다면, 그건 증명이 아니라 속성 쪽 오류일 뿐입니다. (물론 그러면 그 하드웨어에서의 건전성을 증명한 것은 아니게 되겠지만요.)
러스트는 잘 모르지만, 이런 종류의 경우에는 문제가 올바른 프로그램까지 거부하지 않으면서 그 잘못된 코드만 거부하게 만드는 데 있잖아요. 이번 건은 정말 고치기 쉬운 것일 수도 있겠지만, 저는 모르겠네요.
그런 올바른 프로그램은 없습니다. 귀류법으로 증명해 보죠.
올바른 프로그램이라면 러스트의 미정의 동작을 이용하고 있을 텐데, 러스트에는 미정의 동작이 없습니다. 따라서 그런 프로그램은 존재할 수 없습니다.
수정 전에는 어떤 프로그램이 멀쩡히 동작하는 것처럼 보였을 수는 있어도, 애초에 올바른 러스트 프로그램은 아니었습니다.
비꼬는 건지 모르겠지만, 아니라는 전제로 말씀드리겠습니다.
라이스의 정리에 따르면 건전하면서 동시에 완전할 수는 없습니다. 즉 올바른 프로그램을 모두 받아들이면서 잘못된 프로그램을 모두 거부할 수는 없습니다. 대부분의 언어는 건전하지만 완전하지는 않은 쪽을 택합니다. 잘못된 프로그램을 모두 거부하는 대신 올바른 프로그램도 일부 거부하는 겁니다(C와 C++가 대표적인 예외이고, 대부분의 언어에는 탈출구가 있습니다). 원 댓글은 이번 수정이 지금은 컴파일되는 올바른 프로그램을 거부할 수도 있다는 얘기를 한 겁니다. 기존의 일부 건전성 버그에는 맞는 말이지만, 이번 건에도 꼭 그렇다고 할 수는 없습니다.
라이스의 정리는 여기에 적용되지 않습니다. 이건 컴파일러가 하는 일이 아니라 여러분의 프로그램에 관한 이야기입니다. 프로그램이 건전하지 않으면 컴파일러가 받아들이고 제대로 동작하는 것처럼 보여도 유효한 러스트가 아닙니다.
그나저나, 제가 비꼰 게 맞습니다.
용어 문제로 따지자면, 건전성은 개별 프로그램이 아니라 타입 시스템 전체의 속성입니다. 타입 시스템은 올바른 프로그램만 받아들일 때 건전하다고 하고, 프로그램은 미정의 동작을 절대 일으키지 않을 때 올바르다고 합니다.
라이스의 정리에 따르면 소스 코드만 보고 올바른 프로그램과 잘못된 프로그램을 정확히 가려내는 것은 불가능합니다. 그래서 러스트는 건전성을 지키려고 올바른 프로그램도 일부 거부합니다(예: "if false { None.unwrap_unchecked() }").
원글의 버그 리포트라면, 이 건전성 문제를 이용하는 올바른 프로그램이 실제로 많지는 않을 것 같아서, 고치면 잘못된 프로그램을 더 많이 거부하게 될 뿐입니다.
물론 적용됩니다(이번 건에 구체적으로 적용되는 건 아니라고 해도요). 이 이슈가 보여 주듯이 구현된 러스트 의미론은 건전하지 않습니다. 건전한 의미론을 찾아내거나 고쳐야 합니다. 수학적으로는 러스트를 처음부터 다시 설계하는 것과 같은 일입니다(RustBelt 같은 건 시스템 전체를 형식화하지 않았으니 제외하고요). 라이스의 정리 때문에 건전한 프로그램 중 일부는 포기해야 한다는 것도 압니다. 그렇다면 이전 러스트에서 포기했던 프로그램만 정확히 포기할 수 있을까요? 될 수도 있고 안 될 수도 있습니다.
형식화의 까다로운 점은, 형식 건전성 증명을 하려면 보통 타입 체커를 증명 보조기에 다시 구현해야 한다는 겁니다. 그 재구현이 실제 러스트 컴파일러와 똑같은지는 확실하지 않고(사실 증명을 다룰 수 있게 하려면 타입 시스템을 크게 단순화해야 하는 경우가 많습니다), 그래서 타입 시스템의 건전성에 근본적인 결함이 없어도 구현상의 버그 때문에 건전하지 않은 상황이 생길 수 있습니다.
맞습니다. 구현 자체를 증명하는 일은 너무 어려워서 아마 영영 이뤄지지 않을 겁니다. 하지만 러스트의 추상 의미론이 건전하다는 것만 증명해도 그 자체로 큰 진전입니다(RustBelt은 러스트의 일부분에 대해 그걸 해냈습니다).
러스트 의미론은 건전한데 구현이 그걸 온전히 따르지 못하고 있을 가능성을 무시하고 계시네요. 그렇다면 건전한 의미론을 찾을 필요는 없습니다.
제 생각에는 이쪽이 단연 가장 가능성이 높습니다.
이유는 이렇습니다. 그 예제가 컴파일되어야 한다고 주장하는 댓글은 하나도 못 봤고, 그게 러스트가 해야 할 동작이 아니라는 데에는 수많은 사람이(암묵적으로) 동의하고 있으니까요.
저는 건전한 의미론이 있을 가능성을 분명히 무시하지 않았습니다.
그런데 "러스트 의미론"은 형식적으로 정의되어 있지 않습니다. 가장 가까운 것이 러스트가 현재 구현하고 있는 것인데, 여기서 그게 건전하지 않다는 게 드러났습니다. 그 외에는 T-types 팀 일부 구성원의 머릿속에 막연한 구상이 있을 뿐이고, 건전성을 판단할 만큼 구체적이지 않습니다(출처: 타입 시스템 쪽 사람들이 의미론을 형식화하려는 이유가 바로 이것입니다).
그리고 참고로, 우리가 아는 다른 건전성 문제 중에는 해결 과정에서 지금은 받아들이는 올바른 프로그램을 거부하게 될 가능성이 높은 것들이 있고, 남은 문제는 그 수가 얼마나 되느냐뿐입니다.
제가 완전히 헛소리를 하는 걸 수도 있지만, "처음부터 다시 설계"가 어느 정도인지는 수학의 어느 분야를 말하느냐에 따라 다를 수 있습니다. 예를 들어 의미론을 합성 가능한 함수들의 연속으로 모델링하면, 해당 함수들의 의존성 트리만 새로 만들면 됩니다. 사실상 모든 것을 낭비 없이 재사용할 수 있고, 출력 공간도 잘려 나가게 됩니다.
그래서 RustBelt은 제외하자고 한 겁니다. 오늘날에는 형식 의미론이 없고 실제 구현만 있는데, 그 구현은 합성 가능하지 않으니까요.
러스트는 튜링 기계를 대상으로 하지 않으므로 라이스의 정리는 적용되지 않습니다.
그래도 러스트에는 미정의 동작이 있는데요.
이번 경우는 컴파일러가 중첩 블록 끝에 삽입되는 drop 메서드의 암시적 호출을 제대로 타입 체크하지 않는 것이 문제입니다. 제가 알기로는 올바른 코드 중에 그 체크가 없다는 점에 의존하는 코드는 없습니다.
놀랍긴 하지만 아주 드문 일은 아닙니다. 지금 unsound 라벨이 붙은 이슈가 100개가 넘습니다. 오래된 것도 있지만, 제가 알기로는 새 트레이트 솔버(trait solver)가 나오면 그중 일부는 고칠 수 있게 된다고 합니다(다만 원글의 것은 아마 아닐 겁니다).
맞습니다, unsoundness 버그를 찾는 것 자체가 가장 드문 일은 아닙니다. 하지만 이번 건은 문제를 일으키는 코드가 얼마나 단순할 수 있는지가 특이합니다(댓글에 있는 재현 코드의 여러 버전을 보세요). 다른 unsoundness 버그는 컴파일러 검사를 피하려면 코드를 한참 비비 꼬아야 하거든요.