將代碼靜態(tài)分析提高一個層次，Coverity提出布爾可滿足性概念

布爾可滿足性(Boolean satisfiability)的概念正在被用于確定軟件代碼中的“bug”，從而保證代碼基本上不存在bug，滿足編程者的愿望。

在2007年嵌入系統(tǒng)會議上，Coverity宣布了據(jù)稱是第一種基于布爾可滿足性(SAT)的源代碼分析引擎。Coverity公司的SAT引擎利用了它的軟件DNA圖譜，自動、正確和精確地確定源代碼中的缺陷。該軟件DNA圖譜精確地代表人們已寫出來的任何軟件。

Coverity在企業(yè)應(yīng)用領(lǐng)域是領(lǐng)導(dǎo)廠商。它的靜態(tài)分析軟件客戶包括財富500強上面57%的軟件公司和50%的電腦外設(shè)公司。它的主要產(chǎn)品是Prevent Software Quality System (SQS)，SQS通過在編譯時解析源代碼來使復(fù)雜軟件中的缺陷和安全漏洞檢測實現(xiàn)自動化。

目前的靜態(tài)分析引擎依賴數(shù)據(jù)流分析和多個檢驗程序來確定軟件缺陷。與此不同的是，SAT引擎基于布爾可滿足性，將能支持多個解算程序確定軟件缺陷。

這種新的軟件代碼分析方法，得益于Coverity正在申請專利的技術(shù)，該技術(shù)以精確到位(bit)的精度代表軟件系統(tǒng)，每個相關(guān)軟件運算都被翻譯成布爾值真(true)與假(false)和布爾運算符(Not邏輯非)、and(邏輯與)、or(邏輯或)。這允許利用基于SAT的解算程序?qū)υ创a進行分析，這在商業(yè)電腦編程領(lǐng)域還是第一次。

300多家客戶已經(jīng)在依靠Coverity Prevent SQS來分析其應(yīng)用程序中的每個路徑。通過利用SAT，Prevent SQS不僅能夠分析每個路徑，而且能夠分析這些路徑之中每次計算中的每個值。Chelf表示，這樣徹底的靜態(tài)代碼分析，實現(xiàn)了業(yè)內(nèi)對關(guān)鍵性能和安全漏洞的最精確鑒定。

據(jù)Forrester Research的安全與風(fēng)險管理部門的首席分析師Chenxi Wang，“可滿足性”原理用于硬件檢驗已有一段時間，但以前從未用于軟件檢驗。

Wang認為，還有創(chuàng)新空間，具體而言是在嵌入軟件領(lǐng)域。“嵌入軟件通常在復(fù)雜性和狀態(tài)數(shù)量方面比普通應(yīng)用軟件受到的限制多一點，因此，SAT更可能在嵌入編程領(lǐng)域增強軟件驗證的水平。”

Coverity的Chelf表示，“靜態(tài)分析方法一直成功地用于EDA產(chǎn)業(yè)。我們只是把電路設(shè)計工作中使用的同樣的軟件布爾原理用于軟件代碼領(lǐng)域。”

Coverity Prevent SQS的基礎(chǔ)技術(shù)是20世紀90年代在斯坦福大學(xué)電腦系統(tǒng)實驗室開發(fā)出來的，當(dāng)時在此工作的Ben Chelf和同事把該技術(shù)用于商業(yè)應(yīng)用。