模型检测中的CTL形式化描述模板

针对SPS(specification pattern system)和Prospec(property specification)不能将组合命题形式化为模型检测器可以接受的CTL(computation tree logic)公式问题,通过研究SPS和Prospec产生系统性质描述的形式化方法,并对比CTL与FIL(future interval logic)的表达能力以及CTL与LTL(linear temporal logic)两者之间的关系,构造了一类具有较强描述能力的CTL公式模板,并通过重新定义合取逻辑运算符来简化公式.该类模板简洁且易于理解.模板类的正确性证明表示该类模板可以有效地描述系统性质.利用该模板得到的CTL公式可以直接应用到模型检测器中,利于系统性质验证.     

基于IPv6的入侵检测系统

针对IPv6环境下出现的网络安全问题,设计了一种基于IPv6的入侵检测系统模型———IDSMIPv6。该模型的关键技术模块包括特征检测、规则管理和高速匹配及网络阻断。通过构建仿真实验环境,对系统进行攻击检测效果测试,验证本系统的数据包的捕获、解析和检测等性能。实验结果表明,IDSMIPv6系统对攻击的漏报和误报率极低,达到了预期的目标。     

带有异或运算安全协议的自动化检测

针对当前模型检测工具普遍不能检测带有异或运算安全协议的问题,提出了一个新的模型检测器SAT#.该模型检测器通过引入抽象异或项的概念及其运算规则,大大降低了攻击者生成的异或消息数量,解决了由于引入传统异或运算导致的状态空间爆炸问题.在此基础上,通过在SAT模型中增加基于抽象异或项的重写规则,扩展了攻击者的异或运算能力,实现了对带有异或运算安全协议的自动化检测.通过对BULL协议的检测,证明了抽象异或项的实用性,同时也证明了SAT#模型检测器的可靠性.     

NS密码协议的模型检测分析

密码协议安全性的分析是网络安全研究领域的一个主要内容,研究人员提出多种形式化方法来分析这个问题.模型检测工具Spin是一个广泛验证并发系统性质的工具,可用来分析密码协议.对Neeclham-Schroeder(NS)协议认证部分进行了详细的分析,结果表明,Spin可成功检测出NS协议的缺陷,并生成攻击的序列.     

移动IPv6协议安全机制优化

移动LPv6利用IPv6的一些新特点来支持移动IP,IPv6网络中引入移动IP协议给网络带来了安全隐患。分析了IPv6、移动IPv6的安全机制．针对移动IPv6面临的主要安全问题,优化了移动IPv6现有的安全机制。     

多媒体会议的逻辑描述模型

为了对多媒体会议的内在逻辑结构进行描述和研究,提出了一个基于媒体关系和依存关系的逻辑描述模型,对该模型进行了形式化和非形式化的定义,分析了模型内基于上述2种关系的语义规则,并给出了从语义规则和模型结构2方面对模型进行扩展的机制。作为验证,使用该模型对一个多媒体会议的具体实例进行了描述。分析和实践均表明,该模型不但能够清晰而严格地描述多媒体会议中的媒体关系结构和逻辑联系结构,而且还可以通过灵活的扩展机制,适用于各种大规模的、复杂机构的、特定情景的多媒体会议系统。     

IPv6环境下的入侵检测系统模型设计

IPv6将作为下一代Internet的网络协议，对信息安全提出了新的挑战，入侵检测技术也需要进一步发展。针对此提出了IPv6环境下入侵检测系统模型(IDSMIPv6)。探讨了流量分析、网络阻断、灾难恢复、IP追踪、快速捕包和高速地址匹配等关键技术，并利用协同技术，实现了各个模块的总体控制。依据此系统模型构建的IPv6环境下的入侵检测系统软件在实践中得到了良好的验证。     

移动IPv6协议安全性分析与改进

分析了IPv6、移动IPv6协议,重点对移动IPv6的安全性进行了分析．针对移动IPv6所面临的绑定更新（BU）和路由优化（RO）这两种主要安全威胁,提出了移动IPv6的改进方案,以进一步提高其安全性．     

基于IPv6的网络入侵检测技术研究

IPv6技术是下一代互联网的核心技术。通过分析现有网络安全系统的基本原理,针对IPv6网络的特点,提出在IPv6环境下采用基于协议分析和模式匹配技术相结合的入侵检测系统架构。采用该系统架构能够更快、更有效地处理信息数据帧和连接,同时能够判断一个通信的实际内容及具体含义,具有抗躲避性强、系统资源占用小、检测速度高、误报率低的特点。     

基于构造类别代数的数据流和控制流相结合的协议测试

如何从协议规范中生成即考虑控制流又兼顾数据流的测试用例是一个很有挑战的问题, 本文提出了一种基于构造类别代数的数据流与控制流相结合的测试方法, 给出了在其上的测试用例生成算法, 有限状态机模型到构造类别代数模型的转换算法, 并且给出了在一个实际的路由协议RIP 的测试中的应用例子.     

移动IPv6中的QoS保障

移动计算正变得越来越广泛,为Internet设备提供QoS保障和移动支持已成为新一代互联网技术的研究热点.介绍了移动IPv6及为改善其性能的增强协议,分析了在移动环境中提供QoS存在的问题,讨论了在移动环境中RSVP的移动性支持面临的挑战,分析了最近提出的支持RSVP移动性方法的优缺点,给出了研究移动IPv6和RSVP的方向.     

分级移动IPv6中一种新的鲁棒移动性管理方案

提出了一种针对分级移动IPv6的鲁棒移动性管理方案. 采用了ICMPv6消息发现MAP故障，减少了故障发现时间. 利用主备用绑定信息加快了MAP故障恢复的过程. 理论上分析了鲁棒移动性管理方案的性能，并同标准分级移动IPv6协议进行了比较. 数值和仿真结果表明，鲁棒移动性方案的MAP可靠性、分组丢失率以及MAP故障发现和恢复时间都要好于标准分级移动IPv6.     

基于分层移动IPv6的移动组播路由算法

基于分层移动IPv6的体系结构,提出了一种用于解决组播信宿移动的路由算法. 结果表明,通过使用分层结构、本地隧道和域内组播,新算法具有最优的组播树重构率、次优的组播服务中断延迟、目的地传输花费和网络传输总花费,具有很好的应用前景.     

基于OPNET的移动IPv6路由优化研究

为了观察路由优化对移动IPv6网络性能产生的影响,采用OPNET Modeler网络仿真软件创建较为复杂的网络环境,通过切换延时、业务流量、端到端延时等典型的移动IPv6网络性能参数影响实验.仿真结果表明,路由优化对减小网络端到端延时方面是有效的,同时路由优化可能会导致增加切换延时,造成业务流丢失.路由优化策略应考虑采取措施减小切换时延.     

移动IPv6模型安全问题及解决方案研究

通过对移动IPv6移动原理和路由优化等过程的分析和研究,证明了移动IPv6基本模型存在着严重的安全漏洞.针对路由优化绑定更新过程的脆弱性,分析了由于移动IPv6基本模型漏洞而可能带来的两种后果严重的安全攻击模式,对绑定更新过程进行了改进性设计.该设计不依赖于任何新的安全框架,简单易行,能有效遏制互联网上针对移动通信的攻击行为,对下一代互联网的安全稳定性起着积极作用.     

基于移动IPv6的IPSec安全体系

对IPSec协议族进行研究,分析了安全联盟、身份认证报头、封装安全负载和因特网密钥交换等协议的结构及其关键技术,并在此基础上提出了一种IPSec的实现方案,可以有效地保障移动IPv6中数据传输的安全。在具体的实施过程中,可选用传输模式和隧道模式两种实现模式。传输模式只能用于发送方和接收方的系统都应用了IPSec的情况。在大多数情况下,采用隧道模式不需要对所用的系统进行任何修改。     

移动IPv6网络中Anycast服务的实现

提出了一种基于树状结构的在移动IPv6网络中实现Anycast服务模型,该模型采用了Unicast与Multicast技术。在该模型中,每个组成员只通过一个归属地址(无需转交地址)就可以完成与客户端的数据通信;组成员移动到外区时,无需向归属代理注册,也无需在归属代理与转交地址之间建立隧道,针对路由优化情况,Anycast组成员也无需向客户端发送转交地址的绑定消息;根据网络的拥挤情况动态地选择最优组成员,解决了在移动IPv6网络中IPSec很难实现的问题。在IPv6模拟环境下,实验数据证明了该模型的实用性、有效性以及高效性。     

基于JPF的Java程序验证

形式化方法是提高并发系统的安全性与可靠性的重要手段。JPF（Java Pathfinder）是一种精确的Java字节码状态模型检测工具。在阐述JPF工作原理的基础上,提出了一种适用于JPF的Java程序模型检测方法,包括Java程序模型的建立、状态空间搜索算法的扩展和配置,开发了Java程序反例轨迹轻量级的输出监听器。对Java程序实例进行验证,结果表明：该方法能有效地检测出多线程Java应用程序中难以检测到的并行漏洞。