講演・口頭発表等 - 新田 直也
-
実規模オブジェクト指向プログラムの設計評価のための一手法
新田直也, 久米出, 武村泰宏
日本産業技術教育学会, 第21回情報分科会研究発表会
開催年月日： 2005年12月
-
情報隠蔽のための自動リファクタリング
新田 直也
情報処理学会論文誌プログラミング（PRO）
開催年月日： 2005年8月
プログラムの外的振舞いを保ったままソースコードの内部構造を改善する技術として，近年リファクタリングが注目されている．とりわけ，プログラミング工程で発生する予期しない設計変更への対応手段としてリファクタリングに期待されている役割は大きいが，現実の設計変更作業のどの程度の範囲で有効であるかについては今のところ明らかではない．そこで本研究では，ある種の情報隠蔽を目的とした設計変更作業に着目し，それが従来のリファクタリングの組合せでは実現できないことを示す．さらに，新しい基本リファクタリングとして変数隠蔽を導入し，手続き間生存性解析技術を用いてそれを自動化する方法を示す．情報隠蔽は最も基本的な設計活動の1 つであり，その自動リファクタリングによる支援は，開発効率の大幅な向上に寄与するものと期待される．Recently, much attention is paid to refactoring as a technique for improving the internal structure of a existing code while preserving its observational behavior. Refactoring frameworks are expected to play an important role in design change activities occuring in programming process, but there is no comprehensive survey of their applicability to real design changes. In this research, we consider a kind of structural change for information hiding and show that it cannot be handled by existing refactoring frameworks. Further, we introduce a new primitive refactoring named variable hiding, and show that using the interprocedural liveness analysis, the process of the refactoring can be automated. Since information hiding is one of the fundamental design activities, to support the activities by an automated refactoring is expected to improve the efficiency of development peocesses.
-
情報隠蔽のための自動リファクタリング,
新田直也
情報処理学会プログラミング研究会 (2005、学会報告)
開催年月日： 2005年1月
-
バッファオーバーフロー静的検出のための一手法
新田 直也, 王静
第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月