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

> Clean Markdown view of GeekNews topic #14657. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=14657](https://news.hada.io/topic?id=14657)
- GeekNews Markdown: [https://news.hada.io/topic/14657.md](https://news.hada.io/topic/14657.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2024-05-06T08:34:41+09:00
- Updated: 2024-05-06T08:34:41+09:00
- Original source: [github.com/verus-lang](https://github.com/verus-lang/verus)
- Points: 1
- Comments: 1

## Topic Body

### 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 생태계에서 중요한 역할을 할 프로젝트가 될 것 같음. 특히 시스템 프로그래밍이나 블록체인 등 신뢰성이 중요한 분야에서 활용도가 높을 것으로 기대됨

## Comments



### Comment 24978

- Author: neo
- Created: 2024-05-06T08:34:41+09:00
- Points: 1

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