スタック検査機能をもつプログラムに対するセキュリティ検証問題の決定可能性

• 新田, 直也

• 高田, 喜朗

• 関, 浩之

Bibliographic Information

Other Title

• スタック ケンサ キノウ オ モツ プログラム ニ タイスル セキュリティ ケンショウ モンダイ ノ ケッテイ カノウセイ

Abstract

Java development kit 1.2のように，プログラム実行時に制御スタックを検査することでアクセス制御を行うようなプログラム環境がある．Jensenらは，プログラム P 及び時相論理式を用いて記述された検証条件 ψ を与えたときに，P の到達可能な状態すべてが ψ を満たすかどうかを決定する問題として検証問題を定義し，相互再帰を含まないプログラムのクラスに対して検証問題が決定可能となることを示した． 本論文では，時相論理式よりも真に表現能力の大きい正規言語を用いて検証問題を定義する．そして，プログラムのトレース集合がインデックス言語となることを示し，その系としてプログラムが相互再帰を含む場合も含めて検証問題が一般に決定可能となることを示すことにより，Jensenらの結果を改善する．更に，自明なスタック検査のみを含むプログラムのクラスに対する検証問題が，プログラムサイズに対して多項式時間可解であることを示す．

Journal

• 電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems

  電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems J85-D1 (4), 360-370, 2002-04-01

  電子情報通信学会

Keywords

• アクセス制御
• セキュリティ検証
• スタック検査
• Java

Details

• CRID: 1050282676665061888
• NII Article ID: 110003184765
• NII Book ID: AA12099634
• ISSN: 09151915
• NDL BIB ID: 6127234
• Web Site: http://hdl.handle.net/10173/671
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I6127234
• Text Lang: ja
• Article Type: journal article
• Data Source:
  • IRDB
  • NDL
  • CiNii Articles