采用NOP协议实现三模冗余系统的形式化验证

对于安全关键系统容错是其实现安全性的重要手段,为最小化冗余单元之间的关联性,通常采用分布式冗余系统,典型的是三模冗余系统。为了在分布式环境下,实现基于三模冗余机制的容错系统,提出了一种可靠的广播协议-NOP（Node Order Protocol）,它采用预定义的节点顺序解决共享介质冲突,并且在单一故障模式假设下,实现了有序的、可靠的消息传输服务,并采用基于模型检测的形式化方法进行了容错系统安全性的验证。验证结果显示基于NOP协议构建的三模冗余系统,在单一任意故障模式下,能够正确地进行故障的检测和诊断,并保证所有正常节点保持一致状态,从而保证单一故障节点被掩蔽,实现单一故障的容错能力。     

一种基于无效链路的分布式故障诊断一致性协议

故障诊断一致性(fault diagnosis agreement,FDA)是高可靠容错分布式系统的性能和完整性的重要保障.目前,大部分FDA协议还是只考虑单一故障组件的简单网络,而对于实际的分布式应用、故障节点和故障链路并存的系统假设更加有意义.但是,在此假设下,对恶意(拜占庭故障)组件的诊断是不可能满足FDA的.为此,首先提出了一种无效链路(invalid link)故障模型,可以更加准确地描述恶意组件的故障行为对系统的影响,有效提高故障诊断的覆盖率.在此模型基础上,提出了一个基于证据的故障诊断协议--PLFDA,可以同时对恶意节点和恶意链路进行检测和定位,并且能够满足故障诊断一致性要求.     

一种复制数据库恢复协议研究

数据复制是提高数据库系统性能和可用性的重要技术。近年来出现的基于组通信技术的数据库复制协议较之传统的数据库复制协议因其实现简单灵活、性能较优,在构建实用复制数据库系统时得到广泛应用,维持各节点副本一致性是数据复制技术研究的核心问题。本文讨论了当故障节点恢复后重新加入系统或增加新节点后如何恢复、维护系统节节点副本间的一致性的问题。本文提出了一个针对分布复制数据库系统的恢复协议,该协议结合基于组通信技术的复制协议,可在不影响系统正常事务处理的情况下,实现故障恢复后节点或全新节点重新加入系统时的系统正确恢复,并给出了理论证明。同时还证明,该恢复协议对于分布在不可靠网络上的复制数据库的恢复问题同样适用。     

不确定短时延网络控制系统的故障检测

针对远程被控对象为线性模型,且网络诱导时延小于一个采样周期的一类网络控制系统(NCS),假设可能发生执行器故障,对系统进行故障检测。将随机时延对系统的影响转化为未知有界条件下的不确定项,建立了系统的离散数学模型。按照时延补偿策略设计了系统的故障观测器,并基于Lyapunov稳定性定理和线性矩阵不等式理论,推导出了整个观测器系统全局渐近稳定的充分条件。仿真例子验证了方法的有效性。     

基于PROFIBUS的双边剪控制系统的可靠性设计

针对一个兼有高度实时性和多机械联动的双边剪机组基于PROFIBUS的PLC控制系统，分析了造成系统不可靠的因素，提出了一整套故障预防和故障容错方案来提高系统的可靠性；故障预防主要靠硬件结构设计实现，而故障容错主要根据PROFIBUS--DP固有的特性和CPU强大的诊断能力通过软件实现；主要方法有：抗干扰设计、冗余设计、容错的协议机制、失效安全技术和程序测试；系统的稳定运行表明了该系统可靠性设计的有效性。     

一种基于组通信的复制数据库在线恢复策略研究

数据复制是提高数据库系统性能和可用性的重要技术.近年来出现的基于组通信技术的数据库复制协议较之传统的数据库复制协议因其实现简单灵活、性能较优,在构建实用复制数据库系统时得到广泛应用.维持各节点副本一致性是数据复制技术研究的核心问题.讨论了当故障节点恢复后重新加入系统或增加新节点后如何恢复、维护系统节点副本间的一致性的问题.提出了一个针对分布复制数据库系统的在线恢复策略,该策略结合基于组通信技术的复制协议,可在不影响系统正常事务处理的情况下,实现故障恢复后节点或全新节点重新加入系统时的系统正确恢复,并给出了理论证明.同时还证明,该策略对于分布在不可靠网络上的复制数据库的在线恢复同样适用.     

一种电子商务协议形式化分析方法

提出了一种新颖的形式化方法,可以用于分析电子商务协议的安全性质,例如可追究性和公平性.与以前的工作相比较,主要贡献在于:(1)对协议主体的拥有集合给出了形式化定义,且主体的初始拥有集合只依赖于环境;(2)将协议的初始状态假设集合分为3类:基本假设集合、可信假设集合和协议理解假设集合,避免了因非形式化的初始假设而产生的分析错误;(3)对可信假设作细粒度的形式化规范,揭示协议的内涵;(4)建立公理系统,使新方法更为严格与合理.     

具有长时延和丢包的网络控制系统的故障检测

研究了具有长时延和数据包丢失的网络控制系统,针对网络控制系统故障检测问题,假设数据包丢失率一定时,根据执行器接收数据包的情况,设计了系统的故障观测器,用建模为异步动态系统进行了稳定性分析,当条件满足时,整个系统是指数稳定的.通过建立的检测模型,研究了系统的故障检测,并进行仿真.当系统发生故障时,观测器残差能够迅速发生跳...     

安全通信协议的一些误区

为了经济上的利益,很多安全通信协议是在普通通信协议的基础上增加一些措施实现的,有时往往忽略了普通通信协议中还存在的不安全因素,这可能会引起安全协议的不安全。本文列举了一些不安全因素,例如隐性的串联环节在串联较多时会使错帧漏检率增大,可用性下降),冗余处理的片面性;不适当的故障假设,以及底层协议对高层协议的影响等。     

密码协议的一种安全模型

将密码协议与密码算法视为一个系统,建立了密码协议系统的一种安全模型.基于假设/保证的组合推理技术提出了新的假设/保证推理规则和假设/保证推理算法,证明了该规则的完备性,实现了密码协议系统的模型检查,并重点解决了系统分解问题、假设函数的设定问题、进程+逻辑的系统特性描述问题等难题.以kerberos密码协议系统为例,利用该安全模型和假设/保证推理技术对密码协议系统进行了安全验证.     

基于时间触发总线的发动机分布式控制系统原型设计

分布式控制具有重量轻、模块化程度高和可靠性高等特点,是未来航空发动机电子控制系统的发展方向之一。基于时间触发总线TTP/C构建了分布式控制原型系统,根据发动机控制需求将系统划分为监控节点和智能节点的架构,制定了集群级和节点级的TTP/C通信协议。基于Simulink模型设计了智能节点应用软件,基于VxWorks设计了监控节点应用软件。经过系统试验,表明基于TTP/C通信总线的分布式原型系统能够满足发动机分布式控制通信要求,具有实时性好、可靠性高的特点。     

Provably secure E-cash system with practical and efficient complete tracing

E-cash system can guarantee the anonymity of the user, but it also can be misused illegally. So the idea of fair E-cash was introduced, i.e., the anonymity of the user can be revoked when a crime is involved in fair E-cash system. However, it is still an unsolved problem to design a practical and efficient fair E-cash scheme, since there are some problems of the impracticality or the incompleteness in the tracing design of existing schemes. First we discuss the principal reasons of it. The reason of impractical tracing is that many schemes have respective unsolved problems in designing the practical tracing. We solve one kind of the problems, then present the practical tracings in various situations, including the bank’s double-spending tracing without the trusted third party (TTP), the TTP’s unconditional tracing and the bank’s loss-coin tracing without TTP, which we call complete tracing. For some schemes, the reason of incomplete tracing is that the unsolved efficiency problems result in the incomplete design of tracing, whereas for other schemes, the reason of incomplete tracing is that the unconditional tracing and the anonymous spending are contradicting properties of E-cash. Considering that, the TTP can be divided into multiple parties, and the TTP is also removable in our system. Moreover, for solving the efficiency problem of practical tracing, we use a nested structure of signature of knowledge in payment protocol, which is proved to be a secure application. Then we provide the detailed security proofs of all security properties of our E-cash scheme and analyze our system efficiency and system functions comparing with the recent schemes.     

Kerberos协议及其授权扩展的研究与设计

尽管Kerberos协议被证明是一种在分布式网络环境下最理想的身份认证系统,却存在一些安全缺陷和协议结构自身的局限性。虽然大部分得到了有效改进,问题依然存在。在深刻理解Kerberos协议思想的基础上,提出了一种基于Ker-beros认证协议的授权扩展系统。该系统在不改变原Kerberos认证流程的情况下,充分利用票据机制加载基于角色的访问控制信息,成功实现了Kerberos认证与授权功能的无缝集成。     

一个不含可信第三方的多方不可否认协议

现有的不可否认协议一般都包括一个可信的第三方,但是,在实际生活中,要找到这样的可信第三方是很难的。该文参考文献眼1演,提出了一种协议模型,运用组加密方案构造了一个不含可信第三方的公平的多方不可否认协议。该协议不是秘密的逐渐泄露,能抵抗外部攻击与内部否认,安全高效。     

协同虚拟环境中的主动动态负载平衡算法

在基于多服务器体系结构的协同虚拟环境中，用户的随意运动引起某些服务器负载过大而导致系统性能的下降。主动动态负载平衡算法定义了3个主动触发条件，当服务器计算代价过大或任务划分不当引起服务器之间通信量过大或服务器负载接近饱和时，将兴趣隶属度大的用户转移给邻域服务器管理，保证了对虚拟环境中的用户代理进行合理划分。试验数据显示，该方法在均衡各个服务器负载的前提下，可以提高系统的实时性和服务质量。     

基于离线可信第三方的挂号电子邮件协议研究

电子商务中的一些协议大多建立在可信第三方TTP（Trusted Third Party）的基础上，挂号电子邮件协议采用的离线TTP协议在某种程度上解决了TTP的瓶颈问题。但该协议存在某些缺陷，着重分析该缺陷造成的各个参与方的不公平性以及可能存在的攻击方法，并给出对应的解决方法和改进建议。     

基于Zynq的TTP/C总线节点备份与再整合

TTP/C总线节点的备份与故障节点的再整合是提高总线可靠性与实用性的有效方法。参考 TTP/C 总线协议,在自主设计的基于Zynq的TTP/C总线控制器上设计了一种节点备份与再整合的方法,保证节点故障后可以重新整合进入集群,或者启用备份节点来保证集群的正常功能,最后通过试验验证了所设计的节点备份与再整合方法的有效性。     

辫群上的扭结共轭搜索问题和密码体制研究

通过分析辫群的相关性质及群上的判定问题,结合扭结共轭问题、子群成员判断问题及根搜索问题,提出一种辫群上的公钥加密协议和签名协议,对两者的安全性进行分析,证明敌手无法从公钥中恢复密钥,因此协议可以抵抗长度攻击、惟密钥攻击、一般选择消息攻击、定向选择消息攻击和适应性选择消息攻击。     

On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications

The correct operation of time-triggered protocols highly depends on the well-synchronized clocks of the system. To maintain the global time, one strict constraint must be exerted on communication activities (e.g. temporal padding and sparse time base etc.), which not only increases complexity of the protocol design but also incurs a penalty in the network utilization. While for event-triggered protocols, it is difficult to achieve the real-time requirement and determinism. Therefore, it is necessary to explore the combination of the advantages of these two categories of protocol for applications in different scenarios. This paper proposes the Safe Node Sequence Protocol (SNSP), which is a variant of full time-triggered protocol TTP/C. In SNSP, a strict node sequence is defined and the order of communication events is established by this pre-configured order without binding to global time, so the protocol changes communication activities and error detection to an event-triggered model. Therefore, SNSP possesses the characteristics of both time-triggered and event-triggered model. Also, the potential impact of global time, such as byzantine clock failure, on the protocol is eliminated. At the same time, the formal verification of SNSP is much easier in the absence of global time. Moreover, we model the protocol and use formal checker SPIN to validate the basic fault-tolerant requirement of SNSP. The simulation results show the protocol enables better resource utilization and is more effective.