从seL4谈形式化验证

最近seL4的出现再次引起大家对形式化方法的兴趣，一个形式化验证过的OS微内核。它网站自己介绍“seL4 is a high-assurance, high-performance operating system microkernel. It is unique because of its comprehensive formal verification, without compromising performance. ”
对specification和代码做了一致性验证；对代码和二进制做了一致性验证，可以算走了完整的链条了。主要采用定理证明器isabelle。非常扎实的工作！也因为这么扎实，节奏肯定快不了，另外也需要有产业使用。似乎现状不是太容易，希望能坚持下去啊~

-----some background-----
形式化方法使用严格的数学语言对计算机系统（硬件或软件）建模，并在计算机的辅助下验证系统的正确性。与测试不同，形式化方法可以完全排除某些类型的错误。
形式化方法的两大关键技术是约束求解和定理证明。著名的定理证明器isabelle大概30几万行代码（后端30万行ML语言（函数式编程语言），前端Scala语言），著名的约束求解器Z3大概60万行代码（不包括那些生成的，主要是C++，少量python及其他）。要论代码量，当然也大，但令人望而却步的是，要看懂这些代码，需要学习的知识，以及很长的学习周期，以及坐住冷板凳的耐心。

从seL4谈形式化验证相关推荐

操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(7) - C代码的自动验证（转载）
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(10) - 一阶直觉逻辑
操作系统形式化验证实践教程(10) - 一阶直觉逻辑前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍,基础好的同学已经可以基于前面的知识开始自己的工作了. 对于只学过离散数学,而 ...
鉴源论坛 · 观模丨µC/OS内核的形式化验证技术
作者 | 郭建上海控安可信软件创新研究院特聘专家丁继政上海控安研发中心研究员版块 | 鉴源论坛 · 观模操作系统作为软件系统的核心,其安全性与可靠性是构造高可信软件最为关键 ...
形式化验证的原理和过程
形式化验证包含两种方式:定理证明(数学定理的方式,所以对任意状态数的系统都适用,缺点是不能很好的给出反例),模型检测(主要是进行所有的状态检测,并能给出反例,缺点是存在复杂系统的状态爆炸问题).模型检 ...
形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink
在安全关键领域,基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具对算法或者控制逻辑进行可视化建模,然后生成高可靠的二进制代码逐渐成 ...
linux内核形式化验证,说说形式化验证（Formal Verification）吧
原标题:说说形式化验证(Formal Verification)吧前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼 ...

从seL4谈形式化验证

从seL4谈形式化验证相关推荐

最新文章

热门文章