Rust 검증 기술, 저수준 시스템 코드에 적용

 (github.com/verus-lang)
1P by GN⁺ | ★ favorite | 댓글 1개
  • Verus는 Rust로 작성한 코드의 정확성을 검증하는 도구로, 개발자가 코드가 해야 할 일을 명세하면 실행 가능한 Rust 코드가 모든 가능한 실행에서 그 명세를 만족하는지 정적으로 확인함
  • 런타임 검사를 추가하지 않고 강력한 솔버를 사용해 코드가 올바르다는 것을 증명하는 방식이며, 현재는 Rust의 일부만 지원함
  • 일부 경우에는 표준 Rust 타입 시스템을 넘어 raw pointer를 조작하는 코드의 정확성까지 정적으로 검사할 수 있음
  • 프로젝트는 활발히 개발 중이며 기능이 깨져 있거나 빠져 있을 수 있고 문서도 아직 완전하지 않아, 사용자는 Zulip에서 도움을 요청할 준비가 필요함
  • 브라우저용 Verus Playground, 설치 안내, 튜토리얼과 레퍼런스, 표준 라이브러리 API 문서, 동시성 코드 검증 가이드, 예제와 테스트가 학습·실험 경로로 제공됨

Verus가 검증하는 것

  • Verus는 Rust 코드의 정확성을 검증하는 도구임
  • 개발자는 코드가 수행해야 할 동작을 명세로 작성함
  • Verus는 실행 가능한 Rust 코드가 가능한 모든 실행에서 그 명세를 항상 만족하는지 정적으로 검사함
  • 런타임 검사를 추가하는 대신, 솔버를 사용해 코드가 올바르다는 사실을 증명함
  • 현재 지원 범위는 Rust의 부분집합이며, 지원 범위를 넓히는 작업이 진행 중임
  • 일부 경우에는 표준 Rust 타입 시스템을 넘어, 예를 들어 raw pointer를 조작하는 코드의 정확성을 정적으로 확인할 수 있음

개발 상태와 사용 시 주의점

  • Verus는 활발히 개발 중인 프로젝트임
  • 기능이 깨져 있거나 빠져 있을 수 있음
  • 문서는 아직 완전하지 않음
  • Verus를 시도하려면 Zulip에서 도움을 요청할 준비가 필요함
  • Verus 커뮤니티는 여러 연구 논문을 발표했으며, 산업계와 학계의 다양한 프로젝트가 Verus를 사용하고 있음
  • 관련 목록은 publications and projects 페이지에서 확인할 수 있음

시작 방법과 개발 도구

  • 브라우저에서 Verus를 시도하려면 Verus Playground를 사용할 수 있음
  • 더 본격적인 개발을 위해서는 설치 안내를 따라야 함
  • 학습은 Tutorial and reference에서 시작할 수 있음
  • Verus 코드를 위한 자동 포매터 verusfmt도 지원함

문서와 학습 자료

예제와 커뮤니티 참여

  • Verus 사용 예시는 문서 외에도 여러 출발점을 제공함
    • Publications and projects: Verus를 사용하는 출판물과 프로젝트
    • Videos, slides, and exercises: 하루짜리 Verus 튜토리얼의 영상, 슬라이드, 연습문제
    • Standalone examples: 작고 구체적인 작업에서 Verus를 사용하는 독립 예제
    • Small and medium-sized examples: 다양한 Verus 기능을 보여주는 예제
    • Unit tests: Verus 문법과 기능 예시가 들어 있는 테스트
  • 이슈 보고와 토론은 GitHub 또는 Zulip에서 진행할 수 있음
  • 기능 요청과 열린 대화는 GitHub discussions를 사용하고, 기존 기능의 실행 가능한 버그는 GitHub issues에 두는 운영 방식을 사용함
  • 코드 기여를 원하면 Contributing to Verus의 안내를 참고할 수 있음

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • Verus로 형식 검증된 Kubernetes 컨트롤러를 작성해 봤음
    기본적으로 “언젠가는 컨트롤러가 클러스터를 요청된 목표 상태로 조정한다” 같은 활성 속성을 증명할 수 있음
    다만 목표 상태가 빠르게 바뀌는 경우, 비동기성, 실패 등을 생각하면 “정확함”을 명세하는 것 자체에도 미묘한 부분이 많음
    코드: https://github.com/vmware-research/verifiable-controllers/, 관련 논문은 OSDI 2024에 실릴 예정

    • 단위 테스트보다 더 해주는 게 무엇인지 궁금함

  • Verus로 가는 작은 디딤돌로 Rust의 debug_assert를 전제조건과 사후조건에 붙여볼 수 있음
    Rust 컴파일러는 기본적으로 프로덕션 빌드에서 이를 제거함
    Verus 튜토리얼의 검증 예제는 requires와 ensures로 입력 범위와 결과 조건을 적고, 런타임 검사 버전은 debug_assert(-16 <= x1), debug_assert(x8 == 8 * x1)처럼 같은 조건을 실행 중 확인하는 식임

    • 현재 Verus 문법의 한 가지 문제는 전체 코드를 프로시저 매크로로 감싸야 한다는 점임
      Creusot 같은 다른 Rust 증명/검증/계약식 설계 도구는 속성 기반 문법을 쓰는데, 일반적으로 더 가볍고 Rust답게 느껴짐
      향후 Verus 릴리스에서 이런 방식도 가능해지면 좋겠음
    • 이런 식의 assert를 더 많은 사람이 썼으면 좋겠음
      문서화 도구로 훌륭하고, 타입 시스템과 테스트를 아주 잘 보완함
    • "contracts" 크레이트도 써볼 수 있음: https://docs.rs/contracts/latest/contracts/
    • Verus 예제는 내가 Clojure 코드를 쓰는 방식과 비슷함
      대부분 함수에 사전조건과 사후조건을 붙이고, JVM에는 프로덕션 빌드에서 이를 쉽게 제거할 수 있는 플래그가 있음

  • 실제 컴퓨터과학 경험이 많지 않은 입장에서 궁금한데, README의 “코드의 정확성을 검증한다”에서 검증과 다른 곳에서 말하는 “증명”은 무엇이 다른가?
    컴퓨터과학/수학 배경이 강하지 않은 현업 프로그래머가 코드에 대해 “증명”을 배우기 좋은 자료도 궁금함
    추가로 영지식 증명이 왜 그렇게 중요하고 관련성이 큰지도 잘 모르겠음. 예를 들어 x.com/ZorpZK 같은 얘기를 들었는데 왜 멋진지 이해가 안 됨

    • 코드 검증과 함수형 프로그래밍을 함께 배우기 좋은 자료로 Software Foundations가 있음: https://softwarefoundations.cis.upenn.edu
      다만 Verus와 Software Foundations에서 쓰는 Coq는 접근 방식이 다름
      Verus는 SMT 해결기라는 자동 제약 풀이 시스템으로 속성을 자동 증명하려 하고, Coq는 훨씬 더 많은 부분을 수동으로 증명해야 하며 자동화는 제한적임
      둘 다 장단점이 있고, 자동화는 잘될 때는 좋지만 안 될 때는 답답함
      영지식 증명은 좀 다른 분야로 보는 편이 맞고, 형식 검증/증명 일을 하는 많은 사람도 영지식 증명은 건드리지 않음. 암호학 원시 요소로 생각하는 게 더 좋음
    • 여기서는 검증과 증명을 동의어로 쓰고 있고, 첫 문단 뒤쪽에서도 그렇게 분명해짐
      영지식 증명은 오버헤드가 크고 이른바 “킬러 앱”이 부족해서 실용적 용도나 중요성, 관련성은 아직 크지 않지만, 개념적으로는 흥미로움
    • 이 맥락에서는 “검증”과 “증명”이 같음
      학습 자료는 나도 있었으면 좋겠음. Dafny 문서는 꽤 좋지만, 형식 소프트웨어 검증은 컴퓨터과학/수학 박사가 아닌 보통 프로그래머가 쓰기 좋은 단계까지는 아직 아닌 듯함
      예제만 보면 비교적 쉬워 보이지만 곧 “증명할 수 없음”에 부딪히고, 왜 그런지에 대한 답은 작성자만 알 법한 깊은 구현 세부사항으로 들어가곤 함
    • 내가 알기로 영지식 증명은 무엇을 알고 있다는 사실을, 그 내용을 드러내지 않고 증명할 수 있게 해줌
      예를 들어 비밀번호를 서버에 보내지 않고도 비밀번호를 알고 있음을 검증할 수 있어, 악성 서버나 중간자 공격자가 비밀번호를 훔쳐보기 어려움
      신원 확인에도 더 나은 선택지를 줄 수 있음. 정부 발급 신분증을 가지고 있음을 증명하되 문서 자체를 서버에 넘기지 않아도 되므로, “최대 2년/3년/6개월 보관”하다가 결국 유출되는 일을 줄일 수 있음
    • “현업 프로그래머가 코드에 대해 증명한다”는 표현은 아직 모순에 가깝다고 봄
      코드에 대한 증명은 아직 현업 프로그래머가 하는 일이 아님
      Hoare 논리가 좋은 출발점이고, 입문 컴퓨터과학 수업에서도 가끔 가르침
      Coq는 학습 곡선이 가파르고, OCaml이나 비슷한 언어에 익숙하지 않으면 특히 더 어려움. Why3가 더 초보자 친화적일 수도 있음: https://www.why3.org
      증명과 검증은 같은 뜻일 수도 있지만, 증명은 더 상호작용적인 느낌이고 검증은 모델 검사나 주석이 붙은 프로그램의 SMT 풀이처럼 자동화될 수 있다는 느낌이 있음

  • 비슷한 프로젝트를 몰랐던 사람이라면, Dafny는 Rust로 컴파일할 수 있는 “검증 인식 프로그래밍 언어”임: https://github.com/dafny-lang/dafny

  • 정말 멋져 보임. 기존 코드베이스에 증명 추가를 어떻게 하는지에 대한 안내나 예제가 있으면 사람들에게 유용할 것 같음
    예를 들어 텍스트 상자 하나만 있는 최소 GUI 앱이 HTTP 요청으로 컴파일 시점에는 알 수 없고 신뢰할 수 없는 배열을 받아와 버블 정렬한 뒤 표시한다고 해보자
    버블 정렬에는 오프바이원 오류로 마지막 원소가 그대로 남는 식의 의도적 버그가 있고, 단위 테스트는 어쩌다 그 버그를 잡지 못함. 테스트가 불완전할까 걱정하는 것이 증명으로 가는 주된 동기가 될 수 있음
    그런 다음 단위 테스트를 증명으로 대체하면서 버그를 발견하고 고치는 과정을 보여주면 좋겠음
    증명 코드 자체를 자세히 설명할 필요는 없고, 증명된 수학 코드와 증명되지 않은 입출력 코드의 경계, 증명과 빌드에 쓰는 명령줄, 직접 만져볼 수 있는 zip 아카이브 같은 현실적인 세부사항에 초점을 맞추면 됨
    사실 표준 입력에서 읽고 표준 출력에 쓰는 정도만으로도 충분할 듯함

  • 주요 기여자 중 한 명이 Zürich Rust 밋업에서 Verus에 대해 훌륭한 발표를 했음: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    이 “ghost” 코드가 프로그램 안에 얼마나 깔끔하게 들어맞는지 인상적이었고, Ada가 조금 떠올랐음

  • Rust에도 C/C++, Common Lisp, Ada/SPARK2014 같은 표준이 이미 있는지 궁금함
    그런 게 없다면 Ada/SPARK2014용으로 개발된 검증 도구와 비교할 때 움직이는 목표물이 됨
    베어메탈부터 고무결성 안전 필수 애플리케이션까지 이어지는 Ada/SPARK2014의 유산도 무시하기 어려움

  • 이것과 Kani 사이에 어떤 관계가 있는지 궁금함. 서로 다르게 동작하나?
    https://github.com/model-checking/kani

    • 모델 검사기는 보통 제한된 수의 상태만 탐색하므로 버그 찾기에 효율적이고, 프로그램에 추가 주석이 필요 없는 경우도 많음
      Verus, Dafny, F* 그리고 내 VCC 같은 자동 SMT 기반 검증기는 거의 모든 함수와 루프에 주석을 달아야 하지만, 프로그램 정확성에 대해 더 넓은 보장을 제공함
      Coq나 Lean 같은 상호작용 증명기 기반 도구는 보통 사용자의 안내가 더 많이 필요하지만, 더 복잡한 속성까지 보장할 수 있음

  • Verus는 SPARK와 어떻게 비교되는지 궁금함
    같은 일반 부류의 검증기인가? Ada용 검증기가 아니라 Rust용 검증기라는 점 말고 Verus가 어떻게 다른가?

  • Verus를 잘 아는 사람이 Verus와 Lean4의 성능과 표현력 차이를 설명해줄 수 있으면 좋겠음
    Verus는 SMT 기반 검증 도구이고, Lean은 상호작용 증명기이면서 SMT 기반 도구이기도 하다고 이해하고 있음
    다만 형식 검증 분야에 대한 이해가 제한적이라, 소프트웨어 형식 기법을 잘 아는 사람의 견해가 궁금함

    • Lean은 Coq와 비슷함
      예를 들어 Coq의 “Software Foundations” 책처럼 C 코드에 대한 명제를 세우고 증명할 수는 있지만, Lean으로는 거의 아무도 하지 않는 듯하고 도구도 부족함
      Lean4로 프로그램을 작성하고 그 프로그램에 대해 증명할 수도 있는데, 일부가 아주 조금씩 하고 있음
      순수 수학을 형식화하고 그에 대한 논문을 내는 것이 현재 Lean4와 Coq가 주로 쓰이는 방식임
      Lean/Coq가 실제로 진술하고 증명할 수 있는 것의 종류는 더 일반적이지만, 현실 세계 프로그램에는 그 정도의 일반성이 꼭 필요하지 않을 수도 있음
답변달기