2018 Fiscal Year Research-status Report
情報流解析による安全性検証に基づく実用的なソフトウェア開発支援
| Project/Area Number |
17K12666
|
|---|
| Research Institution | Nanzan University |
|---|
Principal Investigator |
桑原 寛明 南山大学, 理工学部, 講師 (30432222)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | ソフトウェア工学 / 情報流解析 / 型システム / プログラム解析 / ソフトウェア開発支援 |
|---|
| Outline of Annual Research Achievements |
本年度は、型検査に基づく情報流解析における制約付き機密度パラメータに関する研究を行った。機密度パラメータは、データ構造の一部を構成するデータの機密度を具体的な機密度ではなくパラメータとして記述するための仕組みであり、データの機密度を定義時ではなく使用時に決定することを可能にする。これにより、一部のデータの機密度のみが異なるデータ構造が必要な場合に、機密度を変えながら大部分が同一の複数のデータ構造を定義しなくてもよい。しかし、機密度パラメータにどのような機密度が指定されても非干渉性を満たしていることが要求されるため、記述できるプログラムに関して柔軟性に欠ける部分があり、この問題の解決を目指した。
解決策として、機密度パラメータに対して制約を与える手法を提案した。機密度パラメータに対して制約を満たす機密度が指定された場合に非干渉性が満たされることを検査する型システムを定義し、その健全性を証明した。これにより、機密度パラメータに対して任意の機密度ではなく制約を満たす機密度が指定された場合に限って型付け可能となるようにプログラムを記述すればよいため、プログラム記述の柔軟性が向上する。健全性により、型付け可能なプログラムであれば機密度の高いデータが機密度の低いデータに影響を与えるような不正な情報流を含んでいないことが保証される。
これらの成果について国内の会議で発表した。また、論文誌に投稿中である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
およそ当初の計画通り進行している。ライブラリとユーザプログラムの情報流解析の統合については完了していないが、制約付き機密度パラメータの応用として解決できると考えている。一方、当初は予定していなかった制約付き機密度パラメータのためのアノテーションについて着手した。
|
| Strategy for Future Research Activity |
次年度についても当初の計画に従って研究を進める。ただし、統合開発環境における情報流解析の実現に関して、既存のツールが特定のコンパイラに依存した実装になっており、統合開発環境のコンパイラに単純に入れ替えられない可能性があり、その場合は独立したツールとして実現する。また、当初は予定していなかった制約付き機密度パラメータに対応した情報流解析の実装方法についても研究を進める。
|
| Causes of Carryover |
旅費に関して他の予算から多く充当できたため次年度使用額が発生した。
物品費あるいは出張旅費に充当する予定である。
|
Research Products
(6 results)
