一种寄存器自动化验证方法

随着芯片功能的不断增加,芯片中寄存器数量日趋庞大,寄存器的属性也日趋复杂,寄存器验证的完备性和高效性成为验证人员迫切需要解决的问题。本文介绍一种寄存器自动化验证方法,只需要提供寄存器的规格文档,极少的人工参与,即可自动生成验证寄存器的仿真验证激励及相应说明文档。对于特殊功能的寄存器或寄存器位,会生成特殊寄存器报告,验证人员根据该报告对特殊寄存器加以补充验证,从而让寄存器的验证更完备。

SET证书申请协议在SPV下的自动化验证及改进

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.

BLP改进模型的形式化描述及自动化验证

在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行相应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述,使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性,从而实现对模型正确性的自动形式化验证,并保证了模型的可靠性。

多Web服务组合兼容性的自动化验证

Web服务组合的目的是实现单一服务无法满足的复杂功能,而保证组合的正确性以实现服务增值是十分必要,因此组合之后的正确性验证是Web服务组合的一个重要研究方向。从Web服务交互行为方面描述多Web服务组合,在提出行为兼容性的相关理论的基础上,给出基于Pi演算的多Web服务组合行为兼容性的自动化验证算法,通过将多Web服务组合自动转化为Pi演算中的组合进程,实现多Web服务组合的自动化验证。

改进Athena算法的多协议攻击自动化验证方法

多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析Athena算法的基础上提出了一种多协议攻击自动化验证方法。该方法扩展了Athena状态表示方法和后继状态生成算法,使得攻击者具备截取其它协议交互消息和计算生成当前协议消息的能力,能够以自动化的方式验证协议是否存在多协议攻击。实验结果表明,提出的方法能够实现多协议攻击的自动化验证。

基于串空间的安全协议自动化验证算法

以串空间模型为理论基础,提出安全协议自动化验证算法IVAP。对于有漏洞的协议,针对不安全属性逆向搜索主体串树,自动生成改进协议并对其进行验证,直至生成一个安全的改进协议。实验结果证明了该自动化验证算法的有效性,与AAAP算法相比,其协议验证效率更高。

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

SoC自动化验证方法的研究与实现

为解决SoC(System-on-Chip)验证覆盖率和工作量问题,基于可重用思想、采用事务验证模型、随机激励生成的方法,建立了一个层次化的具有自主知识产权的自动化功能验证系统(LSAVS:LiShan Automatic Verification System)。采用该验证系统后,SoC验证工程师开发测试向量的工作量由使用传统验证方法的60%降低到10%,同时保证了功能验证100%的覆盖率,达到快速高覆盖率的验证目的。

集成电路工艺设计包PDK自动化验证与界面化的实现方法

分析集成电路的自动化验证PDK方法,以及PDK验证过程中遇到的难点问题。通过Skill汇编语言建立系统化的PDK自动化验证界面工具。这是一套适用于不同工艺,嵌套在Cadence virtuoso平台下的PDK自动化验证方法,可以大大提高PDK验证的质量和效率。

基于自动化安全验证的网络边界防护

互联网边界防护作为企业网络安全的第一道防线,是企业最先建设也是最重视的环节,是安全防护的重中之重。企业在建设网络边界时,都会用到大量的边界防护产品,而这些产品是否真的发挥了它们应有的作用,成为了边界防护有效性的关键。针对这种情况,利用自动化安全验证技术,提升边界防护设备的有效性,以此提高网络边界的安全性。

FPGA功能验证自动化技术研究与实践

深入分析了影响FPGA功能验证效率和质量的各项因素,改进了传统FPGA软件验证平台的搭建方法,阐述了FPGA软件自动化验证平台搭建技术、基于Perl语言的Testbench自动生成技术、受约束的随机激励生成技术、接口时序自动侦错技术、SVA断言以及基于VBA宏的管脚配置自动检查技术等6种改进策略。这些自动化技术将功能验证中程式化和标准化的工作交由工具完成,提高了验证平台搭建和仿真结果检查的效率。

基于自动化分析的风险检测验证技术在环境自动监测中的应用探讨

大气、水质环境自动监测中的自动化系统通过互联网传输环境质量数据,实现环境质量的实时监督,系统中的数据已成为判断环境好坏的重要依据;网络传输是自动监测信息系统的重要一环,其安全性直接影响环境监测数据的真实性和准确性。而网络安全风险检测是保证网络安全的基础工作,探讨在环境监测系统中如何引入自动化的安全风险分析及验证技术,发现环境自动监测系统中的网络安全隐患。

实用模型的自动化形式验证

通过给传统的Biba模型增加相应的敏感级函数,完善其主客体完整性标签,并对其安全操作规则进行相应的改进,使其适应实际的应用需求.采用完全形式化的方法对改进后模型中的各元素、模型必须满足的不变式以及模型迁移规则进行描述,并在此基础上利用定理证明器Isabelle完成对该模型的自动化形式验证,从而实现高等级安全操作系统研发过程中对安全策略模型的形式化需求.

基于计算模型的OpenID Connect协议认证性的自动化分析

分析了OpenID Connect协议的消息结构,基于计算模型应用Blanchet演算对OpenID Connect协议进行了形式化建模,应用自动化验证工具Crypto Verif验证了其认证性.结果表明:在OpenID Connect协议中,客户端能够认证终端用户,但是终端用户与授权服务器之间不能相互认证、令牌终端不能认证客户端.为此,给出了OpenID Connect协议中不具有认证性问题的解决方法.

制药设备自动化系统验证方法

以无菌配液系统的自动化系统为实例,介绍了制药设备的自动化系统如何根据GAMP5的基本概念进行实际的自动化系统验证。并根据验证V型模型,介绍了系统从开发到应用过程的实际情况,以及"规范"与"验证"方面的内容。

基于串空间理论的安全协议自动验证

针对目前串空间理论依赖分析人员主观判断、无法使用自动化工具进行验证的问题,提出了基于串空间理论的协议认证属性标准化验证过程。首先为协议消息项定义类型标签,对串空间及认证测试理论进行扩展;然后通过判断测试元素出现位置、检验测试元素参数一致性、确认变换进行边唯一存在性和检验目标串参数一致性,将基于串空间理论的协议验证过程标准化为可程序实现的步骤。该算法的时间复杂度为O(n2),避免了模型检测方法的状态空间爆炸问题,并在此基础上实现了安全协议认证属性的自动化验证工具。以BAN-Yahalom协议和TLS 1.0握手协议为例进行了标准化的分析验证,找到了对BAN-Yahalom协议的一种新攻击形式。该攻击无需限制服务器对随机数的检查,比Syverson发现的攻击更具普遍性。

基于vManager的大规模IC验证自动化解决方案

;介绍了验证管理工具vManager,通过Python调用vAPI接口与企业级的产品需求管理工具Microsoft TFS和用户数据后台对接,实现了从自动创建验证需求框架(即vPlan)自动执行回归验证,自动提取验证结果反标回Microsoft TFS中的需求状态,自动提取验证结果呈现到验证看板的自动化验证管理全流程。方案旨在自动化、规范化地实现验证需求到vPlan的同步,验证回归状态和覆盖率的实时汇总,实现验证的高效率和高透明度,需求跟踪达到滴水不漏。该方案还采用了vManager最新一代的High Available模式,可实现跨地域的多团队合作与数据共享,并且部署了多引擎验证工具包括Xcelium、JapserGold和Palladium的验证管理,实现了多维度的验证数据汇总。目前该方案已经部署到真实的研发环境中,为vManager在国内比较领先的应用,为业内提供“跨地域合作+多个仿真引擎”的大规模验证方案提供了非常有价值的参考。

汇编级顺序语句块的自动形式化规约及其验证

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。

集成电路的版图比对电路LVS系统化自动验证方法研究

分析集成电路的版图比对电路LVS验证的必要性和难点。提出了LVS自动化验证系统架构。通过Skill汇编语言建立系统化LVS自动化验证桌面工具。这是一套适用于不同工艺的,嵌套在Cadencevirtuoso平台下的LVS自动化验证方法,可以大大提高LVS验证的质量和效率。

基于VCD波形的FPGA实物自动化测试技术

为解决FPGA软件测试过程中仿真测试实时性不高和实物测试不充分的缺点,对FPGA实物验证环境搭建技术和芯片验证机理进行研究,提出一种基于VCD波形的FPGA实物自动化测试技术。通过对VCD波形数据压缩、转换形成自定义测试向量,解决了输入信号量过于庞大的问题。采用PCI-E数据总线和DMA数据共享的方式实现自定义测试向量实时传输,并经过数据-引脚映射完成被测FPGA芯片真实信号注入,保证了信号的实时性和测试的充分性。信号在真实芯片中运行后,通过采集FPGA芯片返回信号,自动完成与VCD波形中期望值的比对。在FPGA验证平台上进行验证,结果表明,该技术能够在保证测试充分性的基础上自动完成对FPGA芯片实物验证,提高了测评效率和测评的真实性。