システム検証・情報セキュリティ

島川昌也准教授

メールやSNSなど身近なものをはじめ、医療、交通、流通、エネルギー、金融などあらゆる分野でソフトウェアが利用されています。ソフトウェアが正しく動作しない場合、またソフトウェアが行う通信が脆弱で悪意ある第三者からの攻撃を許してしまう場合、甚大な人的・経済的被害が生じえます。
本研究室では、欠陥のないソフトウェアや、攻撃に対してセキュアな通信プロトコル（通信手順）の開発を支援するための研究をしています。特に、形式手法（フォーマルメソッド、formal methods）と呼ばれる数学を基盤としたアプローチにより、ソフトウェアやプロトコルのセキュリティを厳密に検証することに取り組んでいます。

現在の研究

ソフトウェアの仕様・設計に欠陥がないかどうかや、暗号プロトコル（暗号技術を使って実現されるプロトコル）が攻撃に対してセキュアであるかどうかを検証する手法について研究しています。ソフトウェアの仕様・設計やプロトコルを数理論理や状態遷移系を基盤とした言語で厳密に記述・モデル化し、コンピュータを使って網羅的かつ自動的に検証します（図に検証技法の１つであるモデル検査技法の概略を示します）。最大の特徴はその網羅性にあり、このアプローチではあらゆる場合を想定した安全性を検証できます。これにより、場当たり的なテストやレビューでは見つけにくい欠陥を検出できます。
上記のような網羅的な検証は計算コストが高いという問題があるため、より効率的に検証を行う手法の検討や、それを基にした検証ツールの開発を進めています。また、上記の検証技術を応用して、安全であることが保証されたソフトウェアやプロトコルを自動合成する研究にも取り組んでいます。

今後の展望

形式手法・セキュリティ検証は発展途上の分野です。各種問題（上記の計算コストの問題や実践的なノウハウの不足など）から適用範囲もまだまだ限られています。それら問題を解決し、形式手法・セキュリティ検証を通して安全なソフトウェアやプロトコルの開発に貢献していきたいと考えています。