WEKO3
アイテム
スタック検査機能をもつプログラムに対するセキュリティ検証問題の決定可能性
http://hdl.handle.net/10173/671
http://hdl.handle.net/10173/6718c14b90b-627f-4f09-9bca-a5a59bf6c257
名前 / ファイル | ライセンス | アクション |
---|---|---|
IEICE_J85-D1_4_360.pdf (437.2 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2011-06-23 | |||||
タイトル | ||||||
タイトル | スタック検査機能をもつプログラムに対するセキュリティ検証問題の決定可能性 | |||||
言語 | ||||||
言語 | jpn | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | アクセス制御 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | セキュリティ検証 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | スタック検査 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Java | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
資源タイプ | journal article | |||||
著者 |
新田, 直也
× 新田, 直也× 高田, 喜朗× 関, 浩之 |
|||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | Java development kit 1.2のように,プログラム実行時に制御スタックを検査することでアクセス制御を行うようなプログラム環境がある.Jensenらは,プログラム P 及び時相論理式を用いて記述された検証条件 ψ を与えたときに,P の到達可能な状態すべてが ψ を満たすかどうかを決定する問題として検証問題を定義し,相互再帰を含まないプログラムのクラスに対して検証問題が決定可能となることを示した. 本論文では,時相論理式よりも真に表現能力の大きい正規言語を用いて検証問題を定義する.そして,プログラムのトレース集合がインデックス言語となることを示し,その系としてプログラムが相互再帰を含む場合も含めて検証問題が一般に決定可能となることを示すことにより,Jensenらの結果を改善する.更に,自明なスタック検査のみを含むプログラムのクラスに対する検証問題が,プログラムサイズに対して多項式時間可解であることを示す. | |||||
書誌情報 |
電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems 巻 J85-D1, 号 4, p. 360-370, 発行日 2002-04-01 |
|||||
ISSN | ||||||
収録物識別子タイプ | ISSN | |||||
収録物識別子 | 0915-1915 | |||||
書誌レコードID | ||||||
収録物識別子タイプ | NCID | |||||
収録物識別子 | AA12099634 | |||||
権利 | ||||||
権利情報 | ©2002電子情報通信学会(IEICE) | |||||
著者版フラグ | ||||||
出版タイプ | VoR | |||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
出版者 | ||||||
出版者 | 電子情報通信学会 | |||||
関係URI | ||||||
識別子タイプ | URI | |||||
関連識別子 | http://search.ieice.org/ | |||||
関連名称 | http://search.ieice.org/ |