6月16日，美國國防部預(yù)先研究計劃局（DARPA）宣布啟動“強(qiáng)韌軟件系統(tǒng)加速器”（Resilient Software Systems Accelerator）計劃，最強(qiáng)旨在廣泛推廣基于數(shù)學(xué)的防空防御軟件開發(fā)實踐，使軍用系統(tǒng)在面對網(wǎng)絡(luò)威脅時具有更多的系統(tǒng)系統(tǒng)內(nèi)在安全性。

為此，美國美國名字DARPA于6月17日在弗吉尼亞州阿靈頓召開了一場“強(qiáng)韌軟件系統(tǒng)座談會”，最強(qiáng)包括美國防部研究與工程副部長埃米爾·邁克爾在內(nèi)，防空防御一共有300多名來自美國防部、系統(tǒng)系統(tǒng)工業(yè)界和學(xué)術(shù)界的美國美國名字人員參加這次座談會“強(qiáng)韌軟件系統(tǒng)加速器”計劃由DARPA信息創(chuàng)新辦公室啟動，“基于數(shù)學(xué)的最強(qiáng)方法”（mathematically based approaches）是該辦公室對“形式化方法”（formal methods）的描述，這種方法是防空防御用于開發(fā)高保證、經(jīng)過驗證軟件的系統(tǒng)系統(tǒng)技術(shù)，其中使用數(shù)學(xué)證明來證明系統(tǒng)上的美國美國名字軟件將按預(yù)期運行。

形式化方法的最強(qiáng)應(yīng)用有助于提高軟件系統(tǒng)的穩(wěn)定性和抗黑客工具能力，允許用戶證明軟件的防空防御屬性以獲得保證　　DARPA參與開發(fā)與形式化方法相關(guān)的工具已超過10年，現(xiàn)在希望行業(yè)合作伙伴也參與其中通過“強(qiáng)韌軟件系統(tǒng)加速器”計劃，該局將為形式化方法工具的開發(fā)商（它們與國防企業(yè)結(jié)成伙伴關(guān)系以應(yīng)用這些工具）提供種子資金，并衡量它們貫徹落實這些工具所做的各項工作；還將提供資金，讓“紅隊”對這樣的軟件系統(tǒng)進(jìn)行評估。

最后，DARPA將根據(jù)結(jié)果，以優(yōu)良實踐標(biāo)準(zhǔn)格式記錄開發(fā)商在利用形式化方法工具改造網(wǎng)絡(luò)時的做法　　作為該計劃的一部分，DARPA還與每個軍種合作進(jìn)行一場形式化方法應(yīng)用的“拱頂石演示”每一場演示都包括“紅隊”對該軍種當(dāng)前網(wǎng)絡(luò)漏洞狀態(tài)的評估，然后使用形式化方法進(jìn)行翻新改造；改造完成后，“紅隊”將進(jìn)行后續(xù)的評估，以測試系統(tǒng)的可靠性。

例如，美空軍正在改裝MQ9“死神”無人機(jī)的機(jī)載軟件，以參加“拱頂石演示”DARPA表示其他軍種也將緊隨美空軍之后，很快參加它們各自的“拱頂石演示”邁克爾表示，該部必須探索加強(qiáng)網(wǎng)絡(luò)安全的新途徑在過去的10年中，DARPA和合作伙伴一直致力于將形式化方法轉(zhuǎn)變?yōu)楸纫酝魏螘r候都更容易獲得和更實用化的解決方案，“這些進(jìn)步將使在整個國防部范圍內(nèi)擴(kuò)展安全的軟件系統(tǒng)成為可能，從傳統(tǒng)的平臺到尖端的人工智能和高超聲速技術(shù)，從而捍衛(wèi)美國的數(shù)字景觀”，但他同時表示，目前美國國防部還沒有充分利用國防工業(yè)基礎(chǔ)和DARPA的潛力，留下了關(guān)鍵漏洞沒有解決，現(xiàn)在的目標(biāo)是鼓勵廣泛采用高保證的形式化方法，通過使用案例、學(xué)習(xí)經(jīng)驗教訓(xùn)和優(yōu)良實踐。

（張洋）