Presentations -
-
実規模オブジェクト指向プログラムの設計評価のための一手法
新田直也, 久米出, 武村泰宏
日本産業技術教育学会, 第21回情報分科会研究発表会
Event date： 2005.12
-
An Automated Refactoring for Information Hiding
NITTA NAOYA
情報処理学会論文誌プログラミング(PRO)
Event date： 2005.8
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、学会報告)
Event date： 2005.1
-
バッファオーバーフロー静的検出のための一手法
新田 直也, 王静
第1回シンポジウム「ネットワークと情報処理」論文集, 甲南大学 知的情報通信研究所, pp.46--52
Event date： 2005.1
-
Aliasing-PDS: オブジェクト指向プログラムのモデル検査のための新しい 計算モデル
新田直也
シンポジウム「システム検証の科学技術」予稿集 (2004、シンポジウム発表)
Event date： 2004.2
-
ネットワーク分散型侵入検知システムにおける最適なProbeの配置について
王静, 新田直也, 関浩之
2004年暗号と情報セキュリティシンポジウム (SCIS), pp.1035-1040
Event date： 2004.1
-
Towards an Optimal Probe Deployment for Network IDS
WANG Jing, NITTA Naoya, SEKI Hiroyuki
Technical report of IEICE. SS
Event date： 2003.11
Misuse accesses cause enormous damage to network system, e. g., disclosing secret information, counterchecking networks service et al. To detect misuse access, Intrusion Detection Systems (IDSs) are used generally. Regular expression-based network IDS is a mechanism which detects misuse accesses by distributed IDSs on intra-network. However, there are only ad hoc algorithms for determining the number of distributed IDSs, deployment hosts and distributed attack scenarios. Hence, in this research, we formally define this problem as IDS partition deployment problem and discuss the computational complexity of this problem and its algorithm.
-
Towards an Optimal Probe Deployment for Network IDS(Knowledge-Based Software Engineering)
WANG Jing, NITTA Naoya, SEKI Hiroyuki
Technical report of IEICE. KBSE
Event date： 2003.11
Misuse accesses cause enormous damage to network system, e. g., disclosing secret information, counterchecking networks service et al. To detect misuse access, Intrusion Detection Systems (IDSs) are used generally. Regular expression-based network IDS is a mechanism which detects misuse accesses by distributed IDSs on intra-network. However, there are only ad hoc algorithms for determining the number of distributed IDSs, deployment hosts and distributed attack scenarios. Hence, in this research, we formally define this problem as IDS partition deployment problem and discuss the computational complexity of this problem and its algorithm.
-
Towards an Optimal Probe Deployment for Network IDS
WANG Jing, NITTA Naoya, SEKI Hiroyuki
電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学
Event date： 2003.11
-
ネットワークの安全性を保証する分散型侵入検知システムの自動構成法
王静, 新田直也, 関浩之
電子情報通信学会技術研究報告, SS2003-31
Event date： 2003.11
-
An Extension of Pushdown System and Its Model Checking Method
NITTA Naoya, SEKI Hiroyuki
情報処理学会論文誌プログラミング(PRO)
Event date： 2003.10
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
Event date： 2003.3
-
A Verification Method for Distributed Policy Control
KUNINOBU Shigeta, NITTA Naoya, TAKATA Yoshiaki, SEKI Hiroyuki
Technical report of IEICE. SS
Event date： 2003.1
This paper proposes a formal semantics and a safety verification method for a policy controlled system. We provide an operational semantics of a Ponder-like policy specification language. Next, we present an abstraction method from a policy controlled system to a pushdown system, for which a model checking can be performed. We also show verification results conducted on our automatic verification tool.
-
プッシュダウンシステムの拡張およびそのモデル検査法
新田 直也, 関 浩之
情報処理学会プログラミング研究会, 2003-01 (2003、学会報告)
Event date： 2003.1
-
A Verification Method for Distributed Policy Control
Sigeta Kuninobu, Yoshiaki Takata, Naoya Nitta, Hiroyuki Seki
電子情報通信学会技術研究報告, SS2002-44
Event date： 2003.1
-
計量器組込みソフトウェアの仕様記述および検証事例
新田 直也, 高橋 孝一
第4回組込みシステム技術に関するサマーワークショップ (2002、学会報告)
Event date： 2002.11
-
An Efficient Security Verification Method for Programs with Stack Inspection.
NITTA Naoya, TAKATA Yoshiaki, SEKI Hiroyuki, 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
Event date： 2002.5
-
スタック検査を含むプログラムに対する効率のよいセキュリティ検証法
新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告, SS2001-7 (2001、学会報告)
Event date： 2001.11
-
An Efficient Security Verification Method for Programs with Stack Inspection
NITTA Naoya, TAKATA Yoshiaki, SEKI Hiroyuki
Technical report of IEICE. SS
Event date： 2001.5
Stack inspection is a key technology for runtime access control of programs in a network environment. In this paper, a verification problem to decide whether a given program with stack inspection satisfies a given security property is discussed. We have already shown that the computational complexity of the problem is PSPACE-hard. Since this result implies the problem is computationally intractable in general, we introduce a practically important subclass of programs which exactly model programs containing checkPermission of Java development kit 1.2. We show that the time complexity of the problem for this subclass is linear in the size of a program.
-
Complexity of the Security Verification Problem for Programs with Stack Inspection
Naoya Nitta, Yoshiaki Takata, Hiroyuki Seki
第3回プログラミングおよびプログラム言語ワークショップ論文集 (PPL2001), pp.53--60
Event date： 2001.3