知名編程語言 Ada 與 SPARK 所屬公司 AdaCore 發(fā)布了一則關(guān)于 NVIDIA 的案例，案例顯示：NVIDIA 的產(chǎn)品運(yùn)行著許多經(jīng)過正式驗(yàn)證的 SPARK 代碼，NVIDIA 安全團(tuán)隊(duì)正嘗試使用 SPARK 語言取代 C 語言，來實(shí)現(xiàn)一些對安全較為敏感的應(yīng)用程序或組件。

SPARK 是一種編程語言和一組驗(yàn)證工具，旨在滿足高保證軟件開發(fā)的需求。SPARK 基于 Ada 語言，它既對 ada 語言進(jìn)行子集化以刪除無法驗(yàn)證的功能，又?jǐn)U展了合約和方面的系統(tǒng)，進(jìn)一步支持模塊化、形式化驗(yàn)證。 SPARK 語言一般用于可預(yù)測和高度可靠操作的系統(tǒng)中的高完整性軟件，它有助于開發(fā)需要高安全性或業(yè)務(wù)完整性的應(yīng)用程序。

早在 2018 年， NVIDIA 就針對 “從 C 轉(zhuǎn)換為 SPARK” 這一過程進(jìn)行了概念驗(yàn)證 (POC) 練習(xí)，在三個月內(nèi)將兩個低級別的安全敏感應(yīng)用從 C 轉(zhuǎn)換為 SPARK 代碼。在對投資回報進(jìn)行評估后，該團(tuán)隊(duì)得出結(jié)論：隨著新技術(shù)的增加（培訓(xùn)、實(shí)驗(yàn)、新工具等），應(yīng)用程序安全性和驗(yàn)證效率也得到了提高，轉(zhuǎn)換為 SPARK 代碼的兩個應(yīng)用程序?qū)崿F(xiàn)了安全穩(wěn)健性的重大改進(jìn)。 （有關(guān)評估結(jié)果的更多信息，請參閱 NVIDIA 的進(jìn)攻性安全研究 D3FC0N 演講：https://blog.adacore.com/when-formal-verification-with-spark-is-the-strongest-link）。 由于 POC 的結(jié)果證明從 C 轉(zhuǎn)換為 SPARK 的可行性，SPARK 語言的使用在 NVIDIA 內(nèi)迅速傳播開來?，F(xiàn)在已有超過 50 名受過專業(yè)培訓(xùn)的開發(fā)人員使用 SPARK 中實(shí)現(xiàn)了許多組件，且許多 NVIDIA 產(chǎn)品現(xiàn)在都附帶 SPARK 組件。 另外，SPARK 有一項(xiàng)很有趣的特性：它可以代碼本身中指定程序需求的能力，并使用相關(guān)的工具集來確保代碼實(shí)現(xiàn)地功能與它的需求相匹配。NVIDIA 更多地使用 SPARK 來實(shí)現(xiàn)最關(guān)鍵的組件，確保它沒有運(yùn)行時錯誤，并確保它符合受信任根應(yīng)用程序的規(guī)范。 此外，完整的案例研究涵蓋了一些有趣的主題，比如與 C 相比，SPARK 的性能 “根本沒有看到任何性能差異 “。

編輯：黃飛