软件形式化验证工具设备单项论证报告

1 设备名称
混合形式化验证工具 (CT-Scan)

2 设备介绍
2.1理论基础
采用C/C++语言进行编写的代码，在进行软件验证的过程中往往需要花费大量时间和精力，迫切需要一款能够自动测试验证软件以提高效率的工具。
为此我们推出CT-Scan，其主要原理是基于代码的形式验证，简单说就是对程序代码进行数学建模，并进行推理，解决代码的正确性，安全性等问题。
CT-Scan能高效地把代码转化为等价的分离逻辑公式，并归结为命题逻辑，进而用命题逻辑判定过程来求解，证明或证伪用户指定的断言。
2.2主要功能
CT-Scan利用提取的代码形式模型，可以完成诸多衍生功能，主要功能如下。
1.支持多种类型的漏洞检测，包括缓冲区溢出、内存越界访问、空指针使用、变量未初始化、除零、断言失败等漏洞问题；
2.具有很高的覆盖率，并且能够自动搜索所有路径，自主增加覆盖率。能形成完整覆盖率的测试用例的最小集合，对于未覆盖部分，通过计算求解输入集，进而生成测试用例完成覆盖；
3.具有很强的主动挖掘代码漏洞的能力，并且能自动标记BUG生成测试用例，方便开发人员快速定位并解决BUG；
4.支持浮点运算的安全验证，是目前所有形式化验证工具中唯一支持浮点运算验证的工具；
5.拥有高度的自动化程度。测试人员配置好参数后即可全部自动执行，全程无需人工参与。

2.3技术突破
CT-Scan核心技术突破，总结如下：

基于云的大规模并行计算，突破了计算瓶颈。
因为形式化验证需要执行系统的路径搜索，求解器需要暴力破解程序路径，遍历搜索空间，这需要巨量的计算资源。CT-Scan采用基于云的大规模并行计算，把问题灵活切分成许多计算子任务，调度到云中的其他计算节点。同时可以根据计算节点的数目，自动实现负载平衡，实现弹性计算。
混合静态/动态分析以及形式验证，从而突破目标代码规模。
以往的形式验证工具由于求解器的能力有限，很难应用于大规模的代码。CT-Scan在实际运行当中，最高可处理近1亿条指令，这源于静态分析和动态分析等多种技术的融合和互补。其中动态验证，和形式验证的混合是关键，可以把搜索集中在关键区域，从而突破代码规模的限制。
全栈优化，突破性能瓶颈。
CT-Scan运用了多种优化算法来提升性能，从顶层的任务调度和分配，到前端的编译器，IR的变换，以及后端的求解器等都进行了相应的优化。正是多重优化的累积，才能使工具在几个小时内挖掘出被遗漏的安全漏洞。

3必要性分析
3.1 承担的任务
CT-Scan混合形式化验证工具利用有限的资源，对路径分支条件和高危代码验证的部分采取建模求解，实现更高质量的软件测试，同时强调程序持续测试，和测试自动化。
3.2相关条件现状及差距
传统的软件测试技术，比如静态测试、动态测试已经不能满足目前的软件安全测试要求。
静态测试主要通过数据流分析和模式匹配技术扫描代码，适合查找浅层的错误，无法挖掘深层的，比如与输入相关的错误。同时，由于忽略了程序的精确语义，容易产生大量误报。人工排查误报，需要消耗测试人员大量的时间资源。
动态测试依赖人工编写大量有效的测试用例。本质上是在输入空间里面采样，目前软件的复杂性决定了大部分的合法输入从没有被测试过，或者说输入空间的覆盖严重不足，这往往意味着遗漏的程序缺陷，带来安全隐患。
考虑到目前的安全现状，高可靠性的C/C++代码测试亟需的，是一种新型的工具，弥补静态/动态测试的不足，自动、深度挖代码漏洞，消除安全隐患。
CT-Scan混合验证平台的提出，正是为了解决以上问题。
3.3 必要性及合理性分析
对软件可靠性要求很高项目，需要对软件进行充分的验证。而对软件进行充分验证是十分困难的事情，使用传统的方法很难实现这一目标。形式化验证是近年来迅速发展的一种软件验证方式。
形式化验证，是指严格建立在数学基础上的软件验证方法，即将软件的逻辑行为进行数学建模，并通过求解来证明成立。因为形式化验证是能够从数学上严格的判定成立与否，所以，软件能否通过形式化验证的检测，成了国际上评定软件安全等级的重要标准，如图所示，最高等级的EA7，就是指软件完全通过形式化验证，由此可见形式化验证对软件安全的重要性。

不同于其他工具采用的纯静态分析和纯动态测试测试技术，CT-Scan采用静态分析动态测试和形式化验证相结合的技术，能够协助软件开发测试人员，深入分析软件的编码和安全漏洞，在更短的时间内以更少的精力处理和解决问题。
CT-Scan模拟程序执行，自动深入遍历程序执行空间，大规模覆盖可能路径。深入运用人工智能领域的约束求解，空间搜索和机器学习技术，模糊测试技术，并与传统静态和动态分析方法紧密结合，深入检查软件的各种错误和漏洞，包括静态分析器中的编码错误检查和安全漏洞检查，提供极低的（0%）误报率。
3.4与静态验证的比较表
形式验证技术对代码进行语义等价变换，并利用数理逻辑逻辑进行精确推理，所以并不存在误报。同时CT-Scan会系统搜索程序的每一条路径，深度挖掘错误，并对每一个路径生成一个覆盖该路径的测试用例，这些都是静态分析所不具备的。

因此，CT-Scan形式化验证工具有多种优点。
（1）安全可靠、稳定性极高，可以达到安全可靠运行要求；
（2）支持多种主流的操作系统，支持二次开发，易于扩展，用户可以多种方式灵活运用CT-Scan的各种功能；
（3）易安装，易运行，配置成功一次，以后可以持续、自动运行，无需值守。

4 设备方案
4.1与同类产品的优势比较表
经调研，北京嘉辰永成软件技术有限公、美国Parasoft和英国LADA均有能力承制该设备。具体对比情况见下表：

5 建设效果分析
• 大量减少调试时间
• 减少软件缺陷提高产品信誉
• 降低维护和支持成本
• 发现一些平时很难发现的BUG
• 支持多平台和跨平台开发
• 能够与开发生命周期无缝集成

软件形式化验证工具设备单项论证报告相关推荐

形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
计算机科学家证书,软件自动验证的追梦者——吴志林，2020年CCF-IEEE CS青年科学家奖获得者...
CCF理事长梅宏教授(左一).百度校园品牌部总监李轩涯博士(右一)为吴志林研究员颁奖吴志林本科就读于中南大学,博士毕业于中国科学院软件研究所计算机科学国家重点实验室.博士毕业之后,先后在中国科学院自 ...
国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink
在安全关键领域,基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具对算法或者控制逻辑进行可视化建模,然后生成高可靠的二进制代码逐渐成 ...
什么是软件形式化方法
软件形式化方法(Formal Method)在软件开发中一直都受到多方面的争议.持肯定态度的拥护者认为形式化方法会引起软件开发的革命,另一些持否定态度者则怀疑甚至反对将数学引入软件开发过程中. 形式化 ...
linux内核形式化验证,说说形式化验证（Formal Verification）吧
原标题:说说形式化验证(Formal Verification)吧前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼 ...
鸿蒙形式化验证,形式化验证在网络中的应用
作者简介:唐昊,现就职于华为,从事云网络研发工作. IBN(基于意图的网络)是近年来网络领域中最热门的话题之一,网络验证是其中最关键的环节.我们在此之前一直专注于网络配置的自动化,例如根据模板创建配置 ...
鉴源论坛 · 观模丨µC/OS内核的形式化验证技术
作者 | 郭建上海控安可信软件创新研究院特聘专家丁继政上海控安研发中心研究员版块 | 鉴源论坛 · 观模操作系统作为软件系统的核心,其安全性与可靠性是构造高可信软件最为关键 ...

软件形式化验证工具设备单项论证报告

软件形式化验证工具设备单项论证报告相关推荐

最新文章

热门文章