Kani：Rustのモデルチェッカーが標準ライブラリで1万6000以上の検証ハーネスを実現

Kani: A Model Checker for Rust

Rustの所有権型システムは安全なコードのメモリエラーを防ぎますが、unsafe操作の健全性、機能的正しさ、実行時パニックの不在など、コンパイルでは保証されない性質があります。本論文では、オープンソースのモデルチェッカーKaniを紹介します。KaniはRustのMIRをCBMCのビット精密な検証エンジンにコンパイルし、ユーザー注釈なしで包括的な安全プロパティを自動チェックします。さらに、関数契約、ループ契約、量化子、関数スタブからなる仕様言語により、有界検証から非有界検証へ拡張します。産業用Rustプロジェクトでのケーススタディでは、契約により検証をパニックフリーから機能的正しさへと昇格させ、6つの未知のバグを発見しました。Kaniは本番CIでスケールし、Rust標準ライブラリ検証キャンペーンではコード変更ごとに16,000以上のハーネスを検証しています。