実現不能な仕様の欠陥情報を用いて部分プログラムを合成する方法に関する研究

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12780194
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
• Keywords: リアクティブシステム / 実現可能性 / プログラム化可能性 / 時間論理 / プログラム合成

Research Abstract

本年度は、実現不能な仕様の欠陥情報を用いて部分プログラムを合成するため欠陥情報の検出方式の形式化を行なった。また、その導出手続きの構成を行った。また、ネットワーク上で、いくつかのセキュリティシステムの構成を行った。
1.仕様の段階的充足不能性の原因について考察し、その形式化を行った。また、その導出手続きを構成し、その手続きについて考察を行った。その結果、出力に関して決定化を行うだけでは、段階的充足不能の原因の健全な手続きを作ることができるが、それだけでは完全とはならないことがわかった。このため、段階的充足不能の原因を充足可能性を検査するタブローから計算するためには、新たな決定化のためのパラメータを付随して、計算する必要がある。
2.HTTPの中継のためのリアクティブシステムの実装を実際に行なった。これは、ファイアーウォールを導入したネットワークにおいて、ユーザインタラクションのパターンに応じて中継の可否を切り替えるシステムである。
ここで取り扱われる中継のための仕組み(状態繊維)単純なので、本研究での仕様と検証における実例として使いたいと考えている。
3.いくつかのセキュリティのためのシステムを組込んだUNIX OSの拡張を行った。これは現UNIXのユーザ権限のデザイン、特にルート権限を見直すことによって、ネットワークを通じての成り済ましなどの可能性を減らす拡張である。
ここで実装を行ったネットワークアクセスを行うまでの権限の委譲のシステムについても上記の検証システムによって実際に検証できればと考えている。

Research Products

• [Publications] K.Masui, M.Tomoishi, N.Yonezaki: "Design of UNIX system for the prevention of damage propagation by intrusion"Proceedings of Information Security Conference(LNCS). 2200. 536-552 (2001)
• [Publications] 増井健司, 友石正彦, 米崎直樹: "送受信内容の相関を利用したHTTPアクセス制御のためのプロキシ"マルチメディア、分散、強調とモバイルシンポジウム. (2001)
• [Publications] 増井健司, 友石正彦, 米崎直樹: "送受信メッセージのパターン解析によるHTTPアクセス制御"日本ソフトウェア科学会第18回大会論文集. (2001)