DARPA力推‘形式化方法’，欲把網絡災難滅於萌芽

美國國防高級研究計劃局（DARPA）的官員已開始敦促國防部管理人員利用閒置的美國國防高級研究計劃局（DARPA）網絡安全工具，這些工具旨在預先防範關鍵項目中的黑客攻擊和意外事故。

DARPA信息創新辦公室主任凱瑟琳·費舍爾（Kathleen Fisher）表示，近年來發生的一系列備受矚目的事件凸顯出國防官員在面對所造成的損害時存在某種消極性。她說，由於認爲系統無法避免由軟件漏洞引發的災難性網絡事件，國防部往往側重於事後補救措施。

不過，她本月早些時候在該機構位於弗吉尼亞州阿靈頓的總部舉行的演示日活動上表示，用於構建更具韌性軟件的主動式工具已經存在於五角大樓的應對措施庫中。

費舍爾說：“我們有許多存在這類漏洞的關鍵任務系統，而我們學會的應對方式是在它們遭到攻擊之後，在我們認識到‘好吧，這個漏洞很嚴重’之後，纔去修復它。我們在事後花費數十億美元來解決這些問題。”

2017年，俄羅斯對烏克蘭發動了一次如今被稱爲‘諾珀蒂亞’（NotPetya）的網絡攻擊。

雖然此次攻擊針對的是烏克蘭的電力基礎設施，但最終擴散到國外，影響了整個歐洲的基礎設施和企業，包括丹麥物流公司馬士基（Maersk），該公司承擔着全球約20%的集裝箱航運業務。在7分鐘內，攻擊摧毀了該公司的5萬臺計算機，幾乎破壞了追蹤其集裝箱船的活動目錄系統。該公司估計損失約爲3億美元。

7年後，即2024年7月，來自安全公司CrowdStrike的故障軟件使數百萬政府和私營部門的計算機掉線，導致數千個商業航班延誤，醫療程序取消，這一全球性故障的一部分。雖然干擾範圍很廣，但根本原因被確定爲一次意外——一個通過常規更新傳播的軟件故障。

像這樣的事件——無論是惡意的還是意外的——近年來變得更常見。費舍爾（Fisher）認爲，這些事件凸顯了關鍵基礎設施中令人擔憂的軟件漏洞。作爲迴應，美國國防部和更廣泛的美國政府在解決軟件漏洞方面產生了一種“習得性無助”的感覺。

在過去10到15年裡，美國國防高級研究計劃局（DARPA）已經證明，一種名爲“形式化方法”的軟件設計方法可以在這些漏洞被編碼錯誤或攻擊利用之前解決它們。不是僅僅在軟件代碼寫完後通過測試來驗證其安全性，而是通過嚴格的數學分析來設計軟件，在構建之前和構建期間驗證其性能。

美國國防部高級研究計劃局（DARPA）開發的一些工具已經被納入美國國防部（DOD）的在冊項目，但應用範圍有限。現在，隨着人們對軍事武器系統網絡安全的擔憂日益加劇，該機構正試圖讓國防採辦部門意識到這些解決方案是存在的並且可供使用。

費舍爾（Fisher）說：“我們可以想象一個沒有這些軟件漏洞的世界，在這個世界裡，我們可以消除在整個國防部的那種習得性無助感，我們可以迅速保護關鍵系統……並且我們可以打造一個可持續的形式化方法工具的生態體系，這些工具是現成的，可供人們使用。”

美國國防部高級研究計劃局（DARPA）的演示

美國國防部高級研究計劃局（DARPA）早期的一個展示形式化方法的實用價值的項目是“高保證網絡軍事系統（High - Assurance Cyber Military Systems effort，簡稱HACMS）”項目。該項目於2012年至2016年開展，並以兩次演示作爲結束，第一次使用了一架小型四軸無人機，然後在2017年使用了波音公司的自主直升機“無人小鳥（Unmanned Little Bird）”。

據柯林斯宇航公司（Collins Aerospace）的首席研究員達倫·科弗（Darren Cofer）稱，在第二次演示期間，一隊紅方黑客試圖入侵飛機，但未能成功。柯林斯宇航公司的前身羅克韋爾·柯林斯（Rockwell Collins）是HACMS項目的承包商。

“在HACMS項目中，我們證明了形式化方法可用於消除真實飛機嵌入式系統中的重要安全漏洞，”科弗在DARPA演示日期間說道。

從那之後，該機構開展了其他幾項工作，以提高形式化方法在國防部平臺上的可用性。其中一個名爲“安全文檔”（SafeDocs）的項目用來解決解析器（一種能把數據轉換成可用格式的軟件工具）裡的漏洞。另一項工作“可靠微補丁”（Assured Micro Patching，簡稱AMP）提供了一種在無源代碼的情況下修復軟件漏洞的方法，並確保修復本身不會造成更多損害。

這些工具都已小規模地應用到國防部的項目，並且DARPA還有其他幾個正在進行的項目，旨在進一步改進形式化方法。費舍爾指出，由於問題尚未完全解決，項目往往會推遲採用這些方法。但DARPA認爲，現在這些技術有更廣泛應用的潛力——既能保護舊平臺上已有的國防部軟件，也能爲未來系統設計軟件。

“我們有大量技術已經成熟，可以投入使用，我們現在就應該着手轉化並使用這些技術，因爲這將極大提高我們系統的安全性，”她說道。“我們不能等到解決了所有問題纔去使用現有的技術。”

傳播消息

國防部採用這些工具的速度和範圍取決於諸多因素，包括軍事部門內部的資金情況和優先順序。

爲了幫助傳播消息並解決採用這些工具的障礙，美國國防高級研究計劃局（DARPA）去年開展了頂點（Capstone）計劃。通過與負責研究和工程的國防部副部長以及作戰試驗與鑑定主任合作，該機構正在與各軍種合作，以確定可從形式化方法中受益的平臺。

DARPA正在提供一些相應資金來使這些工具可用，據項目經理史蒂夫·庫恩（Steve Kuhn）稱，預計將在5月前確定這些平臺。一旦頂點計劃被選中，該機構將幫助識別並修復其中的軟件漏洞，並總結經驗教訓，編入最佳實踐指南，所有計劃都將能夠獲取該指南。

庫恩說，DARPA希望該指南將有助於國防部計劃辦公室瞭解適應性強的軟件工具是如何被應用的，並提供有助於實施的資源。

庫恩說：“我們一直在開展的戰略的一部分實際上是一個採用計劃，該計劃將這些適應性強（可靠的）的軟件工具帶給我們的國防工業基地、我們的合作伙伴以及軍隊本身。我們不會解決所有問題，但我們真的能弄清楚將這些工具推廣給大衆所需要的條件嗎？”