▲

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

 (github.com/verus-lang)
1P by neo 4달전 | favorite | 댓글 1개

Rust 코드의 정확성을 검증하기 위한 Verus 도구

  • Verus는 Rust로 작성된 코드의 정확성을 검증하기 위한 도구
  • 개발자는 코드가 수행해야 할 사양을 작성하고, Verus는 실행 가능한 Rust 코드가 모든 가능한 코드 실행에 대해 항상 사양을 충족하는지 정적으로 검사함
  • 런타임 검사를 추가하는 대신 Verus는 강력한 솔버에 의존하여 코드가 올바른지 증명함
  • Verus는 현재 Rust의 하위 집합을 지원하며(확장 중), 경우에 따라 개발자가 표준 Rust 타입 시스템을 넘어 정적으로 코드의 정확성을 검사할 수 있도록 함(예: 원시 포인터 조작)

Verus의 현재 상태

  • Verus는 활발히 개발 중
  • 기능이 깨지거나 누락될 수 있으며 문서도 여전히 불완전함
  • Verus를 시도하려면 Zulip에서 도움을 요청할 준비가 되어 있어야 함

Verus 사용해보기

  • 브라우저에서 Verus를 시도하려면 Verus Playground를 방문
  • 더 복잡한 개발을 위해서는 설치 지침을 따르고, 튜토리얼과 참조부터 시작하여 아래 문서를 살펴볼 것

Verus 문서

  • 튜토리얼 및 참조
  • Verus 표준 라이브러리에 대한 API 문서
  • 동시성 코드 검증을 위한 가이드
  • 프로젝트 목표
  • Verus에 기여하기
  • 라이선스

연락하기, 이슈 보고, 토론 시작하기

  • GitHub에서 이슈를 보고하거나 토론을 시작하거나, 실시간 토론과 도움이 필요한 경우 Zulip에 가입할 것
  • 기존 기능의 실행 가능한 문제(버그)에는 GitHub 이슈를, 기능 요청 및 예정된 기능에 대한 보다 개방적인 대화에는 GitHub 토론을 사용함
  • 기여를 환영하며, 코드를 기여하고 싶다면 Contributing to Verus의 팁을 살펴볼 것

GN⁺의 의견

  • Rust는 시스템 프로그래밍에 적합한 언어로 안전성과 성능을 보장하는 것으로 잘 알려져 있는데, Verus는 이러한 Rust의 장점을 더욱 강화할 수 있는 프로젝트로 보임. 특히 동시성 프로그래밍 검증 기능은 매우 흥미로워 보임

  • 다만 아직 개발 초기 단계이고 지원하는 Rust 문법이 제한적인 것 같아서, 실제 프로덕션에 적용하기에는 좀 더 개발이 필요해 보임. 하지만 정적 분석을 통해 미리 코드의 안전성을 보장하는 것은 중요하기 때문에 앞으로 발전 가능성이 높아 보임

  • 개발 초기라 아직 문서화가 부족한 점, 지원하는 문법이 제한적인 점 등 개선이 필요해 보이지만, 장기적으로는 Rust 생태계에서 중요한 역할을 할 프로젝트가 될 것 같음. 특히 시스템 프로그래밍이나 블록체인 등 신뢰성이 중요한 분야에서 활용도가 높을 것으로 기대됨

▲
neo 4달전  [-]
Hacker News 의견
  • Verus를 사용하여 공식적으로 검증된 Kubernetes 컨트롤러를 작성함
    • 컨트롤러가 결국 요청된 desired state로 클러스터를 조정할 것이라는 liveness 속성을 증명할 수 있음
    • 정확성을 명시하는 데에는 미묘한 점과 뉘앙스가 많이 있음 (desired state 요구사항의 빠른 변화, 비동기성, 장애 등)
    • 코드는 GitHub 링크에 있으며, OSDI 2024에 게재 예정인 논문과 연결됨
  • Verus를 향한 작은 디딤돌로, Rust의 debug_assert를 사용하여 사전조건과 사후조건을 추가할 수 있음
    • Rust 컴파일러는 기본적으로 프로덕션 빌드에서 이를 제거함
    • Verus 튜토리얼의 예제와 debug_assert를 사용한 런타임 체크 예제 제공
  • "코드의 정확성 검증"과 "코드의 정확성 증명"의 차이점에 대한 초보자 질문
    • CS/수학 배경이 약한 실무 프로그래머를 위한 코드 "증명"에 대한 좋은 학습 자료가 있는지 궁금함
    • "제로 지식" 증명이 왜 중요한지, 왜 이것이 그렇게 관련이 있는지 매우 궁금함
  • Rust 표준은 C/C++, Common Lisp, Ada/SPARK2014와 같이 아직 없음
    • 이는 Ada/SPARK2014 등을 위해 개발된 검증 도구와 비교할 때 움직이는 목표임
  • Dafny는 Rust로 컴파일할 수 있는 "검증 인식 프로그래밍 언어"임 (GitHub 링크)
  • 주요 기여자 중 한 명이 취리히 Rust 밋업에서 Verus에 대한 훌륭한 발표를 함 (YouTube 링크)
    • "ghost" 코드가 프로그램에 깔끔하게 맞는 것이 인상적이었음 (Ada를 약간 연상시킴)
  • Verus와 SPARK의 비교
    • 동일한 일반 클래스의 검증기인가? Verus가 Ada용 검증기가 아닌 Rust용 검증기라는 점 외에 어떤 차이가 있는가?
  • Verus에 정통한 사람이 Verus와 Lean4의 성능과 표현력을 비교해 줄 수 있는지?
    • Verus는 SMT 기반 검증 도구이고, Lean은 대화형 증명기이자 SMT 기반 도구라고 이해함
    • 그러나 형식 검증 분야에 대한 이해도는 제한적이므로, 소프트웨어 형식 기법에 정통한 사람의 의견을 듣는 것이 좋겠음
  • Verus와 Kani의 관계가 있는지? 다르게 작동하는지? (Kani GitHub 링크)
  • 결과 코드가 여전히 바닐라 Rust 도구를 사용하여 컴파일할 수 있는 유효한 Rust 코드가 되도록 구현하는 방법이 있는지?
답변달기