AdaCore 和 Nvidia 已經(jīng)為 Ada 和 SPARK 編程語(yǔ)言開(kāi)發(fā)了一個(gè)開(kāi)源參考流程，用于安全關(guān)鍵汽車(chē)軟件，特別是自動(dòng)駕駛汽車(chē)。

該流程能夠在 Nvidia DriveOS 操作系統(tǒng)上更快地開(kāi)發(fā) ISO26262 軟件。Nvidia 使用 SPARK 開(kāi)發(fā)了 DriveOS，并為其 DRIVE AGX 硬件上的應(yīng)用程序開(kāi)發(fā)了認(rèn)證流程。

基于 Ampere GPU 架構(gòu)和 ARM Cortex A78AE 內(nèi)核的 AGX-Orin 芯片，正被包括沃爾沃、梅賽德斯-奔馳、捷豹路虎、通用汽車(chē)、極氪和吉利以及現(xiàn)在豐田（世界上最大的汽車(chē)制造商）等汽車(chē)制造商使用。

基于 Blackwell 架構(gòu)、搭載 NeoverseV3AE 核心的 AGX-Thor 芯片，預(yù)計(jì)今年晚些時(shí)候開(kāi)始用于自動(dòng)駕駛。中國(guó)電動(dòng)汽車(chē)制造商比亞迪、自動(dòng)駕駛巴士制造商 WeRide、沃爾沃、 卡車(chē)制造商 Aurora、大陸集團(tuán)和理想汽車(chē)都在使用這款芯片。

DriveOS 芯片在 1 月份通過(guò)了 TUD SUD 的 ASIL-D 認(rèn)證，采用了名為 Halos 的 AI 安全框架。

“自動(dòng)駕駛的時(shí)代已經(jīng)到來(lái)，我們將與人工智能在制造、企業(yè)以及汽車(chē)模擬和設(shè)計(jì)方面合作，”英偉達(dá) CEO 黃仁勛表示?！拔覀円呀?jīng)從事自動(dòng)駕駛汽車(chē)研究超過(guò)十年了?！?/p>

參考流程是向前邁進(jìn)的關(guān)鍵一步，包括符合汽車(chē)認(rèn)證標(biāo)準(zhǔn) ISO-26262 最高完整性級(jí)別的軟件組件。使用 SPARK 需要建立一種開(kāi)發(fā)流程，該流程利用 Ada 形式語(yǔ)言的正式方法和其 SPARK 子集的其他安全特性。

AdaCore 和 Nvidia 決定將參考流程作為一個(gè)開(kāi)放且不斷發(fā)展的文檔發(fā)布，使整個(gè)行業(yè)能夠采用 Ada 和 SPARK。

“這對(duì)從事軟件定義汽車(chē)開(kāi)發(fā)的開(kāi)發(fā)者來(lái)說(shuō)是一個(gè)重要的轉(zhuǎn)折點(diǎn)，”AdaCore 首席產(chǎn)品與營(yíng)收官 Quentin Ochem 告訴 eeNews Europe。

“獨(dú)特之處在于 Nvidia 的方法。通過(guò)采用 Ada 和 SPARK 并公開(kāi)發(fā)布其 ISO 26262 合規(guī)性文檔，他們正在重塑這些責(zé)任的處理方式。Nvidia 沒(méi)有讓開(kāi)發(fā)者負(fù)擔(dān)隔離的、抽象的合規(guī)活動(dòng)，而是將這些考慮因素盡可能接近開(kāi)發(fā)者的主要工件：代碼本身。這符合將驗(yàn)證、可追溯性和需求直接集成到開(kāi)發(fā)流程中的趨勢(shì)，使正確性成為代碼庫(kù)的特性，而不僅僅是單獨(dú)的過(guò)程?！?/p>

“傳統(tǒng)上，開(kāi)發(fā)者不得不身兼數(shù)職——除了編寫(xiě)代碼，他們還常常發(fā)現(xiàn)自己承擔(dān)了 QA 工程師、驗(yàn)證工程師甚至需求工程師的責(zé)任，”他補(bǔ)充道。

“像汽車(chē)這樣的安全關(guān)鍵領(lǐng)域，受 ISO 26262 等標(biāo)準(zhǔn)的管轄，需要嚴(yán)格的可追溯性、正確性的證據(jù)和形式化保證——這些責(zé)任遠(yuǎn)遠(yuǎn)超出了傳統(tǒng)軟件工程的范圍?！?/p>

他還指出，英偉達(dá)決定開(kāi)源認(rèn)證工件是一個(gè)關(guān)鍵舉措。

“也很少見(jiàn)看到主要技術(shù)提供者如此程度地開(kāi)放其內(nèi)部安全認(rèn)證流程。英偉達(dá)的 ISO 26262 文檔可以即用型使用，這是一個(gè)大事——它為其他汽車(chē)軟件團(tuán)隊(duì)提供了一個(gè)具體、實(shí)用的起點(diǎn)。它降低了開(kāi)發(fā)者和公司構(gòu)建安全認(rèn)證車(chē)輛軟件的門(mén)檻，而無(wú)需重新發(fā)明輪子。”

ISO-26262 參考流程可在 nvidia.github.io/spark-process/ 上獲得，并且任何人都可以自由使用或定制這些語(yǔ)言。

ISO26262 流程

本文檔定義了一個(gè)基于 SPARK 的、符合 ISO-26262 標(biāo)準(zhǔn)的流程，用于開(kāi)發(fā)安全關(guān)鍵車(chē)輛軟件單元的子集，達(dá)到 ASIL D 級(jí)，并降低 ASIL 等級(jí)。

該流程專(zhuān)門(mén)適用于完全使用 Ada 編程語(yǔ)言開(kāi)發(fā)的軟件單元，但面向的是部分或全部 Ada 代碼符合 SPARK 子集的軟件單元。雖然該流程的一些元素，例如所需的 Ada 編譯器警告設(shè)置，可能適用于一般的安全關(guān)鍵 Ada 軟件開(kāi)發(fā)，但混合使用 Ada 與其他語(yǔ)言（如 C、C++或匯編語(yǔ)言）的軟件單元不能使用該流程進(jìn)行開(kāi)發(fā)。

該流程涵蓋了與語(yǔ)言子集、軟件單元設(shè)計(jì)、軟件單元實(shí)現(xiàn)以及軟件單元驗(yàn)證相關(guān)的 ISO 26262 要求和目標(biāo)。此外，該流程還涵蓋了與軟件接口規(guī)范中表達(dá)的安全要求相關(guān)的 ISO 26262 要求和目標(biāo)。

這個(gè)過(guò)程支持并行進(jìn)行形式化驗(yàn)證和非形式化驗(yàn)證。根據(jù)此過(guò)程開(kāi)發(fā)的單個(gè)軟件單元可以全部進(jìn)行形式化驗(yàn)證，全部進(jìn)行非形式化驗(yàn)證，或者部分進(jìn)行形式化驗(yàn)證和部分進(jìn)行非形式化驗(yàn)證。

“簡(jiǎn)而言之，這一舉措有助于消除開(kāi)發(fā)者對(duì)安全認(rèn)證的神秘感，并為更健壯和高效的軟件定義車(chē)輛架構(gòu)鋪平道路，”O(jiān)chem 說(shuō)。

采用一種新的編程語(yǔ)言涉及部署新環(huán)境、培訓(xùn)團(tuán)隊(duì)適應(yīng)新的形式化規(guī)范、調(diào)整編程模式以及其他許多問(wèn)題。然而，從流程的角度來(lái)看，編程語(yǔ)言在很大程度上是可以互換的，但 Ada 和 SPARK 則是一個(gè)不同的故事。

將其視為一種語(yǔ)言轉(zhuǎn)變是一種可能性，這無(wú)疑會(huì)在傳統(tǒng)的開(kāi)發(fā)過(guò)程中產(chǎn)生價(jià)值。然而，這會(huì)錯(cuò)失該技術(shù)帶來(lái)的關(guān)鍵機(jī)會(huì)，即能夠?qū)㈤_(kāi)發(fā)過(guò)程轉(zhuǎn)變?yōu)橐则?yàn)證驅(qū)動(dòng)的過(guò)程，從而以比傳統(tǒng)方法更嚴(yán)格和更具成本效益的方式展示軟件特性。

Ada 語(yǔ)義旨在最小化漏洞風(fēng)險(xiǎn)，并最大化直接定義在源代碼中的語(yǔ)義信息。SPARK 使用這些屬性來(lái)避免常見(jiàn)漏洞，并允許定義附加屬性以替代動(dòng)態(tài)測(cè)試進(jìn)行形式化驗(yàn)證。

在 SPARK 中，可以保證變量初始化、無(wú)緩沖區(qū)溢出、數(shù)據(jù)范圍等基本屬性，或者更一般地說(shuō)，避免出現(xiàn)防御性代碼，但它也提供了定義更高級(jí)要求的方法，這些要求可以以布爾斷言的形式表達(dá)，并且可以正式證明實(shí)現(xiàn)是正確的，而無(wú)需運(yùn)行任何測(cè)試。

以形式化驗(yàn)證為目標(biāo)的代碼開(kāi)發(fā)對(duì)開(kāi)發(fā)過(guò)程中的各個(gè)層面都有影響。以這種方式開(kāi)發(fā)軟件可能是一個(gè)漫長(zhǎng)的迭代過(guò)程，存在遺漏技術(shù)某些關(guān)鍵方面的風(fēng)險(xiǎn)。

參考流程旨在允許新采用者跳過(guò)這一點(diǎn)，并從已經(jīng)過(guò)當(dāng)局審查和行業(yè)實(shí)驗(yàn)的既定流程開(kāi)始。它不是用來(lái)“照搬不照”，而是作為適合每個(gè)組織具體情況的定制流程的起點(diǎn)。

然而 Nvidia 指出，該流程不包括軟件架構(gòu)設(shè)計(jì)規(guī)范，如何將現(xiàn)有的 C/C++軟件單元移植到基于 SPARK 的流程中，或并發(fā)性或軟件安全分析。