形式検証を組み込んだ
高信頼性認証・認可基盤PoC
高い信頼性が求められる認証・認可基盤のPoCにおいて，Rustによる実装と，形式検証・モデル検査を並行して進める開発に協力しました。既存の形式検証成果を活用しながら，実装レベルではKani，プロトコルレベルではTamarinを用い，異なる層の性質を検討する取り組みです。
- 領域
- Product Engineering / Security & Resilience
- 種別
- Proof of Concept
- 手法
- 形式検証・モデル検査・プロトコル検証
- 実装
- Rust
- ツール・既存成果
- Kani / Tamarin / Project Everest
背景
動くことに加えて，確かめたい性質がある。
認証・認可基盤では，正常な入力に対する動作に加え，想定外の入力や複雑な状態遷移，攻撃者を含む環境で，どのような性質が維持されるかが重要です。このPoCでは，通常のテストとともに，次の点を明示して検討しました。
- どのような前提を置くか
- どの入力や状態を探索するか
- どの安全性に関する性質を確認するか
- 検証結果が実装のどこに対応するか
CoRISEの担当範囲
技術方針を，実装と検証へつなぐ。
↔ 横にスクロールして図全体をご覧いただけます。
図を文章で読む
中央のRust実装を，左のKaniがハーネスを通じて検査します。右のTamarinは別途記述したプロトコルモデルを検証します。Rust実装とモデルの点線は，対応を確認すべき関係を示し，自動変換や証明済みの対応を意味しません。
01
Rustによる実装
認証・認可基盤を構成する機能の一部を実装しました。検証対象となる境界や状態遷移を意識しながら，コードを具体化しました。
02
Kaniによるモデル検査
検証ハーネスで入力，前提，探索範囲，確認条件を定義し，Rust実装の性質を検査する作業に協力しました。
03
Tamarinによるプロトコル検証
メッセージ交換や状態遷移を記号的にモデル化し，攻撃者を含む振る舞いと安全性に関する性質を検討する作業に協力しました。
検証の層
層ごとに検証し，前提と実装の対応を確かめる。
KaniはRustコードを，Tamarinはプロトコルの記号モデルを対象とします。それぞれの検証結果を，対象・前提・適用範囲とあわせて扱います。以下の図は検証の関係を示す概念図です。
↔ 横にスクロールして図全体をご覧いただけます。
図を文章で読む
既存の形式検証成果をRust実装に組み込みます。Kaniではハーネスから到達するコードを検査し，Tamarinでは別途作成した記号モデルを検証します。モデルと実装の対応は確認すべき関係です。それぞれの結果を前提・対象範囲とあわせて整理し，実装の見直しへ戻します。図の枠は検証対象の区分であり，システムの信頼境界ではありません。
既存の形式検証成果
既存の検証成果を，保証範囲を理解して利用する。
このPoCではProject Everestの成果物を利用しました。既存の形式検証成果を組み込む際は，成果物自体の保証と，それを利用するシステムで確認すべき性質を区別する必要があります。
成果物が保証する性質
何について証明された成果なのかを具体的に捉えます。
保証が成り立つ前提
検証結果を適用するために必要な条件を確認します。
組み込み時の境界
成果物の責任範囲と，それを呼び出すコードの範囲を分けます。
利用側に残る責任
システムとして別途確認すべき性質を整理します。
05 — 実装レベルの検査
Rustコードの性質を，ハーネスで定めた条件で検査する。
Kaniでは，検証ハーネスを入り口としてRustコードを解析します。ハーネスから到達するコードを対象に，前提と解析上の境界を明示して性質を確かめます。
検証ハーネス
検査の入り口と対象となる処理を定義します。
入力と探索範囲
非決定的な入力を扱い，ループの展開上限など，解析に必要な境界を設定します。
明示的な前提
入力などへの制約をハーネスに記述し，暗黙の仮定を減らします。
確認する性質
アサーションや安全性チェックによって，何を検査するかを具体化します。
結果の解釈
成功した結果も，解析の完了状況，前提，設定した境界とあわせて解釈します。アプリケーション全体の正しさとは区別します。
↔ 横にスクロールして図全体をご覧いただけます。
図を文章で読む
入力と前提を定めたハーネスから，到達可能なRustコードを解析します。探索の境界と確認する性質を設定し，その条件下での結果を得ます。設定した範囲内の網羅的な検査と，アプリケーション全体の証明は区別します。
06 — プロトコルレベルの検証
プロトコルの振る舞いを，攻撃者を含むモデルで検討する。
Tamarinが扱うのはRustコードそのものではなく，プロトコルの記号モデルです。参加者の通信や状態遷移に加え，モデルに定めた攻撃者の能力を含めて性質を検討します。
記号的なプロトコルモデル
実行中のコードの記録ではなく，プロトコルの論理を抽象化して表します。
メッセージ交換と状態遷移
参加者間のやり取りと，それに伴う状態の変化を扱います。
攻撃者の能力と仮定
傍受や改変など，想定する攻撃者の振る舞いをモデルの前提に含めます。
安全性に関する性質
機密性やイベント間の対応関係など，確認したい性質を記述します。ここでの例示は，本PoCでの証明完了を意味しません。
モデルと実装の対応
モデルの状態や操作が実装のどこに対応するかを検討します。この対応自体も，自動的に証明されるわけではありません。
↔ 横にスクロールして図全体をご覧いただけます。
図を文章で読む
参加者AとBの記号的なメッセージ交換に，想定する攻撃者の能力を含めます。そのモデルに対して性質を検証します。機密性やイベント間の対応関係は性質の例であり，本PoCでの証明完了の主張ではありません。モデルとRust実装の対応は別途検討します。
開発の進め方
設計・実装・検証を往復する。
実装と検証を並行して進め，確認したい性質とコードの対応を見直します。図は，前提や反例を手がかりに設計・実装へ戻る，開発の考え方を表しています。
↔ 横にスクロールして図全体をご覧いただけます。
図を文章で読む
性質の定義，実装，モデル・ハーネスの作成，検証，前提・反例の確認，設計・実装の見直しを順にたどり，再び性質の定義へ戻ります。反復する開発の考え方を示した概念図です。
この事例で取り組んだこと
形式手法を，ソフトウェア開発へ接続する。
- 01Rustによる実装
- 02形式手法を意識した開発
- 03Kaniによるモデル検査
- 04Tamarinによる記号的プロトコル検証
- 05既存の形式検証成果の活用
- 06検証対象と保証範囲の整理
- 07前提と検証結果の対応づけ
- 08実装と検証のフィードバック
保証範囲
検証したことと，保証範囲の外にあることを区別する。
本事例は，認証・認可基盤全体の安全性が形式的に証明されたことを意味するものではありません。
検証結果は，対象となる実装やモデル，前提条件，探索範囲，攻撃者モデルなどに依存します。PoCでの取り組みと，本番運用での信頼性の保証も区別しています。
何が確認されたかとともに，何が保証範囲の外にあるかを明示することも，高信頼性システム開発の一部と考えています。