講演・口頭発表等 - 新田 直也
-
スタック検査機能を持つプログラムの制御フロー解析に基づくセキュリティ検証法
伊加田 恵志, 新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告. ISEC, 情報セキュリティ
開催年月日： 2000年9月
プログラム実行時に制御スタックを検査することでアクセス制御を行うようなプログラム言語がある.このようなプログラムが与えられたとき, どのような実行に対しても, ある望ましい性質(検証条件)が成り立つかどうかを保証できることが望ましい.本研究では, このような検証問題に対する検証法として形式言語を用いた手法を提案する.Jensenらの提案した手法は検証条件を時相論理式を用いて記述し, また, 適用範囲が相互再帰を含まないプログラムに限られているのに対し, 本手法では, 検証条件を時相論理式よりも真に表現能力の大きい正規言語で記述し, かつ, プログラムが相互再帰を含むことを許すことで, より広い範囲の自動検証を可能とした.本稿では, プログラムのトレース集合がインデックス言語となることを示し, その系として検証問題が決定可能となることを示す.
-
スタック検査機能を持つプログラムの制御フロー解析に基づくセキュリティ検証法
伊加田 恵志, 新田 直也, 高田 喜朗, 関 浩之
電子情報通信学会技術研究報告, ISEC2000-78
開催年月日： 2000年9月
-
依存関係に基づく形式論理の提案とそのデータベース設計変更問題への適用
新田 直也, 関 浩之
日本ソフトウェア科学会 第16回大会論文集, D1-2, pp.37--40
開催年月日： 1999年9月
-
ソフトウェア設計変更支援のための依存論理の提案
新田 直也, 関 浩之
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
開催年月日： 1999年5月
本研究では, ソフトウェアの設計変更に伴う問題を形式的に扱うために, 新しい論理体系(依存論理)を提案する. 従来の論理が関数や関係を論理式の構成要素としていたのに対し, 依存論理では, 高階変数間の依存関係という概念を導入して, それを関数や関係を構成するより基本的な要素としている. これにより, ソフトウェアの設計情報とその設計に基づいて作成されたプロダクトを同じ枠組の中で扱うことが可能になる. 本稿では, 依存論理の構文と意味論を定義する. 特に依存論理の重要な部分クラスである一階依存論理に対して公理系を導入し, その公理系の健全性と完全性を証明する. さらに, 一階依存論理が任意の一般帰納的関数を定義できることも示す. また, データベース設計変更問題への適用についても触れる.
-
ソフトウェア設計変更支援のための依存論理の提案
新田 直也, 関 浩之
電子情報通信学会技術研究報告, SS99-1
開催年月日： 1999年5月
-
VRML立体プレイヤソフトの開発
竹本 賢史, 天野 隆平, 泰間 健司, 新田 直也, 小山 幸男, 木原 範昭
電子情報通信学会総合大会講演論文集
開催年月日： 1998年3月
-
16-3 デスクトップ3Dツールの開発
榎本 哲也, 山田 努, 小山 幸男, 木原 範昭, 山田 晃弘, 天野 隆平, 竹本 賢史, 泰間 健司, 平岡 淑子, 松田 武治, 塩野 一彦, 新田 直也
映像情報メディア学会年次大会講演予稿集
開催年月日： 1998年
MPEGやQuickTimeVR, VRMLなどのデータを活用し, 簡単に立体マルチメディアソフトを制作できるデスクトップ3Dツールを開発した.本ツールにより, 従来, 時間とノウハウを要したインタラクティブな立体マルチメディアソフトの制作が容易に実現できる.