知名編程語言 Ada 與 SPARK 所屬公司 AdaCore 發布了一則關于 NVIDIA 的案例，案例顯示：NVIDIA 的產品運行著許多經過正式驗證的 SPARK 代碼，NVIDIA 安全團隊正嘗試使用 SPARK 語言取代 C 語言，來實現一些對安全較為敏感的應用程序或組件。

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

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

編輯：黃飛