802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.     

OpenFlow协议IPv6属性测试研究

鉴于SDN网络中数据转发与控制相互分离的特性,OpenFlow协议在其南向接口中扮演着重要的角色。随着下一代互联网的发展,IPv4可供分配的地址资源已然耗尽,瓶颈地位益发凸显。如何尽快部署IPv6,使其服务于社会生产与生活,使得当前网络与IPv6网络长期共存或平滑过渡到IPv6网络是工业界与学术界要解决的问题。SDN则提供了这样一个选项,其中OpenFlow协议是否支持IPv6协议便成为我们关注的重点。通过形式化方法对OpenFlow协议进行形式化建模,得到其非确定性有限状态机模型,在此基础上得到其测试生成树,以指导测试。同时,对于其是否支持IPv6进行重点关注,利用组合测试的方法,产生了167条测试例。 完成了测试引擎的开发,支持高效的测试生成算法,以及测试执行与判定。利用此测试引擎,以上述测试例为测试输入,执行测试过程,同时进一步对测试结果进行分析,得到了定量的分析结果,符合预期要求。     

FAE:一种OpenFlow协议FlowMod消息的action扩展机制

SDN网络对数据转发平面的抽象是OpenFlow等南向接口协议制定的前提,目前标准OpenFlow协议假设数据平面每个流表项由确定的规则定义和对应的动作集合组成,每个配置数据平面的FlowMod消息会携带这些规则和动作集合。然而,随着SDN应用场景的不断发展,OpenFlow协议有限的预定义动作难以满足一些新的配置需求,例如集中控制的段路由管理配置和SDPA的配置等。为了提高当前SDN对动作定义的灵活性,解除其对动作的限制,首先提出了一种基于OpenFlow协议FlowMod消息的action扩展机制FAE,该机制具有满足用户自定义动作,且动作扩展灵活简单的特点,然后基于开源的Floodlight控制器和FAST交换机实现了FAE机制,实验表明,该机制在集中控制的段路由下,可以有效地支持其管理配置中的动作。     

基于GSPM的安全协议检验工具

介绍一个基于GSPM的安全协议验证的图形化工具。验证工具以GSPM模型为基础形式化地描述了安全协议,并引进线性时序逻辑刻画了安全协议的性质,用基于状态搜索的模型检测方法在安全协议的验证过程中找出漏洞。以简化的NSPK协议为例,描述了该工具如何验证安全协议,表明GSPM模型和验证算法的有效性和正确性。     

基于层次CPN的OpenFlow建模研究

CPN作为一种形式化方法,得到了广泛的研究与应用,其在网络协议上和工业系统中的应用尤为突出。OpenFlow是一种新的网络交换模型,包含OpenFlow交换机和控制器。文中首先介绍了OpenFlow协议及CPN(Coloured Petri Nets),然后基于层次CPN对OpenFlow网络进行了建模,对每一层的模型都做了详细的说明,充分体现OpenFlow的工作机制。在建模的过程中,详细地考虑了模型中token的选取和变量的定义,使得CPN模型的执行可以描述OpenFlow的动态工作过程。通过CPN工具生成的状态空间对模型的性质进行了简单的分析,证明了它的活性、有界性。最后给出了下一步的研究工作。     

利用SPIN实现对OpenFlow协议的形式化验证

为了验证OpenFlow网络中网络控制器NOX系统内典型应用程序Pyswitch的正确性,采用Promela语言对经简化的OpenFlow网络中的网络元素、连接通道及拓扑结构进行建模,并使用SPIN工具对所建模型进行形式化验证。结果表明,Pyswitch在主机不发生移动的情况下结果正确,但在主机发生移动情况下,会由于pyswitch的MAC地址学习算法存在设计缺陷而产生错误。     

SPI演算规范的建模、实现验证研究

针对安全协议安全属性是否满足，缺乏有效性能评价方法的现状，大都使用SPI演算或相近的进程代数方法进行建模。利用这种方法不仅能够有效地形式化描述安全协议，并且能够对安全协议进行多方面的系统评价，但基本上没有说明怎么样寻找设计合适的验证工具，验证其安全属性实现的正确性。本文引入基于SPI演算的验证工具SPRITE来保证建模过程正确性，并设计给出实现映射的具体方法。本方法通过对典型的WOO-LAM单向认证协议予以说明，最后SPRITE产生的具体JAVA代码，给出了安全协议的安全属性，使形式化描述的协议的安全属性是否满足更接近于人的理解而不仅只是机器的解释。     

基于分段模型检测的云服务跨域认证协议的形式化分析与验证

针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。     

基于OpenFlow的数据流管控系统的研究与实现

随着网络技术的不断发展,在现有的网络设备及协议基础之上,对已有网络进行创新性试验变得越来越困难。OpenFlow是为支持网络创新究而提出的新型网络技术,它的出现为部署一个大规模的、完全可控、可定制的实验网络平台提供了可能。本文旨在基于OpenFlow设计实现一个数据流管控系统,其主要思想是利用OpenFlow技术实现控制与转发的分离,通过集中控制的方式,实现对全网数据流的管控,提高OpenFlow网络的安全性。     

RCC高速缓存一致性协议的带参验证

Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统,对此协议的带参验证是一个很大的挑战。 Cubicle是最近出现的基于SMT求解器的带参模型检测工具。我们使用了Cubicle带参模型检测工具,成功对RCC协议进行了建模和验证。实验结果表明, RCC协议在结点个数为任意规模时均满足协议的各种安全性质。     

基于Spin的SET协议模型检测研究

模型检测技术已成功地运用于验证复杂系统的性质。本文提出运用Promela语言对电子商务协议进行建模的方法,对比分析了有无入侵者时简化的SET协议的运行情况。运用Spin模型检测工具,对SET协议的Promela模型进行了检测,对电子商务协议中的关键性质认证性和保密性进行了分析与检测,发现了协议中的缺陷。     

基于SPIN的网络认证协议高效模型检测

为了有效地提高网络认证协议建模和验证的效率,基于模型检测方法提出一个通用的网络认证协议模型描述方法,结合模型检测工具SPIN可以方便地进行性质验证。通过一些模型的简化策略,不仅可以对不同协议进行高效建模,而且减小了模型的状态空间。与现有的文献相比,自动化程度较高,模型验证的效率较好。基于该方法,对PKM认证协议进行了模型检测,实验证明该模型分析验证方法的有效性,可用于其他网络认证协议的分析验证。     

一种保持OpenFlow功能完整性的TCAM流表压缩模型

随着OpenFlow协议版本的不断更新,其在数据平面上细粒度的控制能力得到了很大提升。然而,由于表项匹配域支持的任意通配符依赖TCAM进行匹配处理,随着OpenFlow匹配域支持字段的增加,设备中的TCAM存储空间面临很大压力。为此,提出一种减小TCAM中流表存储空间的数学模型FICO(A Function-Integral TCAM-saving Compression model for flow table of OpenFlow)。FICO首先根据匹配域不同字段间的关系,将字段之间的冗余分为三种。然后基于冗余提出三种预压缩算法,分别为域间字段合并、字段映射、域内字段压缩,最终组合为更小位宽的表项被送往TCAM中进行流匹配。通过仿真表明在保持OpenFlow功能完整性的前提下,较未压缩流表,FICO可以节省60%TCAM存储空间。并且随着流表规模的增大,压缩性能保持稳定。     

基于匹配动作表模型的可编程数据平面流表归并

与传统网络技术相比,SDN技术将网络的控制平面与数据平面分离,使网络具有一定的可编程能力。以OpenFlow、POF、P4等为代表,领域内常见的SDN交换机大多基于匹配动作表模型实现。与协议相关的OpenFlow等技术不同,协议无感知的SDN技术使用{偏移,长度}等结构表示协议字段,从而实现对任意协议字段的解析和处理。然而,待处理的数据包可能带有不同长度的数据包头,所以这些数据包中特定协议字段的偏移也会不同,需要多个匹配域偏移不同的流表去完成数据流的解析,从而造成流表和流水线结构复杂。针对上述问题,本文提出一种基于MAT模型的可编程数据平面流表归并方案,扩展MAT模型中的动作集,在数据包查询流表时使用特定的动作动态地调整数据包的起始偏移,使不同数据包同一协议字段的偏移保持一致,实现匹配域相同的流表的归并。本文方案在兼容VLAN、QinQ的POF Switch实验场景下,以跳转流表时多执行一条动作为代价,缩减了约69%的流表内存消耗。     

Comparing model checking and logical reasoning for real-time systems

We apply both model checking and logical reasoning to a real-time protocol for mutual exclusion. To this end we employ PLC-Automata, an abstract notion of programs for real-time systems. A logic-based semantics in terms of Duration Calculus is used to verify the correctness of the protocol by logical reasoning. An alternative but consistent operational semantics in terms of Timed Automata is used to verify the correctness by model checkers. Since model checking of the full model does not terminate in all cases within an acceptable time we examine abstractions and their influence on model-checking performance. We present two abstraction methods that can be applied successfully for the protocol presented.Received June 1999Accepted in revised form September 2003 by M.R. Hansen and C. B. Jones     

A game-theoretic framework for specification and verification of cryptographic protocols

We model security protocols as games using concepts of game semantics. Using this model we ascribe semantics to protocols written in the standard simple arrow notation. According to the semantics, a protocol is interpreted as a set of strategies over a game tree that represents the type of the protocol. The model uses abstract computation functions and message frames in order to model internal computations and knowledge of agents and the intruder. Moreover, in order to specify properties of the model, a logic that deals with games and strategies is developed. A tableau-based proof system is given for the logic, which can serve as a basis for a model checking algorithm. This approach allows us to model a wide range of security protocol types and verify different properties instead of using a variety of methods as is currently the practice. Furthermore, the analyzed protocols are specified using only the simple arrow notation heavily used by protocol designers and by practitioners.     

OpenFlow技术与商业价值

针对目前流行的OpenFlow技术,本文提出OpenFlow的标准进展、商业价值和连通性测试。该方法根据控制层面和转发层面相分离的技术,采用移动研究院内网拓扑进行测试。实验结果表明,通过在BigSwitch controler上进行相关命令配置就可实现二层的OpenFlow交换机互联的不同网段主机的通信。OpenFlow是SDN技术中一种关键的接口协议,SDN是对网络的抽象, OpenFlow是对单个转发面设备的抽象。OpenFlow交换机和Control er的出现为新型互联网（NGN）体系结构的研究提供了实验途径。     

Model checking communicative agent-based systems

Model checking is a formal technique used to verify communication protocols against given properties. In this paper, we propose a new model checking algorithm aims at verifying systems designed as a set of autonomous interacting agents. These software agents are equipped with knowledge and beliefs and interact with each other according to protocols governed by a set of logical rules. We present a tableauased version of this algorithm and provide the soundness, completeness, termination and complexity results. A case study about an agent-based negotiation protocol and its implementation are also described.