Rust의 core 및 alloc 크레이트를 Coq로 번역하여 형식 검증

 (formal.land)
1P by GN⁺ | ★ favorite | 댓글 1개
  • Rust 프로그램을 Coq로 옮기는 coq-of-rust가 표준 라이브러리의 core·alloc 크레이트까지 다루기 시작하면서, primitive 함수별 Coq 정의를 손으로 작성하던 부담을 줄임
  • 두 크레이트는 unsafe와 고급 Rust 코드가 많은 대형 코드베이스라, 자동 번역 결과를 컴파일·검증 가능한 단위로 다루는 것이 핵심 과제가 됨
  • 출력물을 입력 Rust 파일 단위로 나누자 alloc은 54개 파일 171,783줄, core는 190개 파일 592,065줄이 됐고, 병렬 컴파일과 디버깅이 쉬워짐
  • impl 블록의 모듈 이름 충돌은 where 절 정보를 포함해 완화했지만, 현재 Coq에서 컴파일되지 않는 파일은 전체의 4%로 남아 있음
  • Option::unwrap_or_default 예시는 자동 번역 정의와 단순 함수형 정의의 동등성을 증명해 쓰는 방식으로, 자동화 신뢰와 증명 시점 검사가 함께 필요함

Rust 표준 라이브러리 primitive 처리

  • Formal Land는 Rust 프로그램을 Coq 형식 증명 시스템으로 번역하는 coq-of-rust를 개발 중임
  • 기존에는 Rust 표준 라이브러리의 primitive 구성요소를 다루기 위해 함수마다 동작을 나타내는 Coq 정의를 별도로 만들어야 했음
  • 이 부담을 줄이기 위해 Rust의 core와 alloc 크레이트를 coq-of-rust로 번역함
  • 번역 결과는 다음 경로에서 확인할 수 있음

초기 번역 실행 결과

  • coq-of-rust를 alloc과 core에 처음 실행하자, 각 크레이트 전체에 해당하는 수십만 줄 규모의 Coq 파일 2개가 생성됨
  • 큰 코드베이스에서도 도구가 실행된다는 점은 확인됐지만, 생성된 Coq 코드는 바로 컴파일되지 않았음
  • 오류는 드물게 나타났지만 몇천 줄마다 하나 정도 발생하는 수준이었음
  • cloc 기준 입력 Rust 코드 규모는 다음과 같음
    • alloc: Rust 코드 26,299줄
    • core: Rust 코드 54,192줄
  • 번역 과정에서 매크로 확장이 일어나므로 실제 번역 대상은 원본 줄 수보다 더 큼

생성된 Coq 코드 분할

  • 가장 큰 변경은 coq-of-rust 출력물을 입력 Rust 파일 하나당 Coq 파일 하나로 나눈 것임
  • 이 분할은 번역이 정의 순서에 둔감하고 context-free이기 때문에 가능했음
  • Rust 파일 사이에는 보통 순환 의존성이 있고 Coq에서는 이를 허용하지 않지만, 이 번역 방식에서는 파일 단위 분리가 가능함
  • 분할 후 출력 규모는 다음과 같음
    • alloc: Coq 파일 54개, Coq 코드 171,783줄
    • core: Coq 파일 190개, Coq 코드 592,065줄
  • 파일을 나누면서 생성 코드 탐색과 유지보수가 쉬워짐
    • 컴파일을 병렬화하기 쉬움
    • 한 파일씩 집중해 디버깅할 수 있음
    • 컴파일되지 않는 파일을 제외하기 쉬움
    • 단일 파일 diff를 추적하기 쉬워짐

모듈 이름 충돌 수정과 남은 파일

  • 일부 버그는 impl 블록의 모듈 이름 충돌에서 발생했음
  • 해결 방식은 모듈 이름에 더 많은 정보를 넣어 고유성을 높이는 것이었음
    • 기존에는 빠져 있던 where 절 정보를 포함함
    • 예를 들어 Mapping<K, V>에 대한 Default trait 구현에서는 K와 V가 모두 Default를 구현해야 한다는 조건이 모듈 이름에 반영됨
  • 현재 Coq에서 컴파일되지 않는 파일은 다음과 같음
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • 이는 전체 파일의 4% 에 해당함
  • 컴파일되는 파일 안에도 아직 처리하지 못한 Rust 구성요소가 공리화되어 있어, 이 비율만으로 미지원 범위 전체를 판단하기는 어려움

Option::unwrap_or_default 번역 예시

  • Rust의 Option::unwrap_or_default는 Some(x)이면 x를 반환하고, None이면 T::default()를 호출함
  • coq-of-rust는 이를 monadic 형태의 Coq 정의로 번역함
    • 입력 인자와 타입을 매칭함
    • Some 분기에서는 tuple field를 가져와 복사함
    • None 분기에서는 core::default::Default trait의 default 메서드를 호출함
  • 실제 검증에서는 자동 생성 정의 대신 더 단순한 함수형 정의를 사용함
    • None이면 core.simulations.default.Default.default를 반환함
    • Some x이면 x를 반환함
  • 자동 생성 정의와 단순 정의가 동등하다는 증명은 CoqOfRust/core/proofs/option.v에 있음
  • 원본 Rust 코드가 바뀌면 이 증명을 통해 변화가 포착됨
  • core 라이브러리 번역은 자동으로 이뤄졌기 때문에 손으로 작성한 정의보다 생성 정의를 더 신뢰할 수 있음
  • 다만 coq-of-rust에도 실수나 불완전성이 있을 수 있어, 증명 시점에 코드가 타당한지 확인해야 함

남은 과제

  • Rust 프로그램 검증에서 표준 라이브러리 형식화에 대한 신뢰가 높아짐
  • 다음 목표는 여전히 지루한 증명 과정 단순화임
  • 특히 시뮬레이션이 원본 Rust 코드와 동등함을 보이려면 다음 작업이 필요함
    • 이름 해석
    • 고수준 타입 도입
    • 부작용 제거
  • 이 단계들을 나눠 다루는 것이 앞으로의 개선 방향임

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 정말 인상적임
    이런 자동 번역은 신뢰의 대상을 도구로 옮김. coq-of-rust 자체는 Coq가 아니라 Rust로 작성되어 있어서 재귀적인 구조가 꽤 놀랍지만, David A. Wheeler의 “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0]처럼 두 번째 컴파일러로 Ken Thompson의 Trusting Trusting 공격을 우회하는 방식에 CompCert식 접근을 섞으면 정확성 증명이 가능해 보임
    검증하려면 coq-of-rust로 coq-of-rust 번역기를 Rust에서 Coq로 변환하고, 그 번역은 Rust로 수행됐으니 신뢰하지 않더라도 Coq 안에서 원하는 정확성 성질, 특히 Rust 프로그램을 Coq로 번역할 때 의미론을 보존한다는 점을 증명하면 됨
    논문처럼 생성된 정의보다 더 함수형인 정의로 증명하는 편이 쉬울 가능성이 높으니, 표준 라이브러리에서 하듯 정의 간 동치성을 증명하는 과정을 거치면 됨. 현재 coq-of-rust 번역기, 특히 lib/ [1]가 Rust 6,350줄이라면 Coq로 전체 번역기를 작성하고 생성된 것과 동치임을 증명하는 것도 현실적으로 보임
    그다음 증명된 Coq판 coq-of-rust 번역기를 Rust로 된 coq-of-rust 소스에 실행하면, 출력되는 Coq 정의가 처음에 사용한 Rust판 coq-of-rust 번역기의 출력과 일치해야 함
    여담으로 이런 작업에 산업 자금이 붙는 건 보기 좋음. 암호화폐에는 냉소적인 편이지만, 그쪽의 정확성 요구가 Rust, Coq, 아는 석사과정 학생들 지원 같은 관심 분야의 개선을 밀어붙이는 건 사실임
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • 작성자 중 한 명인데, 실제로 그런 절차는 coq-of-rust 검증에 좋은 방법이 될 수 있음
      다만 코드 자체는 짧아도 입력 Rust 코드를 파싱하고 타입 검사하는 데 Rust 컴파일러에 의존함. 따라서 그 부분도 검증하거나, 적어도 증명 없이 형식 명세는 해야 함. rustc의 API가 꽤 크고 불안정하다는 점이 걸림돌이지만, 그래도 신뢰도를 높이는 한 방법은 될 수 있음
    • 예전에 SPARK Ada로 일하던 때가 떠오름. 지원되는 Ada 대상이 없는 프로젝트, 특히 아주 작은 장치에서는 Ada를 C로 변환한 뒤 해당 대상으로 컴파일하곤 했고, 덕분에 SPARK 쪽에서 여러 형태의 정적 분석을 수행할 수 있었음
      물론 출력물이나 변환기를 검증해야 하는 문제가 생겼지만, 결과 C 코드는 검증 목적상 꽤 읽기 쉽고 스타일도 제한적이었으며 도구에 대한 신뢰도도 높았음. SPARK 정적 분석은 전체 검증·확인 과정의 일부였고, 테스트와 다른 활동이 추가적인 신뢰층을 제공했음. 전체적으로는 꽤 잘 작동한 접근이었음
    • 암호화폐가 이런 일을 돕는 이유는 정확성 제약도 있지만, 컴퓨터 과학에 관심 있는 사람들에게 많은 부가 이전됐다는 점도 큼
      그들이 그 돈을 컴퓨터 과학 연구에 쓰는 건 자신들에게 이익이 되기 때문만이 아니라, 취미와 맞닿은 자선 활동이기도 하기 때문임
    • 그 접근이 바이너리를 만드는 데 쓰이는 Rust 컴파일러가 악성 페이로드를 주입하는 걸 어떻게 막는지는 잘 모르겠음. A를 B로 빌드하고 B를 A로 빌드한 뒤 바이너리를 비교할 수는 있겠지만
      다른 접근은 증명 운반 코드임. Rust 컴파일러가 실행 파일 출력이 입력 소스 코드의 의미론과 일치한다는 Coq 증명을 함께 내보내는 방식임
      물론 Rust의 부분집합 컴파일러를, 예컨대 빌림 검사기나 최적화 없이 특정 아키텍처의 기계어로 작성한 뒤 거기서 모든 걸 부트스트랩할 수도 있음

  • Coq 같은 반자동 연역 증명 시스템으로 처음부터 끝까지 검증된 프로그램의 크기는 작음. 라이브러리는 코드가 서로 상호작용하는 정도가 낮아 더 쉬울 수 있지만, 일반 프로그램은 그렇지 않음
    실제로 이런 방식으로 검증 가능한 프로그램의 크기 증가는 전체 프로그램 평균 크기 증가보다 느렸음. 건전한 소프트웨어 검증, 즉 명세와 100% 일치함을 보이는 일은 핵심 알고리즘의 정확성 증명 같은 곳에서 분명 쓸모가 있지만 잘 확장되지 않음
    그래서 연구가 비건전한 방법으로 옮겨간 측면이 있음. 100% 보장의 비용이 99.9999% 보장의 10배가 될 수 있고, 그 확률 차이는 소프트웨어 외 고장 확률보다 작아질 수도 있음. 물리 시스템은 애초에 명세와 일치함을 증명할 수 없고, 명세 자체가 현실과 충분히 맞지 않을 확률도 있음

    • 핵심은 표준 라이브러리의 unsafe 부분과 Rust의 안전성 보장을 증명하면, 표준 라이브러리만 사용하는 모든 안전한 Rust 코드의 메모리 안전성, 데이터 경합 없음 등을 전이적으로 증명할 수 있다는 것임
      unsafe 코드만 정확하다고 증명하는 것은 모든 Rust 코드를 증명하는 것보다 훨씬 적은 노력으로 가능함. 이는 Rust의 안전성 보장을 이야기할 때 흔히 나오는 “unsafe 코드는 어떡하냐”는 비판에 대한 답이 됨. Rust 타입 시스템만으로 다루기엔 충분히 강력하지 않은 빈틈을 Coq 같은 더 강한 시스템으로 메울 수 있음

  • 이런 시도에서 잘 이해가 안 되는 부분이 있음. 코드를 Coq로 수동 또는 반수동 변환해야 한다면, 그 과정에서 실수할 가능성이 형식 검증으로 얻는 이득보다 훨씬 큰 것 아닌가?
    다시 말해 우리가 증명한 것이 여전히 원본 코드에 유효하다는 걸 어떻게 알 수 있나?

    • 알 수 없음. 결국 하드웨어, 컴파일러, 명세, Coq의 신뢰 커널 등 무언가를 신뢰해야 함
      형식 검증은 버그 가능성을 완전히 없애는 것처럼 논의되는 경우가 많지만, 실제로는 버그 가능성을 훨씬 낮추는 데 가깝다. 그렇더라도 Rust와 Coq 사이의 자동 번역은 신뢰해야 하는 것의 복잡도를 크게 줄이므로, 수동 번역보다 선호되어야 함
    • 맞는 한계이지만, 그렇게 나쁜 한계는 아님
      많은 경우 번역의 버그는 단순히 증명을 불가능하게 만듦. 그러면 누군가 왜 증명이 통과하지 않는지 조사하다가 번역 버그를 찾게 됨
      진짜 문제는 번역 버그가 원본 코드의 버그를 정확히 상쇄하는 경우임. 체계적인 위험이 없다면 두 버그가 이런 식으로 서로를 지우는 일은 꽤 가능성이 낮음
    • 코드는 coq-of-rust로 자동 번역됨. 번역에서 문제가 발견되면 coq-of-rust 도구에서 한 번 고치면 되고, 모든 번역 결과가 갱신됨

  • 관심 있는 독자에게: 이 블로그 글은 같은 블로그의 다른 글들보다 암호화폐 관련 내용이 덜 직접적이라 제출했지만, 그곳에는 기술적으로 더 흥미로운 글이 많음
    특히 최근 두 글은 같은 접근을 Rust가 아니라 Python에 적용하는 내용을 다룸

  • 예전에 형식 검증된 C 컴파일러에서 퍼저가 버그를 찾았다는 강의 [1]가 기억남. 형식 검증이 프런트엔드와 백엔드를 포함하지 않았기 때문이었음
    Coq 자체나 번역을 얼마나 신뢰할 수 있느냐는 질문이 나오는 것도 알고, Rust 업데이트와 어떻게 동기화될지도 의문이지만, 완벽한 형식 검증조차 처음부터 끝까지 100% 정확성을 뜻하지는 않음
    [1] https://youtu.be/Ux0YnVEaI6A

  • 형식 검증 전문가는 전혀 아니지만, Rust의 기본 라이브러리가 형식 검증되고 unsafe 코드를 쓰지 않는다면, 형식 검증된 라이브러리를 사용하는 모든 Rust 프로그램은 메모리 처리 측면에서 사실상 형식 검증 수준의 품질을 갖게 되는 건가?

    • Rust의 안전성은 버그와는 거의 관련이 없음
      Rust에는 자체적인 “safe” 정의가 있고, 이는 메모리 안전성의 부분집합이라고 볼 수 있음. 완전히 안전한 Rust 코드에서도 데이터 경합, 교착 상태, 메모리 고갈 등이 가능하고, 논리 오류는 말할 것도 없음
    • 어느 정도는 그게 꿈이라고 생각하지만, 단서가 많고 몇 가지가 맞아떨어져야 함
      첫째, unsafe Rust의 의미론을 형식화해야 함. Ralf Jung의 선구적인 RustBelt[1] 작업이 큰 진전이었지만 아직 완전하지 않음. 특히 포인터 출처가 까다로운 요소로 드러나고 있음
      둘째, 그 일부로 빌림 검사기의 형식 모델이 필요함. Stacked borrows[2]는 좋은 시도였지만 결함이 있고, Tree borrows[3]가 이를 고칠 수도 있으나 더 정교한 무언가가 나올 가능성도 있음
      셋째, 형식적 메모리 모델이 필요함. 이는 주로 원자적 연산과 동기화의 동작에 관한 것이며, 따라서 Arc 같은 표준 라이브러리 구성 요소에 매우 중요함. Rust의 메모리 모델은 C++와 비슷해야 하고 상호 운용되어야 한다는 점은 널리 받아들여지지만, “out of thin air” 문제와 seqlock 같은 빠진 기능이 남아 있음. Linux 커널이 여전히 자체 모델을 쓰는 이유 중 하나임
      넷째, 안전성 보장이 잘 합성된다는 증명이 필요함. 특히 unsafe Rust로 작성된 건전한 코드와 safe Rust 코드가 합성돼도 안전성 보장이 유지되어야 함. 지금까지 좋은 결과가 있지만 전체 시스템에 대해 증명되어야 함
      다섯째, 그런 증명이 모든 코드에 대해 성립하려면 Rust에 남은 건전성 버그[1]를 모두 닫아야 함. 이런 문제 상당수는 이론적이거나 적대적 코드[5]에서나 실제로 중요해서 진척이 느림
      이 모든 것이 끝나도 여전히 부분적인 보장일 뿐임. 시스템과 접속하는 표면의 엄청난 부분이 unsafe 코드에 기반함. 순수 계산만 한다면 몰라도, 예를 들어 그래픽 UI를 만든다면 여전히 잘못될 수 있는 것이 매우 많음
      그래도 실용적인 전진 경로는 있고, 그것은 오늘날의 취약점투성이 시스템이라는 일반적인 상태보다 훨씬 나은 상황으로 이어짐
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Rust 전문가는 아니지만 core 코드에 unsafe가 꽤 많아 보임. 그럴 만도 함
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      여기서 제시된 방식의 Coq가 모든 unsafe 호출을 검증할 수 있다고는 생각하지 않음

  • 이 접근이 Aeneas나 RustHornBelt와 어떻게 다른지 비교할 수 있나? 포인터와 가변 빌림은 어떻게 다루나?

    • RustHornBelt가 어떻게 작동하는지는 모름. 우리는 안전한 코드에 집중하고 있지만, unsafe 블록도 “최선의 노력”으로 번역은 생성함
      Aeneas와 비교하면 목표는 매우 비슷함. 둘 다 대화형 정리 증명기로 Rust 프로그램을 검증하려는 것이기 때문임. 다만 coq-of-rust에서는 증명 대상이 되는 순수 함수형 버전의 코드를 수작업으로 작성하거나, 반복적인 작업이라 GitHub Copilot의 도움을 받아 작성하고, 이를 자동 번역 결과와 동치임을 증명함. Aeneas는 함수형 버전을 직접 생성하는 것을 목표로 함
      포인터는 모두 가변 포인터, 즉 * 타입인 것처럼 다룸. Rust의 빌림 검사기 정보는 사용하지 않으며, 이 덕분에 번역은 단순해지지만 그 비용을 증명 시점에 치름
      증명에서 포인터를 추론하기 위해 사용자가 메모리가 어떻게 쓰일지에 따라 설계할 수 있는 맞춤 할당자를 제공하게 함. 예를 들어 프로그램이 전역 가변 변수 세 개를 사용한다면, 메모리를 세 항목을 가진 레코드로 둘 수 있음. 이 항목들은 아직 할당되지 않은 상태를 나타내기 위해 처음에는 None임
      이 기법이 얼마나 확장될지는 아직 모르지만, 적어도 지금은 분리 논리 추론을 피할 수 있음. 검증하려는 대부분의 프로그램, 특히 애플리케이션 쪽은 비교적 “단순한” 메모리 규율을 갖기를 기대하고 있음

  • 형식 검증 명세 작성은 더 복잡한 속성 기반 테스트를 쓰는 것과 비슷한가? 복잡하지 않은 프로그램을 넘어가면 속성 기반 테스트 작성도 꽤 어렵고 시간이 많이 들던데

    • 비슷하지만 항상 같지는 않음. 속성 기반 테스트는 보통 시스템의 인터페이스, 함수나 프로시저 수준 또는 그보다 높은 수준에서 입력의 설명을 지정하고 출력이 어떤 속성 또는 속성 집합을 만족하는지 테스트함
      같은 수준에서 형식 검증을 할 때도 꽤 비슷해 보일 수 있음. 하지만 형식 검증 도구는 더 깊게 들어갈 수 있음. 예를 들어 계산 내부의 시스템 상태에 대해 “이 반복문 불변식이 있는데, 모든 반복에서 실제로 유지됨을 증명할 수 있나?” 또는 “이 계산 중 어떤 중간 계산에서도 언더플로/오버플로가 절대 발생하지 않음을 증명할 수 있나?” 같은 질문에 답할 수 있음
      전자는 반복문 핵심을 별도 프로시저로 빼고 많은 중간 상태로 실행해 불변식 속성을 테스트하면 속성 기반 테스트로도 가능함. 후자는 프로그램을 줄 단위로 따로 실행 가능하게 만들 정도로 심하게 쪼개지 않는 한 훨씬 어려움

  • 이런 게 가능하다는 것도 몰랐음
    이런 시도가 커널 도입의 핵심 부분에서 Rust 채택을 빠르게 만들 수 있을지 궁금함

  • 누가 “검증” 개념을 아주 쉽게 설명해줄 수 있나? 왜 이 목적만을 위해 Coq 같은 언어 전체가 존재하는지, 그리고 더 넓은 사회에 어떤 실질적 의미가 있는지 궁금함

답변달기