01 / UNDERSTAND
仕組みと使いどころ
テストが選択した状態や入力で動作を確かめるのに対し、形式検証は定めた検証範囲内の全状態・全入力を対象に、仕様上の性質が成立することを証明します。ソフトウェアでは、定理証明器や証明支援系などを用いて、機能の正しさ、メモリ安全性、機密性・完全性といった性質を検証できます。ハードウェア設計にも適用されます。ただし、保証されるのは形式化した仕様と証明の対象範囲に限られ、コンパイラやハードウェア、証明確認用ソフトウェアなどの正しさを前提とする場合があります。テストを不要にするものではなく、未検証部分や実際の動作を確認するテストと相互に補完します。
02 / IN PRACTICE
Formal Verificationの活用例
たとえば、こんな場面で
暗号通信の実装や仮想マシンの分離機構、プロセッサ設計など、誤りの影響が大きい部分について、期待する安全性や入出力動作を仕様として記述し、その性質が対象範囲の全ケースで成立するかを証明する用途が考えられます。
03 / GOOD TO KNOW
使うときのポイント
「形式検証済み」という表現だけで判断せず、証明された性質、対象となるコードや機能の範囲、使用した仕様、証明が依存する前提条件を確認することが重要です。
参考資料
AWS Nitro Isolation Engine: Formally verifying the hypervisor in the AWS Nitro System | Amazon Web Services （新しいタブで開きます）Project Everest: Reaching greater heights in internet communication security - Microsoft Research （新しいタブで開きます）Oski Technology, an Expert in Formal Verification, Joins NVIDIA （新しいタブで開きます）用語の説明や活用例に関連する参考資料です。
