久久久久精品免费福利电影,国产又黄又大又粗视频,A级毛片免费播放无码,人人妻人人爽人人澡欧美一区

今日，形式化方法的研究人員的目標(biāo)也變得更為現(xiàn)實(shí)。在20世紀(jì)70年代和80年代初期，這些研究人員試圖創(chuàng)建可以驗(yàn)證的計(jì)算機(jī)系統(tǒng)，一個(gè)從硬件電路到軟件程序的完整系統(tǒng)。如今大多數(shù)研究人員側(cè)重于驗(yàn)證系統(tǒng)中較小但特別脆弱或關(guān)鍵的部分，如操作系統(tǒng)和加密協(xié)議。

“我們并不聲稱我們將證明整個(gè)系統(tǒng)是正確的，每一點(diǎn)都百分之百的可靠，從上至下直到電子電路的水平。”微軟研究院的計(jì)算機(jī)科學(xué)家Jeannette Wing指出：“這些做法是荒謬的。我們更清楚我們能做什么，不能做什么。”

HACMS項(xiàng)目顯示了如何通過計(jì)算機(jī)系統(tǒng)分區(qū)隔離以達(dá)到總體的安全保證。該項(xiàng)目的第一個(gè)目標(biāo)是創(chuàng)造一個(gè)無法入侵的娛樂級四軸飛行器。運(yùn)行該飛行器的商業(yè)軟件是一個(gè)整體，這意味著如果攻擊者突破一點(diǎn)，他就可以控制整個(gè)軟件。在接下來的兩年中，HACMS團(tuán)隊(duì)將四軸飛行器的任務(wù)控制計(jì)算機(jī)中的代碼分區(qū)隔離。

該團(tuán)隊(duì)還重新制定了軟件架構(gòu)，使用了被HACMS項(xiàng)目經(jīng)理凱瑟琳·費(fèi)舍爾稱之為“高保證構(gòu)建塊”的技術(shù)，這是一種讓程序員證明其代碼正確無誤的工具。其中一個(gè)經(jīng)過驗(yàn)證的構(gòu)建塊可以保證在某個(gè)分區(qū)內(nèi)具有訪問權(quán)限的操作者無法升級越界進(jìn)入其他分區(qū)。

高保證網(wǎng)絡(luò)軍事系統(tǒng)（HACMS）項(xiàng)目主管 凱瑟琳·費(fèi)舍爾

在四軸飛行器取得經(jīng)驗(yàn)之后，HACMS程序員在“小鳥”軍用無人直升機(jī)上安裝了這個(gè)分區(qū)隔離軟件。在測試中，他們提供了黑客團(tuán)隊(duì)進(jìn)入無人直升機(jī)的某一分區(qū)，例如攝相機(jī)控制分區(qū)，但并不是核心功能分區(qū)。在無情的數(shù)學(xué)公式面前，黑客被死死地卡住在一個(gè)分區(qū)中無法亂說亂動(dòng)。“他們以機(jī)器檢查的方式證明，黑客不能脫離分區(qū)，這毫不奇怪，他們就是不能。”凱瑟琳·費(fèi)舍爾說：“這與定理是一致的，試驗(yàn)也證明了這一點(diǎn)。”

為了幫助非專業(yè)人員了解分區(qū)隔離技術(shù)的基本原理，讓我們回顧一下上世紀(jì)中國絕密軍工廠的管理，這類軍工廠不僅門衛(wèi)森嚴(yán)，而且內(nèi)部分成密級不同的獨(dú)立車間，人員不得互相來往。每個(gè)產(chǎn)品又必經(jīng)多個(gè)車間加工生產(chǎn)。一個(gè)間諜（黑客）進(jìn)入工廠并混進(jìn)某個(gè)車間已經(jīng)非常不易，他下足工夫取得車間主任的信任或許能獲得某種特權(quán)，但他最多只能在一個(gè)車間中活動(dòng)，他對整個(gè)產(chǎn)品的認(rèn)識(shí)和控制是十分有限的，因?yàn)槿魏卧噲D跨越車間界限的行為會(huì)被嚴(yán)格的限制，而且其真實(shí)身份會(huì)立刻受到特別調(diào)查。計(jì)算機(jī)系統(tǒng)的分區(qū)隔離技術(shù)與絕密軍工廠的管理方式有著某種程度的類同。

近年來，計(jì)算機(jī)硬件性能的飛速進(jìn)步也為計(jì)算機(jī)系統(tǒng)的分區(qū)隔離技術(shù)提供了物質(zhì)基礎(chǔ)，今日強(qiáng)大的中央處理器能力和海量的內(nèi)存空間完全可以支持系統(tǒng)的分區(qū)運(yùn)行管理。

在“小鳥”無人直升機(jī)測試之后的一年，DARPA正努力將HACMS項(xiàng)目的工具和技術(shù)應(yīng)用于其他軍事技術(shù)領(lǐng)域，如衛(wèi)星和無人自動(dòng)駕駛車隊(duì)。

為了捍衛(wèi)互聯(lián)網(wǎng)的安全，形式化方法的研究人員正在推動(dòng)更加雄心勃勃的計(jì)劃。DeepSpec合作項(xiàng)目力圖將過去十年中已經(jīng)成功通過形式化驗(yàn)證的許多小型模塊進(jìn)行組合，以構(gòu)建一個(gè)經(jīng)過完全形式化驗(yàn)證的端到端系統(tǒng)，如Web服務(wù)器。

在微軟的研究部門，軟件工程師正在進(jìn)行兩項(xiàng)雄心勃勃的形式化驗(yàn)證項(xiàng)目。第一個(gè)名為珠穆朗瑪峰，這是創(chuàng)建一個(gè)經(jīng)過形式化驗(yàn)證的HTTPS版本，新的協(xié)議可以有效地保護(hù)被稱之為“互聯(lián)網(wǎng)的阿喀琉斯之踵”的網(wǎng)絡(luò)瀏覽器。第二個(gè)是為復(fù)雜的網(wǎng)絡(luò)物理系統(tǒng)（如無人機(jī)）制定形式化驗(yàn)證規(guī)范，這里的挑戰(zhàn)可能更為嚴(yán)峻。無人機(jī)飛行涉及到機(jī)器學(xué)習(xí)，以及在連續(xù)的環(huán)境數(shù)據(jù)流中進(jìn)行概率決定，如何對不確定性進(jìn)行推理并制定形式化規(guī)范是極大的挑戰(zhàn)。但在過去的十年中，軟件工程的形式化方法已經(jīng)有了長足的進(jìn)步，從事該項(xiàng)研究的科學(xué)家們對未來持有謹(jǐn)慎樂觀的態(tài)度。

[1]形式化方法(Formal Method)是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的計(jì)算機(jī)系統(tǒng)研究方法，該知識(shí)體系中有6個(gè)主要領(lǐng)域，分別為:

① 基礎(chǔ)(Foundations);

② 形式化規(guī)格(Formal specification paradigms);

③ 正確性驗(yàn)證及演算(Correctness, verification and calculation);

④ 形式化語義(Formal semantics);

⑤ 可執(zhí)行規(guī)范支持(Support for executable specification);

⑥ 其他(Other Topics)。

本文系觀察者網(wǎng)獨(dú)家稿件，文章內(nèi)容純屬作者個(gè)人觀點(diǎn)，不代表平臺(tái)觀點(diǎn)，未經(jīng)授權(quán)，不得轉(zhuǎn)載，否則將追究法律責(zé)任。關(guān)注觀察者網(wǎng)微信guanchacn，每日閱讀趣味文章。