信息网格安全体系结构的研究

阐述了信息网格Grid环境的独特的安全需求以及现有安全技术的不足,基于协议分层的模式建立了Grid安全体系结构,并着重研究了一站式认证、安全组通信等关键技术,为满足Grid环境的安全需求提供了一体化的解决方案.将该安全体系结构运用于电子商务领域,构建了共享的电子交易场的安全模型,为电子商务提供了安全平台.      

基于Event B的中断管理需求和设计形式化建模与验证方法

随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.     

一种双方不可否认的密码协议及应用

在数据通信中,数字签名技术保证了数据发送不可否认性和数据完整性,而接收数据的不可否认性在安全通信中也是极为重要的.近年来,实现这类型的密码协议主要是通过可信第三方参与数据的加密与传送,因而可信第三方的可靠性和安全性是系统性能的瓶颈.文中提出了一个双方不可否认的密码协议,这个协议解决了可信第三方的性能瓶颈问题,是一个更有效率的密码协议,最后探讨了它在电子邮件中的应用.      

组合服务控制流测试

结合Web服务本体语言(OWL-S,Web Ontology Language for Services)和线性时态逻辑理论(LTL, Linear Temporal Logic),研究用于测试的组合服务流程形式化描述方法和动态测试信息分析方法.将OWL-S作为组合服务的需求参考模型,采用组合服务标准和形式化描述方法相结合的方式,用线性时态逻辑刻画OWL-S控制结构的动态语义,明确地表示出控制结构中各成分的执行顺序.进一步用线性时态逻辑公式集合描述组合服务的控制流需求,从而使原子服务的交互模式有了明确的表示.基于这种交互模式表示,采用LTL在有限状态序列上的语义,对组合服务实现执行过程中获取的动态信息进行分析,测试组合服务实现的执行过程与组合服务控制流需求的一致性.     

基于空间分层组合设计的火箭落点实时计算模型

为保证航天发射任务航区安全,实现火箭落点的高精度实时快速计算,提出一种基于空间分层的数学模型,对落点计算几何模型与动力学模型进行组合设计.该模型将弹道空间分层为自由段和再入段,自由段采用地球扁率修正的落点计算几何椭圆模型,而再入段采用考虑了空气阻力的动力学模型,并加入地球摄动及旋转等因素的修正.经与实际落点数据对比验证,该模型实现了精度和效率的最佳融合,能够满足航天发射任务火箭落点高精度、快实时的计算要求.      

基于描述逻辑DL_(RBAC)的RBAC形式化模型

提出了一种新的基于描述逻辑的形式化表示方法,将组成基于角色的访问控制(RBAC,Role-Based Access Control)模型的集合和关系分别用描述逻辑中的概念和角色表示,并且在基本的描述逻辑语言上引入了可以表示角色的复合关系和包含关系的符号,从而形式化表示出了RBAC与角色继承有关的一些关键性质和约束条件,如角色层次关系(RH,Role Hierarchy)传递性、用户角色分配关系(UA,User-Role Assignment)的继承性和权限角色分配关系(PA,Permission-Role Assignment)的继承性,以及RBAC中的静态职权分离约束和动态职权分离约束等.通过形式化地表示RBAC的继承关系及约束条件,利用描述逻辑本身的推理机制可以限制不符合访问控制策略的继承关系产生.     

混合系统的形式化验证

结合混合系统的研究对余度管理系统进行了形式化的分析和验证.采用的手段是时段演算技术及其扩展.首先进行形式化的需求分析,需求及其假设用时段演算表示,其次严格化地描述算法和参数的选取.在验证过程中,首先应用程序逻辑验证算法,算法的不变量以时段演算表示,最后在时段演算中验证整个系统的行为满足给定的需求.      

基于本体的软件安全性需求建模和验证

由软件引起的灾难性事故原因往往源于安全性需求,目前主观的人工评审方法并不能满足软件安全性需求严格的验证要求.因此,讨论了软件安全性需求的定义,遴选了国内外公认的相关标准和手册作为需求验证的知识基础,根据"七步法"建立了本体模型,利用本体模型中的概念和关联来形式化地描述规则以支持验证;同时基于以上研究内容设计和实现了软件安全性需求形式化建模和验证的工具原型,并对使用工具实施验证和使用人工评审实施验证进行了对比分析实验.实验结果表明形式化工具原型在验证时间和验证次数上都大大优于人工验证方法,同时工具原型具有良好的易用性.     

基于有限状态机的操作系统需求层形式化验证

操作系统是航天器必备的基本软件，操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障，但仍存在不能完全排除缺陷的情况，因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分，本文在分析操作系统需求的基础上，采用有限状态机在操作系统需求层进行形式化描述，并针对应用在某航天器上的SpaceOS2在需求层进行了建模，相应地在定理证明工具Coq中进行了描述建模；然后定义了六条操作系统应满足的全局性质并进行了形式化描述，给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的，为进一步全面形式化验证奠定了基础.     

基于SM4算法的白盒密码视频数据共享系统

基于SM4算法的白盒密码视频数据共享系统是一种保障监控视频数据跨级跨域共享安全的系统，提出了一种基于国密SM4算法的白盒密码实现方式，并分析了算法的安全性，解决了SM4算法在非信任硬件环境中的安全运行问题。研制了基于后台权限控制机制的视频数据安全共享软件系统，包括共享数据上传/下载、共享审核、数据白盒加密处理、访问控制、基于白盒密码算法的共享视频解密播放器，实现了视频数据共享全过程的安全管控。搭建了实验环境，对所提系统进行了功能性能实验。实验结果表明，所提系统功能性能满足设计要求。      

多服务器环境下基于动态ID的轻量级身份认证协议

为了实现用户和服务器之间的通信安全及高效的身份认证,设计有效的身份认证协议成为研究热点。分析了已有协议的安全性,发现仍存在不能抵抗拒绝服务攻击（DOS）和离线口令猜测攻击的缺陷。因此,提出了新的基于动态ID的轻量级单向哈希函数身份认证协议,并通过非形式化安全性分析、随机预言机模型（ROM）分析和AVISPA实验仿真3种安全性分析,以及计算开销和通信开销的分析,比较证明了所提协议能够实现安全高效的身份认证。      

IPSec在移动无线应用场景下的互操作问题

IPSec能够为固定有线网络环境下的IP应用提供端到端通信安全;未来移动无线网络环境下,仍然可以使用IPSec来保障大量移动无线终端之间的通信安全.在移动无线应用场景中,存在IPSec与其它网络应用协议之间的互操作问题.分析了移动无线应用场景中IPSec和性能提升代理及移动管理等网络协议之间的互操作问题,并给出了可行解决方案;分析了现有IPSec体系结构在移动无线应用场景中体现出的不足,指出了下一代IPSec体系结构发展趋势.      

一种嵌入式软件安全漏洞的代码加固方法

软件定义的概念和技术的发展和应用,装备嵌入式系统的功能主要由软件定义完成,导致装备嵌入式软件规模性和复杂性都在急剧增加,软件安全问题已经成为嵌入式系统乃至装备产品研制和运行维护的核心关注点.借助主流软件代码安全性检测技术,对装备嵌入式软件的漏洞行为和结构分析,建立装备嵌入式软件漏洞特征和系统不安全行为属性规约,通过对软件属性规约的逻辑演算,形成软件安全性加固需求,提出基于安全规约属性模板的漏洞加固代码生成技术,对软件代码中潜在的安全漏洞进行修复和加固,实现装备嵌入式软件强制安全保障.