zoukankan      html  css  js  c++  java
  • CPNtools协议建模安全分析(一)

           本文根据最近整理的CPNtools论文和CPNtools官网上的说明,以及参照了乌克兰敖德萨 ---国家电信研究院运输和通信部关于   电信系统协议仿真关于CPNtools的学生讲义。基于此和和自己的理解整理的关于CPNtools在协议建模状态空间分析以及其他的一些特征。具体的介绍基于对CPNtools的工具的实际操作来说明。

           因为CPNtools是丹麦奥尔胡斯大学(Aarhus University)大学团队开发的软件,所以在该学院的 Department of Computer Science 部门有很多相关使用该软件做的工作。 学院官网地址:https://cs.au.dk/  可以在搜索栏中检索相关的CPNtools资料

          因为考虑了一下写的内容可能比较多,所以大体上分成几个章节来写。如果后续写的太多,我会在每个博客做超链接到其他博客页面。(这项工作我会分成大概一周时间完成)

         因为CPNtools官网上的介绍没有针对如何建模协议来讲,而且手册部分也很简单对做协议分析内有什么大的帮助。所以综合了很多材料,对CPNtool如何来建模协议模型想具体的写点东西。算是对自己论文的一个辅助材料,凡做事必须讲究认真。严谨的逻辑,不可捕风捉影,协议的形式化分析也必须是合乎规定,任何协议的形式化建模之前必须要根据协议组织的规范文档来做。

    第一部分:界面的功能组件的介绍

     1.1 CPNtools的安装

         Windows安装:在官网上 http://cpntools.org/ 上下载界面下载 基于Windows版本的最近版本 ,下载之后安装即可

         Linux 安装:Linux安装之后会出现调用公用库的 libxml2.so.2  报错的问题,提示报错信息:: libxml2.so.2 cannot open shared object file: No such file or directory 解决问题的方法:使用   find 命令查询是否存在该库, 如果存在是否是对应软件版本和系统版本的不匹配问题, 如果没有下载安装即可, 如果有但是关联存在问题,使用 ln -sf 命令 对库文件的地址执行关联。 具体的执行步骤见图

          

      如果按照上面的操作还是提示不能读取文件,提示下面的信息:

           ./cpntools: error while loading shared libraries:  libxml2.so.2: cannot open shared object file: No such file or directory

    • 、首先打开/etc/ld.so.conf文件
    • 、加入动态库文件所在的目录:执行vi /etc/ld.so.conf,在"include ld.so.conf.d/*.conf"下方增加"/usr/local/lib"。(具体的看自己的文件库位置)
    • 、保存后,在命令行终端执行:/sbin/ldconfig -v;其作用是将文件/etc/ld.so.conf列出的路径下的库文件缓存到/etc/ld.so.cache以供使用,因此当安装完一些库文件,或者修改/etc/ld.so.conf增加了库的新搜索路径,需要运行一下ldconfig,使所有的库文件都被缓存到文件/etc/ld.so.cache中,如果没做,可能会找不到刚安装的库。 一般情况下可以解决共享库不能加载的问题,但是有时候用户还是提示不能加载库,这个时候应该考虑是否是用户自己添加的软件或者自己生成的 .so动态库没有执行权限。

      安装完成之后操作的主界面如下。

     1.1.1 我们先举一个简单的登录协议的模型

       setp 1 首先创建两个库所,分别表示  Send 和 Reciver ,在创建一个变迁表示 网络 NET

         接下来声明颜色集合变量的类型,建模的简单模型结构件下图:

        

      step2 这里注意,颜色集绑定的数值标记定义好之后,在变迁NEt中会自动出现,变迁的绑定初始值,这个时候我们需要点击变迁的左下方的小三角,来选择需要绑定的初始值,也就是将变迁使能。变迁使能绑定初始值见下图,这里我么选择绑定(n=1,p="one")

    step3 在弧上写上弧表达式, 我们定义了 var n=INT   p=DATA , 所以从 SEND---->Reciver  弧的表达式为 (n,p), 这里 从变迁NET到 Reciver端我们 使用函数 来判断发送的数据。

    step4 ,现在我们来模拟数据从Send 发送到Reciver端,条件不符合的时候输出 fail  ,条件满足的时候输出 sucess

     

     

    这里我们要注意的是几点容易出错的问题

    •     颜色集申明的时候 不能和 默认的(Standard declarations)中的申明重复
    •     在标记颜色集的数值的时候,注意 1`(1,"shijian")++   中的符号  `  不是英文的分隔符  ’  
    •     变迁的初始值绑定是根据在于其输出的库所中的值决定的,但是需要自己手动来绑定

    我本想这将主款工具界面操作部分汉化,但是官网上不发布 CPNtools的源代码版本,只支持对托管源代码的Subversion存储库开放。

    1.1.2 tools BOX 的介绍

          我从最常用的工具开始介绍:

       Creat: 创建工具。  (功能介绍部分我全部放在图像上面,这样方便大家阅读。)

    菱形表示创建一个变迁, 椭圆表示创建一个库所,单箭头表示创建弧

    1.2 Petri网--CPNtools 层级网络介绍

      CPNtools最近被Nokia 被用来模型驱动的新一代手机的开发, CPN建模工具提出了强大的Petri网建模工具,一个抽象对象可以使用层级网络建模分析,简单的()

     第二部分: 原理的介绍

    第三部分:简单协议的建模举例

    第四部分:协议建模分析

    第五部分:协议状态空间分析

    第六部分:协议添加攻击模型的分析

    第七部分:

    参考文献:

    [1] Simonsen K I F , Kristensen L M . Towards a CPN-based modelling approach for reconciling verification and implementation of protocol models.[C]// International Workshop on Model-based Methodologies for Pervasive & Embedded Software. Springer, Berlin, Heidelberg, 2012.

    [2] Yiqin Lu, Fang Fang, Runqing Quan. A simulating model of NGN based on CPN tools[M]// Theoretical and Mathematical Foundations of Computer Science. 2011.

    [3]D.A.Zaitsev, T.R.Shmeleva. Simulatiing of Telecommunication Systems with CPN Tools[M]// Affiliated on meeting of Communication Networks Department Transaction NO 4 of 10.11.2006.

    [4] Wells L . Performance Analysis using CPN Tools[C]// Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, Pisa, Italy, October 11-13, 2006. DBLP, 2006.

    [5]Kent Inge Fagerland Simonsen, Lars M. Kristensen, Ekkart Kindler. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification[M]. Springer Berlin Heidelberg, 2016.

    [6]Kent Inge.Code Generation from Pragmatics Annotated Coloured Petri Nets Simonsen.[M]//

    [7]https://www.cpntools.org

    [8]Ole Martin Dahl. Using Colored Petri NEts in Penetration Testing

     

  • 相关阅读:
    1657: [Usaco2006 Mar]Mooo 奶牛的歌声
    1610: [Usaco2008 Feb]Line连线游戏
    1660: [Usaco2006 Nov]Bad Hair Day 乱发节
    bzoj1207 [HNOI2004]打鼹鼠
    bzoj1046 [HAOI2007]上升序列
    bzoj3594 [Scoi2014]方伯伯的玉米田
    bzoj1878 [SDOI2009]HH的项链
    bzoj1293 [SCOI2009]生日礼物
    bzoj3211 花神游历各国
    bzoj3038 上帝造题的七分钟2
  • 原文地址:https://www.cnblogs.com/xinxianquan/p/12102479.html
Copyright © 2011-2022 走看看