共查询到20条相似文献,搜索用时 0 毫秒
1.
在分析通用软件形式化验证方法的基础上,这里设计提出了一种专门针对密码软件安全性的形式化验证方法。该方法采用ACSL(ANSI/ISO C Specification Language)语言对密码软件的安全性进行形式化描述,并采用自动证明与辅助证明相结合的方法,能够对软件的实现是否满足了对安全性至关重要的一些密码学特性进行有效验证。还以一个开源openssl实现中RC4算法的软件实现部分为例,给出了对其保险性进行验证的过程与步骤,结果表明了该方法的有效性。 相似文献
2.
Kanji Hirabayashi 《Journal of Electronic Testing》1998,13(3):321-322
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. 相似文献
3.
面向寄存器的流水线处理器建模及验证方法 总被引:2,自引:0,他引:2
提出了一种新的流水线处理器功能的验证方法 ,这种方法的主要思想是通过验证流水线处理器中所有寄存器的功能来验证处理器的功能 .流水线处理器绝大部分是由同步电路组成的 ,同步电路的状态则完全由寄存器的状态决定 ,因此如果能够保证每个寄存器功能正确就可以保证整个同步电路功能正确 .对于流水线处理器来说 ,寄存器状态的变迁是由处理器的原始输入和寄存器本身状态决定的 .原始输入包括控制信号 (如复位信号 )和数据输入 (如指令输入 ) .如果把对每个寄存器的赋值操作转换成对控制信号和数据输入的操作 ,就可以生成一个验证序列 ,这个序列包括每个 相似文献
4.
对硬件的形式化验证是硬件验证的一个发展方向,形式化验证一个时序电路就是证明电路的实现是否满足他的规格描述.本文提出了用等式逻辑ε的一个公式Ws来表示电路的实现,用Tempura的程序B表示对该电路的特性描述.公式B(∈)P引入来证明电路的正确性,这里P是电路的初始状态,是从Ws中抽取的,另外还要从Ws提取输出等式.这样,一旦证明了B(∈)P,就能证明实现满足规格描述.最后,给出了一个例子来说明此证明方法. 相似文献
5.
云计算是一种新兴的计算、存储资源使用模式,由于具备低成本、高效率等优点,得到了业界的广泛应用,但安全性仍然是云计算推广最大的障碍之一。虚拟化作为云计算的关键技术,其安全水平直接影响云环境的安全性,目前对云计算虚拟环境多采用传统的覆盖式验证方法,无法彻底解决正确性问题。文中通过结合形式化方法中的模型检测技术,经过配置采集、需求分析和性质检测3个阶段对虚拟化安全性质进行高覆盖率验证,提供了一种对云计算环境进行安全评估的可行思路。 相似文献
6.
给出了一个可用于密码协议形式化验证与设计的简单逻辑.该逻辑采用抽象的通道概念表示具有多种安全特性的通信链路,可在比现有认证逻辑的更抽象的层次上对协议进行处理. 相似文献
7.
由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的. 相似文献
8.
针对类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的实现保持一致,从这种意义上讲,该编译器并不是一个实验性质的假想编译器,而是有其实用意义的. 相似文献
9.
基于虚拟机的兼容微处理器功能验证平台 总被引:1,自引:1,他引:0
本文根据验证兼容指令集微处理器的要求,提出了利用虚拟机快速建立微处理器功能验证平台,使用已有的操作系统和应用程序作测试程序验证兼容微处理器的方法,并给出了在验证兼容Intel486指令集微处理器AMEX86中的具体应用。 相似文献
10.
11.
实现基于VIS平台的GSTE验证方法,并将非阻塞性赋值算法引入VIS中,完成了对UART 的寄存器传输级模型的FSM的状态转移的验证和对发送的数据是否与输入数据一致的符号化验证。实验表明,该方法能够完成测试用例的全覆盖,说明了该方法在实际例子中所具有的重要意义。 相似文献
12.
13.
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. 相似文献
14.
15.
面向x86处理器的代码重用攻击难于防护的一个重要原因是,在x86程序代码中存在大量合法但非编程者预期要执行的指令.这些在代码中大量存在的非预期指令可被用于构造实现CRA的组件.先前研究均采用软件方法解决非预期指令问题,运行开销大且应用受限.本文的主要贡献之一是提出了一种低开销的软硬件协同方法来解决x86的非预期指令问题.实验表明,本文的实现方法仅给应用程序带来了-0.093%~2.993%的额外运行开销.此外,本文还提出采用硬件实现的控制流锁定作为一项补充技术.通过同时采用两个技术,可以极大降低x86平台遭受代码重用攻击的风险. 相似文献
16.
17.
Michael Butler 《Design Automation for Embedded Systems》2002,6(4):355-366
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. 相似文献
18.
SOC层次化验证方法及应用 总被引:5,自引:0,他引:5
首先对SOC功能验证做了简要介绍,然后主要讨论了功能验证中的层次化验证方法,并以一个基于AMBA总线架构的SOC系统为例,从模块级、子系统级和系统级三个方面分别阐述了如何用层次化的方法进行验证。层次化验证方法主要分三层,第一层测试主要验证接口协议;第二层测试是对随机产生的大量的交易序列的测试;第三层测试主要是对特定的逻辑功能进行验证。每一层都是构建于其他层之上,这使得层与层之间衔接非常紧密,以便于在完成了第一层的测试之后可以快速地扩展到第二层进行测试,层次化验证方法的应用大大地提高了验证环境的执行效率。 相似文献
19.
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. 相似文献