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

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

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