符號(hào)執(zhí)行技術(shù)可識(shí)別安全關(guān)鍵代碼中的漏洞

多核處理器在安全關(guān)鍵型應(yīng)用中越來(lái)越受歡迎，因?yàn)樗鼈兲峁┝孙@著的價(jià)格和性能改進(jìn)。但是，為多核硬件編寫(xiě)多線(xiàn)程應(yīng)用程序是出了名的困難，并可能導(dǎo)致災(zāi)難性故障。下面描述了用于識(shí)別問(wèn)題（包括數(shù)據(jù)爭(zhēng)用）的符號(hào)執(zhí)行技術(shù)？最常見(jiàn)的并發(fā)缺陷之一？以及靜態(tài)分析如何幫助開(kāi)發(fā)人員找到并消除它們。

最大化性能對(duì)于軍事嵌入式系統(tǒng)尤為重要，因?yàn)樵谌找鏀?shù)字化的戰(zhàn)場(chǎng)上，人們?cè)絹?lái)越需要保持低成本，同時(shí)滿(mǎn)足連接要求。隨著制造商達(dá)到小型化和集成度提高所能達(dá)到的極限，提高性能的最佳方法是使用多核處理器。

缺點(diǎn)是，為了充分利用并行執(zhí)行的許多內(nèi)核，必須將軟件編寫(xiě)為本質(zhì)上是多線(xiàn)程的。為單核處理器編寫(xiě)為單線(xiàn)程的軟件在多核處理器上執(zhí)行時(shí)將實(shí)現(xiàn)很少或沒(méi)有性能優(yōu)勢(shì)：必須重寫(xiě)或調(diào)整它以使用多線(xiàn)程。關(guān)鍵挑戰(zhàn)是盡可能保持核心繁忙，同時(shí)確保它們正確協(xié)調(diào)對(duì)共享資源的訪(fǎng)問(wèn)。不幸的是，編寫(xiě)這樣的代碼比編寫(xiě)單線(xiàn)程代碼要困難得多。當(dāng)存在死鎖或爭(zhēng)用條件等缺陷時(shí)，它們可能會(huì)以難以診斷的方式表現(xiàn)出來(lái)。查找和消除并發(fā) bug 的傳統(tǒng)技術(shù)可能無(wú)效。

并發(fā)錯(cuò)誤如此困難的核心原因之一是，當(dāng)線(xiàn)程執(zhí)行時(shí)，線(xiàn)程中的事件可以通過(guò)多種方式交錯(cuò)。隨著線(xiàn)程或指令數(shù)量的增加，交錯(cuò)的數(shù)量呈指數(shù)級(jí)增長(zhǎng)。如果線(xiàn)程 A 執(zhí)行 M 條指令，線(xiàn)程 B 執(zhí)行 N 條指令，則兩個(gè)線(xiàn)程可能存在 N+MCN 交錯(cuò)。例如，給定兩個(gè)平凡的線(xiàn)程，每個(gè)線(xiàn)程有 10 條指令，這些指令有 184，756 個(gè)可能的交錯(cuò)。即使使用非常小的程序，很明顯也幾乎不可能測(cè)試所有可能的組合。其次，即使可以識(shí)別導(dǎo)致故障的單個(gè)交錯(cuò)，也很難設(shè)置使用該特定交錯(cuò)的可重復(fù)測(cè)試用例，因?yàn)榫€(xiàn)程調(diào)度實(shí)際上是不確定的。因此，調(diào)試并發(fā)程序可能非常昂貴且耗時(shí)。爭(zhēng)用條件是一類(lèi)并發(fā)缺陷，很容易意外引入，并且很難通過(guò)常規(guī)測(cè)試消除。但是，程序員可以使用一些技術(shù)來(lái)查找和刪除它們。

潛在的災(zāi)難性故障

與單線(xiàn)程代碼相比，并發(fā)程序中可能會(huì)出現(xiàn)全新的缺陷類(lèi)別，包括死鎖、饑餓和爭(zhēng)用條件。這些缺陷主要會(huì)導(dǎo)致開(kāi)發(fā)過(guò)程中難以診斷和消除的神秘故障。我們合作過(guò)的一家航空電子制造商花了兩個(gè)人年的時(shí)間應(yīng)用傳統(tǒng)的調(diào)試技術(shù)，努力找到間歇性軟件故障的根本原因，結(jié)果證明這是一種競(jìng)爭(zhēng)條件。有時(shí)后果可能很可怕——有史以來(lái)最臭名昭著的兩個(gè)軟件故障是由競(jìng)爭(zhēng)條件引起的。Therac-25放射治療機(jī)具有導(dǎo)致幾名患者死亡的種族條件。同樣，2003 年?yáng)|北停電因競(jìng)爭(zhēng)條件而加劇，導(dǎo)致誤導(dǎo)性信息被傳達(dá)給技術(shù)人員。

有幾種不同類(lèi)型的競(jìng)爭(zhēng)條件。最常見(jiàn)和最隱蔽的形式之一 - 數(shù)據(jù)競(jìng)爭(zhēng) - 是涉及訪(fǎng)問(wèn)內(nèi)存位置的競(jìng)爭(zhēng)條件類(lèi)。

當(dāng)有兩個(gè)或多個(gè)執(zhí)行線(xiàn)程訪(fǎng)問(wèn)共享內(nèi)存位置，至少一個(gè)線(xiàn)程正在更改該位置的數(shù)據(jù)，并且沒(méi)有用于協(xié)調(diào)訪(fǎng)問(wèn)的顯式機(jī)制時(shí)，就會(huì)發(fā)生數(shù)據(jù)爭(zhēng)用。如果發(fā)生數(shù)據(jù)爭(zhēng)用，則可能會(huì)使程序處于不一致?tīng)顟B(tài)。

考慮控制襟翼位置的航空電子代碼。在正常情況下，襟翼處于飛行控制軟件指示的位置，但飛行員可以通過(guò)按下控制面板上的按鈕來(lái)覆蓋該位置，在這種情況下，使用手動(dòng)設(shè)置的位置。為了簡(jiǎn)單起見(jiàn)，假設(shè)程序中有兩個(gè)線(xiàn)程：一個(gè)控制翻蓋，另一個(gè)監(jiān)視控制面板上元素的位置。還有一個(gè)名為 is_manual 的共享布爾變量，它對(duì)手動(dòng)覆蓋是否設(shè)置進(jìn)行編碼。擺動(dòng)位置螺紋檢查is_manual的值，如果為 true，則相應(yīng)地設(shè)置位置。控制面板線(xiàn)程偵聽(tīng)按鈕按下事件，如果按下替代按鈕，它將is_manual設(shè)置為 true。圖 1 顯示了為實(shí)現(xiàn)此規(guī)范而可能編寫(xiě)的代碼。此代碼可能在大多數(shù)情況下都有效;但是，由于 is_manual 變量對(duì)兩個(gè)線(xiàn)程共享的狀態(tài)進(jìn)行編碼，因此它容易受到數(shù)據(jù)爭(zhēng)用的影響，因?yàn)閷?duì)它的訪(fǎng)問(wèn)不受鎖保護(hù)。如果在飛行員按下超控按鈕的確切時(shí)間執(zhí)行襟翼定位代碼，則程序可能會(huì)進(jìn)入不一致的狀態(tài)，并且將使用錯(cuò)誤的襟翼位置。圖 2 顯示了這種情況是如何發(fā)生的。

圖1：訪(fǎng)問(wèn)共享變量的兩個(gè)線(xiàn)程中的代碼

圖2：導(dǎo)致數(shù)據(jù)爭(zhēng)用的指令交錯(cuò)

這個(gè)例子巧妙地說(shuō)明了數(shù)據(jù)爭(zhēng)用的一個(gè)屬性，這使得它們難以診斷：損壞的癥狀可能只有在數(shù)據(jù)爭(zhēng)用發(fā)生很久之后才能觀(guān)察到。在這種情況下，只有當(dāng)飛行員注意到飛機(jī)沒(méi)有按預(yù)期響應(yīng)時(shí)，才會(huì)注意到使用錯(cuò)誤的襟翼位置的事實(shí)。

人們普遍認(rèn)為，數(shù)據(jù)競(jìng)爭(zhēng)的某些實(shí)例是良性的，可以容忍。然而，現(xiàn)在毫無(wú)疑問(wèn)，這很少是真的。C 標(biāo)準(zhǔn)［4］ 明確指出，編譯器可以假設(shè)沒(méi)有數(shù)據(jù)爭(zhēng)用，因此優(yōu)化器可以并且確實(shí)進(jìn)行了對(duì)提高單線(xiàn)程代碼性能有效的轉(zhuǎn)換，但在存在明顯良性的競(jìng)爭(zhēng)條件時(shí)引入了錯(cuò)誤。這些都是微妙的影響——即使是經(jīng)驗(yàn)豐富的程序員也經(jīng)常對(duì)它們感到驚訝。（有關(guān)完整的解釋和幾個(gè)令人信服的示例，請(qǐng)參閱參考文獻(xiàn) ［1］。因此，為了實(shí)現(xiàn)高水平的保證并避免災(zāi)難性故障，查找并刪除所有數(shù)據(jù)爭(zhēng)用非常重要。

消除并發(fā)缺陷

鑒于并發(fā)缺陷，尤其是數(shù)據(jù)爭(zhēng)用，風(fēng)險(xiǎn)很大，因此使用多種技術(shù)來(lái)消除它們非常重要。由于不確定性，傳統(tǒng)的動(dòng)態(tài)測(cè)試不太適合發(fā)現(xiàn)許多并發(fā)缺陷。通過(guò)測(cè)試數(shù)百次的程序以后可能會(huì)在具有完全相同輸入的相同環(huán)境中失敗，因?yàn)樵撳e(cuò)誤可能對(duì)時(shí)間非常敏感。尋求高保證的工程師如果要消除并發(fā)缺陷，就必須轉(zhuǎn)向其他技術(shù)。

靜態(tài)分析工具提供了一種查找此類(lèi)錯(cuò)誤的方法。測(cè)試和靜態(tài)分析之間的主要區(qū)別在于，它針對(duì)給定的一組輸入測(cè)試程序的特定執(zhí)行，而靜態(tài)分析查找適用于所有可能執(zhí)行和所有輸入的屬性。（在實(shí)踐中，靜態(tài)分析工具進(jìn)行近似以獲得可接受的性能和精度，因此達(dá)不到這個(gè)理想模型。盡管如此，它們確實(shí)涵蓋了比傳統(tǒng)測(cè)試更多的情況。

粗略地說(shuō)，靜態(tài)分析工具的工作原理是創(chuàng)建程序模型并對(duì)該模型進(jìn)行符號(hào)執(zhí)行，在此過(guò)程中查找錯(cuò)誤條件。例如，GrammaTech的CodeSonar靜態(tài)分析工具通過(guò)創(chuàng)建哪些鎖由哪些線(xiàn)程持有的映射，并通過(guò)推理可能導(dǎo)致對(duì)共享變量的不同步訪(fǎng)問(wèn)的可能交錯(cuò)來(lái)查找數(shù)據(jù)競(jìng)爭(zhēng)。使用類(lèi)似的技術(shù)發(fā)現(xiàn)死鎖和其他并發(fā)缺陷（包括鎖管理不善）。

自定義并發(fā)構(gòu)造：案例研究

當(dāng)程序使用標(biāo)準(zhǔn)方法來(lái)管理并發(fā)時(shí)，標(biāo)準(zhǔn)缺陷檢測(cè)技術(shù)最有用。大多數(shù)工具識(shí)別并推理標(biāo)準(zhǔn)庫(kù)（如POSIX線(xiàn)程庫(kù)）或?qū)Ｓ?a target="_blank">接口（如VxWorks）的特殊屬性。但是，許多系統(tǒng)使用自定義技術(shù)來(lái)管理并發(fā)性。

例如，與我們合作的另一家制造商在使用自定義搶占式多線(xiàn)程軟件接口的平臺(tái)上構(gòu)建了一個(gè)安全關(guān)鍵型設(shè)備。在此設(shè)計(jì)中，一個(gè)關(guān)鍵約束是，必須使用適當(dāng)?shù)谋Ｗo(hù)構(gòu)造保護(hù)可以從多個(gè)優(yōu)先級(jí)線(xiàn)程訪(fǎng)問(wèn)的所有數(shù)據(jù)實(shí)例。在使用靜態(tài)分析之前，驗(yàn)證是否遵守此約束需要花費(fèi)人工月的手動(dòng)分析時(shí)間。為了降低成本，他們通過(guò)轉(zhuǎn)向靜態(tài)分析來(lái)尋求解決方案?，F(xiàn)代高級(jí)靜態(tài)分析工具的一個(gè)重要特性是它們是可擴(kuò)展的：它們提供了一個(gè)帶有抽象的 API，可以方便地實(shí)現(xiàn)自定義靜態(tài)分析算法。使用 CodeSonar 的 API，他們能夠編寫(xiě)一個(gè)解決方案，該解決方案利用現(xiàn)有分析核心使用的算法來(lái)查找代碼中違反設(shè)計(jì)約束的位置。生成的工具作為插件實(shí)現(xiàn)，能夠自動(dòng)查找違反關(guān)鍵約束的情況，所有這些都只需一小部分成本和比以前少得多的時(shí)間。

多核權(quán)衡

轉(zhuǎn)向多核處理器設(shè)計(jì)有令人信服的理由，但風(fēng)險(xiǎn)在于這樣做可能會(huì)在軟件中引入并發(fā)缺陷。這些很容易引入 - 即使是看似無(wú)辜的代碼也可能隱藏令人討厭的多線(xiàn)程錯(cuò)誤 - 并且眾所周知，當(dāng)它們發(fā)生時(shí)很難診斷和消除。僅靠傳統(tǒng)的測(cè)試技術(shù)不足以確保高質(zhì)量的軟件，這主要是因?yàn)楦叨鹊姆谴_定性。使用使用符號(hào)執(zhí)行的高級(jí)靜態(tài)分析工具是一種可以提供幫助的方法，因?yàn)榇祟?lèi)工具可以推理代碼執(zhí)行的所有可能方式。這些工具可以在使用標(biāo)準(zhǔn)多線(xiàn)程庫(kù)的代碼中發(fā)現(xiàn)數(shù)據(jù)爭(zhēng)用和死鎖等缺陷，甚至可以適應(yīng)使用非標(biāo)準(zhǔn)并發(fā)構(gòu)造的設(shè)計(jì)。

審核編輯：郭婷