Presentations -
-
A Security Verification Method for Programs with Stack Inspection
IKADA Satoshi, NITTA Naoya, TAKATA Yoshiaki, SEKI Hiroyuki
Technical report of IEICE. ISEC
Event date： 2000.9
Java development kit 1.2 provides a runtime access control mechanism which inspects the control stack to check that the program has appropriate access permission. For such a programming language, it is desirable to guarantee that each execution of a program satisfies required security properties. Jensen et al. introduced a verification problem of deciding for a given program P and a given security property F written in a temporal logic formula, whether every reachable state of P satisfies F. They showed that the problem is decidable for the class of programs which do not contain mutual recursion. In this paper, it is shown that the set of state sequences (traces) of a program is always an indexed language and consequently the verification problem is decidable. Our result is stronger than Jensen's in that a security property can be specified as a regular language, whose expressive power is properly stronger than temporal logic, and a program can contain mutual recursion.
-
スタック検査機能を持つプログラムの制御フロー解析に基づくセキュリティ検証法
伊加田 恵志, 新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告, ISEC2000-78
Event date： 2000.9
-
依存関係に基づく形式論理の提案とそのデータベース設計変更問題への適用
新田 直也, 関 浩之
日本ソフトウェア科学会 第16回大会論文集, D1-2, pp.37--40
Event date： 1999.9
-
Dependence Logic : A Logic for Software Design Modification
NITTA Naoya, SEKI Hiroyuki
Technical report of IEICE. SS
Event date： 1999.5
We propose a new logic called dependence logic, which can be used for a formal approch to software design modification. An important feature of dependence logic is that the logic uses dependences among higher order variables as the basic logical element, instead of functions and predicates. Using this feature makes it possible to define both a knowledge framework and knowledge itself. In this paper, we first define the syntax and semantics of dependence logic. A sound and complete axiomatization of the first-order dependence logic is presented. We also show that the first-order dependence logic can define an arbitrary general recursive function. An application of the logic to the database schema update problem is briefly discussed.
-
ソフトウェア設計変更支援のための依存論理の提案
新田 直也, 関 浩之
電子情報通信学会技術研究報告, SS99-1
Event date： 1999.5
-
Interactive 3D-VRML Viewer
Takemoto Satoshi, Amano Ryuhei, Taima Kenji, Nitta Naoya, Koyama Yukio, Kihara Noriaki
Proceedings of the IEICE General Conference
Event date： 1998.3
-
Desktop 3D Tool
Enomoto Tetsuya, Yamada Tsutomu, Koyama Yukio, Kihara Noriaki, Yamada Teruhiro, Amano Ryuhei, Takemoto Satoshi, Taima Kenji, Hiraoka Toshiko, Matsuda Takeharu, Shiono Kazuhiko, Nitta Naoya
PROCEEDINGS OF THE ITE ANNUAL CONVENTION
Event date： 1998
MPEGやQuickTimeVR, VRMLなどのデータを活用し, 簡単に立体マルチメディアソフトを制作できるデスクトップ3Dツールを開発した.本ツールにより, 従来, 時間とノウハウを要したインタラクティブな立体マルチメディアソフトの制作が容易に実現できる.