形式検証ネタサーベイ

# 参考文献

## 事例系

[By Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser
Communications of the ACM, October 2018, Vol. 61 No. 10, Pages 68-77
Formally Verified Software in the Real World

### 要約
ボーイング社の軍用ヘリでの事例。seL4ベースにどうシステムをセキュリティを担保したかという話。重要なこととして、
safetyだけ考えていたのでは立ち行かないということが述べられているところだろう。

Key insightは以下。
- 検証済みマイクロカーネルを、低コストで現実レベルのシステムへ適用するアーキテクチャ
- システム内で異なる保証レベルを混在させる。全てのコンポーネントが高保証である必要はない
-　高保証は、適度な再設計とリファクタリングだけで、適切な既存システムに追加導入できる

High-Assurance Cyber Military Systems (HACMS) program での成果らしい。

CAmkESというフレームワークを開発、使用した。
形式検証について、seL4について、seL4ベースでのセキュアなアーキテクチャの考え方、といった話題になる。

証明されたコンポーネントを使えるため、完璧なモジュラリティといったものが実現できたみたい。