NVIDIA 與 AdaCore 聯手利用 Ada 和 SPARK 程式語言來提高軟體的安全性。
軟體定義了我們的出行方式,從出行 app 和即時地圖,再到日漸增加的自動駕駛車,一行又一行的程式碼成為人們交通方式的基礎。
隨著這個軟體變得愈來愈複雜,發生人為失誤的可能性變得更高,也潛藏著更多安全方面的隱憂。
NVIDIA 將針對這個重要軟體的安全性,與開發驗證工具提供商 AdaCore 合作,以確保人們在使用它時能高枕無憂。我們將使用 Ada 和 SPARK 程式語言編寫部分韌體元素,企圖降低發生人為錯誤的可能性。
這兩種語言都有著極高的可靠性、穩健性和安全性,用它們來編寫程式,可以提高確認程式碼無任何錯誤及弱點的效率。
根據顧問公司 VDC Research 所進行的一項研究指出,更佳的軟體驗證過程可為航太與汽車等有著嚴格安全性、可靠性與安全標準的產業,省下近四成的成本和時間。
更容易找出缺失
Ada 內建多種功能,可在軟體生命週期的早期找出程式碼方面的缺失,降低發生人為錯誤的可能性,以及開發後需要進行其它測試和同儕審視等作業的時間。
Ada 的子集合 SPARK 能以數學方式證明使用該語言寫出的程式碼是否未存在任何錯誤,這個證明能訂定軟體應用程式的行為方式,還能判斷是否是照著該定義來執行,找出未瞧見的錯誤或漏洞。
在 NVIDIA 的硬體裡加入這些程式語言,便能將軟體發生故障或出現人為操弄的機會降至最低。可在開發週期裡以更短的時間、更快的速度進行驗證,進而減少浪費。
軟體定義的安全性
尤其是在汽車的自動化程度日漸升高的情況下,在 NVIDIA 的平台加入 Ada 和 SPARK 程式語言一事,有助於讓汽車安全性變得更完善。
該軟體必須經過相同的嚴格標準與專家評估作業,在它運行的硬體上證明一切功能安全無虞。使用這些語言進行驗證,把這個過程納入開發過程,創造出更流暢的審視週期。
NVIDIA 軟體安全部門副總裁 Daniel Rohrer 說:「自動駕駛車極為複雜,需要用到超越最高標準的精密軟體。我們十分期待 Ada 與 SPARK 能滿足此一商業生態體系的關鍵需求。」