2017 Fiscal Year Research-status Report
理論的な安全性評価が可能な耐タンパーソフトウェア技術の研究
| Project/Area Number |
15K00183
|
|---|
| Research Institution | Tokyo University of Technology |
|---|
Principal Investigator |
布田 裕一 東京工科大学, コンピュータサイエンス学部, 准教授 (50706223)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
宮地 充子 大阪大学, 工学研究科, 教授 (10313701)
CHEN Jiageng 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (90640748) [Withdrawn]
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | 難読化技術 / White-Box Cryptography / 形式検証 |
|---|
| Outline of Annual Research Achievements |
携帯端末において、インターネットバンキングなどの高いセキュリティレベルが必要となる場面が増えている。携帯端末アプリケーションをダウンロードして処理を実行するため、プログラムコードや実行中のデータの一部を用いて解析するタンパー技術に対抗する、耐タンパー技術が必要になる。White-Box Cryptography(以下でWBCと略記)技術は、プログラムデータや実行中のデータのすべてにアクセス可能な攻撃者に最も有利な状況においてもセキュリティを維持する技術であるため重要である。平成29年度は、1.AES暗号の WBC技術の方式案に対する理論的検証、2.公開鍵暗号のWBC技術の方式案の検討及び3.WBC技術の安全性や計算量の評価における形式検証で必要な形式検証モデルの検討を実施した。
1に関しては、WBC技術の攻撃であるDifferential Computation Analysis(DCA)について検討した。考案した方式案のダミーテーブル作成において、有効な改良方法として入力によりテーブル選択やダミーの出力値を変化するものを考案した。
2に関しては、プログラムの中間値が漏えいするが、漏洩させる情報を攻撃者がコントロールできないというGray-boxに近い攻撃モデルを検討した。公開鍵暗号の理論における仮定（最上位ビットが1）などが、現実のシステムではNISTのテストデータにおいても前提とできない矛盾が生じている。任意の入力においても、攻撃者が情報を入手できないアルゴリズムを検討した。
3に関しては、暗号プロトコルの攻撃を形式的に導出するProVerifにおいて、観測透過性を利用したWBCの攻撃モデルの記述方法について検討した。プロセス内で公開通信路に中間値のデータを出力させて、攻撃者が取得できるような記述方法を検討し、サンプルコードを作成しProVerifで動作検証を試行した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
平成29年度の目標は、AES暗号のWBC技術の方式案に対する理論的検証と実装検証と、公開鍵暗号のWBC技術の方式案の考案と理論的検証であった。AES暗号に関しては理論的検証が完成しておらず、実装検証については検討が遅れている。公開鍵暗号のWBC技術については、Gray-boxに近い攻撃モデル及び方式案を検討した。White-Boxの攻撃モデルの形式検証については、攻撃モデルの記述方法の検討が進んでいる。これについては、予定を前倒して実施しているが、AES暗号の実装検証が遅れており、全体としてはやや遅れている状況であると判断した。
|
| Strategy for Future Research Activity |
「現在までの進捗状況」で述べたAES暗号のWBC技術の方式案に対し、DCAの攻撃方法を含めた攻撃への安全性の理論的検証を完成する。さらに、方式案を計算機上で実装し計算時間や使用メモリ量を計測して、実装検証を実施する。公開鍵暗号のWBC技術の方式案に対しては、検討した方式モデルに基づいて方式案を考案し、理論的検証及び実装検証を実施していく。また、計算量の見積もり及び安全性検証ための形式検証ライブラリについて作成する。さらに、ProVerifにおけるWBCの攻撃モデルの記述方法を作成し、考案した方式の形式検証を実施する。
|
| Causes of Carryover |
（理由）
方式案の実装検証のための計算機環境の構築についての費用や、研究協力者との打ち合わせによる旅費の執行はできたが、国際会議発表などによる旅費の執行が遅れており、旅費の使用が減ったため。
（使用計画）
H30年度に国際会議発表や研究打ち合わせによる旅費執行を実施していく。考案した方式の形式検証のための計算機環境構築に関する費用も予定通り使用する。
|
Research Products
(6 results)
