日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

細粒度アクセス制御を行うためのフォーマルなソフト
ウェア仕様に対する分析事例
小林 竜太

大森 洋一

荒木 啓二郎ソフトウェアで安全性に関する多層防御を実現するためには，対象を適切な単位に分割し，それぞれに適切なアクセス制御を行う必要がある．また，このような権限に関する機能整理は，ソフトウェア構造の改善にも有用である．本
研究は，仕様記述にフォーマルメソッドを用いることによって，数理モデル上でソフトウェアのケイパビリティ分析を行い，必要な認可ポリシーの抽出，整理を行い，無矛盾性を保証する手法について，大学における PBL で作成したネットワーク上のアイデア共有ソフトウェアの事例について適用した成果を報告する．

Software security with defense in depth requires division of the target system into appropriate modules
and grant appropriate access capabilities to them. The analyzing process also helps improvement of software structure and refactoring. This research reports that a case about networked idea exchange software
constructed during a PBL course in Kyushu University. It applied a formal method to perform capability
analysis, extraction of the access policy, and verification on a mathematical model at specification level.

なるテーマを進める実践型 PBL であり，ロジカルシ

1 ソフトウェアに関する PBL 教育

ンキング，プロジェクトマネジメント，開発プロセス

九州大学では，大学院システム情報科学府 情報知といった PBL スキルに対応する講義とあわせたカリ能工学専攻 社会情報システムコース (QITO) の学生キュラムを実施している [3]．

を対象に， 2006 年度より継続的にソフトウェア開

九州大学の PBL は半年単位で実施されており，開発に関する Project Based Learning (PBL) を実施

発期間や作業時間は限定されている．各プロジェクトしている [2]．平成 24 年からは文部科学省 情報技術においては，問題解決に関する学生のさまざまなアイ人材育成のための実践教育ネットワーク形成事業のデアを形にすることが優先され，実用上重要ではある支援のもとで，九州大学を含む全国 15 大学 (申請代

ものの，新規性に欠ける非機能要件は後回しにされが表校:大阪大学) は，教育プログラム「分野・地域をちである．このような状況は，九州大学の PBL に固超えた実践的情報教育協働ネットワーク ( Education

有のものではなく，開発リソースの不足しがちな多く

Network for Practical InformationTechnologies†
1( enPiT ))」 により，実践的な課題解決力を持ったの学校教育における演習，さらにはスタートアップに人材を育成を図っている．修士 2 年生を対象とした

しかしながら， PBL における開発成果について，PBL 第二・第三は学生が主体となりチームごとに異学内あるいは社内ツールに留まらず，より広範な活用おいてもしばしば見られる．

を目指すには十分なセキュリティ確保は不可欠であA case analysis of formal software specification to role
based access control
Ryuta Kobayashi, Yoichi Omori, and Keijiro Araki,
九州大学 大学院情報システム科学研究院, Graduate
School of Information Science and Electrical Engineering, Kyushu University.
†1 分野・地域を越えた実践的情報教育協働ネットワーク
http://www.enpit.jp/

る．特に，現在のソフトウェアにおいてはネットワー
ク接続を考慮しない実行環境は考えられず，セキュリ
ティ上の欠陥は致命的なデータ流出やシステムダウンに直結する大きな問題になりかねない．ソフトウェア開発におけるセキュリティの考慮という観点は，大学におけるソフトウェア教育に限定しても重要である

が，これまで十分な方法論が提示されているとはいい

銀行の当座預金口座開設は拒否するが，普通預金口座がたい．

開設操作は許可するなど柔軟なアクセス制御が可能

本稿では，機能に関する実装が先行しているソフトとなる．

ウェア開発プロジェクトにおいて，フォーマルメソッ

このようなアクセス制御モデルに基づいてソフトドを利用した仕様記述により，セキュリティ，特に権ウェアを設計することで，安全性に関する一貫性を高限認証について開発時とは異なる観点でソフトウェアめることができる．機能を優先して実装したプログラの数理モデルを抽出し，ソフトウェアの再構成を行う

ムをリファクタリングする際にも，一貫した設計指針手法について，ソフトウェアの分析事例を提示する．のひとつとして利用することができる．

2 ロールベースのアクセス制御

3

最も基本的なソフトウェアの権限認証は，パスワー

PBL 第二及び第三で開発した，企画会議支援アプドなどによるユーザ認証である．ユーザがシステム

リ Bresticky は，オンラインでのブレインストーミを利用する権限をもっているかどうか，どの権限クラングを支援するソフトウェアであり，ホワイトボードスに属すのかを認証する．一方，正当なユーザに対しのメタファとなっている [7]．Bresticky の特徴を図 1ても，システムの全権限が与えられるわけではない．に示す．

Bresticky の実装

ソフトウェア環境については，ユーザが利用するソフトウェアごとに適切なユーザ認証を行い，かつソフトウェアごとにシステムリソースへのアクセスには，適切な権限を与えるのが望ましい．
一般的なアクセス制御は，アクセス主体とアクセスされるリソースの関係により定義されるが，汎用計算機上であらゆる関係を 2 次元の表として表現するのは困難なので，あるセキュリテイポリシーを定義し，それにしたがってアクセス制御を行う．古典的な，リソースの所有者が全面的にアクセス許可を管理する
任意アクセス制御，システムが全面的にアクセス許可

図1

Brestickyを管理する強制アクセス制御に加えて，アクセス主体の属性と対象リソースの属性によりアクセス許可を

Bresticky は，なんらかの文章を記述した「ノート」決定する属性ベースアクセス制御 [5]，推測されるアをホワイトボードのメタファである「ボード」に配置

クセス主体の意図とそれに伴うリスク評価に基づいし，関係のあるノートを近くへ配置するというブレイてアクセス許可を決定する意図ベースアクセス制御

ンストーミングの作業をオンラインで実現する．実[1] など新しい制御モデルも提案されている．

際のホワイトボードのような物理的な制約をもたず，ロールベースアクセス制御 （Role Based Access

保存もできる．ボードの状態は複数人が同時に操作すControl, RBAC) は，こうしたアクセス制御方式のることができて，サーバ上でリアルタイムで更新され１つであり，アクセス主体とリソースに対して，ユーるので一貫性が保証される．

ザから見たロール (Role) を定義する．アクセス制御

クライアントは，マルチデバイスに対応しており，ポリシーは，アクセス主体やリソースの抽象化されたPC 上の ブラウザ， iOS, Android などで動作する．

ロールに対して定義され，ユーザの追加やシステムのクライアント・サーバ間の通信は IBM が提唱する IoT変更に対してより安定性の高いモデルとなっている．

向けの通信プロトコル Message Queuing Telemetry

コンテキストは考慮されないが，事前に定義された，Transport (MQTT) ベースのプロトコルで軽量かつリアルタイムで動作する. HTTP 通信に比べてスケー的なモデルとして記述することにより，その数理体系ラビリティの高い Publish/Subscribe モデルで動作における矛盾や曖昧さを取り除くことが可能となる．

し，クライアントは書き込み時に Publisher ，読み込

フォーマルメソッドは上流工程からのソフトウェア品

み時に Subscriber となる．クライアントのソフトウェ質向上に有用であることが知られており，提案初期か

アは HTML5 により実装されており， JavaScript のら利用されてきたプラント制御や交通管制といった動作する PC 上のブラウザだけでなく，多くのモバクリティカルシステムだけでなく，さまざまな応用分イル環境もサポートする．

野，適用範囲において多くの実用例がある [4]．

バックエンドのサーバは background as a service

VDM はシステムのモデル化と分析，詳細設計や(BaaS) のひとつである Milkcocoa を利用しているコーディングへ至るための技術体系であり，一階述語[10]．Milkcocoa はリアルタイムの Publish/Subscribe

論理と同値性に関する集合論に基づくフォーマルメ通信をサポートし，クライアント数や API 呼び出し数ソッドの一種であり， 1960 年代後半から長期に渡っの規定内で無料で利用することができる．Milkcocoaて使用されており，安定した検証ツールと多くのユーの提供する API は基本的なセッションの開始，終了，ザおよび実用例をもつ [9] [8]．本研究では， VDM のユーザ認証，データストア作成，データストアへの仕様記述言語 VDM-SL を利用した．

データやイベントの追加，削除，読み出しといった一般的な処理である．データストアへ追加するオブジェ

4. 2 業務分析

クトは JSON 形式のオブジェクトを利用可能であり，ブレインストーミングは，図 3 の作業からなる．

メッセージサイズは 4KB 以内という制限がある．
図 2 に Bresticky の構成を示す．

図3

ブレインストーミング

企画会議の間はアイデア出しとアイデア整理を繰り返し，中断時は保存する．１つの会議で複数のボー
図2

クライアント・サーバ構造ドを利用することもできる．また，単なるホワイトボードの代替だけでなく，事前に用意しておいた検討事項に対してい，会議後は議事録を出力することがで4 対象の分析

きる．合意したものは，次の企画変更まで継続するの

4. 1 フォーマルメソッドの適用で，その間の補足事項は「コメント」として別途保持

このようなソフトウェア事例に対して，フォーマする．

ルメソッドによる仕様を数理モデルとして記述した．
フォーマルメソッドは，計算機システムの仕様を数理

これらの作業を実現するために，システムは次のような機能を提供する必要がある．

的に表記することおよび，その仕様を検証基盤として• ユーザの登録，認証利用する手法である [6]．ソフトウェアの仕様を数理• プロジェクトの作成，削除

• ボードの作成，削除，複製を利用しており，仕様から利用可能な実装はそのまま• 議事の登録，削除，更新利用し，そうでない部分は既存のプログラムを改修• 議事録の出力するか，アプリケーション層の機能として追加する．

• ノートの追加，修正，削除，移動，参照

このとき，フォーマルな仕様を利用することにより，• コメントの追加，修正，削除，参照何をどのように変更するかを誤解なく明示できる．リ• ボードのサーバへの保存，復元

ファクタリングの際には，こうした検討を仕様として• ボードの印刷活用できる．

これ以外に，JSON Web Token JWT) を利用し謝辞たユーザ権限の認証も可能である．JWT を利用す

本研究の一部は JSPS 科研費 24220001, 基盤研究 (S)ると任意アクセス制御は容易に実現できる．しかし， 「アーキテクチャ指向形式手法に基づく高品質ソフト

Bresticky において RBAC を実現するには，個々のウェア開発法の提案と実用化」の成果による．

リソースへのアクセス制御機能などが不足していることも明確に分かる．
データ構造としては，「議事」「議事録」「ノート」「コメント」「ボード」「ユーザ」などが定義された．

VDM により，それぞれのデータ構造は集合として定義され，包含関係が明確になる．例えば• 議事録 = set of 議事• ボード = 議事録 * set of ノート * set of コメント

• プロジェクト = set of ボードのように，数学的な集合として表現できる．現状では，ノート間の距離の定義が曖昧であることもわかった．ブレインストーミングでは，ノート間の距離は単なる UI ではなく，モデル上の重要な情報であるが絶対的な距離ではなく，デバイスごとの相対的な距離を定義すべきであると思われる．

5 まとめと今後の課題
九州大学 大学院における PBL で開発した，企画会
議支援アプリ Bresticky の仕様をフォーマルメソッド

VDM により数理モデルとして記述した．Brestickyのサポートするオンラインのブレインストーミングを対象に業務分析を行い，ユーザからみて必要な機能を抽出した．これらの機能は，実装上の制約には囚われず，多くの類似ソフトウェアに対しても仕様レベルでの再利用が可能である．
本 分 析 で は ， Bresticky は ク ラ イ ア ン ト 側 はHTML5 ，サーバ側は Milkcocoa という実装技術

参 考 文 献[ 1 ] Almehmadi, A.: On the Possibility of Insider
Threat Prevention Using Intent-Based Access Control (IBAC), IEEE Systems Journal, Vol. PP,
No. 99(2015), pp. 1–12.
[ 2 ] 廣重法道, 鵜林尚靖, 外村慶二, 福田晃: 九州大学における先導的 PBL 教育の評価分析, 研究報告ソフトウェ
ア工学（SE）, Vol. 2010-SE-170, No. 22, 情報処理学会, 2010, pp. 1–7.
[ 3 ] 細合晋太郎, 石田繁巳, 亀井靖高, 大迫周平, 井垣宏,鵜林尚靖, 福田晃: IoT システムを題材とした PBL の導入提案, 研究報告ソフトウェア工学（SE）, Vol. 2014SE-185, No. 7, 情報処理学会, 2014, pp. 1–7.
[ 4 ] IPA/SEC: 厳密な仕様記述における形式手法成功事
例調査報告書, 技術報告, 独立行政法人 情報処理推進機構,
http://www.ipa.go.jp/sec/reports/20130125.html, 2013.
[ 5 ] Jin, X., Krishnan, R., and Sandhu, R.: A Unified Attribute-Based Access Control Model Covering
DAC, MAC and RBAC, Springer Berlin Heidelberg,
2012, pp. 41–55.
[ 6 ] Jones, C. B.: Software Development basedon Formal Methods, Proceedings of the CRAI
Workshop on Software Factories and Ada, LNCS,
Vol. 275, Springer-Verlag, 1987, pp. 153–172.
[ 7 ] 上 畑 恭 平, 古 賀 祥 造 , 小 林 竜 大, 元 田 彰拓, 林 冬 , 渡 部 誠 俊 :企画会議支援アプリ
Bresticky, https://drive.google.com/drive/folders/
0B0VUsktedAmcdHhIWHJRcm9tMEE.
[ 8 ] Kurita, T., Ishikawa, F., and Araki, K.: Practices for Formal Models as Documents: Evolutionof VDM Application to “Mobile FeliCa” IC Chip
Firmware, Proceedings of the 20th International
Symposium, 2015, pp. 593–596.
[ 9 ] Verhoef, M., Larsen, P. G., and Hooman, J.:Modeling and Validating Distributed Embedded
Real-Time Systems with VDM++, Proc. of the 14thInternational Symposium on Formal Method, 2015,
pp. 147–162.
[10] 株 式 会 社 ウ フ ル:
Milkcocoa HomePage,
https://mlkcca.com/.