DARPA(美國國防部高級研究計劃局)有個HACMS項目，即“高可信軍事網(wǎng)絡(luò)系統(tǒng)”(High-Assurance Cyber Military Systems) ，開發(fā)的主要是“formal verification”技術(shù)。而其項目目標(biāo)就是讓黑客難以入侵到諸如無人機、軍事指揮控制網(wǎng)絡(luò)系統(tǒng)中。
互聯(lián)網(wǎng)鼻祖DARPA(美國國防部高級研究計劃局)
如今我們每天都會使用互聯(lián)網(wǎng)，而你是否考慮過網(wǎng)絡(luò)是由誰發(fā)明的呢?
因特網(wǎng)的發(fā)明最初的用戶群并非普通人，而是國家軍事機構(gòu)，而我們用的因特網(wǎng)是后來轉(zhuǎn)變出來的。如果說到因特網(wǎng)的發(fā)明者不得不提到美國的一個神奇的機構(gòu)：美國國防部高級研究計劃局(DARPA)。DARPA成立于美蘇冷戰(zhàn) 的Dwight David Eisenhower(艾森豪威爾，34任總統(tǒng) )任期內(nèi)，目的是為美國開發(fā)尖端技術(shù)。
DARPA隸屬于五角大樓，是美國國防部一個非常特殊的部門。半個世紀(jì)以來，DARPA都對我們的生活產(chǎn)生了巨大影響。我們現(xiàn)在熟知的因特網(wǎng)、隱身技術(shù)、移動GPS等都是來自于DARPA這個部門。
我們都已經(jīng)知道因特網(wǎng)是DARPA研發(fā)出的，而網(wǎng)絡(luò)黑客也是因這項技術(shù)衍生出的。技術(shù)和互聯(lián)網(wǎng)的迅速崛起成為安全漏洞頻發(fā)的借口，對于高級黑客而言，入侵復(fù)雜的系統(tǒng)就如同小孩過家家。脆弱的系統(tǒng)和技能先進的黑客日益威脅著用戶的安全。如今，DARPA表示自己正在在“防黑客”電腦系統(tǒng)上做出技術(shù)努力，這個項目被稱為HACMS(高可信軍事網(wǎng)絡(luò)系統(tǒng))。
據(jù)悉，DARPA邀請了一批“從良”黑客參與測試，HACMS在研發(fā)過程中讓 這些白帽子黑客肆意入侵系統(tǒng)，他們展示了多種方法，可以輕松破解沒有安裝HACMS的系統(tǒng)和網(wǎng)絡(luò);但是在嘗試入侵安裝了HACMS的系統(tǒng)時，沒有一個人成功。 而這項技術(shù)目前已經(jīng)開始被諸如醫(yī)療設(shè)備等民用領(lǐng)域付諸實踐，并且在Github上公布了源代碼 。
嘗試攻擊“小鳥”無人直升機
去年夏天，亞利桑那州某黑客團隊嘗試控制波音的“小鳥”(Little Bird)無人軍事直升機。該黑客團隊一開始就被授權(quán)了“小鳥”計算機系統(tǒng)的一部分訪問權(quán)限。 他們要做的就是入侵“小鳥”的機載飛行控制計算機，進而控制整架直升機——這對他們而言原本就不應(yīng)該是什么難事。
但是作為HACMS項目的一部分，事情當(dāng)然不會如此簡單。 DARPA的工程師們?yōu)?ldquo;小鳥”開發(fā)了一種新的安全機制：一個無法被攻占的軟件系統(tǒng)。
DARPA給了該黑客團隊6周時間，該團隊始終沒能攻破“小鳥”無人軍事直升機計算機系統(tǒng)的。這其中還需要考慮到，在攻擊之前，黑客團隊就有一定的訪問權(quán)限，即便如此也仍舊不行。
高可靠性軍事網(wǎng)絡(luò)系統(tǒng)(HACMS)項目發(fā)起人、美國塔夫斯大學(xué)計算機科學(xué)教授 Kathleen Fisher 表示：
“黑客們無法以任何方式擴大控制并干擾機器運行。這一結(jié)果讓美國國防部高級研究計劃局非常高興，他們說現(xiàn)在終于能用這一技術(shù)來保護核心計算機系統(tǒng)了。”
“小鳥”無人軍事直升機計算機部署的新系統(tǒng)使用的技術(shù)為形式驗證(formal verification) ，它的代碼就像數(shù)學(xué)證明一樣可靠。每一個證明在邏輯上都承接上一個證明 。一個這樣的程序可以像證明數(shù)學(xué)定理一樣，無論如何測試都一定會得到正確的結(jié)果。
微軟研究院研究形式驗證和安全的研究員 Bryan Parno 表示：
“你寫下的數(shù)學(xué)公式就是用來描述程序行為的，再利用一些證明檢查器來檢查 證明的正確性。”
整個過程包括，反復(fù)檢查代碼是否遵守預(yù)定義形式規(guī)范(formal specification)，這里的形式規(guī)范定義了程序要做什么。
打個比方，比如你要給無人駕駛汽車編寫一個把你送到百貨商店的計算機程序，你需要定義讓汽車實現(xiàn)這一目的的動作：汽車可以左轉(zhuǎn)或右轉(zhuǎn)、剎車或加速、啟動或停車。最終，你的程序就是為了實現(xiàn)這一目的而對基本操作進行的合理組合，要求是把你送到百貨商店而不是機場。
HACMS團隊就是將這一區(qū)塊化的軟件安裝到了“小鳥”無人軍事直升機上。在和黑客團隊的較量中，他們先讓黑客們可以訪問某一次要功能如攝像頭的代碼，但黑客們肯定會被困住，因為這經(jīng)過了數(shù)學(xué)證明。Kathleen Fisher 說道：
“我們用機器從數(shù)學(xué)上證明了紅方肯定無法突破這一代碼塊，因此他們無法突破也就很順理成章了。結(jié)果與定理一致，也很好確認(rèn)。”
在“小鳥”無人軍事直升機上測試后，DARPA還開始將formal verification技術(shù)應(yīng)用到其他軍事技術(shù)上，比如衛(wèi)星和無人駕駛載重卡車。現(xiàn)在，不僅是國防組織(如 DARPA)一直致力于形式驗證技術(shù)，就連微軟、亞馬遜等科技公司也在不斷加注投資，進行相關(guān)產(chǎn)品的研究。
微軟研究院的軟件工程師們已經(jīng)在進行兩個雄心勃勃的形式驗證項目。第一個項目名為 Everest，旨在打造經(jīng)過形式驗證的 HTTPS 協(xié)議。第二個項目則是為擁有復(fù)雜物聯(lián)網(wǎng)系統(tǒng)的無人機開發(fā)一個正式的規(guī)范。
隨著越來越多的關(guān)鍵社會職能轉(zhuǎn)移到網(wǎng)上，研究人員們對形式軟件驗證技術(shù)的興趣也越來越濃厚。在以前，計算機還只是局限于家里和辦公室，程序漏洞最多也就是讓使用者感到不便。但現(xiàn)在，程序漏洞可能會導(dǎo)致巨大危害，任何具備相關(guān)知識的人都能利用同一漏洞自由地進出某個計算機系統(tǒng)。同時，物聯(lián)網(wǎng)也在短短幾年間實現(xiàn)爆發(fā)式增長，智能家居、智慧城市正逐漸滲透入我們的生活，這將勢必為黑客入侵提供更多場所。期待此次技術(shù)開發(fā)能改變目前嚴(yán)峻的網(wǎng)絡(luò)局勢。
京公網(wǎng)安備 11010502049343號