プログラミング
Kani: Rustのためのモデルチェッカー
Kani: A Model Checker for Rust (arxiv.org)
要約
KaniはRustのコードにおけるメモリ安全性以外の特性（unsafe操作の健全性、機能的正当性、ランタイムパニックの不在）を検証するためのオープンソースモデルチェッカーです。MIRからCBMCの検証エンジンにプルーフハーネスをコンパイルし、ユーザー注釈なしで包括的な安全プロパティを自動的にチェックします。Kaniは、関数契約、ループ契約、量化子、関数スタブを備えた仕様言語を提供し、検証を境界付きから無限に拡張します。産業用Rustプロジェクトでのケーススタディでは、6つの未知のバグを発見し、Rust標準ライブラリの検証キャンペーンでは1コード変更あたり16,000以上のハーネスを検証する規模で運用されています。
全文翻訳
Rustの所有権型システムは、安全なコードにおけるメモリエラーを防ぎますが、特定の望ましい特性はコンパイルとは無関係のままです。例えば、unsafe操作（生のポインタの間接参照など）の健全性、機能的正当性、ランタイムパニックの不在などが挙げられます。
私たちはKaniを発表します。これは、バグ発見を超えてこれらの特性の正当性保証を提供する、Rustのためのオープンソースモデルチェッカーです。
Kaniは、Rustの中間表現（MIR）からプルーフハーネスをコンパイルし、CBMCのビット精度の検証エンジンに変換します。これにより、ユーザー注釈なしで包括的な安全プロパティを自動的にチェックします。
検証を境界付きから無限に拡張するために、Kaniは関数契約、ループ契約、量化子、関数スタブを含む仕様言語を提供します。
産業用Rustプロジェクトでのケーススタディを通じて、契約が検証をパニックからの自由から機能的正当性に向上させ、以前は知られていなかった6つのバグを発見したことで、その実現可能性を実証しています。
Kaniは、Rust標準ライブラリの検証キャンペーンにおいて、1コード変更あたり16,000以上のハーネスが検証される規模で、本番CIで運用されています。