セキュリティ・レジリエンス
形式検証を組み込んだ高信頼性認証・認可基盤PoC
- 課題
- 認証・認可基盤のPoCで、実装と形式的な検証を組み合わせる取り組みです。
- 制約
- ツールチェイン選定と基礎設計はクライアントが主導し、その方針に沿って協力しました。
- アプローチ
- クライアントの技術的な指揮のもと、Rustによる実装と証明・モデル検査に協力しました。
- アーキテクチャ
- Project Everestの成果物、Rust、Kaniによるモデル検査、Tamarinによるプロトコル検証。
- 担当範囲
- PoC段階の実装・検証への協力です。検証の対象と前提を区別しながら取り組みました。
- Project Everest
- Rust
- Kani
- Tamarin