Hacker News • 22일 전

러스트 오픈소스 모델 체커, Kani

IMP

7/10

핵심 요약

러스트(Rust) 코드의 안전성과 기능적 정합성을 검증하기 위한 오픈소스 모델 체커 'Kani'가 공개되었습니다. Kani는 유한 범위 모델 검사(Bounded Model Checking)를 넘어 사용자가 직접 명세를 작성하지 않아도 잠재적인 런타임 패닉이나 unsafe 구문의 오류를 자동으로 찾아내고 검증합니다. 이 도구는 산업계 실제 프로젝트와 CI 환경에 적용되어 수많은 코드 변경 사항을 검증하며 그 유용성과 확장성을 입증했습니다.

번역된 본문

제목: Kani: 러스트를 위한 모델 체커 저자: 레미 델마스 (Rémi Delmas), 지아드 하산 (Zyad Hassan), 후 친핑 (Qinheping Hu), 라훌 쿠마르 (Rahul Kumar), 펠리피 R. 몬테이로 (Felipe R. Monteiro), 탄 응우옌 (Thanh Nguyen), 아드리안 팔라시오스 (Adrián Palacios), 셀리나 발 (Celina Val), 마이클 타우트스니히 (Michael Tautschnig), 유스투스 아담 (Justus Adam), 다니엘 슈워츠-나르본느 (Daniel Schwartz-Narbonne), 캐롤린 제크 (Carolyn Zech)

요약: 러스트(Rust)의 소유권(ownership) 타입 시스템은 안전한 코드 내에서의 메모리 오류를 방지하지만, 여전히 컴파일과 무관하게 다루어야 하는 바람직한 속성들이 남아있습니다. 이는 unsafe 연산(예: 원시 포인터 역참조)의 건전성, 기능적 정합성(functional correctness), 그리고 런타임 패닉의 부재입니다.

우리는 단순히 버그를 찾는 것을 넘어 이러한 속성들에 대한 정합성을 보장하기 위해 유한 범위 모델 검사(bounded model checking)를 확장한 러스트 오픈소스 모델 체커인 'Kani'를 제안합니다. Kani는 러스트의 중간 수준 중간 표현(MIR)으로부터 증명 하네스(proof harnesses)를 컴파일하여 CBMC의 비트 정확도 검증 엔진으로 변환합니다. 이를 통해 사용자의 별도 주석(annotation) 없이도 포괄적인 안전 속성들을 자동으로 검사합니다.

또한, 제한된 범위(bounded)에서 무제한(unbounded)으로 검증을 확장하기 위해 Kani는 함수 계약(function contracts), 루프 계약(loop contracts), 정량자(quantifiers), 함수 스텁bing(function stubbing)으로 구성된 명세 언어를 제공합니다. 우리는 산업계 러스트 프로젝트에 대한 사례 연구를 통해 그 실행 가능성을 입증했습니다. 여기서 계약을 통해 패닉 자유 검증을 기능적 정합성 검증으로 업그레이드했으며, 이전에 알려지지 않았던 6개의 버그를 발견했습니다. Kani는 상용 CI 환경에서 대규모로 작동하며, 러스트 표준 라이브러리 검증 캠페인에서는 단일 코드 변경 시마다 16,000개 이상의 하네스를 검증합니다.

참고: 제39회 IEEE/ACM 국제 자동 소프트웨어 엔지니어링 컨퍼런스(ASE 2026), 산업 쇼케이스 트랙(Industry Showcase Track) 채택 주제: 소프트웨어 엔지니어링 (cs.SE); 컴퓨터 공학의 논리 (cs.LO); 프로그래밍 언어 (cs.PL) 인용: arXiv:2607.01504 [cs.SE]

원문 보기

원문 보기 (영어)

--> Computer Science > Software Engineering arXiv:2607.01504 (cs) [Submitted on 1 Jul 2026] Title: Kani: A Model Checker for Rust Authors: Rémi Delmas , Zyad Hassan , Qinheping Hu , Rahul Kumar , Felipe R. Monteiro , Thanh Nguyen , Adrián Palacios , Celina Val , Michael Tautschnig , Justus Adam , Daniel Schwartz-Narbonne , Carolyn Zech View a PDF of the paper titled Kani: A Model Checker for Rust, by R\'emi Delmas and 11 other authors View PDF HTML (experimental) Abstract: Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign. Comments: Accepted at the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2026), Industry Showcase Track Subjects: Software Engineering (cs.SE) ; Logic in Computer Science (cs.LO); Programming Languages (cs.PL) ACM classes: D.2.4; F.3.1 Cite as: arXiv:2607.01504 [cs.SE] (or arXiv:2607.01504v1 [cs.SE] for this version) https://doi.org/10.48550/arXiv.2607.01504 Focus to learn more arXiv-issued DOI via DataCite (pending registration) Submission history From: Felipe R. Monteiro [ view email ] [v1] Wed, 1 Jul 2026 22:05:33 UTC (149 KB) Full-text links: Access Paper: View a PDF of the paper titled Kani: A Model Checker for Rust, by R\'emi Delmas and 11 other authors View PDF HTML (experimental) TeX Source view license Current browse context: cs.SE < prev | next > new | recent | 2026-07 Change to browse by: cs cs.LO cs.PL References & Citations NASA ADS Google Scholar Semantic Scholar export BibTeX citation Loading... BibTeX formatted citation × loading... Data provided by: Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer ( What is the Explorer? ) Connected Papers Toggle Connected Papers ( What is Connected Papers? ) Litmaps Toggle Litmaps ( What is Litmaps? ) scite.ai Toggle scite Smart Citations ( What are Smart Citations? ) Code, Data, Media Code, Data and Media Associated with this Article alphaXiv Toggle alphaXiv ( What is alphaXiv? ) Links to Code Toggle CatalyzeX Code Finder for Papers ( What is CatalyzeX? ) DagsHub Toggle DagsHub ( What is DagsHub? ) GotitPub Toggle Gotit.pub ( What is GotitPub? ) Huggingface Toggle Hugging Face ( What is Huggingface? ) ScienceCast Toggle ScienceCast ( What is ScienceCast? ) Demos Demos Replicate Toggle Replicate ( What is Replicate? ) Spaces Toggle Hugging Face Spaces ( What is Spaces? ) Spaces Toggle TXYZ.AI ( What is TXYZ.AI? ) Related Papers Recommenders and Search Tools Link to Influence Flower Influence Flower ( What are Influence Flowers? ) Core recommender toggle CORE Recommender ( What is CORE? ) Author Venue Institution Topic About arXivLabs arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs . Which authors of this paper are endorsers? | Disable MathJax ( What is MathJax? )

러스트 정적 분석 모델 체킹 오픈소스 소프트웨어 검증