WEKO3
アイテム
実行履歴に基づくアクセス制御の形式モデルと検証
http://hdl.handle.net/10173/650
http://hdl.handle.net/10173/6506261df58-9d36-4048-8300-e69446b85816
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IEICE_J91-D_4_847.pdf (493.4 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2011-03-30 | |||||
| タイトル | ||||||
| タイトル | 実行履歴に基づくアクセス制御の形式モデルと検証 | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 言語ベースセキュリティ | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | スタック検査 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 実行履歴に基づくアクセス制御 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | モデル検査 | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 著者 |
高田, 喜朗
× 高田, 喜朗× 王, 静× 関, 浩之 |
|||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | プログラムが望ましくない動作を行うことを防ぐ動的アクセス制御機構として，Java仮想機械等に実装されているスタック検査が広く用いられている．しかし，スタック検査は，実行が完了したメソッド呼出しに関するセキュリティ情報が消失するという問題点をもつ．これを解決するため，実行履歴に基づく各種のアクセス制御機構が提案されている．本論文では，Abadiらのアクセス制御法を形式的に定義したHBACプログラムモデルを提案し，HBACプログラムに対するモデル検査法について考察する．具体的には以下の2点を行う．（ 1 ） HBACプログラムに対する検証問題は，現実的な仮定のもとでは多項式時間可解であるが，一般の場合は決定性指数時間完全であることを示す．（ 2 ） HBACプログラムの検証におけるいくつかの最適化法を提案する．試作検証ツールを使った簡単な実験により，現実的な時間と領域でHBACプログラムの検証が可能であることを示す． | |||||
| 書誌情報 |
電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems 巻 J91-D, 号 4, p. 847-858, 発行日 2008-04-01 |
|||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 1881-0225 | |||||
| 権利 | ||||||
| 権利情報 | ©2008電子情報通信学会(IEICE) | |||||
| 著者版フラグ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 出版者 | ||||||
| 出版者 | 電子情報通信学会 | |||||
| 関係URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://search.ieice.org/ | |||||
| 関連名称 | http://search.ieice.org/ | |||||
