暗号アルゴリズムのハードウェア実装およびプロトコルの形式検証の研究

点击翻译按钮获取中文摘要

暗号をはじめとするセキュリティ技術は、アルゴリズム・実装・プロトコル・応用からなるが、安全性の確保が重要な課題となる。しかしながら、安全性のチェックには人手が必要であり、正確な評価がしにくい面がある。そこで、論理学的手法を用いて形式的に安全性を評価することを目指す。従来、暗号プロトコルについてはかなりの研究が進んでいるが、アルゴリズムや実装、および応用については不十分であった。そこでここでは論理学、特にModal Logicを用いたモデルリングを行う。Modal Logicは攻撃を定式化すに役立つもので、楕円曲線暗号の解読、コンピュータウィルスをはじめとするマルウェアのアタックの解析、防御に適用していく。実質研究期間は半年であったが、今年度は、昨年度実施したマルウェアに関する不正ソフトウェアや対策システムのフォーマルメソッドによる定式化をさらに一般化し、評価及び改良を行った。これにより、従来人手で行っていた多くのセキュリティシステムの安全性チェックのかなりの部分を改良できた。具体的には、前年度までに行ったマルウェア(malicious software)の概念のフォーマルメソッドでの定義を一般化し、ある種のModal Logic言語における単一文とみなした。この抽象化により具体例とは切り離した形で定式化可能となるが、実際の事例に応用はできるようになる。ベースとなる概念は正当性(不正当性)の因果関係の明確化にあり、マルチエージェントシステムにおけるアカウンタビリティ、トラストエージェントの計算可能性、インターアクティブ計算などを考慮・検証する。副産物として、良性ソフトウェアであるベンウェア(benign software)や耐マルウェアであるanti-malware、具体的な形態のメドウェア(medical software)などを定式化した。また実用的な成果としては、マルウェアやその派生物の検知、比較、分類を行うための理論的基盤を示した。