🦀
kaniで数学的に証明するRust標準ライブラリの安全性

Aoi Sato
2025/12/15に公開
本記事はエクサウィザーズの Advent Calendar  15日目の記事です。

 本記事の目標先端技術開発グループ（WAND）の佐藤碧です。2025年12月にAWSで開催されたAWS re:Inventに参加してきました。

このChalk talkの一つに「Verifying the safety of the Rust standard library」というものがあり、ここで紹介されていたkaniというAmazonが作成しているOSSがとても面白いものでした。kaniがどのようなOSSかを解説し、使い方の一例を紹介します。

 Rust standard libraryRustのcoreとstdクレートには27,000以上の関数が含まれています。このうち、unsafeな関数は7,000以上あり、unsafeなコードを安全にラップしたものは2,300以上あります。

標準ライブラリのバグは、Rustの安全性に対する信頼を損なうことになります。Rustはその安全性を信頼されて、FirecrackerやIAM Policy AutopilotといったAWSの重要なツールに使用されています。一方で、過去には20以上の標準ライブラリに関するCVEが報告されているなど、安全性を100%担保することはとても難しいです。

 kaniこのようなライブラリの安全性検証をするためのツールとしてkaniが開発されました。形式検証ツールで、Rustコードのプロパティを数学的にチェックすることができます。

kaniは、特にRustのunsafeコードブロックの検証に有用です。この部分はコンパイラによるチェックが効かない部分なのですが、その検証をkaniで事前に行うことで、特定の条件を満たしていればunsafeなコードをあたかもsafeなコードとして扱えるようになります。
採用事例としては、下記のようなツールが挙げられます。
Firecracker
S2N
hifitime
rust-bitcoin

 kani を使って実際に検証をする検証をする対象として、簡単な NonZero<u8> 型を使用します。これはメモリ最適化などをコンパイラが自動で行うときに使用されることがある型です。非零が保証されているので、例えば Option<u8> に比べて Option<NonZero<u8>> とすることで、 None を 0 と表現することができ1バイトのメモリ節約をすることができます。コンパイラが自動で行う最適化部分でのunsafe検証は極めて重要です。
#![feature(nonzero_ops)]

use std::num::NonZero;

fn main() {
    let a: u8 = 100;
    let na: NonZero<u8> = NonZero::<u8>::new(a).unwrap();
    let b: u8 = 50;
    unsafe {
        let c = na.unchecked_add(b);
        println!("{}", c.get());
    }
}
このような使い方ができますが、 unchecked_add はunsafeな関数となっています。これはオーバーフローによって足し合わせた結果が 0 になる可能性があるからです。 0 になるときは未定義動作となり、危険な状態になると言えます。これが起こり得ないことを検証したいです。

元の値が非零であることとオーバーフローしないことが unchecked_add の結果が NonZero<u8> 型となるのに十分であることがわかります（厳密に必要十分条件ではありませんが、今回はこの条件で検証します）。
そこで、 a が非零で a + b がオーバーフローをしないとき、この関数の返り値が正しく NonZero<u8> 型であることをkaniを使用して証明します。
#![feature(nonzero_ops)]

use std::num::NonZero;

#[kani::proof]
fn main() {
    let a: u8 = kani::any();
    let b: u8 = kani::any();

    kani::assume(a != 0);
    kani::assume(a.checked_add(b).is_some());

    let nz = unsafe { NonZero::new_unchecked(a) };
    let c = unsafe { nz.unchecked_add(b) };

    assert!(c.get() != 0);
}
上のようなコードによって証明することができます。実際に実行すると以下のような実行ログがでます。
実行ログ% kani src/main.rs
Kani Rust Verifier 0.66.0 (standalone)
warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: 1 warning emitted

Checking harness main...
CBMC 6.8.0 (cbmc-6.8.0)
CBMC version 6.8.0 (cbmc-6.8.0) 64-bit arm64 macos
Reading GOTO program from file /Users/<ユーザー名>/repo/kani-sample/src/main__RNvCslzfVp45ZaId_4main4main.out
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
aborting path on assume(false) at file /Users/runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs line 415 column 15 function std::num::NonZero::<u8>::new_unchecked thread 0
aborting path on assume(false) at file /Users/runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs line 425 column 21 function std::num::NonZero::<u8>::new_unchecked thread 0
aborting path on assume(false) at file /Users/runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs line 415 column 15 function std::num::NonZero::<u8>::new_unchecked thread 0
aborting path on assume(false) at file /Users/runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs line 425 column 21 function std::num::NonZero::<u8>::new_unchecked thread 0
Runtime Symex: 0.0139186s
size of program expression: 419 steps
slicing removed 186 assignments
Generated 16 VCC(s), 8 remaining after simplification
Runtime Postprocess Equation: 7.8709e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000946292s
Running propositional reduction
Post-processing
Runtime Post-process: 6.916e-06s
Solving with CaDiCaL 2.0.0
292 variables, 714 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000231667s
Runtime decision procedure: 0.00123979s
Running propositional reduction
Solving with CaDiCaL 2.0.0
293 variables, 715 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 8.9916e-05s
Runtime decision procedure: 0.000108083s

RESULTS:
Check 1: core::panicking::panic_nounwind_fmt::runtime.unsupported_construct.1
         - Status: SUCCESS
         - Description: "call to foreign "Rust" function `_RNvCsfNd5Qxpi3D5_7___rustc17rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panicking.rs:110:17 in function core::panicking::panic_nounwind_fmt::runtime

Check 2: std::panic::Location::<'_>::caller.unsupported_construct.1
         - Status: SUCCESS
         - Description: "caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panic/location.rs:147:9 in function std::panic::Location::<'_>::caller

Check 3: core::num::<impl u8>::checked_add.arithmetic_overflow.1
         - Status: SUCCESS
         - Description: "attempt to compute `unchecked_add` which would overflow"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/uint_macros.rs:646:31 in function core::num::<impl u8>::checked_add

Check 4: core::num::<impl u8>::unchecked_add.arithmetic_overflow.1
         - Status: SUCCESS
         - Description: "attempt to compute `unchecked_add` which would overflow"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/uint_macros.rs:717:17 in function core::num::<impl u8>::unchecked_add

Check 5: main.assertion.1
         - Status: SUCCESS
         - Description: "assertion failed: c.get() != 0"
         - Location: src/main.rs:16:5 in function main

Check 6: std::num::NonZero::<u8>::new_unchecked.unreachable.1
         - Status: SUCCESS
         - Description: "unreachable code"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs:415:15 in function std::num::NonZero::<u8>::new_unchecked

Check 7: std::num::NonZero::<u8>::new_unchecked.unreachable.2
         - Status: SUCCESS
         - Description: "unreachable code"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs:425:21 in function std::num::NonZero::<u8>::new_unchecked

Check 8: std::num::NonZero::<u8>::new_unchecked.pointer_dereference.1
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/nonzero.rs:415:15 in function std::num::NonZero::<u8>::new_unchecked

Check 9: core::fmt::rt::<impl std::fmt::Arguments<'_>>::new_const::<1>.pointer_dereference.1
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/fmt/rt.rs:196:34 in function core::fmt::rt::<impl std::fmt::Arguments<'_>>::new_const::<1>

Check 10: std::option::Option::<u8>::is_some.pointer_dereference.1
         - Status: SUCCESS
         - Description: "dereference failure: pointer NULL"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/option.rs:635:18 in function std::option::Option::<u8>::is_some

Check 11: std::option::Option::<u8>::is_some.pointer_dereference.2
         - Status: SUCCESS
         - Description: "dereference failure: pointer invalid"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/option.rs:635:18 in function std::option::Option::<u8>::is_some

Check 12: std::option::Option::<u8>::is_some.pointer_dereference.3
         - Status: SUCCESS
         - Description: "dereference failure: deallocated dynamic object"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/option.rs:635:18 in function std::option::Option::<u8>::is_some

Check 13: std::option::Option::<u8>::is_some.pointer_dereference.4
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/option.rs:635:18 in function std::option::Option::<u8>::is_some

Check 14: std::option::Option::<u8>::is_some.pointer_dereference.5
         - Status: SUCCESS
         - Description: "dereference failure: pointer outside object bounds"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/option.rs:635:18 in function std::option::Option::<u8>::is_some

Check 15: std::option::Option::<u8>::is_some.pointer_dereference.6
         - Status: SUCCESS
         - Description: "dereference failure: invalid integer address"
         - Location: ../../../runner/.rustup/toolchains/nightly-2025-11-05-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/option.rs:635:18 in function std::option::Option::<u8>::is_some


SUMMARY:
 ** 0 of 15 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.26984867s

Manual Harness Summary:
Complete - 1 successfully verified harnesses, 0 failures, 1 total.
この VERIFICATION:- SUCCESSFUL によって、検証が成功したことがわかります。

試しに、一つ kani::assume(a != 0) を削除して実行してみます。 VERIFICATION:- FAILED とでて、検証が成功しなかったことがわかります。これは反例として a == 0 && b == 0 があるからで、kaniが正しく検証してくれていることがわかります。

 主要なチェック項目ログから判断できる主要なチェック項目を解説していきます。


チェック内容
説明


arithmetic_overflow
加算でオーバーフローしない

assertion

c.get() != 0 が常に成立

unreachable
到達不可能コードに到達しない

pointer_dereference
不正なポインタアクセスがない


 検証の流れ実際にどのように検証が進んでいるかを解説していきます。

記号実行：a と b を具体的な値ではなく、すべての可能な値を表す記号として扱う

制約の追加：kani::assume で検証対象を絞り込む

網羅的検証：制約を満たすすべての入力（256×256通り）で安全性を確認

数学的証明：SAT/SMTソルバーで論理式の充足可能性を判定
これにより、「テストが通った」ではなく「数学的に安全である」ことを証明できます。
kaniはどのようにして検証をしているのでしょうか？実は検証条件をSAT問題に変換しています。例えば、 a.checked_add(b).is_some() は (a + b <= 255) && (a >= 0) && (b >= 0) となります。このように条件と結果をSAT式で書き表してSATソルバーを使用して検証しています。

一般にSAT問題は、NP-hardであることが知られています。しかし、今回のような小さなケースはSATソルバーを使用することで現実的な時間で解くことができるので、これを用いて検証が進んでいます。

 Contract現状のassumeとassertを用いた検証は、再利用性が低いです。また、可読性も検証途中のコードをいちいち読む必要があり低いです。そこでContract機能を使用した書き方が推奨されています。
#[kani::requires(a != 0)]
#[kani::requires(a.checked_add(b).is_some())]
#[kani::ensures(|result: &NonZero<u8>| result.get() != 0)]
fn safe_unchecked_add(a: u8, b: u8) -> NonZero<u8> {
    let nz = unsafe { NonZero::new_unchecked(a) };
    unsafe { nz.unchecked_add(b) }
}

#[kani::proof_for_contract(safe_unchecked_add)]
fn check_safe_unchecked_add() {
    let a: u8 = kani::any();
    let b: u8 = kani::any();
    safe_unchecked_add(a, b);
}

 事前条件事前条件は、 #[kani::requires(...)] という記法で書きます。 assume の代わりとなります。今回の場合だと、元の値が 0 でない（元の値が NonZero<u8> 型の値である）ことと、オーバーフローをしないことが事前条件です。

 事後条件事後条件は、 #[kani::ensures(...)] という記法で書きます。 assert の代わりとなります。今回の場合だと値が 0 ではない（計算結果が NonZero<u8> 型の値である）ということが事後条件となります。

 LLMによるContractの記述の自動化re:Invent 2025のChalk talkで紹介されていた内容として、2つのLLMベースのエージェントを使用してContractを生成・評価する取り組みが行われているようです。LLMによる具体的な成果としては、194の事前条件などを数分で生成するそうです。
従来、開発者は関数の事前条件・事後条件を手動で考えて記述する必要がありました。この取り組みでは、LLMがコードを解析して自動的にContractを生成します。
impl NonZero<u8> {
    pub unsafe fn unchecked_add(self, rhs: u8) -> NonZero<u8> {
        NonZero::new_unchecked(self.get() + rhs)
    }
}
上記のコードを書いてあげるだけで、
impl NonZero<u8> {
    #[kani::requires(self.get().checked_add(rhs).is_some())]
    #[kani::ensures(|result| result.get() == self.get() + rhs)]
    #[kani::ensures(|result| result.get() != 0)]
    pub unsafe fn unchecked_add(self, rhs: u8) -> NonZero<u8> {
        NonZero::new_unchecked(self.get() + rhs)
    }
}
上記のようなContractがLLMによって自動生成されるということです。

今後、この取り組みが盛んに行われていけば、検証を進める速度が指数関数的に増加していくことも期待できます。
この取り組みですが、公開されている情報が見つかりませんでした。Chalk talkのみで公開された情報かもしれません。今後の続報がとても楽しみです。

 まとめ本記事では、kaniによるRustの標準ライブラリの安全性検証に関して解説しました。Rustは近年、その安全性で注目されていますが、100%安全と現在では言い切ることができません。この検証が進んでいくことで、Rustプロジェクトの安全性がさらに評価されていくことが期待できます。
kaniの他にもさまざまなツールが開発されています。また実際に検証するべき課題はGitHubにて公開されています。 実際に課題を確認してみることもRustの安全性検証でどのような問題を解決しようとしているかの理解が進んでいくと思います。
今後は、その他の安全性検証ツールの解説や、kaniが内部でどのようにして検証しているか、未解決となっている課題の概要の解説などもしていければと思います。またLLMによるContract記述の自動化についても、続報を楽しみに待ちたいと思います。
チェック内容	説明
`arithmetic_overflow`	加算でオーバーフローしない
`assertion`	`c.get() != 0` が常に成立
`unreachable`	到達不可能コードに到達しない
`pointer_dereference`	不正なポインタアクセスがない
エクサウィザーズ Tech Blog
株式会社エクサウィザーズのテックブログ
本記事の目標

Rust standard library

kani

kani を使って実際に検証をする

主要なチェック項目

検証の流れ

Contract

事前条件

事後条件

LLMによるContractの記述の自動化

まとめ

Discussion
