基于ACSL的密码软件形式化验证方法

在分析通用软件形式化验证方法的基础上,这里设计提出了一种专门针对密码软件安全性的形式化验证方法。该方法采用ACSL（ANSI/ISO C Specification Language）语言对密码软件的安全性进行形式化描述,并采用自动证明与辅助证明相结合的方法,能够对软件的实现是否满足了对安全性至关重要的一些密码学特性进行有效验证。还以一个开源openssl实现中RC4算法的软件实现部分为例,给出了对其保险性进行验证的过程与步骤,结果表明了该方法的有效性。     

A Method of Formal Verification of Cryptographic Circuits

In this letter we report the formal verification of encryption and decryption circuits. After we describe algebraically a simple modular arithmetic circuit at both function and logic levels, we apply the symbolic manipulation of Mathematica.     

面向寄存器的流水线处理器建模及验证方法

提出了一种新的流水线处理器功能的验证方法 ,这种方法的主要思想是通过验证流水线处理器中所有寄存器的功能来验证处理器的功能 .流水线处理器绝大部分是由同步电路组成的 ,同步电路的状态则完全由寄存器的状态决定 ,因此如果能够保证每个寄存器功能正确就可以保证整个同步电路功能正确 .对于流水线处理器来说 ,寄存器状态的变迁是由处理器的原始输入和寄存器本身状态决定的 .原始输入包括控制信号 (如复位信号 )和数据输入 (如指令输入 ) .如果把对每个寄存器的赋值操作转换成对控制信号和数据输入的操作 ,就可以生成一个验证序列 ,这个序列包括每个     

时序电路的形式化证明

对硬件的形式化验证是硬件验证的一个发展方向,形式化验证一个时序电路就是证明电路的实现是否满足他的规格描述.本文提出了用等式逻辑ε的一个公式Ws来表示电路的实现,用Tempura的程序B表示对该电路的特性描述.公式B（∈）P引入来证明电路的正确性,这里P是电路的初始状态,是从Ws中抽取的,另外还要从Ws提取输出等式.这样,一旦证明了B（∈）P,就能证明实现满足规格描述.最后,给出了一个例子来说明此证明方法.     

云计算虚拟环境的形式化安全验证

云计算是一种新兴的计算、存储资源使用模式,由于具备低成本、高效率等优点,得到了业界的广泛应用,但安全性仍然是云计算推广最大的障碍之一。虚拟化作为云计算的关键技术,其安全水平直接影响云环境的安全性,目前对云计算虚拟环境多采用传统的覆盖式验证方法,无法彻底解决正确性问题。文中通过结合形式化方法中的模型检测技术,经过配置采集、需求分析和性质检测3个阶段对虚拟化安全性质进行高覆盖率验证,提供了一种对云计算环境进行安全评估的可行思路。     

一种用于密码协议形式化验证的简单逻辑

给出了一个可用于密码协议形式化验证与设计的简单逻辑.该逻辑采用抽象的通道概念表示具有多种安全特性的通信链路,可在比现有认证逻辑的更抽象的层次上对协议进行处理.     

微内核架构内存管理的形式化设计和验证方法研究

由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS（Verified Secure Operating System）内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.     

mJava到Micro-Dalvik虚拟机的编译验证

针对类Java的面向对象语言_mJava到类Dalvik的寄存器架构虚拟机Micro-Dalvik的编译验证,给出了_mJava语言和Micro-Dalvik的操作语义.从_mJava语言程序到Micro-Dalvik虚拟机指令的编译分为两步,首先将_mJava语言程序中的本地变量名转换为相应的序号,得到一个中间语言程序,再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序.在给出中间语言的操作语义后,构造了_mJava语言程序与编译后的中间语言程序的语义保持定理并证明,以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明.整个形式化编译验证在定理证明助手Isabelle/HOL中进行了机器检测._mJava语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象,是我们兼顾语言的真实性和形式化的清晰性的结果.但是,所有形式化的语义严格遵从语言规范中的定义,并与Dalvik VM的实现保持一致,从这种意义上讲,该编译器并不是一个实验性质的假想编译器,而是有其实用意义的.     

基于虚拟机的兼容微处理器功能验证平台

本文根据验证兼容指令集微处理器的要求，提出了利用虚拟机快速建立微处理器功能验证平台，使用已有的操作系统和应用程序作测试程序验证兼容微处理器的方法，并给出了在验证兼容Intel486指令集微处理器AMEX86中的具体应用。     

基于 GSTE的验证在 UART模块中的应用研究

实现基于VIS平台的GSTE验证方法,并将非阻塞性赋值算法引入VIS中,完成了对UART 的寄存器传输级模型的FSM的状态转移的验证和对发送的数据是否与输入数据一致的符号化验证。实验表明,该方法能够完成测试用例的全覆盖,说明了该方法在实际例子中所具有的重要意义。     

SOC形式验证中的故障诊断

在集成电路设计过程中，随着设计规模的不断增大，验证和故障诊断日趋重要。文章首先介绍了SOC形式验证中故障诊断的概念和思想，然后分别讨论了两类故障诊断法：模拟诊断法和符号诊断法。     

An Adaptive Utterance Verification Framework Using Minimum Verification Error Training

This paper introduces an adaptive and integrated utterance verification (UV) framework using minimum verification error (MVE) training as a new set of solutions suitable for real applications. UV is traditionally considered an add‐on procedure to automatic speech recognition (ASR) and thus treated separately from the ASR system model design. This traditional two‐stage approach often fails to cope with a wide range of variations, such as a new speaker or a new environment which is not matched with the original speaker population or the original acoustic environment that the ASR system is trained on. In this paper, we propose an integrated solution to enhance the overall UV system performance in such real applications. The integration is accomplished by adapting and merging the target model for UV with the acoustic model for ASR based on the common MVE principle at each iteration in the recognition stage. The proposed iterative procedure for UV model adaptation also involves revision of the data segmentation and the decoded hypotheses. Under this new framework, remarkable enhancement in not only recognition performance, but also verification performance has been obtained.     

基于指令校验的软硬件协同代码重用攻击防护方法

面向x86处理器的代码重用攻击难于防护的一个重要原因是,在x86程序代码中存在大量合法但非编程者预期要执行的指令．这些在代码中大量存在的非预期指令可被用于构造实现CRA的组件．先前研究均采用软件方法解决非预期指令问题,运行开销大且应用受限．本文的主要贡献之一是提出了一种低开销的软硬件协同方法来解决x86的非预期指令问题．实验表明,本文的实现方法仅给应用程序带来了-0．093％～2．993％的额外运行开销．此外,本文还提出采用硬件实现的控制流锁定作为一项补充技术．通过同时采用两个技术,可以极大降低x86平台遭受代码重用攻击的风险．     

适用于异步徽处理器的16位自定时ALU

针对嵌入式微处理设计中提出的高性能,低功耗的要求,提出了一种面向异步微处理器的由动态电压级联逻辑电路（DCVS）构成的16位自定量ALU。在综合考虑面积、速度、功耗及指令的统计分布情况下,该ALU具有优异的性能。     

A System-Based Approach to the Formal Development of Embedded Controllers for a Railway

We describe a formal approach to the development of embedded controllers for a railway. The approach starts with a system-level specification modeling the system under control and the desired control behavior. Correctness-preserving refinement is then used to add more and more implementation detail to the models and to decompose the models into sub-systems to arrive at models of individual controllers. The B Method is used as the formal notation and methodology.     

SOC层次化验证方法及应用

首先对SOC功能验证做了简要介绍，然后主要讨论了功能验证中的层次化验证方法，并以一个基于AMBA总线架构的SOC系统为例，从模块级、子系统级和系统级三个方面分别阐述了如何用层次化的方法进行验证。层次化验证方法主要分三层，第一层测试主要验证接口协议；第二层测试是对随机产生的大量的交易序列的测试；第三层测试主要是对特定的逻辑功能进行验证。每一层都是构建于其他层之上，这使得层与层之间衔接非常紧密，以便于在完成了第一层的测试之后可以快速地扩展到第二层进行测试，层次化验证方法的应用大大地提高了验证环境的执行效率。     

Formal verification and implementation of safety computer communication management mechanism

In order to improve the system compatibility of the safety computer of the next generation train operation con-trol system, first of all, the structure was analyzed and the management mechanism was designed, the state transition model of management unit was established, and the correctness of the model was verified by formal verification tools at the same time. Then the software and hardware which based on micro controller unit (MCU) were designed and imple-mented. The verification and test results show that the management mechanism design meets the design requirements, the management unit can achieve the expected state transfer function.     

一种可配置的EDA仿真验证方法

介绍了一种适用于5000逻辑单元以上规模电路的可配置EDA仿真验证方法.它由可配置的测试台生成器自动产生测试台,并管理测试向量的注入和仿真状态的存储.与以往研究采用的定时触发的激励信号注入方式不同,本方法采用事件触发,从而保持了与被测电路仿真过程的实时交互.自动生成测试台代码可避免设计人员进行重复性编码并提高了可靠性.事件触发的仿真状态保存机制大大节省了存储空间.