整理 | 朱珂欣 責編 | 張紅月
近日，在 AdaCore 上一篇關於 NVIDIA 正嘗試使用 SPARK 語言取代 C 語言的案例研究，引發了大家關注。
本次案例研究聚焦於 NVIDIA 面對網路安全問題時存在的挑戰，並嘗試使用 SPARK 語言實現一些對安全較為敏感的應用程序或元件。同時，還說明了 NVIDIA 在關鍵元件開發中加大對 SPARK 的使用的方法，以及 NVIDIA 通過採用 SPARK 獲得的好處及對潛在 SPARK 採用者的建議。
圖源：AdaCore 官網截圖
安全性幾乎無法通過測試來驗證
NVIDIA 軟體安全副總裁 Daniel Rohrer 曾坦言：「安全性是幾乎無法通過測試來驗證的。「隨後，NVIDIA 安全團隊開始尋找方案來應對日益惡劣的網路安全環境，並質疑過往的軟體開發和驗證策略，也意識到面向測試的軟體驗證，根本無法確保安全性。
Daniel Rohrer 還表示：「希望強調可證明性作為首選的驗證方法，而不是測試。」
值得慶幸的是，可以從數學的角度，依託數學計算和形式證明程式碼的行為完全符合其規範，也因此使 NVIDIA 開始研究了 SPARK 。
從 C 轉換為 SPARK 的原因：安全性和穩健性得到重大改進
SPARK 作為一種程式語言和一套驗證工具，可以滿足高保證軟體開發的需求。SPARK 基於 Ada，既能對語言進行了子集化以刪除無法驗證的功能，又能擴展合同和方面的系統以支持模組化的形式驗證。
早在 2018 年， NVIDIA 就進行了概念驗證 （POC） 演習。在短短三個月內，兩個安全級別較低的應用程序上實現了從 C 到 SPARK 的遷移。
在對投資回報評估後， NVIDIA 安全團隊得出結論：伴隨著培訓、實驗、新工具等新技術的提升，應用程序安全性和驗證效率的也得到了提高。兩個應用程序，在安全性和穩健性兩個方面的重大改進。
由於 POC 的結果驗證了最初的策略，SPARK 的使用也在 NVIDIA 內部迅速傳播。現有的 50 名經過專業培養的開發人員在 SPARK 中實現了大量元件，許多 NVIDIA 產品現在都附帶了 SPARK 元件。
網友：性能與 C 相比，沒有看到任何性能差異？
然而，在 Hacker News 上，關於 NVIDIA 安全團隊正嘗試用 SPARK 語言取代 C 語言的案例，也引發了大家激烈的討論：
「相信如果我們擺脫了 C 語言，所有軟體安全問題都會得到解決」；
「有許多 C 語言開發人員會堅持認為他們已經獲得了足夠的經驗，永遠不會編寫易受各種記憶體安全漏洞攻擊的程式碼」；
「性能與 C 相比，我根本沒有看到任何性能差異」。
未來，SPARK 還將給 NVIDIA 及其客戶提供哪些保證，我們拭目以待。
參考連結：
https://www.adacore.com/papers/nvidia-adoption-of-spark-new-era-in-security-critical-software-development
https://blog.adacore.com/nvidia-security-team-what-if-we-just-stopped-using-c
https://news.ycombinator.com/item?id=33504206
