Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

-セキュリティ-:セキュリティの形式的証明の実世界での応用(1)

 

ある種のセキュリティの勉強を継続しているのですが、論文を調べているとこの辺の研究を実世界で活用しよう、という実証研究も見つかります。今回はこちらの論文:

Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018

を紹介したいと思います。Communications of the ACM の2018年10月号に掲載されてウェブサイトにも公開された記事です。CACMでは全文を読むのは有料なのですが、同じ論文がCSIROのサイトでも無料で公開されています。こちらからダウンロードできます。論文の著者らはオーストラリアのCSIROという、お国の研究機関に所属してる研究グループです。

 

このブログ記事は論文の翻訳ではなく、私の理解に基づく解説です。間違いがありましたらご指摘ください。

 

論文は刺激的なストーリーから始まります。

2017年2月、偵察訓練に飛び立った軍用AH-6ヘリコプターは完全自動操縦で飛行を続けた。ただこの飛行の最中に模擬のサイバー攻撃を受けた。ミッションコンピュータはカメラ内の不正ソフトウェアやメンテナンス時に挿入されたUSBメモリから感染したウィルスによる攻撃に晒された。この攻撃を主導したのはDARPAのred teamのハッカーだった。しかしこの一連の攻撃が航空機の安全な運行に影響を与えることはなかった。

AH-6のオリジナルソフトウェアはこの攻撃には耐えられず、機体の安全運行に重大な支障が生じました。当然「セキュリティ対策はどうなっているんだ!」となります。普通であれば、ソフトウェアに対してセキュリティレビューやセキュリティテストを実施して脆弱性を見つけ出し、それらを潰していくことになります。ウィルスを発見、隔離する対ウィルスソフトの搭載、ウィルスを実行させないホワイトリストの実施、など様々な対策を施す、、、のが並みのセキュリティエンジニアの仕事です。

この論文はそのような対策の話ではありません。前回少し触れた、システムのセキュリティの数学的な証明の話の流れから、絶対に守りたいシステムの安全性を数学的証明で保証するセキュリティ技術というものがあります。これを現代のコンピュータ制御されたヘリコプターに応用した報告がこの論文の趣旨です。

ここで用語の解説ですが、Formal verificationという英語は形式的検証などと訳されるのですが、実際の意味は「数学的証明」ということです。有るシステムのセキュリティが形式的に検証されている、とはそのシステムの秘匿性、完全性、可用性のいずれかの性質が数学的に証明されている、ということを意味します。

現代のヘリコプター制御はおそらく相当に複雑で大規模なソフトウェアの塊です。ソースコードの行数で1000万行以上と言われても驚きません。現在のソフトウェアの形式的検証技術ではここまで大きなソフトウェアを数学的な証明の対象とすることは不可能です。

では著者らはどのようにしてこれを可能にしたのでしょうか。

(次回に続く)

 

By Dave1185 - Dave1185による作品, CC 表示-継承 3.0, https://commons.wikimedia.org/w/index.php?curid=9425199