豪研究所、カーネルの安全性を数学的に検証する手法を開発

　オーストラリアの民間研究機関Information and Communications Technology Centre of Excellence（NICTA）の研究者らは現地時間8月12日、ミッションクリティカルなシステム向けの中核ソフトウェアが安全であることを検証する方法を発表した。

　研究者らによると、この方法により、飛行機や自動車におけるシステムの安全性とセキュリティを管理するソフトウェアが、エラーを含む大型クラスを持たないことを数学的に検証できるという。

　NICTAは、汎用OSカーネルに対する、マシンチェックによる初のフォーマル検証が完了したと発表した。このカーネルは、「Secure Embedded L4」（seL4）マイクロカーネルと呼ばれる。

　ケンブリッジ大学のコンピュータ研究所で演算論理学の教授を務めるLawrence Paulson氏は、英国時間8月13日にZDNet UKの取材に応じ、このマイクロカーネルの飛躍的進歩は企業各社にトリクルダウン効果をもたらすだろうと述べた。同氏は定理証明支援プログラム「Isabelle」を開発した人物で、NICTAはIsabelleを改変して同団体のカーネルをチェックした。

　「私はソフトウェア業界が完全に混乱していると考えている。コンピュータを使ったことがある人なら、それがどれほど不安定なものかを知っている。これは、安定性を改善する重要な手段になる」（Paulson氏）

　Paulson氏によれば、高品質のコードを厳密にテストするには費用がかかるが、こうした専門用途のテストやOSを開発することは、一般的なソフトウェアの向上という二次的効果をもたらすという。

　Paulson氏は、ドイツの「Verisoft」プロジェクトを例に挙げながら、欧州のチームがコンピュータシステムのフォーマル検証において飛躍的進歩を遂げたと付け加えた。

　フォーマル検証の研究チームを率いるNICTAの主任研究者Gerwin Klein氏は声明の中で、これまでの研究では特定システムの特性を検証することに注力していたと述べた。

　「特定（システム）の特性へのフォーマル検証は比較的小さなカーネルで実施されてきたが、われわれが実行したのは、実世界でこれまで1度も実現しなかった、これほど複雑な高性能ソフトウェアに対する一般的かつ機能的な正当性の検証だ」（Klein氏）

　NICTAは、seL4マイクロカーネルに対して、バッファオーバーフローの脆弱性を悪用する攻撃など、さまざまな攻撃が失敗に終わるはずだと主張した。

　NICTAの研究によって生み出された知的財産は、さらなる開発のため、NICTAからスピンオフした企業Open Kernel Labsに受け渡されることになる。今回の研究には4年を要し、NICTAの研究者12人がニューサウスウェールズ大学と合同で実施した。