精华内容
下载资源
问答
  • 各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件...MesaTEE(源自“Memory Safe TEE”)除了遵循混合内存安全模型(Hybrid Memory Safety)用Rust等内存安全语言重构关键组件,还对其他的C/C++代码进行了静态扫...

    各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性。诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机。因此,软件内存安全保护极其重要。MesaTEE(源自“Memory Safe TEE”)除了遵循混合内存安全模型(Hybrid Memory Safety)用Rust等内存安全语言重构关键组件,还对其他的C/C++代码进行了静态扫描、动态测试和形式化验证。

    静态扫描通过分析程序编码模式,能快速报出浅层漏洞,但会有相对较高的误报和漏报;以模糊测试(Fuzzing)为代表的动态测试通过提供随机改变的输入来触发问题,准确率高,但很难完整覆盖程序的所有状态,难以证明程序是无缺陷的。因此在高安全需求场景下,静态扫描和动态测试是不够的,需要形式化验证用严格的数学方法推演程序的完整状态空间符合安全设计规范,证明程序在设立条件下一定不会出问题。因此形式化验证是安全实践里非常重要的一环。

    百度安全实验室在云计算、区块链、自动驾驶等工业级场景的部署里都有形式化验证的实践。例如在MesaTEE TPM项目里,形式化验证对TPM核心软件栈(tpm2-tss 2.1.0版本)进行了验证,保证了该项目约6.7万行代码在MesaTEE调用场景下不会出安全问题。验证期间发现并修复空指针引用、越界读写、内存泄露等等多种共计140+处安全缺陷,验证过的tpm2-tss版本发布在了GitHub上(https://github.com/mesalock-linux/tpm2-tss-verified)。除此之外,在内存安全的Python解释器MesaPy项目里,形式化验证保证了C backend的代码在MesaPy所有使用场景下是内存安全的。验证期间发现并修补了包括空指针引用,整数溢出等14处安全缺陷,验证方法和结果也发布在了GitHub上(https://github.com/mesalock-linux/mesapy/tree/mesapy2.7/verification)。

    一.形式化验证介绍

    形式化验证是指使用严格的数学方法来推理验证程序是否符合安全规范的过程。该方法具体包括源码准备、基于抽象解释(Abstract Interpretation [1] [2] [3],下文简称AI)的值域分析(Value Analysis)、最弱前置条件验证(Weakest Precondition)和程序缺陷报告等阶段。如下图所示。

    8b7955b2daf4cadedb0c900bc4e26524.png

    图1  形式化验证方法流程

    1.1 源码准备

    理想情况下,形式化验证需要在程序的完整代码上进行。这里不仅包括目标程序本身的源代码,还需要依赖的第三方库的源代码。然而很多情况下第三方库没有给出源码,或者第三方库的源码过于庞大无益于关注程序主体的安全性,这种情况可以对项目中调用依赖库的函数写抽象描述辅助验证。

    接下来是要确定需要验证的目标函数,为目标函数写测试用例。形式化验证任务中,测试用例中的函数参数用Interval表示,来覆盖所有可能取值。同时,还要覆盖到函数调用的所有场景,如下面示例:

    fe49be5ef9ca5132527f007e8c68a253.png

    我们可以从项目自带的Unit Test和Integration Test入手,来编写Interval版本的测试用例。这两类测试用例一般会涵盖项目中关键函数和关键功能逻辑,从这里入手能够覆盖验证目标,保证验证质量。

    1.2 基于抽象解释的值域分析 (Abstract Interpretation Based Value Analyis)

    在这个阶段中,分析人员对源代码的标注(Annotation),配置分析策略(Analysis Policy),然后依赖抽象解释(Abstract Interpretation)技术来执行执行值域分析(Value Analysis)。分析引擎会对标注的源码进行分析,插入运行时错误检查(Runtime Error Check)语句标注,分析程序控制流、数据流并计算程序中变量的所有可能取值,验证标注属性的真假。分析过程中无法确认为真的标注属性所对应的语句归类为未定义行为(Undefined Behavior),在实际分析过程中,可能需要分析人员对Undefined Behavior加入额外的标注属性来消减误报。接下来,最弱前置条件分析引擎(Weakest Precondition)会验证这些人工额外标注,将最终发现的Undefined Behavior将呈报给分析人员,进行最后确认。

    a. 抽象解释 (Abstract Intepretation)

    抽象解释是指使用另一个抽象对象域(Abstract Domain [3])上的计算,来抽象逼近程序具体对象域(Concrete Domain [3])上的计算。抽象语义涵盖所有可能的情况,是具体程序语义的超集,因此如果抽象语义是安全的,那么具体语义也是安全的。每一个抽象对象域规定了抽象对象(或变量)之间的运算规则体系(Lattice)[3]。最常见的抽线对象域是Interval Domain [3],它的运算规则与具体数值计算规则相似(如下面示例所示)。由于Interval Domain易于理解并且计算复杂度不高,所以实际程序验证分析任务中采用Interval Domain来进行Value Analysis。

    f9b79641a49701c7ac6ff4dc5f530950.png

    Abstract Interpretation对变量的计算推演可能存在Over-approximation [3]。原因是为了保证程序在合理时间内分析结束,分析引擎常常会扩展变量的值域,以减小计算复杂度。这样,由于变量值域扩大,在Runtime Error Check时可能由于它不在合法数值范围内而报告为Undefined Behavior,但实际上变量真实取值并没有超出合法范围。这种情况需要由稍后介绍的程序标注来消减误报。

    b. 分析策略(Analysis Policy)

    AI-based Value Analysis在计算推演过程中会记录变量的取值情况。随着程序分析的不断深入,变量的取值会随着程序分支而划分开来,在各自分支分别计算推演。最终会使得在某程序点上,变量取值出现很多种可能。理论上,对于任何程序,分析时保留变量的所有取值情况将会产生最为精准的结果,但是随之而来的是巨大的空间和时间开销,难以保证分析在合理的时间内结束。这时需要设定合理的分析策略,来实现分析消耗时间和分析结果精度的平衡。

    我们用State来代表一个变量取值的所有可能。实际分析中,通常设定一个State Level,表示任意程序点允许保存变量状态的最大数量,如果某点处,变量所有取值情况的数量超过了设定,就需要合并状态。此外,变量之间关系记录的细致程度,也会对验证分析结果产生影响。这一点主要体现在函数之间相互调用时,子函数返回时如何记录多个返回变量State之间(函数有返回参数时认为有多个返回值)的关联关系(State Split)。下面的示例代码分别展示了State Level和State Split设定对分析结果的影响。

    fdecdec07b9fd978c131151cc6343862.png

    如果State Level限定很小(比如1),那么在L处,x取值为 x ∈ [1..9],y取值为 y ∈ [6..10]。但如果状态空间足够大(State Level大于等于2),那么x和y的取值会进一步细化,拆分为 y == 6 ⋀ x ∈ [1..4]或者 y == 10 ⋀ x ∈ [5..9]这两个状态。可见State Level越大,分析粒度越细,结果越精确。

    94fa815f79d1241f8820df2e88dfe5c7.png

    上述代码中,当State Split的粒度设置较低时,在(3)处会报出“使用danlging pointer hd”的Undefined Behavior,原因是它认为在(2)处已经free掉了hd,(3)处不应该再使用。然而经过分析我们可以发现,(2)的free只有当(2)处err为true时才会执行。这种条件下,(2)处free执行后,(3)处分支根本不会执行。当State Split粒度调高时,Value Analysis会记录err和hd的关系,就不会产生误报。

    虽然更高的State Level和更细致的State Split粒度能为我们带来更为准确的分析结果,但在程序代码量庞大而且逻辑复杂的情况下,这两个策略设置过高,可能导致分析无法在合理时间内结束。所以实际分析中,需要评估State Level和State Split,达到分析效果和分析时间的平衡。

    c. 程序标注 (Annotation)

    程序标注是利用形式化描述语言(如ACSL [3])来描述程序语义,辅助分析引擎生成验证约束。在实际的验证分析过程中,有时由于受限于分析粒度的设定,Value Analysis阶段无法产生十分精细的结果,产生Undefined Behavior的误报,这时就需要分析人员加入Annotation,辅助分析过程产生更准确的分析结果。而这些Annotation的正确性,也需要在下文的最弱前置条件验证中验证。

    在下面例子中,假定没有配置很高的分析粒度,L1处x和y之间的大小关系不会被记录下来,在程序中L3处,会产生“x可能超出数组T的合法范围“的误报。如果,在L3处加入//@ assert 0 < x < 10这个约束,就可以引导分析过程来消除该误报。

    452c3f93f78aff02281e07cf0808b077.png

    除了assert,程序标注还包括函数合约(Function Contract)和循环不变式(Loop Invariant)等。函数合约描述函数的输入和输出的约束;Loop Invariant描述循环的约束,帮助Value Analysis更好的理解程序中复杂循环的语义,有助于消减分析过程中产生的误报。

    d. 运行时错误检测(Runtime Error Check)

    Value Analysis分析引擎会加入Runtiem Error Check要求程序符合特定属性。例如在下面示例中,在内存数据访问操作之前,value analysis会加入类似于/*@ assert ret: mem_access: \valid_read(); */对访问地址合法性判断的标注属性。如果内存地址的值域不在合法范围之内(比如为NULL),就报出Undefined Behavior。

    e9c602e3ecba50932512df75e745a32f.png

    1.3 最弱前置条件验证(Weakest Precondition)

    函数合约和Runtime Error Check相关的标注属性在Value Analysis过程中验证。然而,有些assert标注是分析人员为了辅助Value Analysis加入的,例如//@ assert 0 < x < 10。这类约束条件,Value Analysis始终认为它们为真。为了确保这些约束条件自恰,必须单独对这部分约束进行验证。最弱前置条件(WP, Weakest Precondition)正是用来验证这些约束的。

    Weakest Precondition [5]可以形式化描述为wp(S, R)。对于某程序位置P,S为从P处开始执行的语句,R为从P处执行语句S后所达到的约束条件(Postcondition)。wp(S, R)表达的含义是,在执行语句S之后,为了能让R符合特定的Postcondition,P处所需要满足的最弱前提条件。换言之,WP求解工具可以根据R和S,求解出P处要满足的最弱前提条件。

    这样,对于每一个向Value Analysis提供的assert标注,通过WP都可以求得它的最弱前提条件。如果所有前提条件都能满足所在上下文的约束,就能得到自恰的保证。

    二.案例分析

    2.1 TPM 验证分析

    我们用形式化验证的方法,借助形式化验证工具TIS [6]对若干工业级别的项目进行了分析实践。这些项目涉及云计算、区块链、自动驾驶等。其中,以TPM可信计算的核心软件栈tpm2-tss(https://github.com/tpm2-software/tpm2-tss)项目为例,我们验证了该项目2.1.0版本的代码,共验证了约1300个函数 / 约6.7万行代码,发现并修补了包括空指针引用、内存泄露,越界读写等在内的140+多处程序缺陷。下面是在验证过程中发现的程序缺陷(左图)和对应的修补方案(右图),这些程序缺陷均已经报给开发者并得到最终确认,并已在最新代码中修补。

    示例1:空指针引用

    6507ba14a2862e66e9319197c501b0a0.png

    示例2: 内存泄露

    add8913b0d8c4fce59bad04f949297c3.png

    示例3:循环条件错误导致数组越界读

    71223217061244cc5bb9be7a848ef458.png

    示例4:free错误导致内存破坏

    75ab97826a5849360ae76d80b2b3dcb4.png

    2.2 Mesapy 验证分析

    Mesapy(https://github.com/mesalock-linux/mesapy)是基于pypy的内存安全Python解释器。我们结合多种形式验证工具smack[6], seahorn[7] 和 TIS[5]对Mesapy backend的C库函数(共计5044行代码)进行了验证,发现并修补了包括空指针引用,整数溢出等14处程序缺陷。下面是在验证过程中发现的安全缺陷案例。

    示例1:空指针引用

    8aa0115cd52c17625029b5dc3375180c.png

    示例2:整数溢出

    f40b6367cc74d5abbebe45b93c71ed95.png

    三. 形式化验证实践经验分享

    虽然形式化验证方法能够检测和消除安全缺陷,但具体应用时也存在局限和需要考量的地方。主要体现在如下几个方面:

    3.1 分析时间和分析精度的取舍

    正如前文反复提及,程序验证任务不仅需要保证很高的精度,也要保证分析任务在合理时间内结束。在实际验证过程中,我们发现对于一些验证目标,设定较低的State Level和State Split策略,并不会对分析精度产生任何影响。而对于一些非常耗时的验证目标,通过调整上述两个参数,能够在理想的分析时间内结束,再辅以少量的人工确认,也能够实现验证目标。

    此外,如果确定验证耗时是在特定的子函数上,可以对这个子函数写Function Contract,并且在验证时使用Contract,也能够提升分析效率。但如前文所述,给函数写Contract需要确保对函数语义完全的理解,否则会适得其反。

    另外为了提升分析效率,我们也可以对耗时的子函数进行改写。例如下面的例子:

    1565246444879492.jpg

    假设分析children函数非常耗时,通过函数定义发现它会通过参数返回两个int,那么我们可以用Interval去改写。如果能够验证y和z在所有可能取值情况下是正确的,那么在它们各自真实取值情况下也一定是正确的。

    1565246444525187.jpg

    3.2 需要适量人工参与

    形式化验证很难全自动完成。受限于要验证约束条件的复杂程度和证明器的验证求解能力,有些验证约束条件无法验证,以Undefined Behavior的形式报告出来,此时需要人工确认这些是否是真正的安全缺陷。这一步的工作量会与分析策略的设定有关,分析粒度越大,此步骤需要人工参与的工作可能越少。此外,Over-approximation也有可能引入误报,也需要人工参与剔除掉这部分误报。

    3.3 测试用例影响验证质量

    验证效果也取决于提供的测试用例的质量。编写测试用例的原则是尽可能提升分支验证的覆盖率。总体而言,在编写测试用例时可以用Interval来为参数赋值,覆盖它所有可能取值,这种方式也有助于提升代码验证覆盖率。对于具有复杂类型的参数(例如结构体变量中嵌套包含其他的结构体),有时也需要结合函数实现逻辑,来决定哪些变量需要赋值为Interval、哪些可以保留Concrete赋值,因为并不是所有变量都使用Interval就一定能带来最好的验证效果,Interval推演计算会对分析时间带来显著的开销,延长分析时间。

    3.4 验证给与的保障

    最后需要说明的是,实践中采用的形式化验证,并不能保证验证过的程序不存在任何安全缺陷——它能够保证的是,对于特定的验证对象(特定版本目标代码,和特定版本依赖库),验证给定的测试样例所能触发的代码,一定不会存在指定验证策略(例如缓冲区溢出检查、整数溢出检查等等)所约束的安全问题。但凡”软件被形式化验证过,所以绝对不会出任何安全问题“的声明,都是夸大、不严谨的。

    总结

    本文诠释了形式化验证的原理,分享了MesaTEE对实际工程项目进行形式化验证的经验,特别是对TPM核心软件栈和MesaPy C backend的验证。为了让业界少走弯路,我们列举了采用形式化验证需要考量的问题。实践证明,通过形式化验证来保证代码安全虽然成本昂贵,但通过精心设计还是切实可行的。相比于利用静态分析或动态测试的方案来评估程序安全性,形式化验证还是能够更透彻地发现程序安全缺陷,并且保障程序在给定约束下是安全的。

    作者:王明华,冯倩,张煜龙,韦韬

    [1]. Abstract Interpretation: http://www.cs.utexas.edu/~isil/cs389L/AI-6up.pdf

    [2]. A gentle introduction to formal verification of computer systems by abstract interpretation. https://www.di.ens.fr/~cousot/publications.www/CousotCousot-Marktoberdorf-2009.pdf

    [3]. Abstract Interpretation and Abstract Domains. http://www.dsi.unive.it/~avp/domains.pdf

    [4]. ACSL Mini-Tutorial. https://frama-c.com/download/acsl-tutorial.pdf

    [5] Weakest Precondition. https://en.wikipedia.org/wiki/Predicate_transformer_semantics

    [6]. TIS. https://trust-in-soft.com

    [7]. Smack. https://github.com/smackers/smack

    [8]. Seahorn. http://seahorn.github.io

    更多内容请移步:

    展开全文
  • 原标题:说说形式化验证(Formal Verification)吧 前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼儿园没毕业的水平,因此...

    原标题:说说形式化验证(Formal Verification)吧

    8e13650dcc1d43b47e93046e7027939f.png

    前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼儿园没毕业的水平,因此尽量不涉及任何数学问题,也欢迎真正的专家认真打脸。

    作者:王健 达闼

    说形式化验证(Formal Verification)之前,就不能不提一下形式化方法(Formal Method)。形式化方法简单的说就是用数学工具进行定义、开发和验证(specification, development and verification)。数学家们认为,不论硬件还是软件工程,就像世间万物一样,所有的学问一样,归根结底是数学问题。“一个不懂数学的工程师不是一个好工程师”。如果所有的设计开发都能够按照严格的数学方法进行,那么开发出来的系统就会像数学本身一样的完美:软件不会出错,硬件永远正常。当然,这是数学家的理想。

    5ab00e17e0b9f66260d8398d926cee49.png

    实际上,形式化方法是从硬件设计开始普及的,举一个例子:当年Intel的Pentium CPU浮点运算单元出错(FDIV Bug),数以万计的CPU不得不回收和替换,给Intel造成了巨大损失(475M $)。

    笔者按:小钱钱是推动社会进步的真正动力啊。

    再按:IBM,AMD,ATMEL,STMicro等等半导体巨头也都是形式化方法的使用者…

    从那之后,Intel开始在其芯片设计中广泛采用形式化方法。话说回来,软件方面的形式化方法进展如何呢?很不幸,软件行业对于形式化不太感冒。原因无非是如下几个:

    a. 对数学技能的要求太高:域啊,格啊,建模啊,你的明白?(按:码农的数学水平看来是不入法眼啊)

    b. 时间成本太高:先做纯数学的specification,然后需求一变,再来一次,互联网时代这个很致命啊,现在这个版本迭代的速度,文字上的spec有时候都是糊弄的c. 用户习惯:用户已经习惯了软件崩溃(码农的耻辱…)

    好,啰嗦了这么久了,那么我们就往回拉拉,说说形式化验证(Formal Verification)。前面已经说了,形式化验证是形式化方法的重要组成部分。如果用形式化方法来做设计开发,必然涉及到形式化验证的问题。

    在有了形式化的spec的情况下,那么可以Verification就大致可以分为“手算”和“机算”两种了(不要打我,高明的数学家的“手算”未必就比纯自动化的“机算”差)。举个例子,全自动化的Verification里面有一个叫做“Model Checking”的方法,简单的说就是穷举系统运行过程中所能达到的所有状态(States),这个如果建模,也就是写Spec的时候不是那么高明的话,嘿嘿嘿… 还有一个就是 “机器定理证明”,听起来很高大上,对不对?1954年,Martin Davis第一次用机器证明了一个定理:“两个偶数相加还是偶数”,不过在更早之前,图灵就已经通过一个著名的“停机问题”证明了图灵完备的机器的不可解问题。

    好吧,似乎又扯远了,再拉回来。如果一个系统的开发不是形式化方法的,咋办?还能做形式化验证么?比如说给定代码,然后直接做形式化验证?

    答案是“uncomputable”,呵呵,开个玩笑。其实道理上来讲很简单,就是你把没有做的Formal Specification补上就行了。当然,说着容易做着可就难了。从代码里面直接转换为形式化描述语言的工具有,但是别忘了specification是对功能,对需求的描述。直接转换的描述语言不是人类能够理解的,如果这个specification你都不知道它到底定义了什么,那么所谓的验证就没有任何意义了,于是“然并卵”了。

    那么怎么办呢? 老老实实的建模吧,从需求出发,从头开始。需求的specification做好了,证明代码和需求(的形式化描述)是(数学)等价的就是形式化验证。建模是个手艺活,如果完全从需求出发,那么恭喜你,你可以完整的跑一遍形式化方法的开发流程了,代码慢慢重构去吧… 当然,比较聪明的方法是从代码出发,手动建模,兼顾需求和实际的实现,尽量避免对代码的重构。

    这个“聪明”的办法看起来是唯一可行的,但有两个缺点

    f869fe45719d5e11d7c943f41629e44f.png

    对人的素质要求太高了,既要熟悉代码,又要熟悉形式化方法。时间成本随着代码量的增加达到了不可接受的程度,可以类比正向和逆向的开发。

    现阶段对于软件的形式化验证多集中在几个微内核的OS上(如OKL4),也仅仅是对微内核那区区数千行代码的验证。这里再扯两句,微内核顾名思义就是最简单的,构成一个操作系统的要素都有了的内核,一切从简的目的就在于保证其安全性和稳定性。如果有人说他准备对某个宏内核系统(比如Linux)进行形式化验证,那么他一定不懂形式化验证…

    好吧,代码层面的形式化验证做完了,那么是不是就万无一失了呢?且不说形式化验证的结果只是验证了系统“are we building the system right”,我们不能忘记编译器啊,还有runtime呢?前文提到了,Ada这个语言的编译器是形式化方法做的,就是为了保证其稳定性和安全性,加上执行环境呢?执行环境(比如OS)有没有做形式化验证啊?那么有同学问了,你这样是不是有点变态?我的回答是,有现成的例子,比如大家熟悉的智能卡,其硬件和OS(Firmware)均是通过形式化方法开发的,所有的API和Protocol均有形式化验证背书,所以,涉及到小钱钱的事情,大家是真的不含糊的。

    扯了这么多,其实起因是因为有人要对以太坊(Ethereum)的EVM做形式化验证。EVM(Ethereum Virtual Machine)其实是一个很好的,好的不能再好的理想化目标,其功能需求明确,实现简单,而且最重要的,也是涉及小钱钱的事情。这里大胆的想一下,有人能够按照智能卡的方案,从硬件(比如说ASIC)到OS(比如专用micro kernel),再到EVM,做一个完整的基于形式化方法开发的产品,那就完美了。

    最后扯一下Verification和Testing的关系。形式化验证是验证系统是否正确(are we building the system right),这个就很了不起了,完美,但是成本(金钱、人力和时间)太高。而testing就像穷人的“verification”,对人的技能要求低,时间成本也低,但是只能找到存在的问题,不能找到所有问题(vs. Formal Verification)。但从另一个层面来说,测试是在“真实”环境里进行的,形式化验证只是数学层面。在“真实”环境中的测试是形式化验证无法取代的,除非“真实”的环境本身也是形式化验证过的…

    嗯,世界大同,数学家赢了…

    责任编辑:

    展开全文
  • 我们在此之前一直专注于网络配置的自动,例如根据模板创建配置进行编排并在网络上部署,这确实可以有效的减少人为上操作错误。但是随着网络基础设施变得越来越复杂,网络规模也越来越大,验证是否能够达到预期结果...

    作者简介:唐昊,现就职于华为,从事云网络研发工作。

    IBN(基于意图的网络)是近年来网络领域中最热门的话题之一,网络验证是其中最关键的环节。我们在此之前一直专注于网络配置的自动化,例如根据模板创建配置进行编排并在网络上部署,这确实可以有效的减少人为上操作错误。但是随着网络基础设施变得越来越复杂,网络规模也越来越大,验证是否能够达到预期结果也至关重要。对网络验证领域的研究最早是在学术研究实验室,比如卡梅隆大学,AT&T实验室,斯坦福大学和微软研究院。该技术的灵感来自计算机科学领域,即形式化验证,基于严格的数学表述和模型去验证网络中的问题。

    维基百科对形式化验证的解释是这样的: 在计算机硬件(特别是集成电路)和软件系统的设计过程中,形式化验证的含义是根据某个或某些形式化规范或属性,使用数学的方法证明其正确性或非正确性。 在芯片设计领域中,最知名的失败案例,是Intel的Pentium处理器浮点运算单元出错(FDIV Bug),数以万计的Pentium处理器不得不回收和替换,给Intel造成了约4.7亿美元的损失。在那之后,Intel开始在其芯片设计中广泛采用形式化验证。除了在芯片领域,形式化验证还在许多领域中应用,例如航天,操作系统,金融领域等等。

    无论是硬件还是软件工程,归根结底是数学问题。如果我们可以验证软件,为什么不验证网络?从某种意义上说,网络就像软件一样,可以对不同网络层进行抽象建模。它接受输入,例如网络配置,拓扑,路由表,数据包起始位置等等,并根据这些输入逐步执行操作,例如使用转发规则,如果数据包的IP目的地址是10.2.1.0/24,然后将其发送到指定的出接口。最后计算出验证结果,例如数据包被丢弃,修改,转发到指定出接口。

    下文将介绍形式化验证在网络领域中的应用,主要分为四个小节:

    模型检查(Model Checking)

    定理证明(Theorem Proving)

    符号执行(Symbolic Execution)

    SAT/SMT求解器(SAT/SMT Solvers)

    模型检查(Model Checking)

    模型检查(Model Checking)是一种基于状态迁移系统的自动验证技术。它最早是由Clarke和他的研究生Emerson以及Sistla在1981年提出来的,基本想法是将系统建构为一个有限状态机(Finite State Machine),通过有效的搜索方法(状态空间检索state-space search)来检查给定的系统是否满足规范,检查系统是否满足所需的不变式。它将转换模型系统分解成逻辑公式,然后计算出能够满足公式的条件。当检查出不满足时,会返回一个反例可以帮助人们去解决这个系统的问题。由于模型检查的工作机制会导致系统状态空间的大小呈指数增长,存在状态空间爆炸的问题。因此学术界和业界提出了许多优化的方法,例如:

    有界模型检查(Bounded Model Checking),使用SAT(Boolean satisfiability)求解器在一定边界条件下寻找反例。

    符号模型检查(Symbolic Model Checking),使用二元决策图(Binary Decision Diagrams)而非独立的状态列表来表达状态空间。进一步简化的有序二元决策图(Reduced Ordered Binary Decision Diagrams),可以缓解状态爆炸问题。

    模型检查在网络领域中的应用,例如Flowchecker使用二进制决策图(BDD)根据openflow控制器转发行为构建状态机,然后使用符号模型检查工具NuSMV检测网络配置错误。当数据包从服务器A发往服务器B时,每个网络中的设备可以在特定接口上转发数据包,丢弃包,或修改包头并转发。

    以下图为例,交换机SA有一些转发表,例如规则RA1将目的IP是192.168.1.0/24网段的报文通过接口pa0发出去。网络系统的状态(State)由数据包头空间p以及所在位置l决定,例如初始状态数据包是一个全空间(表示所有的报文),对应的位置是主机PA,那么初始状态(Initial State)可以编码为(p, PA)。交换机上在接口之间转发数据包的规则可以被认为是状态转换(State Transitions),例如(p, SA) → (p′, SB) (p.dst ∈ 192.168.2.024 & p.dst′ = p.dst)表示SA设备上RA2的转发逻辑。

    7fad254627b7ebae507a3f31dca6106b.png

    当对报文初始状态以及状态之间的转换编码完成后,可以定义属性(property),例如查看是否存在一个报文可以从主机PA转发到主机PB上。在CTL的语法中,从PA到PB的值可以表示为EF(l=PB),可以输入模型和属性到模型检查器引擎(例如NuSMV)。如果引擎返回pass,该属性保留在系统模型上。如果模型不满足该属性,系统将返回一个反例。上面的例子中,模型满足输入的属性。

    定理证明(Theorem Proving)

    定理证明是另一个重要的形式验证方法。它对系统用严格语义的数学符号进行描述和推理,将模型抽象为逻辑公式,然后使用自动的逻辑推理技术去验证。针对不同的应用领域,运用不同的形式演算方法,出现了多种定理证明系统,主要分为交互式定理证明器(interactive theorem prover)和自动化定理证明器(automated theorem prover)两大类。交互式定理证明器以人机交互为基础,使用者先指定每一个证明步骤所需要做的工作,然后由计算机完成具体的工作细节。因此对用户而言十分复杂,而且并没有办法确保事先人为制定的规则和定理的正确性,因此最终的正确性也值得怀疑,即前提若有错误,则最终的验证结果就不一定正确。与模型检查不同,定理证明没有状态的概念,不需要对系统的状态空间建模。通常用户使用定理证明作为主要验证,以避免状态爆炸问题。

    定理证明在网络领域中的应用,例如VeriCon验证无限状态SDN程序。以下图为例,输入网络拓扑,例如(SA,pa1,pb1,SB)可以表示为交换机SA接口pa1连接到交换机SB接口SB。输入转发规则,例如SB.recv(p.dst∈192.168.2.0/24,pb1)表示目的IP为192.168.2.0/24数据包p可以在交换机SB的接口pb1接受。判断是否来自PA的数据包可以到达PB。当查看报文能否从主机PA转发到主机PB上,我们可以证明PAsent(p.dst∈0.0.0.0/0)=>PB.recv(p.dst∈192.168.2.0/24)公式为true。值得一提的是,当不满足公式时,定理证明不能提供反例,所以用户没办法依据反例进行分析和调试。

    84fdd99c15d483a1a1e728c140aed19a.png

    符号执行(Symbolic Execution)

    维基百科对符号执行的解释是这样的: 符号执行是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时,该程序会使用符号值作为输入,而非一般执行程序时使用的具体值。在达到目标代码时,分析器可以得到相应的路径约束,然后通过约束求解器来得到可以触发目标代码的具体值。

    符号执行技术是一种白盒的静态分析技术。从表面上看,网络与软件代码有些不同,网络包括路由器,网卡,线缆等。整个网络也可以被视为”程序“,例如路由器的转发表可以被认为是一条程序语句表示转发特定的报文到出接口。在网络领域中,应用符号执行技术项目有HSA,SymNet等等。那么如何形式化地表示符号执行的过程呢?程序的所有执行路径可以表示为树,叫做执行树。每一个条件分支都会产生两个不同约束,符号执行要探索的执行路径按照指数增长。以下图为例,该程序段表示了转发规则如何在设备接口之间转发报文。每次迭代(第12行)都会处理一个报文,分为两个步骤:1. 转发数据包到当前链路。2. 然后将其作为参数转发到于此链路相连的设备上。我们可以定义一个断言声明:定义从主机PA的数据包转发到主机PB,A[i].s_Tag表示原始报文,A[i].d_Tag表示当前位置上的报文。我们将程序和断言输入到符号执行引擎。该引擎输入一个符号值表示报文,然后分析程序的执行路径,最终会返回断言是否成立。

    46cc446fb263503b3cd92a2173a04a86.png

    SAT/SMT求解器(SAT/SMT Solvers)

    SAT求解器采用基于David-Putnam的搜索技术(也称DP方法)解决逻辑公式的可满足性问题。SMT起源于对SAT的扩充。SAT的表达能力有很大的局限性, 许多问题需要用更强大的逻辑来表达。如果给定一个公式,如果存在一个赋值使该公式为真,那么称该公式是可满足的,否则称该公式是不可满足的。SAT求解器的输入用逻辑表达的公式,求解器自动决定相应内容是否可满足。以下图为例,对设备转发表进行编码G(SA,SB)=p.dst∈192.168.2/24是一个布尔公式,表示为设备SA到设备SB之间数据报文转发的约束。如果想验证报文从主机PA是否能到主机PB,将两条路径PA→SA→SB→PB和PA→SA→SC→SB→PB的逻辑表达的公式输入到求解器中进行运算,如果不满足会输出一个反例。

    5421301dd604753d05929fd6e584b2a3.png

    SAT/SMT求解器大量的应用在网络验证中,AWS有一个ARG(Automated Reasoning Group)团队,他们借助自动推理技术检测可能潜在暴露脆弱数据的各类配置错误。例如Zelkova策略分析引擎可以自动检测各种类别的资源配置错误,它翻译策略成SMT约束公式,然后使用Z3,Z3AUTOMATA和CVC4求解器进行证明是否能够满足Ture,或者返回一个反例满足为False。当用户下发这个策略后,S3会对这个bucket打上public标签提醒用户,这是怎么做到的呢?Zelkova翻译用户的策略转换为数学公式,仅当其左侧和右侧均为真时才为真。Resource和Principal是变量,就像在代数中使用x和y一样。

    Java

    (Resource = “arn:aws:s3:::test-bucket”) ∧ (Principal ≠ 11112222333)

    1

    (Resource=“arn:aws:s3:::test-bucket”)∧(Principal≠11112222333)

    下一步是要确定此策略公式是否允许公共访问,Zelkova通过对比两个策略决定哪个策略更宽松(permissive)。Zelkova具有一项特殊的策略,该策略允许未经授权的匿名用户访问S3资源。Zelkova将用户下发的策略​​与此策略进行比较。如果用户的政策更为宽松(permissive),则表明政策允许公共访问。如果用户的策略严格限制访问,例如基于源VPC endpoint(aws:SourceVpce)或源IP地址(aws:SourceIp),那么用户的策略就不会比这个特殊策略更为宽松,因此Zelkova认为用户的策略不允许公共访问。延伸阅读:AWS基于模型的网络验证

    参考文献

    展开全文
  • 形式化验证工具调研

    2021-08-03 20:46:12
    形式化验证主要分为:模型检测(又称模型检验)和定理证明两种方法。 以下为调研后整理的笔记。 (其中模型检测工具部分,引用了博主yisun03的这篇博客。) 模型检测步骤与工具 模型检测的步骤: 1. 抽象出系统的数学...

    形式化验证主要分为:模型检测(又称模型检验)和定理证明两种方法。
    以下为调研后整理的笔记。
    (其中模型检测工具部分,引用了博主yisun03的这篇博客)

    模型检测步骤与工具

    模型检测的步骤:

    1. 抽象出系统的数学模型

    • 迁移系统(Trasition system)
    • 马尔可夫链(Markov chain)
    • Kripke结构(Kripke structure)

    2. 给出能够描述该系统性质的语言

    • 线性时序逻辑LTL:
      关心系统的任意一次运行中的状态以及它们之间的关系
    • 计算树逻辑CTL:
      分叉时序逻辑,用来描述状态的前后关系和分支情况
    • μ \mu μ-演算:
      关心系统的动作与状态之间的关系

    在这里插入图片描述

    模型检测工具:

    1.面向形式化规格语言的模型检测工具

    • SMV符号模型检测工具
      SMV用以检测一个有限状态系统是否满足CTL公式。
      它的建模方式是以模块为单位,模块可以同步或异步组合,模块描述的基本要素包括非确定性选择,状态转换和并行赋值语句。
      其模型检测的基本方法是以二叉图表示状态转换关系,以计算不动点的方法检测状态的可达性和其所满足的性质。

    http://www.cs.cmu.edu/~modelcheck/smv.html

    • NuSmv(New Symbolic Model Verifier) 新符号模型检测工具
      对SMV重构的一个模型检测工具
      支持计算树逻辑CTL和线性时序逻辑LTL描述的所有规范
      整合了以SAT为基础的有界模型检测技术

    http://nusmv.fbk.eu/

    • nuXmv 分析同步有限状态和无限状态系统的新符号模型检测工具
      扩展于NuSMV
      对于有限状态的情形,nuXmv特点是基于SAT算法的有效验证引擎
      对于无限状态的情形,nuXmv特点是基于SMT的验证技术,与MathSAT5紧密集成

    https://nuxmv.fbk.eu/

    • Uppaal(Uppsala University & Aalborg University) 时间自动机的模型检测工具
      建模和模拟及验证实时系统的工具

    http://www.uppaal.org/

    • STeP(Stanford Temporal Prover) 斯坦福时间验证器
      用模型检测器处理子系统的验证问题
      用定理证明器将结果汇总处理
      不限于有限状态系统
      用推论方式联合模型检测应用于更广泛的系统,包括无限数据域的程序

    http://www-step.stanford.edu/

    • CWB(Concurrency Workbench) 适用于并发系统操作与分析的自动化工具
      可以检测系统模型之间的等价关系、FRE-ORDER关系和系统是否能够满足 μ \mu μ-演算的公式
      建模方法使用CCS语言或LOTOS语言的子集
      能分析给定程序的状态空间及检测多种语义的等价性和序列性

    http://homepages.inf.ed.ac.uk/perdita/cwb/

    • VIS(Verification Interacting with Synthesis) 用于形式验证、综合和模拟有限状态系统的工具
      能够综合有限状态系统并验证这些系统的属性

    http://vlsi.colorado.edu/~vis/

    2.面向源程序语言的模型检测工具

    • SPIN(Simple Promela Interpreter) 显式模型检测工具
      SPIN用以检测一个有限状态系统是否满足PLTL公式及其他一些性质,包括可达性和循环。
      建模方式是以进程为单位,进程异步组合,进程描述的基本要素包括赋值语句,条件语句,通讯语句,非确定性选择和循环语句。
      基本方法是以自动机表示各进程和PLTL公式,以计算这些自动机的组合可接受的语言是否为空的方法检测进程模型是否满足给定的性质。
      建模语言为PROMELA(PROcess MEta LAnguage),基于进程结构,有类似C语言的结构

    http://spinroot.com/spin/whatispin.html

    • BLAST(Berkeley Lazy Abstraction Software Verification Tool) C程序的时序安全属性自动验证工具
      基于反例引导的抽象求精框架对C语言程序进行检测
      采用懒惰抽象(lazy abstraction)技术,有效地提高了效率

    http://cseweb.ucsd.edu/~rjhala/blast.html

    • SLAM C程序模型检测工具
      将原C语言程序抽象为布尔程序进程验证工作
      抽象后的程序仅剩下布尔变量
      依靠C2bp,Bebop,Newton3个工具分别负责完成抽象、检测和抽象求精任务

    https://www.microsoft.com/en-us/research/project/slam/

    • JPF(Java Path Finder) Java程序验证工具
      实现了一个MC-JVM来解决内存分配和垃圾回收等问题

    http://babelfish.arc.nasa.gov/trac/jpf

    • VeriSoft 直接测试C源代码

    • Eraser 能够检测Java代码

    • Jchecker C程序模型检测工具
      基于谓词抽象理论
      采用基于谓词抽象的反例引导的抽象求精框架
      能够针对C程序源码抽象出模型并完备地搜索其状态空间,以此验证程序的安全属性
      最大限度缩减状态空间

    • Bandera 并发Java程序的模型检测工具
      工具平台
      基于程序切片技术,将Java程序转换成中间代码
      后端接口适应多种模型检测器,包括SPIN和SMV

    http://bandera.projects.cs.ksu.edu/

    • Klocwork InsightPro 可以检测多种语言类型的多种质量缺陷和安全漏洞

    • CMC 可以检测C语言程序在执行时OS层级的调度

    • MaceMC 用于检测分布式系统
      http://www.macesystems.org/wiki/macemc

    • Chess 用于检测多线程的Windows程序

    https://www.microsoft.com/en-us/research/project/chess-find-and-reproduce-heisenbugs-in-concurrent-programs/

    • FDR

    https://www.cs.ox.ac.uk/projects/fdr/

    • Murphi 一种枚举显示状态的模型检测器,针对C语言

    http://formalverification.cs.utah.edu/Murphi/

    • MoonWalker 针对.NET应用的模型检测工具

    • XMC 对JAVA程序中同步操作算法检测

    • FLAVERS(FLow Analysis for VERification of Systems 针对ADA语言的工具

    http://formalverification.cs.utah.edu/Murphi/

    • Mocha 针对C语言的模型检测工具

    https://www.cis.upenn.edu/~mocha/

    • CBMC 针对C语言/C++的模型检测工具

    http://www.cprover.org/cbmc/

    • MAGIC(Modular Analysis of proGrams In C) 针对C语言的模型检测工具

    http://www.cs.cmu.edu/~chaki/magic/

    其他模型检测工具

    • OFMC
      一种用于安全协议的符号模型检测工具
    • CoPS
      持久安全性检测器
    • Rational Tau
    • F-Soft
    • IMPACT
    • Astree analysis tool
    • Saturn
    • Calysto
    • Terminator
    • SATABS
    • Terminator
    • mCRL2(micro Common Representation Language) 并发系统检测工具
    • LTSA(Labeled Transition System Analyzer) 并发系统检测工具
    • Maude 基于逻辑语义的工具
    • ISP MPI程序的检测工具
    • CHIC(Checker for Interface Compatibility) 模块行为兼容性的验证工具
    • MRMC(Markov Reward Model) 对离散和连续时间的马尔可夫激励模型
    • UMLChecker UML模型检测工具
    • BACH(Bounded ReachAblity CHecker) 用于分析线性混成自动机有界可达性分析
    • LDPChecker 针对正环闭合自动机(Positive Loop-closed Automata)检验线性时段性质
    • QRDChecker 针对时段时序逻辑QRDC(Quantified Restrictred Duration Calculs)的检验工具
    • Kronos
    • HyTech
    • AUTOABS
    • FeaVer
    • 3VMC
    • aSpin

    其他分类方式(1)

    结合模型检测与定理证明

    • STeP

    符号模型检测

    1. 用有序二叉图OBDDs(Ordered Binary Decision Diagrams)描述状态迁移图
    2. 用布尔逻辑公式描述系统属性

    定界模型检测技术(bounded model checking)

    1. 依赖于布尔可满足性问题(boolean satisfiability problem, SAT)的求解器
    2. 在限定步数k内,确定系统是否满足性质。
    3. 若不能确定,则增加k值,重新进行验证

    其他分类方式(2)

    基于自动机理论

    • SPIN
      基于不动点定理
    • SMV

    其他分类方式(3)

    针对实时系统的模型检测工具

    • UPPAAL, Kronos, STeP

    针对并发系统的模型检测工具

    • Spin, JPF, Verisoft

    针对混成系统的模型检测工具

    • HyTech, HySAT, BACH, LDPChecker

    定理证明工具

    交互式定理证明器(Interactive Theorem Prover)

    • Coq:

    https://coq.inria.fr/

    在这里插入图片描述

    Coq是一个形式化证明管理系统。它提供了一种形式化语言来编写数学定义、可执行的算法和定理,并为机器检查证明的半交互式开发提供了一个环境。典型应用包括编程语言属性的认证(例如CompCert编译器认证项目、用于验证C程序的已验证软件工具链或用于并发分离逻辑的Iris框架)、数学的形式化(例如Feit-Thompson定理的完全形式化,或同伦类型理论)和教学。

    • HOL:

    https://hol-theorem-prover.org/

    在这里插入图片描述

    HOL 交互式定理证明器是高阶逻辑的证明助手:一个可以证明定理并实现证明工具的编程环境。 内置的决策程序和定理证明器可以自动建立许多简单的定理(用户可能必须自己证明难的定理!) oracle 机制允许访问外部程序,例如 SMT 和 BDD 引擎。 HOL 特别适合作为实现演绎、执行和属性检查组合的平台。

    展开全文
  • 混合形式化验证工具 (CT-Scan) 2 设备介绍 2.1理论基础 采用C/C++语言进行编写的代码,在进行软件验证的过程中往往需要花费大量时间和精力,迫切需要一款能够自动测试验证软件以提高效率的工具。 为此我们推出CT-...
  • 一 引言 女娲是飞天分布式系统中提供分布式...本文即从程序员视角介绍形式化验证工具TLA+。 从理论上证明一个程序或者算法的正确性往往是困难的,工程中一般使用测试来发现问题,但再多的测试也无法保证覆盖到了..
  • 计算机系统形式化验证中的模型检测方法综述论文1 形式化方法概述形式化方法是用数学和逻辑的方法来描述和验证系统设计是否满足需求。它将系统属性和系统行为定义在抽象层次上,以形式化的规范语言去描述系统。形式化...
  • 当今行业的最新技术是基于UVM和基于形式化(Formal)的验证流程。事实证明,这两种技术都可以显著提高验证质量,但缺点是测试用例或激励不能“重复使用”。 测试用例的可移植性一直是整个行业验证团队的目标。没有...
  • 形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体,在国内外持续被关注和研究.在各种领域...
  • 为此,我们可以考虑两种不同的模式来实现目标:通用验证方法(UVM)方法(经典方法)和基于形式化的方法(新方法)。 本文将介绍基于形式化的方法是如何显著减少验证时间的。 经典的方法 多年来,我们一直...
  • 浅谈形式化方法

    2021-04-03 11:18:05
    软件工程中的形式化方法就是通过严格的符号系统和数学模型来描述和验证一个目标软件系统的行为和特性,包括需求规格、设计和实现等。形式化方法所使用的是严格的数学语言,其语法和语义都是无二义的、精确的。 2.主要...
  • 技术领域本发明涉及芯片设计验证领域,具体地说是一种实用性强、连接UVM验证平台的搭建方法。背景技术:伴随着芯片集成度增加,各种通信与信号处理算法被集成到系统芯片中,这些算法通常需要先利用Matlab或Simulink...
  • 什么是形式化方法

    2021-06-27 22:28:16
    在计算机科学和软件工程领域,形式化方法是基于 数学的特种技术,适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计,是期望能够像其它工程学科一样,使用适当的数学分析以提高设计的可靠性...
  • UI 设计代码化,即将软件的 UI 设计与 UI 交互转换为特定的领域语言,并使用代码的方式来进行管理。它可以直接将需求转换为 UI 原型,让设计人员基于此进行设计;还负责将其转换对应的 ...
  • 关于Java类加载,主要弄清楚三个问题 :为什么需要类加载什么时候进行类加载怎么进行类加载一、为什么需要类加载我们编写好的程序经过编译之后,会形成Class文件,Class文件描述了类的各种信息,而Java虚拟机想要...
  • 背景介绍近年来,关于低代码(LowCode)和无代码(NoCode)的讨论在前端社区内越来越火,简单的说低代码就是通过编写少量代码的方式完成应用的开发及上线,而无代码则更进一步,不需要编写...
  • 了解形式化方法

    2021-04-02 10:40:48
    在计算机科学和软件工程领域,形式化方法是基于数学的特种技术,适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计,是期望能够像其它工程学科一样,使用适当的数学分析以提高设计的可靠性和...
  • 近年来,关于低代码(LowCode)和无代码(NoCode)的讨论在前端社区内越来越火,简单的说低代码就是通过编写少量代码的方式完成应用的开发及上线,而无代码则更进一步,不需要编写代码通过...
  • 算术约束在形式推理和(困难的)问题解决的每个方面都是普遍存在的,LA和LP都是建立这些模型和解决问题的非常有力的工具。 从计算机科学的观点来看,大多数LA和LP问题都可以通过专用软件或库来解决,IBM非常流行的...
  • 众所周知,在数字IP设计以及SoC设计中,验证任务迫在眉睫。目标是使RTL代码和功能覆盖率都...一些验证工程师还使用形式化的方法来验证模块的专用部分,例如标准接口,从而完成IP验证。 本文将介绍一种基于形式...
  • 一、Java 类加载过程、 0、字节码编译、 1、加载、 2、连接、 3、初始、 总结、
  • 在先前的一系列《云研发:研发即代码》文章里,我们介绍了软件工程的代码化闭环。同时,在《Water:云研发架构模式》介绍了设计这样的开发环境里,我们所需要的一些模式。今天呢,作为这一系列的落...
  • 什么是形式化方法?

    2021-04-20 21:44:13
    软件形式化方法最早可追溯到20世纪50年代后期对于 程序设计语言编译技术的研究,即J.Backus提出BNF描述Algol60语言的语法,出现了各 种语法分析程序自动生成器以及语法制导的编译方法,使得编译系统的开发从“手工艺...
  • 上一章[《曲鸟全栈UI自动教学(七):使用Pytest来搭建自动测试框架》的教学中,我们搭建了一个自动测试框架的雏形,做到了数据和代码的分离。这篇会为对框架代码进行讲解
  • 文章目录前言Java反序列源码审计分析IDEA 部署环境序列过程分析 前言 在前面的一篇文章:Apache Shiro Java反序列漏洞复现 曾介绍了 CVE-2016-4437 漏洞的复现过程和利用方式,为了不再当个“脚本小子”工具人...
  • 点击上方蓝字关注我们基于上下文的智能化代码复用推荐彭鑫1,2,陈驰1,2,林云31复旦大学计算机科学技术学院,上海 2004382上海市数据科学重点实验室,上海 2004383新...
  • 更系统来讲,它还包括编译仿真的流程、结果分析报告和覆盖率检查等。狭义上说,主要关注验证平台的结构和组件部分,他们可以产生设计所需要的各种输入,也会在此基础上进行设计功能的检查。 各个组件之间是相互独立...
  • CPU系统级验证

    千次阅读 2020-12-25 10:26:02
    系统级验证中的形式化验证是近期较流行的一种验证方式,它是可以在simulation之前做的验证,在芯片设计流程通常处于CPU的RTL代码尚未设计好的阶段,此外,在simulation进行的同时,同样可以采用形式化验证并行工作,...

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 234,200
精华内容 93,680
关键字:

代码形式化验证的基本流程