2009 Fiscal Year Annual Research Report
| Project/Area Number |
21500046
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
NOWAK David National Institute of Advanced Industrial Science and Technology, 情報セキュリティ研究センター, 研究員 (40443212)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山田 聖 独立行政法人産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (80415760)
|
|---|
| Keywords | ディペンダブル・コンピューティング / ソフトウェア学 / 暗号・認証等 / 形式手法 |
|---|
| Research Abstract |
1.代表者であるNowakは、暗号のソフトウェア実装の安全性を証明するための、新たな手法を提案した。本手法は、暗号アルゴリズムの安全性証明法である、安全性の問題をゲームで定義しそれを変換していくことで数学的問題との等価性を証明する手法(game-based手法)の拡張である。本手法はて(1)アルゴリズムレベルの安全性定義を現実の製品に近い実装レベルの安全性定義へと引き上げる手法と(2)実装レベルにおける、新たなゲームの変換手法から構成されている。
Nowakは中国科学院のZhang氏と共同で、任意の一様なデータを標本抽出するという処理をランダムビットとして実装する問題と、それがgame-basedな安全性証明においてどのような影響を与えるかについて研究を行った。本課題を研究するにあたり、Nowakは9月8日から17日の間北京にZhangを訪問し、Zhangを12月6日から11日の間日本に招聘した。本課題の予備的な結果は、international workshop on Developments in Implicit Computational complExity(DICE 2010)で発表された。
2.平成21年度、Nowakがこれまで開発してきた、アセンブリ言語で書かれたプログラムの検証Toolboxを拡張した。分担者である山田は、コンピュータ上での整数表現を扱うライブラリを開発し、その結果を第12回プログラミングおよびプログラミング言語ワークショップ(PPL2010)で発表した。
3.産総研の同僚であるAffeldtと連携し、Nowakと山田は、アセンブリ言語で書かれた疑似乱数生成器の実装に対し、安全性の証明を付与することに成功した。本成果は9th international workshop on Automated Verification of Critical Systems(AVoCS 2009)で発表された。
|
