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

【文/ 觀察者網(wǎng)專欄作者 徐令予】

5月12日早上醒來，全球人終于明白互聯(lián)網(wǎng)上不全是音樂和鮮花。一個(gè)名為“想哭”的勒索病毒襲擊了全球上百個(gè)國家和地區(qū)使用微軟操作系統(tǒng)的電腦，原來網(wǎng)上的江湖波譎云詭、危機(jī)四伏。

怎樣打造攻不破、摧不垮、毒不侵的電腦，怎樣才能還太平與網(wǎng)民，科學(xué)家們?yōu)榱司W(wǎng)絡(luò)維穩(wěn)真是操碎了心。

據(jù)《量子雜志》報(bào)道，2015年的夏天，一群黑客企圖控制一架名為“小鳥”（LITTLE BIRD H-6U）的軍用無人直升機(jī)，那是在亞利桑那州的波音工廠為美軍特種作戰(zhàn)任務(wù)研制的裝備。當(dāng)時(shí)黑客作了這樣的安排：他們開始操作時(shí)已經(jīng)可以訪問無人機(jī)電腦系統(tǒng)的一部分。從那里開始，他們只需入侵“小鳥”的機(jī)上飛行控制電腦，無人機(jī)就是他們的了。

LITTLE BIRD H-6U 軍用無人直升機(jī)

當(dāng)項(xiàng)目開始時(shí)，黑客團(tuán)隊(duì)可以像侵入家庭Wi-Fi一樣輕松地接管直升機(jī)，易如囊中探物。但在隨后的幾個(gè)月中，美國國防高級(jí)研究計(jì)劃局（DARPA）的工程師們開發(fā)并實(shí)施了一種新型的安全機(jī)制，一種百毒不侵的軟件系統(tǒng)。“小鳥”的計(jì)算機(jī)系統(tǒng)的關(guān)鍵部分是現(xiàn)有技術(shù)完全無法入侵的，其代碼的正確可靠能像數(shù)學(xué)一樣被證明。盡管把無人機(jī)的計(jì)算機(jī)網(wǎng)絡(luò)完全開放，黑客團(tuán)隊(duì)一直無法掌握“小鳥”的控制系統(tǒng)，他們經(jīng)過連續(xù)六周的攻擊而不能越雷池于一步，黑客以徹底失敗而告終。

“黑客無法以任何方式突破系統(tǒng)和破壞正常的飛行。”塔夫茨大學(xué)計(jì)算機(jī)科學(xué)教授和高保證網(wǎng)絡(luò)軍事系統(tǒng)（HACMS）項(xiàng)目的主管凱瑟琳·費(fèi)舍爾指出，“這個(gè)結(jié)果使所有的DARPA人員信服，我們實(shí)際上可以在我們關(guān)心的系統(tǒng)中使用這種技術(shù)。”

壓制黑客的技術(shù)是一種稱為軟件編程的形式化方法[1]。過去對傳統(tǒng)計(jì)算機(jī)代碼的評(píng)估主要是檢查它是否在各種情況下都能正常工作，而形式化軟件驗(yàn)證如同數(shù)學(xué)證明：程序中每個(gè)語句的前后都遵循嚴(yán)格的邏輯關(guān)系，整個(gè)程序測試的確定性就像數(shù)學(xué)家證明定理一樣。

大多數(shù)傳統(tǒng)計(jì)算機(jī)的程序是如何工作的呢？設(shè)想為無人駕駛車編寫一個(gè)計(jì)算機(jī)程序。在操作層面上，你可以定義汽車在行程中各種必須的操作行為，它們可以是左轉(zhuǎn)、右轉(zhuǎn)、制動(dòng)或加速。而程序則是按照適當(dāng)順序排列的基本操作的匯編，以確保讓你到達(dá)雜貨店而不是機(jī)場。

長期以來，對此類程序的評(píng)估和驗(yàn)收的傳統(tǒng)方法是進(jìn)行簡單的測試。把各種起始點(diǎn)和目標(biāo)的位置輸入程序，檢查在程序控制下的無人駕駛車輛是否正確到達(dá)預(yù)定目標(biāo)。這種測試方法在大多數(shù)情況下可以滿足我們的要求。但是這種測試法不能保證軟件將百分之百地正常工作，因?yàn)楦鞣N輸入和輸出的組合無窮無盡，現(xiàn)實(shí)環(huán)境中總會(huì)有罕見的情況發(fā)生，總會(huì)有不能預(yù)測到的“角落”，從而導(dǎo)致程序出錯(cuò)。

在程序的運(yùn)行中，這些出錯(cuò)和故障當(dāng)然要不得，但更大的危害是可能引起計(jì)算機(jī)內(nèi)存緩沖區(qū)溢出，為黑客攻擊系統(tǒng)提供了跳板，軟件中的任何一個(gè)缺陷都可能就是系統(tǒng)安全的漏洞。

再舉一個(gè)例子，考慮對一串?dāng)?shù)字排序的程序。程序員對排序程序的定義可能會(huì)寫成這樣：

對于列表中的每個(gè)元素j，確保元素j≤j+1

然而，這種定義——確保列表中的每個(gè)元素小于或等于其后面的元素——隱含了一個(gè)錯(cuò)誤：程序員假定輸出總是輸入的一種置換。也就是說，對于輸入列表[7,3,5]，她期望程序?qū)⑤敵鯷3,5,7]以滿足排序定義。然而，列表[2,5,7]也同樣滿足定義，它是一個(gè)排序列表，但它不是我們希望的排序列表。嚴(yán)格地說，除了排序還必須確保輸出與輸入的元素集合完全一致，這在以往的程序設(shè)計(jì)中常常被忽視。

換句話說，將一個(gè)程序應(yīng)該做些什么的想法轉(zhuǎn)化為一個(gè)正式的規(guī)范，同時(shí)又要排除對此可能產(chǎn)生的各種不正確的解釋，這常常是十分困難的。上面的例子只是一個(gè)簡單的排序程序。現(xiàn)在想象一下比排序更抽象的程序，比如保護(hù)密碼，這在數(shù)學(xué)上又是什么意思？ 它可能涉及為保護(hù)密碼進(jìn)行數(shù)學(xué)描述，或者對加密算法的安全性作出定義。這些問題提岀并不太難，但找到正確簡單的方案卻十分不易。

使用形式邏輯規(guī)則來指導(dǎo)程序設(shè)計(jì)起源于上世紀(jì)七十年代。1973年10月，艾茲格·迪科斯徹(Edsger Dijkstra)提出了創(chuàng)建無錯(cuò)代碼的想法。在會(huì)議期間他住在酒店，半夜三更產(chǎn)生了讓編程更加數(shù)學(xué)化的靈感。他在后來回憶道：“我的大腦在燃燒，凌晨2:30離開了我的床，伏案書寫了一個(gè)多小時(shí)。”這些材料成為了他于1976年完成的“編程規(guī)則”這部著作的基礎(chǔ)，他因此獲得了圖靈獎(jiǎng)——計(jì)算機(jī)科學(xué)的最高榮譽(yù)。

但是將正確性證明納入計(jì)算機(jī)程序編制一直沒有得到廣泛的應(yīng)用，計(jì)算機(jī)科學(xué)的發(fā)展畢竟不能單純依靠愿望。主要是因?yàn)殚L年以來，使用形式邏輯規(guī)則來指定程序的功能，即便并非不可能，似乎也是不實(shí)際的。包含形式驗(yàn)證信息的程序可能是相同的傳統(tǒng)程序的五倍長度。這種編程的額外負(fù)擔(dān)可以通過專用的編程語言和輔助程序減輕一些，但那些旨在幫助軟件工程師的工具在上世紀(jì)七八十年代并不存在。

即使輔助工具有所改進(jìn)，推廣程序驗(yàn)證的更大障礙是：沒有人確定是否有必要。雖然一些專家一再強(qiáng)調(diào)編碼小錯(cuò)誤會(huì)導(dǎo)致災(zāi)難性的后果，但是吃瓜群眾看到的是計(jì)算機(jī)程序大多數(shù)情況下工作正常。當(dāng)然，有時(shí)候會(huì)丟失數(shù)據(jù)或藍(lán)屏死機(jī)，但是天又塌不下來，讓文秘重新輸入數(shù)據(jù)或者偶爾重新啟動(dòng)計(jì)算機(jī)又有什么大不了。

到了20世紀(jì)90年代，程序驗(yàn)證的鼻祖也開始懷疑它的用處了。圖靈獎(jiǎng)得主Tony Hoare——“霍爾邏輯”的創(chuàng)始人——也承認(rèn)軟件編程的形式化方法可能既勞民傷財(cái)又無的放矢。他在1995年寫道：十年前，形式化方法的研究人員（而我是其中最為錯(cuò)誤的一位）預(yù)測，軟件業(yè)界將會(huì)懷著感激之情擁抱形式化方法帶來的成果，而事實(shí)證明：我們企圖要解決的問題實(shí)質(zhì)上對世界并沒有產(chǎn)生多大的影響。

但是互聯(lián)網(wǎng)改變了一切，如同航空旅行的普及導(dǎo)致傳染病的飛速傳播，當(dāng)計(jì)算機(jī)都互相聯(lián)接在一起，一臺(tái)計(jì)算機(jī)的編碼錯(cuò)誤可能會(huì)被黑客利用，導(dǎo)致成千上萬計(jì)算機(jī)被非法入侵控制，甚至使網(wǎng)絡(luò)局部癱瘓。至少2017年5月12日全世界嘗到了苦頭。

當(dāng)研究人員開始了解互聯(lián)網(wǎng)對計(jì)算機(jī)安全的威脅時(shí)，程序驗(yàn)證技術(shù)終于有了用武之地。首先，研究人員在基于形式化方法的編程技術(shù)上取得了巨大進(jìn)步：改進(jìn)了支持形式化方法的Coq和Isabelle等驗(yàn)證輔助程序；開發(fā)新的邏輯系統(tǒng)，為計(jì)算機(jī)對代碼的推理提供了全新的框架；并且改進(jìn)了所謂的“操作語義”——本質(zhì)上是一種具有確切詞匯用以表達(dá)程序究竟應(yīng)該做什么的語言。