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

面對(duì)如此巨大的風(fēng)險(xiǎn)，企業(yè)內(nèi)部的軟件開發(fā)團(tuán)隊(duì)通過踐行代碼審查、各種測(cè)試以及代碼分析以期減少代碼中的漏洞從而提高代碼質(zhì)量。然而，這些方法往往也只能確?！按u塊”可用，由這些“磚塊”搭建起來的建筑是否符合設(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)后再組裝整合。大量簡單的業(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á)翻譯為編程語言，將籠統(tǒng)的語言描述到細(xì)節(jié)的代碼實(shí)現(xiàn)，其中可能產(chǎn)生的偏差不是代碼審查、各種測(cè)試和代碼分析能夠輕易發(fā)現(xiàn)的。同時(shí)，如果開發(fā)團(tuán)隊(duì)在不同模塊接口之間的功能描述不夠清晰、實(shí)現(xiàn)存在偏差，程序一旦運(yùn)行，問題就會(huì)浮出水面。尤其是在增強(qiáng)軟件功能、對(duì)原有功能改造以及新加入開發(fā)人員時(shí)，發(fā)生類似狀況的風(fēng)險(xiǎn)也會(huì)上升。

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

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

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

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

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

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

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

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

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

關(guān)于作者

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