Web アプリケーションの形式検証に関する研究

(1)

2011 年度修士論文

UML モデルからの変換による

Web アプリケーションの形式検証に関する研究

2012 年 1 月 31 日 ( 火 ) 提出

指導 : ^{深澤良彰教授}

早稲田大学大学院基幹理工学研究科情報理工学専攻

学籍番号 : 5110B027-5

大須賀隆彦

(2)

第1章はじめに 1

第2章研究背景 3

2.1 Webアプリケーション . . . . 3

2.1.1 Webアプリケーション概要 . . . . 3

2.1.2 携帯電話向けのWebアプリケーション概要 . . . . 4

2.1.3 携帯電話向けのWebアプリケーションにおけるセッション管理 . . . . 4

2.1.4 携帯電話向けのWebアプリケーションにおけるセッション管理の問題点 . . . . 6

2.2 形式手法 . . . . 7

2.2.1 形式手法の概要 . . . . 7

2.2.2 モデル検査法 . . . . 8

2.2.3 テスト手法とモデル検査法の相違点 . . . . 8

第3章関連研究 10 3.1 関連研究 . . . . 10

第4章手法の概要 12 4.1 Promelaで用いるプロセス全体の構成 . . . . 12

4.1.1 ユーザプロセス . . . . 12

4.1.2 ゲートウェイプロセス . . . . 13

4.1.3 サーバプロセス . . . . 14

4.1.4 攻撃者プロセス . . . . 14

4.2 入力となるUMLモデルの構成. . . . 14

4.2.1 画面の遷移情報と設計情報を表すクラス図 . . . . 15

(3)

4.3.1 画面情報の抽出と抽象化 . . . . 20 4.3.2 変換と変換されたPromelaの不変部分への組込 . . . . 21 4.4 検証すべき項目の定義 . . . . 23

第5章適用事例と結果 25

5.1 適用事例で用いたWebアプリケーションとUMLモデルの概要 . . . 25 5.2 変換結果 . . . . 26 5.3 検証結果と考察 . . . . 27

5.3.1 Cookie，リファラ，ユーザIDの全てを送出する端末による検証 . . . . 27 5.3.2 Cookieを送出せず，リファラ，ユーザIDを送出する端末に

よる検証 . . . . 28

第6章今後の課題 31

第7章おわりに 33

謝辞 34

付録A 適用事例で用いたUMLモデル 38 付録B 適用事例におけるUMLモデルのPromela記述への変換結果 43

(4)

ソフトウェアの開発工程において，開発者間の相互理解を目的とした統一モデリング言語であるUMLの普及が進んでいる．開発の上流工程においては，UML[1]

を用いた設計や分析のモデルを生成することが多く，その開発成果物であるモデルを基に実装や検証を進めていくことが多い．

一方で，ソフトウェアの正しさを証明するために，形式検証手法の一つであるモデル検査法が注目を浴びてきている[5]．モデル検査法は，ある特定の振舞に着目して対象のシステムを抽象化し，その抽象化した有限オートマトンを網羅的に検査して，満たすべき性質を満たしているか，デッドロックが発生しないかといった検査を行う．このモデル検査法は，抽象化したモデルに対する検査であるため，

実コードに対する検証を行うテスト手法よりも早い段階の開発工程から適用することが可能となる．しかし，検証を行うために用いるSPIN[2]などのモデル検査器は，検証のために対象システムの振舞を変えない形で適切に抽象化することが必要であり，また，抽象化を行う際に独自言語によるオートマトン記述を用いて，それを入力としなければならない．先に述べた開発成果物としてのUMLモデルは記述に厳密さを欠くため，モデル検査器への入力として用いる際には直接入力として使用できず，改めて振舞を定義し，モデル記述言語で記述しなければならない．

そこで本研究では，SPINによるモデル検査法で検証可能なオートマトンの作成を，UMLのモデルから行う手法を提案する．UMLモデルからモデル検査法で検証可能なオートマトンを作成する手法はいくつか報告されているが，関連研究では，UMLモデルにオートマトン記述言語の構文要素を付加している．しかしながら，上流工程の開発成果物としてのUMLモデルを扱うことを前提とすると，このような方法は不適切な情報を必要とすることになる．本研究では，検証におけるオートマトン生成のための情報を付加することを前提とせず，上流工程における開発成果物であるUMLモデルに記述された情報のみに基づいて，オートマトンに変換する方法を提案する．

本論文では，アプリケーションを手法の適用対象とした．その中でも，機

(5)

の変換を行った．

本論文の構成を述べる．第2章では本研究の背景として，携帯電話向けのWeb アプリケーションの概要と形式検証手法の概要について述べる．第3章では，関連研究と本研究のアプローチについて説明し，第4章では手法の概要について説明する．第5章では実際にあるWebアプリケーションに対して本手法を適用した事例と考察を述べ，第6章では今後の課題について述べる．

(6)

本項では，Webアプリケーショの概要や，携帯電話向けのWebアプリケーションとの相違点，セッション管理の方法について説明する．また，検証のために用いる形式手法の概要について述べる．

2.1 Web アプリケーション

2.1.1 Web アプリケーション概要

WebアプリケーションはWebの機能を利用したアプリケーションであり，クライアントサーバシステムに基づいて，サービスを利用する側であるクライアントとそのサービスを提供する側であるサーバの2者間を，HTTP通信によって接続している．

従来のWebページとは異なり，Webアプリケーションではプログラムの実行によってデータの処理やその処理結果を動的にページ内に埋め込むことができ，それをクライアント側にレスポンスとして返すことができる．これにより，クライアント側では時間の掛かる処理をサーバ側のアプリケーションで行ったり，アクセスをしてきたクライアントに識別のためのIDを紐付け，以降はIDによってアクセス元がどのクライアントであるかの判別を行うセッション管理を実現したりするなど，静的なWebページに比べてより高機能なアプリケーションの利用が可能となっている．一般的なWebアプリケーションの構成を図2.1に示す．

(7)

平成23年度修士論文

早稲田大学基幹理工学研究科情報理工学専攻深澤研究室

図 2.1: 一般的なWebアプリケーションの構成

2.1.2 携帯電話向けの Web アプリケーション概要

携帯電話の端末は，機種ごとにWebアプリケーションを利用するためのブラウザの機能が異なり，使える機能が限られている．また，携帯電話からWebアプリケーションを利用する際には，一般的な端末とは異なり，端末であるブラウザからサーバまでリクエストが送られるまでに一度ゲートウェイを通過し，そこでリクエストの加工が行われる．携帯電話向けのWebアプリケーションの構成を図2.2 に示す．

2.1.3 携帯電話向けの Web アプリケーションにおけるセッション

管理

一般的なWebアプリケーションでは，アクセスされたクライアントを識別するためのIDを，Cookieを用いて管理する場合が多い．しかし，2.1.2節で説明したように，携帯電話の端末では使える機能に制限があり，Cookieをサポートしてい

(8)

図 2.2: 携帯電話向けのWebアプリケーションの構成

ない機種も多い．ここで，携帯電話向けのWebアプリケーションで一般的に使われるセッション管理の方式について説明する．

Cookieによるセッション管理

Cookieによるセッション管理は，アプリケーションがリクエストを送信してきた

携帯端末のブラウザに対してHTTPヘッダに乗せたCookieを発行し，以降はブラウザがリクエストヘッダにCookieを埋め込んで送信することで，セッションを確立する方式である．Cookieを用いたセッション管理は通常のWebアプリケーションにおいて広く用いられているが，携帯端末ではこの機能が実装されていない場合も多く，その場合は別の方法でセッション管理を行わなくてはならない．一般的

に，CookieはHTTPによる通信において平文でパケットの送受信が行われるため，

HTTPヘッダに埋め込まれたCookieはパケットの盗聴に遭った時点で漏洩してしまう．本論文においても，HTTPによる通信ではCookieの盗聴が可能なものとして扱う．これを防ぐための方法として，HTTPS(HTTP over SSL/TLS)通信を用いて暗号化を行うことや，Cookieにsecure属性を付け，HTTP通信ではCookieを送出しないようにするような対策を取ることが考えられる．

(9)

URLリライティングによるセッション管理

URLリライティングは，URLのクエリストリング上にセッションIDを埋め込んで，セッション管理を行う方式である．URLリライティングは，Cookieを保存する機構がない携帯端末においてセッションの判定を行うために利用されてきた．

URLリライティングでは，もしクエリストリング上のセッションIDのみで判定を行っていた場合，端末のリファラが送出されることによってアクセス先のサーバへセッションIDが漏洩してしまう．悪意のある第三者がユーザの端末を自分の管轄内のサーバへと誘導し，そこでリファラが送出された場合，そのログから取り出したセッションIDを用いて，第三者がログイン状態となってしまう可能性がある．

ユーザIDによるセッション管理

携帯電話向けのWebアプリケーションにおいてはしばしば端末や契約者固有の IDによってセッション管理が行われる．これは，契約者や端末ごとに一意に与えられたIDを，ゲートウェイや端末から送信し，それを基にセッション管理を行う方式である．このIDはキャリアによって種類が異なり，また名前や仕様が異なるため，本論文ではこのIDをユーザIDと呼び，ユーザの端末から送信されるものとする．ユーザの端末から送信されるため，HTTPS通信でも送出されるが，ゲートウェイを通したアクセスではユーザも攻撃者もユーザIDの偽装は不可能とする．

ここで，ユーザIDの特長として，セッションIDとして用いる場合に全てのアプリケーションへ同じIDが送信されるという性質がある．そのため，ユーザID は前述の盗聴が起こりえずとも，攻撃者が自分の管轄内のサーバへのアクセスを誘導することによって簡単に取得されてしまう情報である．さらに，このユーザ IDは更新等の動作が行えるセッションIDとは違い，半永久的に使用可能である．

そこで，本論文ではユーザIDは攻撃者も既知のものであり，IPアドレスによって携帯電話によるアクセスであると判断された場合には，HTTP/HTTPS通信に関わらず，ユーザIDの詐称は起こらないものと仮定して，このユーザIDによる検査を行う．

2.1.4 携帯電話向けの Web アプリケーションにおけるセッション

管理の問題点

携帯電話向けのセッション管理は，携帯電話の端末では使える機能に制限があり，Cookieをサポートしていない機種も多いという背景から，開発者が端末の持

(10)

つ機能の差異に対応しなければならないという問題がある．もし，端末の持つ機能に応じて適切なセッションIDの管理方式を実現できなければ，そこからセッションIDが攻撃者に漏れ，情報が漏洩するという事態が起こってしまう．しかし，上流工程の成果物である仕様から，一般的に行われるレビューなどの方法で「抜け」

や「漏れ」なく検証を行うことは難しい．

2.2 形式手法

本項では，形式手法の概要と，本研究で用いるモデル検査法の説明，またシステムの検証にテスト手法を適用した場合とモデル検査法を適用した場合の相違点について述べる．

2.2.1 形式手法の概要

形式手法は，数理論理学に基づいて，ハードウェアやソフトウェアの品質や信頼性向上のための記述や検証を行うための技術である．開発工程において，開発の対象となるシステムの仕様は何らかの形で記述されている必要がある．一般的に用いられる自然言語による仕様は，あいまいな表現や記述があり，定義が明確であるとは言い難い．そこで，対象とするシステムの性質や条件などを記述する際，

曖昧さや矛盾などを排除した厳密な記述方法で仕様を定義するために，形式仕様記述という技術が用いられている．

形式仕様記述は，形式手法の一つであり，形式仕様記述言語を用いて記述する．

事前条件や事後条件，処理の内容や性質などを明確に定義できる形式仕様記述言語を用いて仕様を記述することによって，自然言語による仕様で散見していた曖昧さなどを排除し，仕様の品質を向上させることができる．形式仕様言語としては，VDMやZ記法，Bメソッドが代表的なものとして挙げられる．

また，形式仕様記述言語によって定義された仕様を用いてシステムが正しいことを検証する，形式検証と呼ばれる手法がある．形式検証の中でも，厳密に定義された仕様と，システムの振舞の整合性が取れているかどうかを検査する手法をモデル検査法といい，本研究で用いるモデル検査法も，この形式検証に分類できる．モデル検査を行うモデル検査器としては，SPINやUPPAALといったツールが多く使われている．

(11)

2.2.2 モデル検査法

モデル検査法は，形式検証の一つである．検証の対象となるシステムを抽象化した有限オートマトンに対して，デッドロックの検出や満たすべき性質をあらわした時相論理式が満たされているかを網羅的にチェックすることのできる技術である．抽象化した有限オートマトン，時相論理式をモデル検査ツールに入力すると，

自動で検証を行い，入力されたシステムが時相論理式を満たしているかどうかを解析する．時相論理式が満たされない場合は，満たされない状態に至るまでの具体的なパス(経路)を出力し，それを解析することで何が原因で検証に失敗したかを知ることができる．

2.2.3 テスト手法とモデル検査法の相違点

モデル検査法は網羅的な探索を行うため，抽象化されたオートマトンが取りうる全ての状態を検査し，レビューやテストといった検証手法に見られるような「抜け」や「漏れ」の可能性を排除して対象システムを完全に検査することができるという特徴がある．さらに，モデル検査法ではオートマトンに非決定的な振舞を記述することで，非決定的に発生するデッドロックやバグについても検証を行うことができる．非決定的な振舞を考慮したオートマトンを網羅的に探索することで，テストでは発見が難しかったり，想定していなかったりした不具合を検出できる可能性があることが特徴として挙げられる．

次に，手法適用の上で前提となる入力を考えてみる．テストにおいて適用に必要なものを考えると，実装したプログラムコード，適用するためのテストケースが挙げられる．一方，モデル検査法において適用に必要なものは，抽象化したオートマトンと，満たすべき性質を記述した時相論理式である．そのため，適用工程に関して，テスト手法の適用は実装が終わった後の下流工程に限られるのに対し，

モデル検査法は対象システムの適切な抽象化を行えば，下流工程だけでなく，プログラムコードの実装が終わっていない上流工程においても検証を行うことが可能である．そのため，上流工程で不具合が発見できた場合は，手戻りも少なく，修正にかかる手間も少ないというメリットが挙げられる．一方，テスト手法が実際のプログラムコードに対して正しさを検証するのに対し，モデル検査法では抽象化を行ったオートマトンに対して検証を行う．そのため，捨象されることとなった振舞や，実装上の不具合といった部分に関しては，正しさを検証することができない．

また，テストを行った場合には，バグが見つかると異常を示す結果だけが出力される．それに対して，モデル検査法を適用した場合は，満たすべき性質が満たさ

(12)

れないと判定された状態やデッドロックが発見されたときに，その反例となる状態に至るまでの遷移を出力することができる．その状態遷移の出力を解析することで，どこに不具合があるのかを検証することが可能となるといった違いがある．

(13)

第 3 ^{章関連研究}

本章では，Webアプリケーションに対してモデル検査を適用する関連研究やUML モデルから変換を行ってモデル検査を行う既存研究について説明する．また，本研究の対象とそれらの既存研究との違いを述べる．

3.1 関連研究

形式検証の技術は注目を浴びている．従来はハードウェアの分野への適用が多かった形式検証技術だが，CPUの性能の向上や，効率的な手法が実装されたことにより，ソフトウェアへの適用例も徐々に増えてきている．それに伴い，モデル検査法をソフトウェアに適用した研究は数多く報告されている．

Webアプリケーションへの適用に関する研究を挙げると，文献[6][7][8]のように，画面遷移仕様の整合性をモデル検査法によって形式的に検証するという手法が多く報告されている．これらは画面の遷移情報を基に，デッドロックの発生や，

リクエストの二重送信時の動作などを検証対象としている．

文献[9]では，Webアプリケーションの画面遷移図と内部状態を統合した有限オートマトンを作成し，モデル検査を行う方法が提案されている．

文献[10]では，状態爆発を防ぐためにWebアプリケーションを階層別にモデル化して，モデル検査を行う方法を提案している．この文献中では検証用のモデル生成のための支援ツールの提案も行っているが，これはWebアプリケーションフレームワークであるStrutsを用いて開発されたWebアプリケーションを対象としている．

文献[11]では攻撃者をモデル化し，Cookieを用いたセッション管理の欠陥をモデル検査法で発見する手法の提案を行っている．これはCookieによるセッション管理に限られ，またWebアプリケーションの画面遷移仕様からの抽象化，抽象化した画面遷移仕様からのPromelaへの変換は手動で行っている．

ソフトウェア開発では対象となるシステムの構造や振舞のモデルを記述するためにUMLを用いることが多くある．UMLはモデリング言語であり，形式仕様記

(14)

述や形式検証を目的として言語仕様が定義されているわけではない．しかし，現実の開発成果物としてUMLモデルが広く用いられていることから，これを用いた形式検証技術が提案されている．それらの技術では，UMLモデルからのオートマトンなどの形式記述に変換することで形式検証技術を適用可能にする手法が多く用いられている．

UMLモデルからオートマトンへの変換を行う研究としては文献[12]がある．この文献では，UMLのアクティビティ図に直接Promelaの構文を記述することで，

自動でPromelaを生成する手法を実現し，その手法をWebアプリケーションの設

計へと適用し，有用性を確認している．

本研究は、特定のフレームワークに依存しない形で開発されるWebアプリケーションを変換の対象としている．また，携帯電話向けのWebアプリケーションにおけるサーバ側の処理のみを変換の対象とすることから，Promelaの情報をモデリングの前提としておらず，Promelaの構文を知らない開発者でも検証可能となるため，これらのアプローチとは異なる．

(15)

第 4 ^{章手法の概要}

本章では，変換に必要となるUMLモデルの情報やそれぞれの図の記述方法，そのUMLモデルの情報を用いてSPINで検証可能なPromela記述へと変換する手法について述べる．

4.1 Promela で用いるプロセス全体の構成

一般的なWebアプリケーションでは，リクエストがユーザの操作するブラウザ上からサーバに直接送られるため，関係するのはユーザとサーバ(アプリケーション) のみである．だが，2.1.2節で述べた通り，携帯電話向けのWebアプリケーションを考える上で，ユーザの送信したリクエストがゲートウェイ上で加工されてサーバへと送信されることを考慮しなければならない．この動作を表現するために，ユーザプロセスとサーバプロセスの他にゲートウェイプロセスを定義し，検証を行うこととした．

図4.1に想定している携帯電話向けWebアプリケーションにおける通信の構造を示す．また，以下にユーザプロセス，ゲートウェイプロセス，サーバプロセス，

攻撃者プロセスについて，詳細を説明する．

4.1.1 ユーザプロセス

ユーザプロセスは，Webブラウザを通してリクエストの送信を行うものとして設計される．本研究では，携帯電話向けのWebアプリケーションを携帯電話の対象としているため，携帯電話のWebブラウザを通したアクセスとして，ゲートウェイに対してリクエストを送信し，サーバからのレスポンスを待つという動作を繰り返すものとして扱う．

この時，ユーザはブラウザの「戻る」ボタンや，別のウインドウ(タブ)からのアクセスを行うなど，通常のリンクによらない画面の遷移を行う可能性がある．これを考慮し，ユーザプロセスはページを選択する際，ページ内に含まれるリンク

(16)

図 4.1: 携帯電話向けWebアプリケーションにおける通信の構造

情報に限定されず，Webアプリケーションが持つ全てのページを(非決定的に)選択可能とする．

4.1.2 ゲートウェイプロセス

ゲートウェイプロセスは，ユーザ(携帯端末)とサーバ(アプリケーション)間の通信を中継するものとして設計され，ユーザからのリクエストやサーバからのレスポンスに対して，ユーザIDの付加や加工，Cookieの格納といった動作を行い，

送信先へと送信することを繰り返すものとして扱う．

通常，携帯電話からのアクセスを識別するために，IPアドレスの帯域を参照することによってその端末がゲートウェイを通った携帯端末であるかどうかを判別する場合が多い．そこで，本論文においてゲートウェイを通したアクセスは全て，

IPアドレスの帯域を判定することにより携帯端末が送信元であるかが識別できることが保証されていると仮定し，さらにこのIPアドレスは詐称できないものとして扱うこととする．

(17)

4.1.3 サーバプロセス

サーバプロセスは，リクエストを受け取って処理を行うアプリケーションとして設計され，リクエストの受信や処理，レスポンスの送信といった動作を繰り返す．

サーバプロセスにおいて可変な部分は，ロジックによって動作が変わる処理の部分である．この処理の部分を変換の対象とすることで，チャネルによって実現されるプロセス間の通信に依存せず，情報の付加を必要としないUMLモデルからのPromelaへの変換を実現している．

4.1.4 攻撃者プロセス

セッション管理における検証を考えたときに，セッションの引き継ぎが正常に行われているかと同時に，セッションIDの漏洩が起こっていないかを検査しなくてはならない．セッションIDが漏洩することにより，IDやパスワードを知らない人間が他人の個人情報や内部の情報を閲覧可能になってしまう可能性があるためである．そこで，文献[11]と同様に，通常のユーザの動作とは異なる動作を行う攻撃者プロセスを用意する．

この攻撃者プロセスは，通常のアクセスに紛れて，ゲートウェイを通したアクセスや，通常のWebアプリケーションに対するアクセスと同様に直接サーバに対してアクセスを試みる(図4.1における点線部を参照)ように設計される．その他にも，HTTP通信の盗聴，ユーザIDの詐称やユーザへのリクエスト強制といった行為を選択可能にしている．もし，これらの動作によって攻撃者が(本来アクセスすることのできない) ログイン後のページを取得することができたならば，検証対象となるWebアプリケーションにおけるセッション管理の脆弱性が存在していることを確認でき，反例によってどのような手段でその状態に至ったかを解析できる．

これら全てのプロセスにおける，リクエストやレスポンスの送受信は，Promela の機能の一つであるチャネルを用いて実現することとした．

4.2 ^{入力となる} UML ^{モデルの構成}

本手法は，Webアプリケーション開発における上流工程の開発成果物として生成されるUMLモデルを基に，変換を行う．本研究において入力とする情報は，Web アプリケーションにおける画面の遷移情報や設計情報を表すクラス図と，その画

(18)

面個々が行っているセッション関連の処理を記述したアクティビティ図である．以下，二つの図について必要な情報や定義についての説明を行う．

4.2.1 画面の遷移情報と設計情報を表すクラス図

Webアプリケーション開発において，上流工程の開発成果物として画面の遷移情報を表す画面遷移図を作成することが多い．画面遷移図の記述方法としては様々なものがあるが，本研究ではJim Conallenの手法[13]を参考に，一つのクラス図と画面を対応させ，クラス図によって画面の遷移情報・設計情報を記述するという方法を用いることとする．

ステレオタイプ<<Secure Page>>

クラス図によって画面の遷移情報や設計情報を記述する際に，セッションの管理を判定するための情報として，<<Secure Page>>というステレオタイプを定義し，

これによってページが秘匿されていることを表すこととする．<<Secure Page>>タ グはオートマトン生成のための付加ではなく，Jim ConallenによるUMLモデルでは表現できない部分を補うための拡張となっているため，Webアプリケーション開発における上流工程の成果物として自然なモデリングとなっている．この<<Secure Page>>タグはタグ付き値としてUseHTTPSとRestrictedByIPAddressという値を持っている．これらはどちらもBoolean型の変数として定義されており，UseHTTPS は該当するページ(クラス)がHTTPS 通信を要求する際にtrueとしてHTTP通信を要求する際にはfalseとなる．RestrictedByIPAddressは該当するページがIP アドレスによって携帯電話からのアクセスであるかを判定して携帯端末以外からのアクセスをはじく場合にtrueとして，携帯電話からのアクセスに制限せず全てのアクセスを許容する際にはfalseとなる．<<Secure Page>>の定義を，図4.2に示す．また，実際に<<Secure Page >>タグを使用してクラス図を記述した記述例を，図4.3に示す．本例では，topページとprofileページの二つのページの設計情報・遷移情報をクラス図によって表している．これらのページは双方向にリンクがあり，topページはIPアドレスによる制限のみが掛けられていてHTTPによる通信でページを要求すること，profileページにはIPアドレスによる制限の他に

HTTPSによる通信が要求されていることを，タグ付き値から読み取ることがで

きる．

(19)

図 4.2: <<Secure Page>>の定義

図 4.3: <<Secure Page>>タグの使用例

のようにどちらもfalse(HTTPS通信を要求せず，IPアドレスによる制限も行わない)として扱うこととする．

4.2.2 画面の処理を表すアクティビティ図

4.2.1節で記述されたそれぞれの画面には，Webアプリケーション固有のロジッ

クが存在している．どの画面を表示するかの情報や，セッション関連の処理をどのように行うかのロジックは，アクティビティ図を用いて記述する．本手法においては変換を容易にするため，アクティビティ図に記述できる情報は，開始状態・

終了状態・遷移・ディシジョンノード・アクティビティとし，それらの要素のみでロジックの記述を行うこととした．

(20)

図 4.4: <<Secure Page>>タグ省略時の解釈

アクティビティ図は処理の手順を示すための図であり，そのアクティビティには自然言語で動作を記述する．しかし，自然言語で書かれたアクティビティは開発者の記述方法によって解釈の違いが発生し，形式的な意味を定義できないため，

そのままではオートマトンへと変換することは難しい．そこで，Webアプリケーションのセッション管理関連の動作に振舞を限定し，記述の限定を行った．

まずは，セッションの管理を行う上でその処理の判定として，以下の情報が必要だと考えられる．

• どの機構でセッションを行うかを判断する時に使用する端末の機能の情報

• セッション管理の処理に用いる送信されたセッションIDの情報

• ユーザから送信されたパスワードの情報

そこで，これらの情報を表4.1，表4.2，表4.3で表す形式の変数で表現し，アクティビティ図へ記述することとする．また，セッション管理の情報を用いた処理フローを考えたときに，セッションIDを用いて行われる処理の典型的な動作は，以下の4つに分類できる．

表 4.1: 端末の機能の情報

機能判定用の変数名型説明 true false mobileCookie bool 端末のCookie機能保存可保存不可

mobileReferer bool 端末のリファラ送信送信非送信

mobileSubID bool 端末の固有ID送信送信非送信

(21)

表 4.2: セッションIDの情報セッション判定用の

変数名

型説明

cookie byte CookieのセッションID

scookie byte Cookie(secure属性)のセッションID

query byte クエリストリングのセッションID

subID byte ユーザID

表 4.3: パスワードの情報

パスワード型説明 true false

pass bool パスワードの値正誤

• 送信されたセッションIDを開始(有効に)する

• 送信されたセッションIDを新たなセッションIDに書き換える

• 送信されたセッションIDを終了(無効に)する

• 送信されたセッションIDが有効か無効かを判定する

そこで，セッションIDを用いて行われる処理は表4.4 のような表記方法でアクティビティ図へ記述することとする．

ステレオタイプ<<display>>

また，サーバ側のロジックとして，セッション管理に関する処理の情報以外にも，画面の表示に関する情報も必要である．認証の成功によってどのページが表示されるのか，失敗によってどのページが表示されるのかを，セッションの処理に併せて記述しなくてはならない．そこで，サーバ側がどのページを表示するかという情報を<<display>>というステレオタイプを定義してアクションに付加することで，画面の表示と情報を表すこととする．<<display>>の定義を，図4.5に示す．また，実際に<<display>>タグを使用してアクティビティ図を記述した記述例を，図4.6に示す．

(22)

表 4.4: セッションの処理を行うアクションの情報

アクション名(引数) 返り値説明 true false

start(byte) void 該当のセッション

IDを有効にする regenerate(byte) void 該当のセッション

IDを再生成する destroy(byte) void 該当のセッション

IDを無効にする

check(byte) bool 該当のセッション

IDを判定する

認証済未認証

<<display>>タグも前述の<<Secure Page>>タグと同様に，Jim ConallenによるUMLモデルの拡張となっているため，オートマトン生成のための付加ではない自然なモデリングとなっている．

この<<display>>タグはタグ付き値としてnameという値を持っている．これはString型の変数として定義されており，このnameに4.2.1節で定義した画面を表すクラス図の名前を対応付ける．

アクティビティ図における終了状態の前には必ず<<display>>タグの付いたアクティビティが配置されるという条件を設けることで，ユーザのリクエストに対して何らかのページの表示を行うことができ，ページの表示ができないデッドロックの状態を回避することができる．

これらの方法により，アクティビティ内の自然言語の曖昧さに寄らない変換を可能とした．

4.3 UML モデルから Promela への変換方法

本手法はUMLモデルからPromelaを生成するまでに，情報の抽出を行い抽象化を行ってから，変換してSPINで検証可能なコードを出力するという手順を踏む．

以下にそれぞれの手順を示す．

(23)

図 4.5: <<display>>の定義

図 4.6: <<display>>タグの使用例

4.3.1 画面情報の抽出と抽象化

変換のために，まずはUMLモデルから必要な情報を抽出することが必要である．ここで，モデル検査法は網羅的な探索が可能な反面，状態数の増加によって指数関数的に増大する検証時間が問題となる．そこで，情報を抽出して変換を行う過程において，ページの抽象化を行い，状態数の削減を行う．抽象化の手順を，

以下のように定義する．

1. クラス図やアクティビティ図からタグ付き値や変数の値など，必要な情報を抽出する．(本研究ではUMLモデリングツールであるastah*[4]を用いてクラス図，アクティビティ図を作成しているため，astah*におけるAPIを用いて情報の抽出を行う．)

2. 画面の設計情報を表すクラス図から，HTTPS通信を行うかどうか，IPアド

(24)

レスによる制限を行うかどうかなど，<<Secure Page>>のタグ付き値を取得し，その有無の情報によって4つのグループ分けを行う．

3. セッションの判定を行っていないページ(<<display>>タグによる表示の遷移しかないもの)の集合を取り，それを一つのページとして抽象化する．

4. セッションの判定に同じ機構を使っており，かつセッションの判定が成功時と失敗時の2パターンに分かれているページを抽出し，その集合Sを取る．

5. 前述の集合Sにおいて，セッションの判定に失敗した場合(認証に失敗した場合)の遷移が同じページで，かつ判定に成功した場合(認証に成功した場合) の遷移が前述の集合Sに含まれていた場合，それらのページを一つのページとして抽象化する．

4.3.2 変換と変換された Promela の不変部分への組込

次に，抽象化されたページを変換し，Promelaで検証可能な形に組み込む手法を説明する．

1. 4.3.1節において抽象化されたページについて，そのうちの一つのページ(任

意)の名前を抽出し，「display ページの名前」という形式で該当のページとラベルの対応付けを行う．

2. セッションの処理を記述したアクティビティをPromelaへと変換する．その際，ディシジョンノードはif文の分岐として扱い，ガード条件をif文の分岐条件として扱う．(変換前のディシジョンノードの様子を図4.7に表し，その図をPromelaへと変換した結果となるPromelaの構文を図4.8に示す．) start() などのアクションは，それぞれ対応付けられたPromelaへと変換を行う．

3. ページ番号と「display ページの名前」を対応付けて，ページ番号をユーザや攻撃者プロセスの選択肢として選択可能な状態にする．その際，番号の選

択肢はPromelaのif文を利用して常に全ページが選択可能な状態とし，非決

定的にページを選択していくものとする．

4. HTTPS通信が要求されているページや，IPアドレスによって携帯電話から

(25)

早稲田大学基幹理工学研究科情報理工学専攻深澤研究室クセス不可である旨を示すページ番号を用意し，そこへと誘導することで，

アクセス不能である事を表現する．

図 4.7: ディシジョンノードの記述例

図 4.8: 記述例で用いたディシジョンノードの変換後となるPromela構文

(26)

4.4 検証すべき項目の定義

Webアプリケーションのセッション管理が適切に行われているかを調べる上で，

満たすべき性質として考えられるのは，以下の2項目である．

(A) (パスワードを知っている)ユーザがセッションの情報を引き継いでログイン

状態になることができる

(B) 攻撃者(ログインする権限を持っていないユーザ)がログイン状態になることはない

これを検出するためには，セッションの引継ぎが正常に行われたかの判定と，攻撃者がログイン状態となった判定が必要である．そこで，今回はセッションの判定が成功した時にtrueとなる変数V1と，攻撃者が有効なセッションIDを持ったままアプリケーションにアクセスし，ログイン状態となった時にtrueとなる変数 V2を用意した．

V1は，認証を行っているページにおいて，認証が成功したら成功したことを示すためにtrueとなるbool型の変数であり，モデル内のセッションによる判定(check()) がtrueとなった後にtrueとすることで，自動的に付与することができる．V2は，

攻撃者が有効なセッションID持った状態でログイン状態にアクセスした時を定義することで，人手によって付与することができる．よって，LTL式で表される時相論理式は，以下の二つの式で表すことができる．それぞれが前述の性質(A)，(B) に対応する．

(A’) ! <>p #define p V1 == true (B’) ! <>p #define p V2 == true

検証の結果として，(A’)ではnot valid(満たさない)としてユーザがセッションを保って正常にアクセスできることを期待し，(B’)ではvalid(満たしている)として攻撃者がログイン状態とならないことを期待する．モデル検査法においては，not

validとして検証式が満たされない場合，満たされない状態に至るまでのパスが出

力される．よって，(A’)で期待した出力があった場合，ユーザがログイン状態となるまでの遷移(の一例)を確認することができる．

もし，で満たしているという期待しない結果が出た場合は，ユーザ

(27)

早稲田大学基幹理工学研究科情報理工学専攻深澤研究室ことを示している．この場合においても，反例に至るまでのパスが出力されるため，どのような手順で攻撃者が盗聴を行いログイン状態まで至ったかという経緯の一例を出力させることができるため，開発者がモデルを修正する上で，どこに不具合があるかの解析に役立たせることができる．

以上の手順により，UMLのモデルからPromelaへの変換を行う．

(28)

この節では，あるWebアプリケーションに対して本手法を適用して変換を行い，

検証を行った結果について述べる．

5.1 ^{適用事例で用いた} Web ^{アプリケーションと} UML モデルの概要

適用対象となるWebアプリケーションは，9個のページを持っており，うち3個のページはログインに成功しないと閲覧ができない保護されたページを表すものである．このアプリケーションの画面遷移情報を表すクラス図を，図5.1 に示す．

また，各々のクラス図にはページ内の処理を表すアクティビティ図が対応している．図5.2に一例として，loginページに対応付けられたアクティビティ図の一部を示す．

(29)

図 5.1: 適用対象のWebアプリケーションのクラス図

なお，今回はクラス図における<<Secure Page>>タグに付随するタグ付き値のうちUseHTTPSとRestrictedByIPAddress を可視化するため，クラスの属性部分にタグ付き値と設定されている値を記述している．また，ディシジョンノードには 4.2.2節で定義した変数・動作が対応しており，<<display>>タグにはタグ付き値としてnameが付随しており，それぞれ表示するページの名前が格納されている．

これらのUMLモデルに対して，本手法を用いて変換を行い，Promelaを出力．

4.4節で定義した検証すべき項目を記述した時相論理式と生成したPromelaを入力として，SPINによる検証を行った．

5.2 変換結果

Promelaへ変換する前の段階として，抽象化と変換を行った結果，ページ数は4

つとなった．それらのページに対して変換を行った結果として，loginページにおけるPromlea出力の一部を図5.3に示す．

本来であれば全ての機能を組み合わせた端末に対して検証を行いたいが，一度に端末の機能の取りうる組み合わせを全て網羅すると，状態数が増大してしまい，

状態爆発と呼ばれる現実的な時間内での検証が不可能な状態になってしまう可能性が高い．そこで，今回の事例では組み合わせを網羅せず，手動で機能の切り替え

を(Promelaの編集によって)行い，検証を行うこととした．

(30)

図 5.2: loginページのアクティビティ図の一部

5.3 ^{検証結果と考察}

変換によって生成されたPromelaに対して，端末の機能を手動で切り替えて検証を行い，その結果の考察について述べる．

5.3.1 Cookie ，リファラ，ユーザ ID の全てを送出する端末による検証

まずはCookie，リファラ，ユーザIDの全てが送出可能な端末をユーザと仮定し

て，検証を行った．

その結果，4.4節の論理式の形式(A’)ではnot validが出力され，セッションによる判定が成功し，ユーザがログイン状態となるまでのパスが提示された．形式

(31)

図 5.3: 出力されたPromelaの一部

形式(A’)の検証結果として出力された，反例に至るまでのパスを確認してみると，ユーザはパスワードを使ってログインに成功した段階で有効なsecure属性の

付いたCookieを持ち，以降のアクセスはそのCookieを用いてセッションを引き継

いでいることが確認できた．secure属性の付いたCookieはHTTPS通信でしか送信されず，攻撃者の盗聴が不可能であるため，形式(B’)の攻撃者のログインが不可能かの検証においても，セキュリティ欠陥の不存在を証明することができた．

5.3.2 Cookie を送出せず，リファラ，ユーザ ID を送出する端末による検証

次に，Cookieの送出を行わず，リファラとユーザIDを送出する端末をユーザと仮定して，検証を行った．その結果，形式(A’)では5.3.1節同様，not validとしてセッションによる判定が成功するまでの経緯が確認できたものの，形式(B’)の

(32)

検証において，not validとして攻撃者がログイン状態となることがあり得るという結果が出力された．出力された反例と反例に至るまでのパスの一部を図5.4，5.5 に示す．

図 5.4: 出力された反例の一部

図 5.5: 出力された反例に至るパスの一部

この反例を解析してみると，アプリケーションは端末の機能を参照した上で，

CookieとURLリライティングによるセッション管理ができないためユーザIDに

よってセッション管理を行っており，ログイン後のページにおいてはそのユーザ IDによってユーザの判別を行っていた．一方，攻撃者は盗聴可能な通信を盗聴することや，他のアプリケーションにアクセスしたユーザのユーザIDを取得することで他人のユーザIDを取得することができる．今回の適用事例では，全てのペー

ジがHTTPSによって保護されており，攻撃者がリクエストの強制を行わない限り

通信を盗聴することはできないが，2.1.3節で説明したようにこのユーザIDはアプリケーション固有のものではなく不変なものである．そのため，秘匿情報と言うことはできず攻撃者が詐称可能であるため，攻撃者は攻撃者の持つユーザIDをユーザの持つユーザIDとして偽装することが可能である．この際，ゲートウェイを介したリクエストを送信すると，ゲートウェイのチェックにより本来の攻撃者が持

(33)

早稲田大学基幹理工学研究科情報理工学専攻深澤研究室用事例で用いたアプリケーションはIPアドレスによる端末のアクセス制限を掛けていなかったため，このゲートウェイを介さないリクエストを受け取ってしまい，

その結果としてユーザIDの書き換えが起こらずにユーザからのリクエストであると判定，ログイン状態でなければ見ることができないページをレスポンスとして送信していた．

この検証結果を踏まえ，topページやloginページ，ログイン後に見ることがで

きるmembertopページなど，全てのページをIPアドレスによって携帯端末から

のアクセスに限定した．UMLモデル上では，クラス図における全てのクラスに付随する<<Secure Page>>タグのタグ付き値であるRestrictedByIPAddressの値を

true (制限を掛ける)とすることで，アクセス制限の修正を行った．修正後のクラ

ス図・アクティビティ図から再び変換を行い，同様の手順で検証を行ったところ，

形式(B’)において前述のようなユーザIDを偽装した攻撃は成立せず，攻撃者がログイン状態となることはないという出力を得ることができた．

(34)

本章では本研究における今後の課題について述べる．

評価法の策定

本論文では，提案した手法をあるWebアプリケーションへと適用し，検証を行ったが，その評価を行うまでには至らなかった．そのため，今後は本手法の評価を行っていきたいと考えている．現段階での具体的な評価案としては，モデリングに掛かる時間量を，提案手法によるモデリングと手動によるモデリングの双方で比較する方法や，本手法を用いて抽象化を行った場合に，抽象化を行わなかった場合との検証に掛かった時間の変化量を比較するといったことを，評価の尺度として用いることを考えている．

複雑な振舞への対応

今回の変換のために抽出したUMLモデルの情報は，ユーザのみがログイン可能なWebアプリケーションという前提の下に成り立っている．Webアプリケーションの振舞として，一人のユーザのみのログインではなく，複数人が別々のログインの権限を持っている場合や，それぞれ権限の違う多段階の認証を行うセッション管理の機構を持つものが多い．また，Webアプリケーションとしては，セッション管理だけでなくデータの読み書きや共有変数を扱うような動作を行うものなど，

より複雑な振舞があると想定される．今後は，そうした事例にも対応できるようにしたい．

反例の解析に対する支援

(35)

早稲田大学基幹理工学研究科情報理工学専攻深澤研究室う際，現在はどのプロセスがどのような動作を行っているのかを，反例に至るパスを表した膨大なログの中から，手動で解析しないといけないという問題がある．

これに対して，例えば関連性の高い変数を抽出して表示したり，一定の期間ごとにその時点でのプロセスの動作の内容を出力させる，などの支援を行うことができれば，反例の解析に掛かるコストを低減できるのではないかと考えている．今後はそうした反例の解析に対する支援策についても考えていきたい．

(36)

開発の上流工程においてモデル検査法を適用することは，手戻りを減少させる反面，早い段階での仕様の形式化が必要となる．そこで本論文では，アプリケーションの振舞をセッション管理に関する処理と限定することで，UMLモデルから情報の抽出や抽象化を行い，変換によってPromelaを生成する手法を提案した．また，

適用事例を通して，提案手法によって生成されたPromelaをモデル検査器SPINを用いて検証を行ったところ，この手法が適用可能なことや，仕様から起こる誤りの発見が行えることを確認できた．第6章でも挙げたように，今後はアプリケーションのセッション以外のロジックに関する検査や評価法の策定，反例に対する支援も考えていきたい．

(37)

謝辞

本研究を進めるにあたり，数々のご指導，ご助言を頂いた深澤良彰教授に深く感謝致します．

また，様々なご指導，問題点の指摘をして頂き，最後の最後まで大変ご迷惑をお掛けした，日本IBM(株)東京基礎研究所の小野康一氏に深く感謝致します．

最後に，共に研究に励み，様々な面でご協力頂いた深澤研究室，鷲崎研究室の皆様に深く感謝致します．

(38)

[1] UML2.0 Specification ”http://uml.omg.org/”

[2] SPIN ”http://spinroot.com/”

[3] UPPAAL ”http://www.uppaal.com/”

[4] astah* ”http://astah.change-vision.com/ja/”

[5] 岸知二，高橋弘，徳田寛和，モデル検査技術を活用したソフトウェア設計・

検証手法に関する考察(モデル表記・モデル検査)，情報処理学会研究報告．

ソフトウェア工学研究会報告2008，no. 55，pp. 95-100，2008

[6] 藤原貴之，岡野浩三，楠本真二，”SPINによるStruts アプリケーションの動作検証を目的としたモデル生成手法の提案，”電子情報通信学会技術研究報告．

SS，ソフトウェアサイエンス，Vol. 105，No. 491，pp. 73-78，2005

[7] 崔銀惠，河本貴則，渡邊宏，”画面遷移仕様のモデル検査，”コンピュータソフトウェア，Vol. 22，No. 3，pp. 146-153，2005

[8] 崔銀惠，渡邊宏，”Webアプリケーションのクラス設計仕様に対するモデル化と検証，”ソフトウェアテストシンポジウム，2005

[9] 本間圭，高橋薫，富樫敦，”形式的手法によるWeb アプリケーションのモデル化と検証，”電子情報通信学会技術研究報告．KBSE，知能ソフトウェア工学，Vol. 109，No. 41，pp. 43-48，2009

[10] 浜口優，吉村顕，岡野浩三，楠本真二，”SPINを用いたウェブアプリケーションにおける階層別モデル検査支援方法，電子情報通信学会技術研究報告．SS，

ソフトウェアサイエンス，Vol. 106，no. 202，pp. 29-34，2006

森川郁也，山岡裕司，中山裕子，モデル検査によるセッションのセキュ

(39)

[12] 山田豊，和崎克己， UMLアクティビティ図からSPINモデル検査用コードの自動生成とWebアプリケーション設計への適用，電子情報通信学会技術研究報告．SWIM，ソフトウェアインタプライズモデリング，Vol. 110，No.

427，pp. 23-28，2011

[13] J. Conallen，Building Web Applications with UML，Addison-Wesley，1999

(40)

大須賀隆彦, 小野康一, 深澤良彰, ”UMLモデルからの変換によるWebアプリケーションの形式検証”, 知能ソフトウェア工学研究会, November 10-11, 2011.

(41)

付録 A ^{適用事例で用いた} UML ^モデル

本項では，適用事例で用いたクラス図，アクティビティ図を掲載する．

図 7.1: 画面の遷移情報・設計情報を表すクラス図

(42)

図 7.2: topページのアクティビティ図図 7.3: infoページのアクティビティ図

図 7.4: linkページのアクティビティ図図7.5: contactページのアクティビティ図

(43)

図 7.6: loginページのアクティビティ図

(44)

図 7.7: membertopページのアクティビティ図

図 7.8: membernewsページのアクティビティ図

(45)

図 7.9: memberinfoページのアクティビティ図

図 7.10: logoutページのアクティビティ図

(46)

Promela

本項では，適用事例におけるUMLモデルのPromela記述への変換結果を掲載する．なお，適用事例において用いたページは，

{top，info，link，contact，login，membertop，membernews，memberinfo，logout} の9つだが，本手法を用いて抽象化を行った結果，ページは

{top，login，membertop，logout}

の4つとなった．以下にその4つのページのアクティビティ図から変換した結果となるPromela記述を載せる．

top

goto display_top;

login if

::(mobileCookie == true) ->

if

::(checks[scookie] == false) ->

if

::(PASS == true) ->

regenerate(scookie);

starts(scookie);

goto display_membertop;

::(PASS == false) ->

goto display_login;

fi;

::(checks[scookie] == true) ->

goto display_login;

fi;

::(mobileCookie == false) ->

if

::(mobileReferer == false) ->

if

(47)

startq(query);

goto display_login;

fi;

::(checkq[query] == true) ->

goto display_login;

fi;

::(mobileReferer == true) ->

if

::(mobileSubID == true) ->

if

::(checkI[subID] == false) ->

if

::(PASS == true) ->

startI(subID);

goto display_login;

fi;

::(checkI[subID] == true) ->

goto display_login;

fi;

::(mobileSubID == false) ->

goto display_login;

fi;

membertop if

if

::(checkq[query] == false) ->

if

goto display_login;

fi;

logout if

destroys(scookie);

if

destroyq(query);

if

(48)

destroyI(subID);

goto display_logout;

fi;

if

destroyI(subID);

fi;

if

destroyq(query);

if

destroyI(subID);

fi;

if

destroyI(subID);

fi;

Web アプリケーションの形式検証に関する研究

2011 年度 修士論文

UML モデルからの変換による