2020 Fiscal Year Annual Research Report
Practical Software Development Support based on Safety Verification using Information Flow Analysis
| Project/Area Number |
17K12666
|
|---|
| Research Institution | Nanzan University |
|---|
Principal Investigator |
桑原 寛明 南山大学, 理工学部, 講師 (30432222)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | ソフトウェア工学 / 情報流解析 / プログラム解析 / 安全性検証 / ソフトウェア開発支援 |
|---|
| Outline of Annual Research Achievements |
本年度は、機密度パラメータ付き情報流解析における機密度ワイルドカードおよび機密度ワイルドカードのためのJavaアノテーションに関する研究を進めた。機密度パラメータは情報流解析の対象となるプログラムの記述性を向上させるための仕組みであるが、機密度ワイルドカードによって柔軟性が改善され、プログラムの書きやすさがさらに向上する。既に提案済みである機密度パラメータ付き情報流解析のための型システムを拡張して機密度ワイルドカードに対応した型システムを構築した。また、情報流解析に必要な機密度などをJavaプログラム中に記述するためのJavaアノテーションも既に提案しているが、機密度ワイルドカードを記述できるようにアノテーションを拡張した。以上の成果について国内の会議で発表した。
期間全体を通して、情報流解析における機密度のパラメータ化、制約付き機密度パラメータ、機密度ワイルドカードを提案し、それぞれに対応した型システムを構築した。また、Javaプログラムに対する情報流解析を実現するために、機密度パラメータや機密度ワイルドカードを記述するためのJavaアノテーションを定義し、型検査アルゴリズムを構築した。さらに、危険なメモリ操作を排除する機構を備えたRust言語のサブセットを対象とする情報流解析のための型システムの構築も行った。これらにより、研究目的である「情報流解析に基づくソフトウェアの安全性検証」の理論的基礎を確立できた。以上の成果は雑誌論文や会議で発表している。今後は、これらの手法を実用に供するために、型検査アルゴリズムやJavaアノテーションの処理系を実装しソフトウェア開発環境に組み込んでいく必要がある。
|
Research Products
(4 results)
