2019 Fiscal Year Research-status Report
情報流解析による安全性検証に基づく実用的なソフトウェア開発支援
| 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アノテーションは既に提案していたが、これを拡張して機密度パラメータのためのアノテーションを追加した。
本年度は、Rustプログラムに対する情報流解析のための型システムの研究にも取り組んだ。当初の計画にはなかったが、Rust言語が注目を集め始めているため着手し、Rustのサブセット言語を対象に情報流解析のための型システムを構築した。Rust言語は、メモリ操作の安全性を静的に保証し、かつシステムプログラムの開発が可能であるため、今後広く利用される可能性がある。このようなプログラミング言語に対して、機密情報の観点からプログラムの安全性を検証する情報流解析を実現することは、安全なプログラムの実現のために重要である。
以上の成果について国内の会議で発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初計画していた非機密化機構については研究が進展していないが、計画していなかったRust言語向けの情報流解析について研究を進めることができた。そのため、総合的には順調に研究が進展していると判断した。
|
| Strategy for Future Research Activity |
本年度に研究を進めた型検査アルゴリズムとJavaアノテーションに関してさらに研究を進める。特に、実装を完了して実際に動作するツールとして実現し、統合開発環境との融合を図る。また、昨年度に研究を行った制約付き機密度パラメータへの対応を進める。
|
| Causes of Carryover |
参加予定の会議や研究会が開催中止となり、計画していた旅費が執行できなかったためである。
次年度の物品費あるいは旅費に充当する計画である。
|
Research Products
(3 results)
