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

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

偏差是漏洞之源

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

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

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

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

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

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

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

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

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

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

關(guān)于作者

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