iddqd, 또는 가장 어려운 종류의 unsafe Rust

 (oxide.computer)
1P by GN⁺ | ★ favorite | 댓글 1개
  • iddqd는 값에서 키를 빌려오는 Rust 맵 라이브러리로, Oxide의 Omicron 제어 평면에서 디스크와 sled inventory 같은 큰 레코드의 인메모리 인덱스를 유지해 정확성이 중요함
  • 표준 BTreeMap은 키와 값을 따로 저장해 전달이 번거롭거나 중복 키가 어긋날 수 있지만, IdOrdMap은 레코드 안의 필드에서 키를 추출해 조회함
  • unsafe Rust는 컴파일러가 증명하지 못하는 안전한 프로그램을 표현하는 탈출구이며, 제네릭 코드가 사용자 제공 trait 구현을 호출할 때 병적인 안전 Rust까지 견뎌야 함
  • iddqd의 mutable iteration은 인덱스가 모두 다르다는 불변식에 의존해 수명을 확장하며, 병적인 Ord 구현이 B-tree와 item set을 어긋나게 만들어 같은 항목에 대한 중복 인덱스를 만들 수 있었음
  • 수정은 키와 인덱스를 함께 비교하고 실패 시 사용자 코드를 호출하지 않는 선형 스캔으로 되돌아가며, Miri·모델 기반 테스트·panic fault injection·LLM 적대적 리뷰를 함께 써야 충분한 신뢰를 얻음

iddqd가 해결하는 문제

  • iddqd는 키를 값에서 빌려오는 맵을 제공하는 Rust 라이브러리이며, Oxide는 이를 Omicron 제어 평면에서 광범위하게 사용함
  • Omicron은 Oxide rack의 중심에서 compute와 storage 같은 리소스를 프로비저닝하고 rack이 계속 동작하도록 유지하는 소프트웨어이며, iddqd가 오작동하면 제어 평면이 예측하기 어렵고 진단하기 힘든 방식으로 잘못 동작할 수 있음
  • Rust 표준 라이브러리의 BTreeMap<Email, User> 같은 구조는 키인 email을 값과 따로 저장함
  • 키와 값을 함께 넘기려면 get_key_value로 (email, user)를 가져와야 하고, fetch 시점에 UserRecord 같은 별도 구조체를 만들면 레코드 타입이 많을 때 다루기 어려워짐
  • email을 User 안에도 복제하면 맵의 키와 값 안의 email이 서로 달라질 위험이 생김
  • IdOrdMap은 IdOrdItem trait로 레코드에서 키를 추출하게 하며, 키 타입은 type Key<'a> = &'a Email처럼 값에서 빌려올 수 있음
  • Oxide에서 이 패턴은 데이터베이스 조회 결과처럼 큰 레코드에 잘 맞았고, 제어 평면 전반의 큰 레코드 인덱싱에 유용하게 쓰임

추가 기능

  • iddqd는 여러 필드에서 빌려오는 복잡한 키를 1급으로 지원해 dynamic dispatch 같은 우회 없이 다룰 수 있음
  • BiHashMap과 TriHashMap은 항목 하나를 두 개 또는 세 개의 키로 각각 인덱싱해, 여러 맵을 손으로 유지하는 일반적 패턴을 피하게 함
  • Serde 구현은 맵이 아니라 시퀀스로 직렬화해 JSON에서 non-string 키도 직렬화할 수 있게 하며, 중복 키를 거부함
  • 하위 호환성을 위해 맵 형태 직렬화도 지원함

unsafe Rust가 어려워지는 지점

  • Rust에서 핵심 위험은 정의되지 않은 동작(undefined behavior, UB)이며, 안전한 코드가 어떤 방식으로도 UB를 일으킬 수 없으면 sound, 그렇지 않으면 unsound임
  • 안전 Rust 안에서 컴파일러는 UB가 있는 프로그램을 거부하지만, 정적 분석의 한계 때문에 UB가 없는 일부 프로그램도 함께 거부함
  • unsafe 키워드는 이런 프로그램을 표현하는 탈출구이며, 작성자가 soundness에 대한 책임을 지고 컴파일러에게 신뢰를 요청하는 방식임
  • unsafe 코드가 지켜야 하는 Rust 규칙에는 데이터 레이스 금지, 초기화되지 않았거나 해제된 메모리 읽기 금지, 같은 메모리 영역에 대한 여러 &mut alias 금지, immutable 데이터 변경 금지가 있음
  • 이 규칙은 특히 mutable aliasing 때문에 추론하기 어렵고, 안전한 추상화 뒤에 unsafe를 캡슐화하는 방식이 보통 필요함

안전 추상화 검증의 단계

  • split_at_mut은 mutable slice를 두 부분으로 나누는 안전 메서드지만, 안전 Rust만으로는 이런 분할을 표현할 수 없어 unsafe가 필요함
  • split_at_mut의 soundness는 &mut [T]를 받았는지, mid <= slice.len()을 확인했는지, 남은 길이를 정확히 계산했는지 같은 주변 안전 코드의 불변식에 의존함
  • MyVec<T>의 get은 len이 정확하고 범위 안에 있다는 조건에 의존하며, 이 조건은 같은 모듈 안의 다른 모든 메서드가 유지해야 함
  • 제네릭 unsafe 코드가 사용자 제공 코드를 호출하면 난도가 가장 높아짐
  • 안전 Rust 코드는 아무리 병적이거나 적대적으로 작성되어도 unsafe 코드가 UB를 일으키게 만들어서는 안 됨
  • ExactSizeIterator의 len()을 믿고 capacity만큼 쓰는 collect_exact 같은 코드는 iterator가 거짓 길이를 반환하면 할당되지 않은 메모리에 쓰게 되어 일반적으로 unsound함
  • std::io::Read도 buggy 구현이 읽은 바이트 수를 잘못 반환할 수 있는 trait이며, Rust RFC 2930이 이 문제를 다룸
  • iddqd는 사용자 제공 trait 구현을 호출하는 제네릭 데이터 구조라서 이 가장 어려운 범주에 속함

iddqd의 내부 구조

  • iddqd는 항목 목록인 ItemSet과 slot 인덱스를 담는 테이블을 결합함
  • IdHashMap<T>은 ItemSet<T>와 ItemIndex를 담는 hashbrown::HashTable을 사용함
  • ItemSet<T>는 Vec<ItemSlot<T>>를 가지며, ItemSlot<T>는 Occupied(T) 또는 Vacant { next: ItemIndex }임
  • free_head는 최근 해제된 Vacant slot 또는 free slot이 없다는 sentinel을 가리키며, free_head와 Vacant slot들이 free chain을 이룸
  • 새 항목을 넣을 때는 free_head로 재사용 가능한 slot을 확인하고, 있으면 Vacant slot을 Occupied로 덮은 뒤 free_head를 다음 값으로 옮김
  • free slot이 없으면 끝에 새 Occupied slot을 push하고, 이후 키를 가져와 해시를 계산한 뒤 새 인덱스를 hash table에 기록함
  • 제거는 반대로 hash table에서 키로 인덱스를 찾고 제거한 뒤, 해당 ItemSlot을 Vacant로 바꾸고 기존 free_head를 next로 연결함
  • IdOrdMap은 hash table 대신 B-tree index를 쓰며, BiHashMap과 TriHashMap은 각각 두 개와 세 개의 hash table을 저장함

mutable iteration과 수명 확장

  • IdOrdMap::iter_mut은 키 순서로 항목을 mutable iteration함
  • Rust iterator는 반환된 값이 iterator 자체를 빌리지 않아야 하며, collect 같은 조합자는 iterator가 사라진 뒤에도 Vec<&mut T> 같은 값을 남길 수 있음
  • 이 동작이 안전하려면 iterator가 같은 값을 두 번 반환하지 않아야 함
  • borrow checker는 목록에 대한 연속 접근만 보고 인덱스가 모두 다르다는 사실을 알 수 없음
  • iddqd는 std::mem::transmute::<&mut T, &'a mut T>로 수명 확장(lifetime extension)을 사용하며, 이는 self.iter가 반환하는 인덱스가 모두 다르다는 불변식에 의존함

병적인 Ord 구현이 만든 버그

  • 다섯 항목이 키 0부터 4까지 순서대로 들어 있는 IdOrdMap에서 Entry API로 키 0을 조회하면 OccupiedEntry가 index 0을 내부에 저장함
  • 이후 Key의 Ord 구현이 값과 무관하게 항상 Equal을 반환하도록 바뀌면, OccupiedEntry::remove가 B-tree를 다시 내려갈 때 key 비교만으로 잘못된 항목을 제거할 수 있음
  • 예를 들어 B-tree에서 (key = 2, index = 2)를 먼저 비교하면 Equal 때문에 그 entry가 제거되고, OccupiedEntry가 들고 있던 index 0 때문에 item set에서는 item 0이 제거됨
  • 이 상태에서 B-tree에는 index 0이 남아 있지만 item set의 slot 0은 vacant가 되고, item 2는 item set에 남아도 B-tree 포인터가 없어짐
  • 이후 Ord가 정상 동작으로 돌아가고 key 1000 항목을 삽입하면 free_head가 가리키는 slot 0을 재사용함
  • 결과적으로 B-tree 안에 같은 slot을 가리키는 중복 인덱스가 생기며, IterMut이 같은 메모리에 대한 여러 &mut 참조를 만들 수 있어 unsound해짐

수정 방식과 성능 절충

  • B-tree를 내려갈 때 key뿐 아니라 index equality도 함께 확인하도록 바꿈
  • 알려진 index를 가진 key를 찾을 때 (key, index) 둘 다 비교하므로, 병적인 Ord가 Equal을 반환해도 (key = 2, index = 2)와 찾는 index 0의 비교는 index tie-breaker 때문에 Less가 됨
  • 이 검색이 성공하려면 저장된 index가 찾는 index와 실제로 같아야 함
  • tie-breaker는 잘못된 항목 매칭을 막지만 올바른 항목을 항상 찾게 해주지는 않음
  • B-tree는 key로 정렬되어 있고 tie-breaker는 index를 비교하므로 두 순서는 일반적으로 독립적임
  • tree search가 실패하면 사용자 코드를 호출하지 않는 linear scan으로 B-tree에서 해당 index를 제거함
  • 이 fallback은 제거 연산을 logarithmic time 대신 linear time으로 만들지만, buggy user code가 있어야만 도달하므로 수용 가능한 절충으로 다뤄짐

검증 계층

  • iddqd는 foundational data structure로 쓰이기 때문에 분석적 검토와 여러 실증적 검증을 함께 사용함
  • 모든 unsafe block과 unsafe pattern은 한 명에서 세 명의 Rust 작성자와 리뷰어가 분석함
  • 각 unsafe block 위에는 // SAFETY: 주석으로 reasoning을 남기고, Clippy의 undocumented_unsafe_blocks lint로 주석 존재를 확인함
  • example-based test는 맵을 만들고 연산을 수행한 뒤 결과를 확인하며, iddqd는 내부 unit test와 public API integration test를 갖고 있음
  • 이 테스트들은 doctest로도 존재해 문서 역할을 함께 함
  • 병적인 테스트는 buggy Ord와 다른 trait 구현을 공급함
  • CI에서는 regular test와 pathological test를 Miri 아래에서 실행해 여러 종류의 UB를 탐지함
  • 중복 인덱스가 없어야 한다는 불변식 같은 조건은 Miri 밖의 일반 테스트 환경에서도 확인할 수 있음

모델 기반 테스트와 fault injection

  • iddqd는 두 계층의 randomized testing을 사용함: 올바른 oracle과 비교하는 model-based testing, 그리고 그 위의 fault injection
  • model-based testing 또는 stateful property-based testing은 무작위 연산 시퀀스를 타입 인스턴스에 적용하고, 결과를 올바르다고 알려진 oracle과 비교함
  • iddqd는 비효율적이지만 명확하게 올바른 NaiveMap oracle을 기준으로 광범위한 model-based test를 실행함
  • fault injection은 user code에 버그를 무작위로 넣는 방식이며, iddqd에서는 panic safety가 특히 유효한 축이었음
  • user code가 연산 중간에 panic하더라도 맵의 불변식이 깨지면 안 됨
  • 각 맵 연산에 무작위 panic countdown을 붙이고, user code 호출마다 countdown을 1씩 줄이다가 0이 되면 panic하게 해 무작위 panic safety testing을 수행함
  • 이 방식은 iddqd에서 미묘한 버그 여러 개를 찾았고, 일부는 unsoundness로 이어졌음
  • model-based test는 각 연산 뒤에 no-duplicate-index 같은 내부 불변식도 검증함
  • model-based test는 Miri 아래에서 실행하기에는 너무 느려서, soundness와 correctness가 의존하는 불변식을 별도로 확인함

LLM 적대적 리뷰와 형식 기법

  • current-generation frontier model은 맵을 손상시키는 병적인 user code 구현을 여러 개 찾아냄
  • 한 notable case에서는 custom allocator가 panic하고 unwind할 때 맵 불변식이 깨지는 경로를 LLM이 구성함
  • 이는 기존 panic safety test가 다루던 Ord 구현 같은 일반 user code panic과 다른 panic safety 문제였음
  • LLM은 그럴듯하지만 틀린 soundness claim도 만들 수 있으므로, Miri를 oracle로 쓰는 red-green TDD가 방어책이 됨
  • soundness bug에서는 먼저 Miri 아래에서 UB를 보이는 테스트를 만들고, 수정 뒤 같은 테스트가 통과하는지 다시 확인함
  • Kani 같은 model checker로 맵 불변식을 증명하는 접근은 iddqd가 너무 복잡해 필요한 proof가 도구가 감당하기 어려운 수준으로 커짐
  • Creusot은 Rust 코드가 panic과 다른 오류에서 자유롭다는 점을 증명하는 데 도움을 줄 수 있지만, user code가 panic하거나 잘못 동작해도 유지되어야 하는 불변식은 현 시점에서 증명하지 못함
  • NaiveMap은 iddqd에 가장 가까운 specification 역할을 하며, CI에서 model-based test를 수천 번 실행해 구현이 specification과 맞는지에 대한 높은 신뢰를 얻음
  • cargo-anneal은 unsafe Rust 옆 doc comment에 Lean soundness proof를 넣을 수 있게 하는 개발 중 도구로 관심 대상임
  • iddqd는 명확한 불변식과 제한적이지만 사소하지 않은 범위를 갖고 있어 형식 검증 도구의 benchmark 후보가 됨

결론

  • unsafe generic Rust는 임의의 trait 구현과 적대적 구현까지 고려해 각 불변식을 유지해야 하므로 극히 어렵다
  • iddqd의 버그는 병적인 Ord 구현이 맵을 속여 같은 메모리에 대한 mutable alias를 만들 수 있음을 보여줌
  • 단일 기법만으로 모든 버그를 잡을 수 없으므로, 사람의 line-by-line unsafe reasoning, example-based test, pathological test, randomized test, frontier model adversarial review를 함께 사용함
  • Oxide는 foundational infrastructure에서 이런 수준의 엄격함이 정당하다고 봄

함께 보면 좋은 글 β

GN⁺   [-]
Lobste.rs 의견들

  • 내가 제대로 이해했다면(이동 중이라 폰으로 봄), 이건 래퍼 타입과 HashMap/BTreeMap 대신 HashSet/BTreeSet을 쓰면 풀 수 있어 보임
    래퍼 타입이 꼭 필요하진 않지만, 안전성과 이후 유지보수를 생각하면 좋은 선택임
    필요한 건 객체를 감싸는 0 크기 래퍼뿐이고, 관심 있는 필드만 보는 커스텀 PartialEq/Hash 구현을 넣으면 됨. 전체 값을 만들지 않고 검색하려면 값 타입에 대해 AsRef를 구현하는 두 번째 타입을 만들 수 있음
    이 방식은 unsafe 없이 기존 HashSet/BTreeSet 인터페이스를 그대로 재사용하는 방법임. 값/키 타입을 감싸는 대신, 이런 동작을 대신 해주는 새 HashSet/BTreeSet 래퍼를 만들 수도 있음

    • 여기서 키는 레코드 타입의 필드와 하위 필드를 임의로 조합한 것이고, GAT로 표현됨. 또 정수 인덱스/슬랩 패턴은 다중 인덱스 맵으로도 자연스럽게 일반화됨
      Entry API, 가변 접근/반복 같은 것도 들어 있음. iddqd 안에서는 가변성을 꽤 조심스럽게 다루며, 일부 위치에서는 내부 가변성을 허용하려고 원자적 값을 사용함. 이런 처리는 인덱스 간접 참조 없이는 꽤 어려웠을 것임

  • iddqd를 형식 검증하려면 처음엔 Kani 같은 모델 검사기로 맵이 내부 불변식을 깨지 않는지 증명하려고 할 것 같음. 그런데 iddqd는 Kani가 다루기엔 조금 복잡하고, 필요한 증명이 도구가 감당하기 어려울 만큼 커진다는 대목이 궁금함
    이 부분을 더 자세히 공유해줄 수 있을까? 알고리즘의 계산 복잡도가 최악 사례로 퇴화한다는 뜻인지 궁금함
    전반적으로 형식 기법 사례 연구로 흥미롭고, 이 부분을 다뤄줘서 좋았음. 기존 형식 검증 도구라면 대규모 프로젝트에서의 성공 사례를 보면 적어도 자료구조의 정확성 정도는 증명할 수 있으리라 순진하게 생각할 수 있는데, 실제로는 자료구조마다 난이도가 다르고, Rust처럼 무제한 별칭을 허용하는 언어보다 증명에 유리하다고 여겨지는 언어에서도 실무적으로는 쉽지 않다는 점이 드러남
    약간 주제에서 벗어나지만, 다이어그램은 어떻게 만들었는지도 궁금함. 일회성 스크립트를 짰는지, Oxide 블로그/웹사이트 디자인에 맞춘 특수 제작물처럼 보이고 범용 도구 같진 않음

    • 글 하단에 “Diagrams courtesy Ben Leonard.”라고 되어 있고, Ben Leonard는 Oxide의 디자이너임. 그래서 아마 수작업 다이어그램일 가능성이 있어 보임
    • 구체적이고 잘 동작하는 trait 구현을 대상으로 아주 기본적인 걸 증명하려 해도, CBMC가 CPU를 돌리면서 10분 이상 지나도 끝나지 않았음
      범위를 줄여보기도 했음. 예를 들어 hashbrown이 올바르다고 가정했지만, 그것도 크게 진전되지 않았음. 그쯤에서 거의 포기함. 잘 동작하는 trait 구현에 대해서는 iddqd가 맞다고 꽤 확신하고 있고, 내가 형식 기법에서 정말 관심 있었던 건 임의의, 잘못 동작하는 구현에 대해서도 성립하는 증명이었음
      다만 내가 Kani를 가장 잘 쓰는 사람은 아님. 당신이나 다른 누군가가 이걸 시도해보면 정말 좋겠음
      다이어그램은 먼저 Mermaid로 스케치를 만들었고, 그다음 훌륭한 디자이너 Ben Leonard가 우리 색상 팔레트와 테마에 맞춰 손으로 다이어그램으로 다듬었음

  • 객체를 그 객체의 필드 중 하나를 키로 삼아 인덱싱하는 필드 기반 맵 패턴은 C#에서도 항상 쓸 수 있으면 좋겠다고 느끼는 것임
    예전에 직접 간단한 걸 만들어보려 했지만 인터페이스가 아주 깔끔하진 않아서 접었음. 이 글을 보니 다시 한번 시도해보고 싶어짐

    • 맞음, 정말 유용한 패턴임. 회사에서 필요한 일 때문에 만들었지만, 이후에는 cargo-nextest 같은 프로덕션 코드베이스부터 개인용 프로젝트까지 온갖 곳에 쓰게 됨
      필드 하나만 키로 쓰는 게 가장 흔한 용례이긴 하지만, iddqd는 충분히 유연해서 필드, 하위 필드, 또는 필드에서 순수하고 저렴하게 계산 가능한 함수의 어떤 조합도 사용할 수 있음. 예를 들어 https://docs.rs/iddqd/latest/iddqd/ 에서 ArtifactKey를 검색해보면 됨(Rust 문법에 익숙하지 않다면 양해 바람)
      iddqd를 설계할 때는 사용자가 Rust 타입 시스템의 모든 힘을 쓸 수 있어야 한다고 강하게 생각했음. 라이브러리 작성자인 내가 얼마나 많은 우회로를 거쳐야 하든 상관없이 말임. iddqd가 사용자들, 특히 내 동료들이 쓰기에 즐거운 라이브러리가 되길 정말 원했음
답변달기
GeekBots 가 이제 오픈소스 기반 사내 협업도구 Mattermost 도 지원합니다. 긱뉴스를 사용중인 팀 채널에서 받아보세요.