2018 Fiscal Year Research-status Report
| Project/Area Number |
18K11262
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
小島 英春 大阪大学, 情報科学研究科, 助教 (90610949)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
矢内 直人 大阪大学, 情報科学研究科, 助教 (30737896)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | モデル検査 / 状態爆発抑制 / 経路保証プロトコル / 無線マルチホッププロトコル / 形式検証 |
|---|
| Outline of Annual Research Achievements |
本研究は，モデル検査を行うにあたって，モデル検査の問題点である状態爆発を抑制するために，トポロジの同型判定を利用した状態数削減手法を用いて複数の状態を等価なものとして扱う方法を開発，さらに，状態を等価と扱う際に署名も等価であることを示すことで署名の正しさも検証する手法を開発することである．その進め方は，１：状態数抑制手法を進め，AODVやDSRなどに適用したのちに２：署名に関する研究開発を進め，ISDSR など経路保証プロトコルを対象にする予定である．現時点では，モデル検査器SPINを対象に，１：の状態数削減手法を進めるにあたり，トポロジの同型判定を利用した状態数削減手法を用いて進めており，研究会において発表を行った[1][2]．AODVをSPINで用いるモデル言語であるPromelaを用いて実装し，その実装に対して状態数削減手法適用の基本的な考え方や実装方法について述べている．現時点では，状態数削減手法を実装するにあたって，SPINのソースコードの解析やSPINによって出力されるモデル検査を行うC言語のソースコードの解析を行い，手法の実装を進めている．
[1] 小島英春, 矢内直人, 経路保証プロトコルを対象にしたSPIN を用いたモデル検査にむけて, 第16回電子情報通信学会ネットワークソフトウェア研究会, 2018
[2]小島英春, 矢内直人, アドホックネットワークプロトコルのモデル検査における状態数削減手法, 第18回電子情報通信学会ネットワークソフトウエア研究会予稿集, 2019.
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
SPINとProverifを対象に状態数削減手法の実装を進める予定であったため，両方に適用できるように手法を進めていたが，どちらにも適用できるような汎用的な手法として進めていた点も進捗を遅らせた理由の１つであると考えている．そのため，SPINを対象に状態数削減手法を進める．
そのSPINは，モデル言語Promelaで作成したモデルをSPINに入力し，モデル検査器として動作するC言語のソースコードを出力する．状態数削減手法を実装するにあたって，SPINのソースコードの解析やSPINが出力するC言語のモデル検査を行うソースコードの解析を行い，どこをどのように修正することが必要かを調べる必要があった．その調査に時間がかかった点が研究の進捗を遅らせた原因であると考える．
特に，SPINが出力するC言語のモデル検査を行うソースコードは，探索を行う際に利用される構造体，関数のコード量が多く複数のファイルに分散して記載されているため，解析が遅れた．また，当初予定していた，大学院生１名と共に進める予定であったが，適任者がいなかったため，現時点では，代表者と分担者で研究を進めている点も進捗が芳しくない理由の１つである．しかし，現時点では，SPINによって出力されるC言語のソースコードの解析に目処が立ち，実装を進めており，国際会議に１編投稿済みである．
|
| Strategy for Future Research Activity |
本研究は，当初の目標として，以下の２点を行う予定である．
１：トポロジに注目した状態数抑制手法を進め，AODVやDSRなどに適用する．（１-１：トポロジの同型判定方法の確立，１-２：モデル検査器への状態削減手法の実装）
２：署名に関する研究開発を進め，ISDSR など経路保証プロトコルを対象にする（２-１：１：の手法を適用した際の署名アルゴリズムの改良，２-２：経路保証プロトコルの署名の安全性検証）．
１の手法については１-１が完了し，１-２の実装を進めており，SPINに実装中である．２：については，まずは１が完了する必要があるため，今年度前半に１：を完了させる予定である．また，１：では，AODVやDSRとしているが，２：で対象としているISDSRはDSRを拡張したものであるため，１：についてはDSRを優先的に進め，それが完了したのち，１：の続きとしてAODVを進めつつ，ISDSRを対象にした２：も並行して進めていく．
１：と２：の手法については完成すると考えているが，それを実現するためのモデル検査器をSPINとProverifの両方を同時に進行していくのは難しいと考えているため，SPINを優先して進めていく予定である．
|
| Causes of Carryover |
当初予定していた，国際会議への参加が行えなかったため，そのための旅費が使用されていないことが大きな要因である．
平成３１年度は，国際会議への参加回数の増加と論文誌への投稿を行うことで，平成３０年に使用することが出来なかった金額に対して使用をする予定である．
|
