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

21 hours ago 4
  • 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 같은 우회 없이 다룰 수 있음
  • BiHashMapTriHashMap은 항목 하나를 두 개 또는 세 개의 키로 각각 인덱싱해, 여러 맵을 손으로 유지하는 일반적 패턴을 피하게 함
  • 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에서 이런 수준의 엄격함이 정당하다고 봄
Read Entire Article