重一步邏輯驗證，省百步漏洞補(bǔ)缺

近年來，隨著人工智能和物聯(lián)網(wǎng)等新興科技的廣泛應(yīng)用，各種“智能”、“自動”的科技服務(wù)已經(jīng)滲透到人們生活的方方面面。在這些服務(wù)的背后，是無數(shù)個應(yīng)運(yùn)而生的軟件和應(yīng)用程序在支撐。遺憾的是，軟件行業(yè)的大繁榮并沒有帶來軟件代碼質(zhì)量的明顯提升。Forrester研究數(shù)據(jù)顯示，82%的漏洞來源于應(yīng)用程序。與軟件規(guī)模、數(shù)量的井噴一同出現(xiàn)的，是軟件漏洞的大爆發(fā)，以及隨之而來的隱私泄漏、網(wǎng)絡(luò)欺詐等漏洞“后遺癥”。

面對如此巨大的風(fēng)險，企業(yè)內(nèi)部的軟件開發(fā)團(tuán)隊通過踐行代碼審查、各種測試以及代碼分析以期減少代碼中的漏洞從而提高代碼質(zhì)量。然而，這些方法往往也只能確保“磚塊”可用，由這些“磚塊”搭建起來的建筑是否符合設(shè)計、是否安全可靠就很難驗證了。由此，用以檢測軟件設(shè)計或功能實(shí)現(xiàn)上的缺陷或偏差的“業(yè)務(wù)邏輯驗證”就應(yīng)運(yùn)而生了。

偏差是漏洞之源

一款軟件從設(shè)計到實(shí)現(xiàn)，往往會被拆分成許多小的功能模塊，分別實(shí)現(xiàn)后再組裝整合。大量簡單的業(yè)務(wù)邏輯被用于構(gòu)建復(fù)雜而又豐富的業(yè)務(wù)邏輯，設(shè)計或?qū)崿F(xiàn)上的偏差或缺陷都會導(dǎo)致漏洞的產(chǎn)生。實(shí)踐中，團(tuán)隊在拆解實(shí)現(xiàn)時，即使頂層描述十分清晰，將文字表達(dá)翻譯為編程語言，將籠統(tǒng)的語言描述到細(xì)節(jié)的代碼實(shí)現(xiàn)，其中可能產(chǎn)生的偏差不是代碼審查、各種測試和代碼分析能夠輕易發(fā)現(xiàn)的。同時，如果開發(fā)團(tuán)隊在不同模塊接口之間的功能描述不夠清晰、實(shí)現(xiàn)存在偏差，程序一旦運(yùn)行，問題就會浮出水面。尤其是在增強(qiáng)軟件功能、對原有功能改造以及新加入開發(fā)人員時，發(fā)生類似狀況的風(fēng)險也會上升。

此外，開發(fā)人員對第三方或者庫函數(shù)的理解偏差，也會導(dǎo)致漏洞的發(fā)生。如谷歌瀏覽器Chrome的0day漏洞cve-2019-5786就是由于開發(fā)者對std::move()的理解不全面而造成的。對新標(biāo)準(zhǔn)、新接口的嘗鮮心理普遍存在于軟件開發(fā)者中，但在真正使用這些新事物之前，開發(fā)者自身需要投入時間精力，去學(xué)習(xí)并真正理解它。而且，并不是所有的新標(biāo)準(zhǔn)、新接口的設(shè)計都合理，如std::move()，其功能在一個編譯器的優(yōu)化流程中就能自動實(shí)現(xiàn)。通過開放一個接口，讓開發(fā)者來嘗試實(shí)現(xiàn)編譯器優(yōu)化未能完成的工作，同時提供了一個可能導(dǎo)致大量漏洞的來源，其目的和意義讓人費(fèi)解。

業(yè)務(wù)邏輯驗證的重要性

業(yè)務(wù)邏輯驗證，這個步驟可以幫助企業(yè)在被認(rèn)可的合理范圍內(nèi)交付軟件，而不是提供一個擁有過多或過少功能的半成品。功能過少的彌補(bǔ)方法相對簡單，延長交付時間進(jìn)行添加即可；而功能過多，則有可能提供了通往用戶隱私數(shù)據(jù)的入口，從而導(dǎo)致不可挽回的嚴(yán)重后果，這類例子比比皆是。

圖： 國家信息安全漏洞共享平臺收集整理信息系統(tǒng)高危漏洞數(shù)量

在智能家居普及的今天，黑客利用監(jiān)控設(shè)備的漏洞將監(jiān)控片段上傳至互聯(lián)網(wǎng)，造成用戶隱私泄露，甚至財產(chǎn)損失的事件屢見不鮮。據(jù)CNCERT披露的《中國互聯(lián)網(wǎng)絡(luò)發(fā)展?fàn)顩r統(tǒng)計報告》顯示，2020年信息系統(tǒng)的高位漏洞數(shù)量同比2019年增長52.2%。諸多例子都在警醒我們軟件安全問題就潛伏在身邊。

驗證業(yè)務(wù)邏輯，就是從語言描述轉(zhuǎn)換成掃描工具能夠認(rèn)識的檢測原語，并證明其成立的一個過程。傳統(tǒng)的驗證方法是將語言描述轉(zhuǎn)換為嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)表達(dá)，證明過程繁復(fù)且困難，不僅用人門檻極高，且費(fèi)時費(fèi)力。而且一旦頂層的語言描述發(fā)生變化，整個推導(dǎo)過程又需要從頭開始。在傳統(tǒng)形式化方法的實(shí)踐中，為了驗證一行軟件源代碼，驗證過程中需要寫17行的代碼去驗證。此外，傳統(tǒng)形式化方法在證明失敗的地點(diǎn)分析問題的癥結(jié)所在并不容易，往往需要沿證明路徑倒推檢查。一般的開發(fā)者并不具備輕易掌握傳統(tǒng)方法的能力。

為提供高效的業(yè)務(wù)邏輯驗證服務(wù)，最好的方法是在靜態(tài)代碼掃碼工具上提供接口，讓用戶將其業(yè)務(wù)邏輯映射到對應(yīng)的開發(fā)語言上，再由機(jī)器快速高效的完成驗證工作。即，如果有某語言編寫的一段程序，又有它的一段語言描述，只要代碼掃碼工具提供了相同編程語言的接口，就可將語言描述的業(yè)務(wù)邏輯映射到的驗證引擎可以識別的接口函數(shù)上，對軟件進(jìn)行掃描，查看真正的實(shí)現(xiàn)是否符合了語言描述中所要實(shí)現(xiàn)的功能。全程由機(jī)器執(zhí)行的工具不僅擁有更快的速度、更高的效率，其對使用者的水平要求也更低，更能直觀地幫助客戶了解軟件開發(fā)的具體癥結(jié)所在。在實(shí)踐中，80%的客戶的定制化驗證需求是可以通過有限的掃描引擎描述接口由客戶自行實(shí)現(xiàn)的，而另外20%的客戶的特定的需求，則需要花費(fèi)大量精力去幫助解決。

左移已是開發(fā)標(biāo)配

軟件生命周期包括：設(shè)計、實(shí)現(xiàn)、測試以及交付使用。早發(fā)現(xiàn)問題早解決，彌補(bǔ)的成本也隨之而下降。在用戶開始使用時才暴露出來的錯誤，其修復(fù)的人力和時間成本最高，遠(yuǎn)超過開發(fā)時就發(fā)現(xiàn)并修復(fù)的成本。與其在用戶使用后才報錯，不如在內(nèi)部開發(fā)的早期就踐行業(yè)務(wù)邏輯驗證，確保 “我做的是客戶想要的”，因為一個軟件到實(shí)現(xiàn)功能之后再重新設(shè)計改造，其時間、人力成本都會很高。

關(guān)于作者

李隆博士專注于代碼驗證基礎(chǔ)架構(gòu)，現(xiàn)任鑒釋科技首席科學(xué)家。李隆于2008年在中科大獲得計算機(jī)軟件和理論博士學(xué)位。其學(xué)術(shù)研究集中在應(yīng)用基于程序設(shè)計語言理論的技術(shù)構(gòu)建可靠高效的軟件上，并發(fā)表了數(shù)篇期刊和會議論文。畢業(yè)后，李隆博士加入了三星電子，從事高級技術(shù)小組的統(tǒng)計機(jī)器翻譯工作。并于2010年加入HP編譯器團(tuán)隊，從事HP Non-Stop編譯器后端和SDK。