电子技术论坛_中国专业的电子工程师学习交流社区-中电网技术论坛

标题: 将代码静态分析提高一个层次，Coverity提出布尔可满足性概念 [打印本页]

作者: 我是MT 时间: 2015-12-23 16:36 标题: 将代码静态分析提高一个层次，Coverity提出布尔可满足性概念

布尔可满足性(Boolean satisfiability)的概念正在被用于确定软件代码中的“bug”，从而保证代码基本上不存在bug，满足编程者的愿望。
在2007年嵌入系统会议上，Coverity宣布了据称是第一种基于布尔可满足性(SAT)的源代码分析引擎。Coverity公司的SAT引擎利用了它的软件DNA图谱，自动、正确和精确地确定源代码中的缺陷。该软件DNA图谱精确地代表人们已写出来的任何软件。
Coverity在企业应用领域是领导厂商。它的静态分析软件客户包括财富500强上面57%的软件公司和50%的电脑外设公司。它的主要产品是Prevent Software Quality System (SQS)，SQS通过在编译时解析源代码来使复杂软件中的缺陷和安全漏洞检测实现自动化。
目前的静态分析引擎依赖数据流分析和多个检验程序来确定软件缺陷。与此不同的是，SAT引擎基于布尔可满足性，将能支持多个解算程序确定软件缺陷。
这种新的软件代码分析方法，得益于Coverity正在申请专利的技术，该技术以精确到位(bit)的精度代表软件系统，每个相关软件运算都被翻译成布尔值真(true)与假(false)和布尔运算符(Not逻辑非)、and(逻辑与)、or(逻辑或)。这允许利用基于SAT的解算程序对源代码进行分析，这在商业电脑编程领域还是第一次。
300多家客户已经在依靠Coverity Prevent SQS来分析其应用程序中的每个路径。通过利用SAT，Prevent SQS不仅能够分析每个路径，而且能够分析这些路径之中每次计算中的每个值。Chelf表示，这样彻底的静态代码分析，实现了业内对关键性能和安全漏洞的最精确鉴定。
据Forrester Research的安全与风险管理部门的首席分析师Chenxi Wang，“可满足性”原理用于硬件检验已有一段时间，但以前从未用于软件检验。
Wang认为，还有创新空间，具体而言是在嵌入软件领域。“嵌入软件通常在复杂性和状态数量方面比普通应用软件受到的限制多一点，因此，SAT更可能在嵌入编程领域增强软件验证的水平。”
Coverity的Chelf表示，“静态分析方法一直成功地用于EDA产业。我们只是把电路设计工作中使用的同样的软件布尔原理用于软件代码领域。”
Coverity Prevent SQS的基础技术是20世纪90年代在斯坦福大学电脑系统实验室开发出来的，当时在此工作的Ben Chelf和同事把该技术用于商业应用。

欢迎光临电子技术论坛_中国专业的电子工程师学习交流社区-中电网技术论坛 (http://bbs.eccn.com/)