高級(jí)靜態(tài)分析工具不再是新鮮事物，而是成為標(biāo)準(zhǔn)專業(yè)開發(fā)人員工具包中真正的戰(zhàn)略元素。

一些早期的靜態(tài)分析工具嚴(yán)格按照逐個(gè)函數(shù)或逐個(gè)模塊的方式運(yùn)行，很少或根本沒有跨模塊分析。接下來(lái)是“整個(gè)程序”分析，工具可以在其中找到可能的運(yùn)行時(shí)故障，但前提是給出感興趣程序的所有源代碼。今天，我們看到的工具可以對(duì)程序的某些部分有效，例如軟件庫(kù)或軟件子系統(tǒng)，而無(wú)需人工“驅(qū)動(dòng)程序”代碼來(lái)激活庫(kù)或子系統(tǒng)中的代碼。

靜態(tài)分析正在成為專業(yè)開發(fā)人員工具集的標(biāo)準(zhǔn)部分。美國(guó)國(guó)防部已經(jīng)認(rèn)識(shí)到靜態(tài)分析在幫助識(shí)別軟件密集型系統(tǒng)中的安全漏洞和弱點(diǎn)方面的重要性。 許多非國(guó)防組織也開始將靜態(tài)分析作為其日常軟件衛(wèi)生的一部分，因?yàn)殪o態(tài)分析在早期識(shí)別使用更傳統(tǒng)的測(cè)試不易檢測(cè)到的問題方面提供了獨(dú)特的優(yōu)勢(shì)。但是現(xiàn)在已經(jīng)確定了它們的好處，我們需要更仔細(xì)地研究各種工具的功能，并了解如何在現(xiàn)代開發(fā)環(huán)境中最有效地部署它們。

幾乎所有軟件開發(fā)組織都提倡代碼庫(kù)或代碼子系統(tǒng)的重用，至少在組織內(nèi)是這樣。不幸的是，許多靜態(tài)分析工具不能很好地適應(yīng)分析完整可執(zhí)行程序以外的任何內(nèi)容。這是因?yàn)樵S多靜態(tài)分析工具首先找到給定例程的所有調(diào)用者，然后有效地替換在任何這些調(diào)用中傳遞的參數(shù)值集，以確定感興趣的例程是否可能在給定輸入上失敗。因此，要對(duì)庫(kù)執(zhí)行靜態(tài)分析，程序員必須首先創(chuàng)建范圍廣泛的單元測(cè)試集，然后將靜態(tài)分析應(yīng)用于這些測(cè)試。這在一定程度上降低了靜態(tài)分析工具的潛在優(yōu)勢(shì)，

通過一種基于從代碼本身推斷構(gòu)建的前置條件和后置條件（通常稱為“合同”）的軟件庫(kù)靜態(tài)分析方法，同時(shí)還適應(yīng)程序員提供的斷言和前置條件和后置條件合同，分析工具非常有效地分析了庫(kù)中的所有代碼，并且作為一個(gè)附帶好處，生成了人類可讀的合同，總結(jié)了每個(gè)庫(kù)例程的要求和效果。

分析可重用庫(kù)

一種新型的靜態(tài)分析工具正在出現(xiàn)，它擺脫了為正在分析的代碼提供驅(qū)動(dòng)程序或線束的需求（圖 1）。這些工具可以自下而上地工作，從程序的葉例程或庫(kù)開始，并朝著更高級(jí)別的例程工作。此類工具從代碼本身推斷例程的契約（前置條件和后置條件），確定例程的算法可以處理哪些值范圍或值組合，以及哪些值集或組合將導(dǎo)致運(yùn)行時(shí)問題，例如在數(shù)組外部建立索引、溢出數(shù)值計(jì)算或取消引用可能為空的指針。這種自下而上、基于契約的方法允許這些高級(jí)靜態(tài)分析工具提供對(duì)程序片段的寶貴見解，從單個(gè)模塊到庫(kù)和子系統(tǒng)。推斷的合同被設(shè)計(jì)成人類可讀的，它提供了有用的竣工文檔，以幫助促進(jìn)手動(dòng)代碼審查，以及識(shí)別原始需求和當(dāng)前現(xiàn)實(shí)之間的不匹配。此類工具的示例包括 AdaCore 的 CodePeer 分析器和 Microsoft Research 的 CC-Check 工具 。

圖 1：可重用庫(kù)的靜態(tài)分析。

推斷前置條件和后置條件

在手動(dòng)代碼審查期間，由高級(jí)靜態(tài)分析工具推斷的合同可以幫助識(shí)別代碼的直接問題。這是一個(gè)例程的示例，其中例程的名稱顯然與其功能不匹配，如分析工具生成的推斷后置條件所示（圖 2）。

圖 2：推斷后置條件的示例。

推斷的后置條件（由 --#postcondition 注釋標(biāo)識(shí)）表明例程返回給定月份自年初以來(lái)的天數(shù)，而例程的名稱暗示它應(yīng)該返回在月。顯然，無(wú)論是程序員還是命名例程的人都感到困惑。這只是分析器推斷竣工合同的好處的一個(gè)例子。許多其他情況發(fā)生，其中推斷的前置條件或推斷的后置條件表明程序員選擇的算法顯然是錯(cuò)誤的，給定例程的要求。

靜態(tài)分析器可以通過使用一種巧妙的技術(shù)來(lái)推斷例程的前置條件和后置條件，該技術(shù)首先假設(shè)例程的輸入可以采用任何可能的值，然后通過消除可能導(dǎo)致的輸入值或輸入組合繼續(xù)進(jìn)行執(zhí)行期間的運(yùn)行時(shí)故障。一旦分析器到達(dá)例程的末尾，剩余的不會(huì)導(dǎo)致運(yùn)行時(shí)失敗的值代表了唯一可以始終安全地傳遞給例程的值，因此代表了例程的有效前提條件。后置條件是通過獲取滿足前置條件的輸入值集并計(jì)算它們?yōu)槔痰妮敵錾傻闹导瘉?lái)確定的。

有條件的先決條件

這種推斷合同的技術(shù)對(duì)于簡(jiǎn)單的直線例程非常有效，但不能捕獲具有在某些但不是所有調(diào)用上執(zhí)行的代碼的例程的完整故事。對(duì)于這些，我們需要考慮條件前置條件，即僅適用于通過例程的某些路徑的前置條件。這是一個(gè)示例，說明了條件前置條件的必要性（圖 3）。

圖 3：條件前置條件示例。

此處分析器已推斷出在計(jì)算 Y +/- 1 時(shí)防止數(shù)值溢出的先決條件，但它需要為通過例程的兩條路徑提供不同的先決條件。它通過發(fā)出條件前置條件來(lái)處理這個(gè)問題，其形式為“不或者?！斑@相當(dāng)于蘊(yùn)涵” ? ?！?在分析典型的可重用庫(kù)時(shí)，條件前置條件非常重要，因此能夠捕獲適用前置條件的條件對(duì)于對(duì)庫(kù)或其他可重用子系統(tǒng)進(jìn)行精確的自下而上靜態(tài)分析至關(guān)重要。

記錄關(guān)于未分析代碼的假設(shè)

分析庫(kù)或子系統(tǒng)時(shí)出現(xiàn)的另一個(gè)問題是它們通常依賴于其他較低級(jí)別的庫(kù)或子系統(tǒng)，并且希望相對(duì)獨(dú)立于它可能依賴的庫(kù)來(lái)分析一個(gè)庫(kù)。這為高級(jí)靜態(tài)分析器帶來(lái)了不同的挑戰(zhàn)，即處理從正在分析的代碼到當(dāng)前分析中未包含的代碼的調(diào)用。當(dāng)調(diào)用發(fā)生在當(dāng)前分析中包含的較低級(jí)別的例程上時(shí)，自下而上的分析方法為被調(diào)用的例程提供推斷的前置條件和后置條件，從而能夠?qū)^高級(jí)別的例程進(jìn)行進(jìn)一步分析。當(dāng)被調(diào)用的例程不在當(dāng)前分析中時(shí)，一種不同的方法是合適的——即，靜態(tài)分析工具可以跟蹤這個(gè)未經(jīng)分析的例程返回的值是如何使用的，并指出正在分析的例程中對(duì)這個(gè)未經(jīng)分析的代碼進(jìn)行了哪些假設(shè)。例如，如果對(duì)返回指針的例程進(jìn)行調(diào)用，并且調(diào)用例程立即取消引用該指針而沒有首先檢查它是否為空，則顯然假定此未經(jīng)分析的例程返回的指針是非空的（在例如，調(diào)用發(fā)生在第 12 行，由 @12 表示，圖 4）。

圖 4：調(diào)用未分析代碼的假設(shè)示例。

類似地，調(diào)用代碼可能會(huì)對(duì)數(shù)字返回值的值范圍或更復(fù)雜的返回對(duì)象的初始化狀態(tài)做出假設(shè)。通過顯式記錄調(diào)用代碼的所有此類假設(shè)，分析器可以讓庫(kù)實(shí)現(xiàn)者更深入地了解對(duì)較低級(jí)別庫(kù)的期望。然后可以將這些假設(shè)與低級(jí)庫(kù)的實(shí)際行為進(jìn)行比較，以驗(yàn)證低級(jí)庫(kù)是否被正確使用。

靜態(tài)分析工具的重要性

隨著靜態(tài)分析工具的使用成為軟件開發(fā)過程中不可或缺的一部分，這些工具的功能可以決定獲得的整體價(jià)值。成熟的軟件組織一直致力于以庫(kù)或子系統(tǒng)的形式創(chuàng)建可重用的軟件，因?yàn)楸娝苤w生產(chǎn)力的關(guān)鍵在于為每個(gè)應(yīng)用程序編寫更少的新代碼。高級(jí)靜態(tài)分析工具可以通過直接分析庫(kù)或子系統(tǒng)來(lái)幫助測(cè)試可重用組件的可重用性和穩(wěn)健性這一具有挑戰(zhàn)性的任務(wù)，而無(wú)需創(chuàng)建完整的可執(zhí)行程序可能需要的驅(qū)動(dòng)程序、線束或存根。這些工具可以通過自下而上的方式實(shí)現(xiàn)這一目標(biāo)，首先從可重用組件的葉例程開始，然后以前提條件、后置條件和假設(shè)的形式推斷人類可讀的信息。通過這樣做，它們使庫(kù)或子系統(tǒng)開發(fā)人員能夠準(zhǔn)確了解組件的構(gòu)建行為，而無(wú)需開發(fā)擴(kuò)展的動(dòng)態(tài)測(cè)試套件。

審核編輯：郭婷