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

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

偏差是漏洞之源

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

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

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

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

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

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

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

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

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

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

關于作者

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