修 士 論 文 概 要 書
Summary of Master’s Thesis
Date of submission: 01/31/2012 (MM/DD/YYYY) 専攻名（専門分野）
Department
情報理工学専攻
氏 名Name
大須賀 隆彦
指 導 教 員 Advisor
深澤 良彰 印 Seal 研究指導名
Research guidance
ソフトウェア開発 工学研究
学籍番号 Student ID
number
CD
5110B027-5 研究題目
Title UML
モデルからの変換による
Webアプリケーションの形式検証に関する研究
１． はじめに
ソフトウェアの開発工程において，開発者間の相互 理解を目的として統一モデリング言語である UML の普 及が進んでいる．一方で，ソフトウェアの正しさを証明 するためにモデル検査法が注目を浴びてきている．モ デル検査法は実コードに対して検証を行うテスト手法 よりも開発工程の早い段階から適用することが可能で ある．しかし，検証を行う SPIN[1]などのモデル検査器 は，検証のために独自のオートマトン記述を必要として おり，それを入力としなければならない．前述の UML モデルは記述に厳密さを欠くため，モデル検査器への 入力として直接用いることができず，改めて振舞を定 義してモデル記述言語で記述しなければならない．
そこで本研究では，SPIN によるモデル検査法で検 証可能な Promela の作成を，UML モデルから行う手法 を提案する．本論文では，Web アプリケーションを手法 の適用対象とし，その中でも，機能の多様さからくるセ ッション管理の困難さに注目し，携帯電話向けの Web アプリケーションをモデリングの対象とした．
２． 関連研究
Web アプリケーションへのモデル検査法の適用に関 する研究は，文献[2][3]のように画面遷移仕様の整合 性をモデル検査法によって検証するという手法が多く 報告されている．また，文献[4]では，状態爆発を防ぐ ために Web アプリケーションを階層別にモデル化して モデル検査を行う方法を提案している．この文献中で は検証用のモデル生成のための支援ツールの提案も 行っているが，これは Struts を用いて開発されたものを 対象としている．UML モデルからオートマトンへの変換 を行う研究としては文献[5]がある．この文献では UML のアクティビティ図に直接 Promela の構文を記述するこ とで，自動で Promela を生成する手法を提案している．
本研究は特定のフレームワークに依存しない形で開 発される Web アプリケーションを変換の対象としており，
Promela の情報をモデリングの前提としていないため，
これらのアプローチとは異なる．
３． 手法の概要
本手法では，UML モデルから変換によって Promela を生成し，それを組み込んだ 4 つのプロセスを用いて 検証を行う．
図 1 携帯電話向けWebアプリケーションにおける通信の構造
３．１ 情報の抽出と抽象化の手順
本手法は J. Conallen の表記法[6]の拡張を基に，画 面設計を表すクラス図と画面内の処理を表すアクティ ビティ図を対象として情報を抽出し，抽象化(ページ数 の削減)を行って Promela を生成，用意されている Promela に組み込むことで検証を行う．以下に情報の 抽出から抽象化までの手順を示す．
１．クラス図やアクティビティ図からタグ付き値や変数の 値など，必要な情報を抽出する．
2．画面の設計情報を表すクラス図から，HTTPS 通信 を行うかどうか，IP アドレスによる制限を行うかどうか などの情報を取得し，その有無の情報によって 4 つ のグループ分けを行う．
3．(以下グループごとに，)セッションの判定を行ってい ないページ(表示の遷移しかないもの) の集合を取り，
それを 1 つのページとして抽象化する．
4．セッションの判定に同じ機構を使っており，かつセッ ションの判定が成功時と失敗時の 2 パターンに分か れているページを抽出し，その集合 S を取る．
5．前述の集合 S において，セッションの判定に失敗し た場合(認証に失敗した場合)の遷移が同じページ で，かつ判定に成功した場合(認証に成功した場合) の遷移が前述の集合 S に含まれていた場合，それ らのページを 1 つのページとして抽象化する．
３．２ 全体の構成
検証に用いるプロセスの構成を図１に示し，以下に それぞれのプロセスについて簡単に説明を行う．
・ユーザプロセス
携帯電話を通したアクセスとしてゲートウェイに対してリ クエストを送信する動作を繰り返す．
・ゲートウェイプロセス
ユーザのリクエストやサーバからのレスポンスを加工し
て送信先に送信する動作を繰り返す．
・サーバプロセス
リクエストを受け取って処理を行い，レスポンスを返す 動作を繰り返す．UML モデルからの変換は，主にこの 処理の部分を対象としている．
・攻撃者プロセス
セッション管理が適切に行われているかを検証するた め，盗聴を試みたりリクエストの強制を行ったりといった 動作を繰り返す．対象の Web アプリケーションのセッシ ョン管理に脆弱性が存在するならば，攻撃者プロセス がログイン状態となる事例が確認できると考えられる．
３．３ 満たすべき性質の定義
この方法で生成した Promela に対して，以下の 2 つ の項目を満たすべき性質として定義し，検証する．
(A)ユーザがセッションを引き継ぐことが出来るか (B)攻撃者がログイン状態とならないか
４．適用事例
本手法をある Web アプリケーションに対して適用し，
検証を行った結果について述べる．適用対象の Web アプリケーションは 9 つのページを持っており，うち 3 つはログインに成功しないと見ることの出来ない保護さ れたページである．Web アプリケーションの画面を表す クラス図とアクティビティ図の一部を図 2，3 に表し，変 換した Promela 記述の一部を図４に表す．
図 2 適用対象のWeb アプリケーションのクラス図
図 3 アクティビティ図の一部 図 4 出力されたPromela の一部
抽象化と変換を行った結果，ページ数は 4 つとなっ た．変換によって生成された Promela に対して，まず は Cookie，リファラ，ユーザ ID の全てが送出可能な端 末をユーザとして，検証を行った．その結果，(A)，(B) は と も に 期 待 し た 出 力 を 得 る こ と が で き た ． 次 に ， Cookie の送出を行なわず，リファラとユーザ ID の送 出を行う端末をユーザとして検証を行った．その結果，
(A)では期待した出力がされたものの，(B)では攻撃者 がログイン状態となる可能性があるという結果が出力さ れた(図 5，６)．この出力を解析してみると，ユーザはユ
図 5 反例の出力
ーザ ID を用いてセッション管理を行っており，アプリケ ーションはログイン状態をユーザ ID によって判断して いた．ここで，攻撃者プロセスがリクエストを改竄してサ ーバにリクエストを送信したところ，サーバがそのリクエ ストを正常なものとして受け取ってしまい，攻撃者にロ グイン後のページをレスポンスとして送信する，という 手順が得られた．これを踏まえ，クラス図の画面設計に おいて，全てのページに IP アドレスによる制限を掛け，
携帯端末からのアクセスに限定して(ユーザ ID の改竄 を行えない状態にして)再度変換を行い，検証を行っ たところ，(B)においても攻撃者がログインできないとい う期待した結果を得ることができた．
５．おわりに
本論文では， Web アプリケーションのセッション管理 に関する記述に振舞を限定した UML モデルから，情 報 の 抽 出 や 抽 象 化 を 行 い ， SPIN で 検 証 可 能 な Promela へと変換する手法を提案した．また，適用事例 を通してこの手法が適用可能なことや，検証によって 仕様から起こる誤りの発見が行えることを確認できた．
今後は本手法に対する評価法の策定や，反例の解析 への支援策の提案を行いたい．また，今回の変換に用 いた情報はセッション管理に限定しているので，共有 変数を扱う動作を含めるなど，より複雑な事例へも対 応できるようにしていきたい．
参考文献 [1] SPIN ”http://spinroot.com/”
[2] 藤原貴之，岡野浩三，楠本真二，"SPIN による Struts アプリケーションの動作検証を目的としたモデ ル生成手法の提案，"電子情報通信学会技術研究報 告．SS，ソフトウェアサイエンス 2005
[3] 崔銀惠，河本貴則，渡邊宏，"画面遷移仕様のモ デル検査，"コンピュータソフトウェア 2005
[4] 本間圭，高橋薫，富樫敦，"形式的手法による Web アプリケーションのモデル化と検証，"電子情報 通信学会技術研究報告．KBSE，知能ソフトウェア工学 2009
[5] 山田豊，和崎克己，”UML アクティビティ図から SPIN モデル検査用コードの自動生成と Web アプリケ ーション設計への適用，”電子情報通信学会技術研究 報告．SWIM，ソフトウェアインタプライズモデリング 2011
[6] J. Conallen，Building Web Applications with UML，
Addison-Wesley，1999
図6 反例に至るパスの出力(一部)
