講演・口頭発表等 - 新田 直也
-
バッファオーバーフロー静的検出のための一手法
新田 直也, 王静
第1回シンポジウム「ネットワークと情報処理」論文集, 甲南大学 知的情報通信研究所, pp.46--52
開催年月日: 2005年1月
-
Aliasing-PDS: オブジェクト指向プログラムのモデル検査のための新しい 計算モデル
新田直也
シンポジウム「システム検証の科学技術」予稿集 (2004、シンポジウム発表)
開催年月日: 2004年2月
-
ネットワーク分散型侵入検知システムにおける最適なProbeの配置について
王静, 新田直也, 関浩之
2004年暗号と情報セキュリティシンポジウム (SCIS), pp.1035-1040
開催年月日: 2004年1月
-
ネットワークの安全性を保証する分散型侵入検知システムの自動構成法
王 静, 新田 直也, 関 浩之
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
開催年月日: 2003年11月
ネットワークシステムヘの不正アクセスは, 機密情報の漏洩や, ネットワークサービスの妨害など, システム全体に甚大な被害をもたらす. 不正アクセスを検知するシステムとして侵入検知システム(IDS, Intrusion DetectionSystem)が広く用いられている. 正規表現ネットワーク型IDSは, ネットワーク上に分散配置された複数のIDSで不正検出を行うものであるが, IDSの配置数, 配置ホストおよび分散攻撃シナリオを決定するアルゴリズムは場あたり的なものしか知られていない. そこで, 本研究では, この問題をIDS分割配置問題として形式的に定義しその計算複雑さや, それを解くアルゴリズムについて考察する.
-
ネットワークの安全性を保証する分散型侵入検知システムの自動構成法
王 静, 新田 直也, 関 浩之
電子情報通信学会技術研究報告
開催年月日: 2003年11月
ネットワークシステムヘの不正アクセスは, 機密情報の漏洩や, ネットワークサービスの妨害など, システム全体に甚大な被害をもたらす. 不正アクセスを検知するシステムとして侵入検知システム(IDS, Intrusion DetectionSystem)が広く用いられている. 正規表現ネットワーク型IDSは, ネットワーク上に分散配置された複数のIDSで不正検出を行うものであるが, IDSの配置数, 配置ホストおよび分散攻撃シナリオを決定するアルゴリズムは場あたり的なものしか知られていない. そこで, 本研究では, この問題をIDS分割配置問題として形式的に定義しその計算複雑さや, それを解くアルゴリズムについて考察する.
-
ネットワークの安全性を保証する分散型侵入検知システムの自動構成法
王 静, 新田 直也, 関 浩之
電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学
開催年月日: 2003年11月
-
ネットワークの安全性を保証する分散型侵入検知システムの自動構成法
王静, 新田直也, 関浩之
電子情報通信学会技術研究報告, SS2003-31
開催年月日: 2003年11月
-
プッシュダウンシステムの拡張およびそのモデル検査法
新田 直也, 関 浩之
情報処理学会論文誌プログラミング(PRO)
開催年月日: 2003年10月
現在,無限の状態空間を持つ遷移システムに対するモデル検査法の研究がさかんに行われており,特にプッシュダウンシステムやペトリネットに対するモデル検査において良い結果が得られている.本発表では,プッシュダウンシステムを拡張した遷移システムを項書き換え系の部分クラスとして定義し,そのLTL (線形時相論理)によるモデル検査が決定可能となることを示す.プッシュダウンシステムの項書き換え系による定式化は,一般に文字列で表現されるスタック構造の木構造への拡張を意味し,この拡張によってより豊かなデータ構造を持った遷移システムの自動検証が可能になることが期待される.Recently, in the field of model checking, many researches for infinite systems have been done. Particularly for pushdown systems and petri nets, there are good decidablity results on model checking. In this presentation, we define a class of transition systems which is an extension of pushdown systems as a subclass of TRS (term rewriting systems) and show that LTL (linear temporal logic) model checking problem for the class is decidable. Formulating pushdown systems as a subclass of TRS, we can extend the structure of stacks to tree structure. By this extension, it is expected that transition systems with richer data structure become verifiable.
-
Infinite State Model Checking and Its Application to Software Verification
Hiroyuki Seki, Naoya Nitta, Yoshiaki Takata, Sigeta Kuninobu
第2回クリティカルソフトウェアワークショップ(WOCS)予稿集, pp.20--22
開催年月日: 2003年3月
-
分散ポリシー制御の自動検証法について
國信 茂太, 新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
開催年月日: 2003年1月
個々のオブジェクトがポリシーを持ち,それに基づいて実行制御を行うような分散モデルが注目されている.本稿では,設計者の記述したポリシーが,本来の意図通りに,オブジェクトの動作を制御するかを検証する方法を提案する.本手法では,検査対象のプログラムとポリシーをプッシュダウンシステムヘ抽象化した後,モデル検査を行う.本稿では,実装したポリシー自動検証システムから得られた結果も示す.
-
プッシュダウンシステムの拡張およびそのモデル検査法
新田 直也, 関 浩之
情報処理学会プログラミング研究会, 2003-01 (2003、学会報告)
開催年月日: 2003年1月
-
A Verification Method for Distributed Policy Control
Sigeta Kuninobu, Yoshiaki Takata, Naoya Nitta, Hiroyuki Seki
電子情報通信学会技術研究報告, SS2002-44
開催年月日: 2003年1月
-
計量器組込みソフトウェアの仕様記述および検証事例
新田 直也, 高橋 孝一
第4回組込みシステム技術に関するサマーワークショップ (2002、学会報告)
開催年月日: 2002年11月
-
スタック検査機能を持つプログラムに対する効率のよいセキュリティ検証法(<特集>プログラミング及びプログラミング言語)
新田 直也, 高田 喜朗, 関 浩之, Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki, 奈良先端科学技術大学院大学情報科学研究科, 奈良先端科学技術大学院大学情報科学研究科, 奈良先端科学技術大学院大学情報科学研究科, Graduate School of, Information, Science Nara, Institute of Science, Technology, Graduate School of, Information, Science Nara, Institute of Science, Technology, Graduate School of, Information, Science Nara, Institute of Science, Technology
コンピュータソフトウェア = Computer software
開催年月日: 2002年5月
-
スタック検査を含むプログラムに対する効率のよいセキュリティ検証法
新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告, SS2001-7 (2001、学会報告)
開催年月日: 2001年11月
-
スタック検査を含むプログラムに対する効率のよいセキュリティ検証法
新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
開催年月日: 2001年5月
実行時に制御スタックを検査することでアクセス制御を行うプログラム環境がある. 著者らはこれまでに, このようなプログラムがセキュリティ条件を満たすかどうかを決定する検証問題について考察し, その計算量の下界がPSPACE困難であること等を示した. 本発表では, Java development kit 1.2におけるアクセス制御をモデル化できるプログラムの部分クラスを導入し, そのクラスに対して検証問題がプログラムサイズの多項式時間で可解であることを示す.
-
Complexity of the Security Verification Problem for Programs with Stack Inspection
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
第3回プログラミングおよびプログラム言語ワークショップ論文集 (PPL2001), pp.53--60
開催年月日: 2001年3月
-
スタック検査機能を持つプログラムの制御フロー解析に基づくセキュリティ検証法
伊加田 恵志, 新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告. ISEC, 情報セキュリティ
開催年月日: 2000年9月
プログラム実行時に制御スタックを検査することでアクセス制御を行うようなプログラム言語がある.このようなプログラムが与えられたとき, どのような実行に対しても, ある望ましい性質(検証条件)が成り立つかどうかを保証できることが望ましい.本研究では, このような検証問題に対する検証法として形式言語を用いた手法を提案する.Jensenらの提案した手法は検証条件を時相論理式を用いて記述し, また, 適用範囲が相互再帰を含まないプログラムに限られているのに対し, 本手法では, 検証条件を時相論理式よりも真に表現能力の大きい正規言語で記述し, かつ, プログラムが相互再帰を含むことを許すことで, より広い範囲の自動検証を可能とした.本稿では, プログラムのトレース集合がインデックス言語となることを示し, その系として検証問題が決定可能となることを示す.
-
スタック検査機能を持つプログラムの制御フロー解析に基づくセキュリティ検証法
伊加田 恵志, 新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告, ISEC2000-78
開催年月日: 2000年9月
-
依存関係に基づく形式論理の提案とそのデータベース設計変更問題への適用
新田 直也, 関 浩之
日本ソフトウェア科学会 第16回大会論文集, D1-2, pp.37--40
開催年月日: 1999年9月