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

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

偏差是漏洞之源

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

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

業務邏輯驗證的重要性

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

圖： 國家信息安全漏洞共享平臺收集整理信息系統高危漏洞數量

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

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

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

左移已是開發標配

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

關于作者

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