随想录（形式化验证小结）

形式化验证，英文是formal verification，是验证软硬件逻辑很重要的一种方法。特别是对于芯片开发、高安全性的系统开发来说，是非常必要。这主要是因为系统失败的代价很高，传统的测试也无法验证整个系统的安全性和可靠性。

1、目前主要的测试方法

当前，验证的主要方法就是将软件、或者硬件代码转变成逻辑代码，接着用专门的逻辑验证软件来执行这些逻辑代码。

2、编程语言和工具

现在使用比较多的工具有Isabelle/HOL、CSP/PAT等，其中pat是新加坡的一所大学开发的，推荐大家作为入门使用。

3、已经使用形式化验证的软件

sel4，一个用形式化验证的操作系统内核

4、适合用作入门资料的几个链接

a，https://www.cnblogs.com/LoganChen/p/7729820.html

b，https://www.cnblogs.com/LoganChen/p/7735802.html

c，https://www.cnblogs.com/LoganChen/p/7741785.html

d，https://www.cnblogs.com/juandx/p/4225373.html

e，https://www.bbsmax.com/A/kPzOx2V7Jx/

f，https://github.com/seL4/seL4，形式化验证的os

g，https://github.com/AbsInt/CompCert，形式化验证工具

h，https://pat.comp.nus.edu.sg/，形式化验证的c编译器

5，形式化验证的几个注意点

a，形式化验证最难的部分就是需要将c&汇编语言转变成逻辑语言

b，形式化验证其实是一个白盒验证，它不仅需要了解软件的写法，还要做出抽象和提炼，对测试者要求很高

c，形式化验证不能保证100%的正确，但是会大幅度较少出错的风险

6，怎么简单地理解形式化

就好比c语言大家都会写，但是如何保证C语言都是正确的、没有二义性，穷举是没有用的。那么需要对c语言的bnf范式进行验证和确认，这才是验证的根本。

7，形式化验证的主要方法

a，等效性检验

b，定理证明

c，模型检验

8，形式化中的assert

目前看来形式化中的assert是需要自己设计的，除此之外，还需要自己确认哪些状态可达、哪些路径可以执行、哪些语句没有二义性，这个也比较复杂。看上去，形式化验证有点像单元测试，但是两者的内容还是不一样的。

9，最简单的形式化验证

这个例子来自https://www.cnblogs.com/LoganChen/p/7741785.html，

代码为，

//The classic Readers/Writers Example model multiple processes accessing a shared file.The Model//
//the maximun size of the readers that can read concurrently
#define M 2;
var writing = false;
var noOfReading = 0;Writer()     = [noOfReading == 0 && !writing]startwrite{writing = true;} -> stopwrite{writing = false;} -> Writer();
Reader()     = [noOfReading < M && !writing]startread{noOfReading = noOfReading+1;} -> //the following guard condition is important to avoid infinite state space, because noOfReading can go negtively infinitely([noOfReading > 0]stopread{noOfReading = noOfReading-1;} -> Reader());//there are infinite number of Readers and Writers
ReadersWriters() = |||{..} @ (Reader() ||| Writer());The Properties//
#assert ReadersWriters() deadlockfree;
#define exclusive !(writing == true && noOfReading > 0);
#assert ReadersWriters() |= [] exclusive;
#define someonereading noOfReading > 0;
#assert ReadersWriters() |= []<>someonereading;
#define someonewriting writing == true;
#assert ReadersWriters() |= []<>someonewriting;

10，形式化验证的另外一个战场

金融领域，特别是虚拟数字货币。

PS：

目前形式化验证国内的资料比较少，大家可以看一些论文、或者直接用bing搜国外的文章，用pat软件来学习也可以。只要有一些数理逻辑、离散数学的抽象思维和思想，理解起来没那么复杂。

后续如果发现更好的资料，我也会在这个page下面进行更新。

随想录（形式化验证小结）相关推荐

操作系统形式化验证实践教程(11) - 结构化证明语言Isar（转载）
操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言.使用Isar语言,还可以写得更加形 ...
操作系统形式化验证实践教程(11) - 结构化证明语言Isar
操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言.使用Isar语言,还可以写得更加形 ...
形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink
在安全关键领域,基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具对算法或者控制逻辑进行可视化建模,然后生成高可靠的二进制代码逐渐成 ...
linux内核形式化验证,说说形式化验证（Formal Verification）吧
原标题:说说形式化验证(Formal Verification)吧前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼 ...
linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(7) - C代码的自动验证（转载）
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
鸿蒙形式化验证,形式化验证在网络中的应用
作者简介:唐昊,现就职于华为,从事云网络研发工作. IBN(基于意图的网络)是近年来网络领域中最热门的话题之一,网络验证是其中最关键的环节.我们在此之前一直专注于网络配置的自动化,例如根据模板创建配置 ...

随想录（形式化验证小结）

随想录（形式化验证小结）相关推荐

最新文章

热门文章