長崎QDG2016_招待講演_01長崎QDG2016の最後のセッションとなる招待講演は「形式手法と、モバイルやアジャイル」と題して、長崎県立大学の日下部 茂 氏にご登壇いただきました。

開発対象のトレンドの観点からAndroidアプリを対象にしたセキュリティモデルの分析での形式手法の活用、開発プロセスの観点からはアジャイルと形式手法の組み合わせによる相乗効果の追求といった事例、動向をご紹介いただきました。セッションのアブストラクトは次の通りです。

■アブストラクト

「 形式手法なんて日々の活動とは縁遠いイメージをお持ちでしょうか? 本発表では、開発対象のトレンドの観点からはAndroidアプリを対象にしたセキュリティモデルの分析での形式手法の活用、開発プロセスの観点からはアジャイルと形式手法の組み合わせによる相乗効果の追求、といった事例や動向を紹介します。」

セッションでは、何かと堅いイメージで捉えられる形式手法を最近の動向を交えてご解説いただきました。この様子をレポートします。

 ■アジャイルと形式手法の組み合わせ

 形式手法の動向として、より効果的に開発を進める取り組みから、開発プロセスにおけるアジャイルと形式手法の組み合わせについて紹介いただきました。開発プロセスをいくつかの要因の組み合わせで評価した資料を取り上げ、ライフサイクル全体で評価した時アジャイルはプロセスとしてどう評価できるかを解説いただきました。アジャイルを適用すれば全てがうまくいくということはなく、全体で評価してみるとアジャイルにも設計ドキュメントの整備などの弱点があり、形式手法を活用することでアジャイルの欠点を補完できるとしました。Agileフレームワークの検証へのモデル検査の適用、TDDへの適用、自然言語記述からのモデル生成など、効果的に組み合わせることで相乗効果が発揮できるとのことです。また、証明を用いるような形式手法であっても、開発メンバ、開発プロセスを整えることができればアジャイルへの適用は可能であり、実際に事例もあるとのことです。

■Androidアプリを対象にしたセキュリティモデルの分析での形式手法の活用

 次に、アプリケーション単体ではなく、アプリケーション間連携時におけるセキュリティの問題を検出したいという目的で、形式手法を活用した事例を紹介いただきました。この事例では仕様記述言語としては”Alloy”を選択し、分析器は”Alloy Analyzer”を使用したとのことでした。Alloyを選択した理由としては、理解が容易であることやツールの支援が充実していることなどが挙げられました。

 セキュリティの問題として”Intent Hijack” が例示されました。例えば「デバイスの位置情報を外部に送信するため、アプリケーションの脆弱性を利用する」というものです。 Androidフレームワークの形式的モデルは、モデル抽出器とシグネチャを対応付け、モデルをインプットにして反例を見つけるものだとのことでした。これにより、想定していないパーミッションがないかなどを発見できるそうです。また、検証するためにソースコードは必要なく、スマートフォンから検証できるというのも目新しく感じられました。

 ■ハザード分析法 ”STAMP”の紹介

 ソフトウェア関連の事故や障害の発生を防ぐため、安全性の向上が求められています。しかし、IoTに代表されるように様々なものがつながって相互作用を持ち得る現代においては個々のソフトウェアの信頼性を高めるだけでは不十分であり、より包括的な観点で確認しなければ安全性を確保することは難しくなってきています。この問題への対応として、相互作用とコントロールに着目したハザード分析法”STAMP”が紹介されました。STAMPを用いることで、ソフトウェアやハードウェア、社会システムも含む包括的な分析が可能になるということです。また、STAMPは相互作用に着目するので、プロセス改善といった技術分野にも応用することもできるとのことでした。

STAMPについては日本でもワークショップが開催されるとのことで、興味のある方は参加を検討してみてはいかがでしょうか。(第1回 STAMPワークショップ in Japan

 当日の参加者は、普段の開発は形式手法について触れる機会がそれほど得られていないようでしたが、それだけに参考になったようです。ソフトウェア品質を確保していくためにはソフトウェアテスト技術以外の技術も活用していく必要があり、形式手法の活用も今後さらに重要になっていくと感じました。

(報告:藤沢 耕助)