Verus로 올바름이 증명된 Rust 코드 개발하기 — Amazon의 형식 검증 도구

본문

Rust는 C 수준의 성능과 유연성을 제공하면서 타입 시스템으로 다양한 버그와 보안 취약점을 자동으로 방지해, Amazon의 Firecracker, 서버리스 분산 SQL 데이터베이스, Nitro Isolation Engine 등에 널리 채택되고 있습니다. 그러나 '더 올바르고 안전한' 코드가 '실제로 올바르고 안전한' 코드를 의미하지는 않습니다. C에서 배열 범위를 벗어난 접근은 예측 불가능한 결과를 낳지만, Rust는 프로그램을 중단시킬 뿐이며 애초에 그런 접근이 없어야 진정으로 올바른 프로그램입니다. Rust는 프로그램이 기대한 결과를 계산하는지, 접근 가능한 비밀을 누출하지 않는지도 보장하지 못합니다. 바로 이 지점에서 Verus가 등장합니다.

Verus란 무엇인가

Verus는 Rust를 위한 오픈소스 자동화 프로그램 검증기(automated program verifier)입니다. 프로그램 검증기는 코드가 어떻게 동작해야 하는지에 대한 형식적 수학 명세(specification)를 입력받아, 모든 가능한 입력에 대해 코드가 그 명세와 일치하는지 기계적으로 확인합니다. 예를 들어 정렬된 배열에서 특정 값을 찾는 최적화된 이진 탐색을 구현했다면, 명세는 '코드가 인덱스를 반환할 때 배열의 해당 원소가 목표 값과 일치한다'는 내용이 될 수 있고, 검증기는 이것이 모든 입력 배열과 목표 값에 대해 성립하는지 확인합니다. 전통적인 테스팅은 몇 가지 구체적 배열만 시험하므로 목표 값이 마지막 원소이거나 배열에 아예 없는 경우 같은 코너 케이스를 놓칠 수 있습니다. 검증의 핵심은 코드가 명세와 일치함을 보이는 수학적 증명의 구성인데, Verus 같은 자동화 검증기는 저수준의 지루한 증명 단계를 도구가 처리하고 개발자는 귀납법 설정이나 루프 불변량(loop invariant) 제시 같은 고수준 안내를 제공합니다. 최근에는 이런 고수준 단계조차 AI로 자동화되는 경우가 많다고 원문은 덧붙입니다.

Rust 소스 안에 직접 쓰는 명세와 증명

Verus를 사용하면 개발자가 기존 Rust 코드에 대한 명세와 증명을 Rust 소스 파일 안에 직접 추가할 수 있습니다. 이진 탐색 예시에서 'requires' 키워드로 표시된 사전조건(precondition)은 함수 실행 전에 참이어야 할 조건, 즉 배열이 정렬되어 있다는 것을 요구합니다. 'ensures' 키워드의 사후조건(postcondition)은 함수가 'Some(index)'를 반환하면 그 인덱스가 배열 범위 안이고 해당 위치의 값이 찾던 값과 일치함을 명시합니다. 중요하게는 함수가 'None'을 반환하면 목표 값이 배열에 존재하지 않는다는 조항도 포함되는데, 이것이 없으면 항상 'None'만 반환하는 구현도 명세를 만족해 버리기 때문입니다. 일반 Rust 컴파일러는 이 주석들을 무시하므로 Verus가 주석된 코드는 Cargo를 쓰는 프로젝트를 포함해 검증 여부와 무관하게 그대로 소비할 수 있습니다.

이는 다른 Rust 검증 접근법과 구별되는 핵심 설계 결정입니다. 개발자는 Rust와 유사한 문법으로 명세와 증명을 작성하고, 증명이 실패하면 소스 수준에서 Rust 스타일의 오류 메시지를 받습니다. 증명이 실제 코드와 동기화 상태를 유지하고, 개발자가 새 언어와 도구를 배울 필요가 없으며, 코드를 작성한 개발자가 직접 정확성 증명에 참여할 수 있게 합니다. Verus는 또한 빠르고 강력한 자동화에 초점을 두어 여러 솔버로 프로그램과 명세에서 생성된 증명 의무를 해소하며, 실무에서는 보통 1초 미만의 피드백을 제공해 VS Code의 '빨간 밑줄' 같은 대화형 개발 루프가 가능합니다. 프로젝트 수준에서는 수천 줄의 코드와 증명을, 과거 자동화 검증기가 개별 함수 하나 검증하는 데 걸린 시간 안에 검증할 수 있다고 합니다. 이 빠른 자동화는 AI 에이전트가 Verus 증명을 개발할 때도 작업량을 줄이고 반복을 가속하는 이점이 됩니다.

unsafe 코드와 동시성 검증

Rust의 타입 시스템은 강력하지만 때때로 고성능 코드 작성을 막기 때문에 명시적으로 표시된 'unsafe' 코드를 허용합니다. unsafe 코드도 safe 코드의 모든 기대를 충족해야 하지만 컴파일러가 기계적으로 검사해주지 않아 개발자 책임인데, Verus로는 unsafe Rust 코드의 안전성을 수학적으로 증명해 기계 검증된 안전성 보장을 복원할 수 있습니다. 동시성 분야에서도 Rust의 '겁 없는 동시성(fearless concurrency)' 위에 Verus는 동시성 코드가 안전할 뿐 아니라 올바름을 증명하게 합니다. 예를 들어 락(lock)에 불변 속성을 부여해 락을 획득한 스레드가 그 속성을 만족하는 값을 얻고, 해제 시 그 속성이 여전히 유지됨을 증명하게 할 수 있으며, 락 구현 자체의 정확성 증명도 지원합니다. 이는 고성능을 위해 복잡한 커스텀 락킹 방식에 의존하는 Nitro Isolation Engine 같은 프로그램에 특히 중요합니다. Amazon은 이미 Nitro Isolation Engine의 핵심 프리미티브와 내부 핵심 인프라 여러 부분의 정확성을 Verus로 증명했다고 밝혔습니다.

신뢰의 전제와 오픈소스 생태계

모든 프로그램 검증기와 마찬가지로 Verus의 보장은 Verus 자체의 정확성, 의도한 동작의 '최상위' 명세, Rust 표준 라이브러리 같은 런타임에 대한 '최하위' 가정, 그리고 소스를 실행 파일로 변환하는 컴파일러 도구체인의 정확성에 의존합니다. Amazon 외에도 오픈소스 생태계에서 다양한 활용 사례가 있습니다. 바이너리 데이터 형식 기술로부터 정확성·보안 증명이 포함된 파싱·직렬화 Rust 코드를 생성하는 Vest, 사용자 정의 검증 정책을 지원하는 증명된 x.509 인증서 검증 라이브러리 Verdict, 시스템 충돌·정전에도 데이터를 보존하는 영구 메모리 로그의 정확성과 크래시 안전성을 검증한 CapybaraKV, Verus로 정확성이 검증된 Rust 마이크로커널 Atmosphere, Kubernetes 컨트롤러가 합리적 가정 하에 시스템을 결국 안정 상태로 이끎(liveness)을 증명한 Anvil, 확장 가능한 락킹 프로토콜의 트랜잭션 인터페이스를 갖춘 메모리 관리 시스템 CortenMM 등입니다. Verus 자체는 학계와 산업계 연구자의 분산 협업으로 개발되는 자유 오픈소스 프로젝트입니다.

Reddit 반응

• @98f00b2 — 오랫동안 써 보기를 기대해 왔습니다. F*를 대체하면서 Rust 코드를 직접 작성하게 해주는 도구라는 점이 매력적이며, 비형식적으로 검사되는 명세의 정확성 우려 없이 이 분야에서 LLM이 매우 생산적이라는 이야기를 고려하면 더욱 그렇습니다.
• @Amadex — Amazon에는 이미 Kani가 있는데 여기서 무엇을 하는 걸까요, 또 다른 형식 검증 도구를 시작할 만큼 다를까요? (수정) Verus는 상위 수준의 형식 명세가 필요하고 그것으로 증명을 생성하는 방식인 것 같습니다. 심볼릭 실행에 가까운 Kani와는 다르네요.
• @nonotan — 명세 문법은 꽤 좋아 보입니다. 다만 명세도 결국 또 다른 Rust 코드일 뿐이라는 점에서, 주어진 명세와 대조해 검사된 코드를 '증명 가능하게 올바르다'고 부르는 것은 다소 어색합니다. 아주 좁은 의미에서는 맞지만 일반적으로 이해되는 의미는 아니며, 같은 것을 두 가지 방식으로 작성해 일치하는지 확인하는 것에 가깝습니다. 물론 그것만으로도 잠재적 문제를 많이 잡아낼 수는 있습니다.

원문: Amazon Science / 번역·요약: Trawling