経路保証プロトコルの効率的な安全性検証手法の開発

路由保证协议高效安全验证方法的开发

• 批准号: 21K11866
• 负责人: 小島 英春
• 金额: $ 2.58万
• 依托单位: Osaka Institute of Technology (2022)Osaka University (2021)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2021
• 资助国家: 日本
• 起止时间: 2021-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21K11866/
• 关键词: 安全性検証; 経路保証プロトコル; モデル検査; 無線マルチホッププロトコル

本研究では，経路保証プロトコルの安全性の検証を行う．対象となる経路保証プロトコルは，無線アドホックネットワークや無線センサネットワーク上で動作することを想定しており，端末が動的にネットワークへ参加や離脱を行うことが考えられる．このようなネットワークでは，さまざまな経路が構築される可能性がある．どのような経路が構築されても，適切に経路保証を行うことができることを示す．検証を行うにあたって，端末数が増加すると構築可能な経路の数が爆発的に増加することが挙げられる．その場合，全ての構築可能な経路を対象に検証を行うことは非常に難しい．そこで，効率的に検証を行う方法を開発する．検証を行うために，安全性を検証するためのツールを用い，そのツールのためのモデルを構築する．このモデルは，経路保証プロトコルの動作を表しており，端末間の接続状況を用いてどのような経路が構築されているかを表すネットワークトポロジも表現する．このトポロジを表現する際に，トポロジ形状が同じ場合には，同じ状態とみなすことで，検証の対象となる経路を削減することを目指す．対象となる経路削減方法を開発し，その方法を用いて安全性検証を行う．ツールにその方法を適用し，実行時間の比較，使用メモリ量の比較を行うことで，効率的に検証を行うことが可能であることを示す．

在本研究中，我们验证了路由保证协议的安全性。假设目标路由保证协议运行在无线自组织网络和无线传感器网络上，并且可以想象终端将动态地加入和离开网络。在这样的网络中，可以构建各种路由。我们表明，无论构建什么路由，都可以适当地执行路由保证。在进行验证时需要注意的是，随着终端数量的增加，可构建的路由数量呈爆炸式增长。在这种情况下，验证所有可能的路线是极其困难的。因此，我们将开发一种有效执行验证的方法。为了执行验证，我们使用工具来验证安全性并为该工具构建模型。该模型代表了路由保证协议的运行，也代表了网络拓扑，它显示了利用终端之间的连接状态构建什么样的路由。在表示此拓扑时，我们的目标是通过假设如果拓扑形状相同，则它们处于相同状态，从而减少需要验证的路由数量。我们开发了一种目标路线缩减方法，并使用该方法进行安全验证。我们证明，通过将该方法应用于工具并比较执行时间和内存使用情况，可以有效地执行验证。