Rust的安全系統編程

在編程語言設計中，兩種看似不可調和的需求之間存在著長期的緊張關系。
?安全。我們需要靜態地排除大類錯誤的強類型系統。我們想要自動內存管理。我們需要數據封裝，這樣我們就可以對對象的私有表示強制不變量，并確保它們不會被不受信任的代碼破壞。
控制。至少對于“系統編程”應用程序(如Web瀏覽器、操作系統或游戲引擎)來說，性能或資源約束是主要關注的問題，我們希望確定數據的字節級表示。我們希望使用低級編程技術優化程序的時間和空間使用。我們希望在需要的時候能夠接觸到“裸金屬”。
可悲的是，就像傳統智慧所說的，我們不可能擁有我們想要的一切。像Java這樣的語言為我們提供了強大的安全性，但這是以控制為代價的。因此，對于許多系統編程應用程序，唯一現實的選擇是使用像C或c++這樣的語言來提供對資源管理的細粒度控制。然而，這種控制需要付出高昂的代價。例如，微軟最近報告說，他們修復的70%的安全漏洞是由于內存安全違規造成的，而強類型系統恰恰排除了33種類型的漏洞。同樣，Mozilla報告說，他們在Firefox中發現的絕大多數關鍵bug都與內存有關如果有一種方法能做到兩全其美就好了:一種安全的系統編程語言……
進入生銹。由Mozilla贊助，并在過去十年中由一個大型的、多樣化的社區貢獻者積極開發，Rust支持許多常見的低級編程idi- oms和源自現代c++的api。然而，與c++不同的是，Rust使用一個強靜態類型系統來強制這些api的安全使用。

關鍵的見解

Rust是第一種行業支持的編程語言，它克服了較高級語言的安全保證和較低級“系統編程”語言提供的資源管理控制之間長期存在的權衡。
?它使用基于所有權和借用思想的強類型系統解決了這一挑戰，該系統靜態地禁止共享狀態的變化。這種方法允許在編譯時檢測許多常見的系統編程缺陷。
有許多數據類型的實現基本上依賴于共享的可變狀態，因此不能根據Rust嚴格的所有權規則進行類型檢查。為了支持這樣的數據類型，Rust選擇了明智地使用封裝在安全api中的不安全代碼。
?語義類型可靠性的證明技術，連同分離邏輯和機器檢查證明的進步，使我們能夠開始為Rust建立嚴格的正式基礎，作為Rust belt項目的一部分。

正文

特別地，像Java一樣，Rust保護程序員不受內存安全的侵害(例如，“釋放后使用”的錯誤)。但是Rust更進一步，保護程序員不受其他主流語言無法阻止的更隱蔽的異常。例如，考慮數據競爭:對共享內存的非同步訪問(其中至少有一個是寫)。即使數據競爭有效地構成了未定義的(或弱定義的)并發代碼行為，大多數“安全”語言(如Java和go)允許它們，而且它們是并發錯誤的可靠來源35相反，Rust的類型系統在編譯時排除了數據競爭。
Rust的受歡迎程度一直在穩步上升，現在許多主要的工業軟件供應商(如Dropbox、Facebook、Amazon和Cloudflare)都在內部使用它，并且在過去五年中一直高居Stack Over- flow“最受歡迎”的程序編程語言榜單之首。微軟的安全響應中心團隊最近宣布，他們正在積極探索投資使用Rust來阻止系統軟件中的安全漏洞
Rust的設計深深汲取了安全系統編程的學術研究的源泉。特別是，與其他主流語言相比，Rust的設計最顯著的特點是它采用了所有權類型系統(在學術文獻中，這是十種被稱為仿射或次結構類型系統36)。所有權類型系統通過對對象的別名(引用)進行限制來幫助程序員實施低級編程的安全模式，這些別名(引用)可以在程序執行的任何給定點上使用。
然而，Rust至少以兩種新穎而令人興奮的方式超越了之前工作的所有權類型系統:

1. Rust使用了借用和生存期機制，這使得表達通用c++風格的習慣用法更加容易，并確保它們被安全地使用。
2. Rust還提供了一組豐富的api—例如，用于并發ab- stractions、高效的數據結構和內存管理—這些api通過支持混疊和變異的更靈活組合從根本上擴展了語言的能力，這比Rust的核心類型系統所允許的更靈活。相應地，這些api不能在Rust的安全片段中實現:相反，它們在內部使用了可能不安全的c風格的語言特性，但是以一種安全的封裝方式，聲稱不會影響Rust語言級別的安全保證。
   Rust設計的這些方面不僅對它的成功至關重要——它們還提出了關于它的語義和安全保障的基本研究問題——這些都是編程語言社區剛剛開始探索的問題。
   在這篇文章中，我們首先給讀者一個對Rust編程語言的概覽，并強調Rust的一些基本特性，這些特性使它有別于同時代的其他語言。其次，我們描述了銹帶項目的初步進展，這是一個由歐洲研究理事會(ERC)資助的正在進行的項目，其目標是為銹帶的安全聲明提供第一個正式的(和機器檢查的)基礎。通過這樣做，我們希望激勵計算機科學研究社區的其他成員開始更密切地關注Rust，并幫助開發這一開創性的語言。

動機:指針 在c++失效

為了演示在系統編程語言中常見的內存安全問題，讓我們考慮圖1頂部所描述的c++代碼。在第一行中，這個程序創建了一個std::vector(一個可增長的數組)的整數。v的初始內容，即兩個元素10和11，被存儲在內存的緩沖區中。在第二行中，我們創建了一個指針vptr，它指向這個緩沖區;具體來說，它指向存儲第二個元素(當前值為11)的位置。現在v和vptr都指向同一緩沖區(重疊部分);我們說這兩個指針混疊了。在第三行中，我們將一個新元素推到v的末尾。在支持v的緩沖區中，元素12被添加到11之后。如果沒有更多的空間來容納額外的元素，則分配一個新的緩沖區，并移動所有現有的元素。讓我們假設這就是這里發生的事情。這個案例為什么有趣?因為vptr仍然指向舊的緩沖區。換句話說，向v添加一個新元素，vptr就變成了一個懸浮指針。這是可能的，因為兩個指針都有別名:通過指針(v)的操作通常也會影響它的所有別名(vptr)。圖1可視化了整個情況。
vptr現在是一個懸空指針的事實在第四行成為一個問題。這里我們從vptr加載，因為它是一個懸空指針，這是一個免費后使用的bug。
事實上，這個問題非常常見，它的一個實例有自己的名稱:迭代器失效，它指的是迭代器(通常在內部使用指針實現)失效的情況，因為迭代器所遍歷的數據結構在迭代期間發生了突變。它最常見的情況是在循環中迭代某些容器數據結構時，間接地但偶然地調用了改變數據結構的操作。請注意，在實踐中，對改變數據結構的操作的調用(在我們的示例的第3行中向后推_)可能深深嵌套在幾個抽象層之后。特別是當代碼被重構或新特性被添加時，通常幾乎不可能確定推送到某個向量是否會使程序中其他地方將要再次使用的指針失效。

與垃圾收集語言的比較。

Java、Go和OCaml等語言使用垃圾收集避免了釋放后再使用的錯誤:內存只在程序不再使用時才被釋放。因此，不會有懸空指針，也不會有after-free。
垃圾收集的一個問題是，為了提高它的效率，這些語言通常不允許內部指針(即指向數據結構的指針)。例如，Java中的數組int[]的表示類似于c++中的std::vector(除了Java中的ar射線不能增長)。然而，與c++不同的是，我們只能獲取和設置Java數組的元素，而不能對它們進行引用。要使元素本身可尋址，它們需要是單獨的對象，然后可以將對這些對象的引用存儲在數組中——也就是說，元素需要“裝箱”。這犧牲了性能和對內存布局的控制，以換取安全。
最重要的是，垃圾收集甚至不能正確解決迭代器失效的問題。在Java中迭代集合時改變集合不會導致懸空指針，但可能導致運行時拋出ConcurrentModifica- tionException。類似地，雖然Java確實防止了由空指針誤用引起的安全漏洞，但它通過運行時檢查來做到這一點，這會引發NullPoin- terException。在這兩種情況下,結果明顯優于相應的c++程序的未定義的行為,它仍有很多不足之處:而不是船運incor——矩形的代碼,然后在運行時檢測問題,我們要防止錯誤發生在第一個地方。
Rust解決指針失效的方法。在Rust中，像迭代器失效和空指針誤用這樣的問題是由編譯器靜態檢測的，它們會導致編譯時錯誤，而不是運行時異常。為了解釋這是如何工作的，考慮一下圖1底部的c++示例的Rust轉換。
和c++版本一樣，在內存中有一個緩沖區，vptr指向緩沖區的中間(導致混疊);Push可能會重新分配緩沖區，這將導致VPTR成為一個懸空指針，并導致在第4行中出現use-after-free。
但這些都沒有發生;相反，編譯器會顯示一個錯誤:“一次不能多次借用可變的v。”我們很快就會回到“借用”的問題，但是關鍵的思想——即Rust在指向數據結構的指針存在時實現內存安全的機制——已經在這里可見了:類型系統強制這樣的原則(有一個顯著的例外，我們將在后面討論):引用永遠不能同時別名化和可變。這個原則在并發環境中應該聽起來很熟悉，實際上Rust也使用它來確保沒有數據競爭。然而，正如我們被Rust編譯器拒絕的例子所示，不受限制的混疊和變異的組合會導致災難，即使對順序程序也是如此:在第3行，VPTR和v別名(v被認為指向它的所有內容，與VPTR重疊)，我們正在進行一個突變，這將導致在第4行內存訪問bug。

所有權和借款

Rust防止不受控制的混疊的核心機制是所有權。Rust中的內存總是有一個唯一的所有者，如圖2中的示例所示。
在這里，我們構造與第一個例子相似的v，然后將它傳遞給consume。操作上，就像在c++中一樣，形參是按值傳遞的，但復制是淺指針，但它們的指針不會被復制，這意味著v和w指向內存中的相同緩沖區。
如果程序同時使用v和w，那么這種混疊就會出現問題，但是在第6行嘗試這樣做會導致編譯時錯誤。這是因為Rust認為v的所有權已經轉移到了consume上，這意味著consume可以對w做任何它想做的事情，并且調用者可能不再訪問支持這個向量的內存。
資源管理。在Rust中，所有權不僅可以防止內存錯誤——它還形成了Rust內存管理方法的核心，更普遍地說，是資源管理方法。當一個擁有自己內存的變量(例如，一個類型為Vec的變量，它擁有支持vector的內存中的緩沖區)超出作用域時，我們可以確定這段內存將不再需要——因此編譯器可以在此時自動釋放內存。為此，編譯器透明地插入析構函數調用，就像在c++中一樣。例如，在consume函數中，實際上并不需要顯式調用析構函數方法(drop)。我們可以讓函數體為空，它會自動釋放w本身。因此，Rust程序很少需要擔心備忘管理:它在很大程度上是自動的，盡管缺少垃圾收集器。此外，內存管理也是靜態的(在編譯時確定)，這一事實帶來了巨大的好處:它不僅有助于降低最大內存消耗，還可以在響應性系統(如Web服務器)中提供良好的最壞情況下的延遲。在此之上，Rust的方法概括了內存管理之外的內容:其他資源，如文件描述符、套接字、鎖句柄等等，都是用相同的機制處理的，因此Rust程序員不必擔心，例如，關閉文件或釋放鎖。使用析構函數進行自動資源管理是在c++的RAII(資源獲取即初始化)形式中率先提出的;31在Rust中關鍵的區別是，類型系統可以靜態地確保資源在被析構后不再被使用。
可變的引用。一個嚴格的所有者-所有者紀律是好的和簡單的，但不幸的是不太方便工作。通常情況下，我們想要快速地向某個函數提供數據，但是在該函數完成后再返回數據。例如，我們希望v.push(12)授予push修改v的權限，但我們不希望它消耗向量v。
在《Rust》中，這是通過借鑒而實現的，它從之前關于區域類型的工作中獲得了很多靈感。13,34圖3給出了一個借位的例子。函數add_ something接受一個類型為&mut Vec的參數，表示對Vec的可變引用。操作上，這就像c++中的引用，也就是說，Vec是通過引用傳遞的。在類型系統中，這被解釋為添加_某物，從調用者那里借用Vec的所有權。
函數add_something演示了在格式良好的程序中借位是什么樣子的。要了解為什么編譯器接受這段代碼，而拒絕前面的指針失效例子，我們必須引入另一個概念:生存期。就像在現實生活中一樣，借東西的時候，可以通過事先約定借東西的時間來避免誤解。所以,當創建的引用,就像——簽署了一輩子,該記錄的完整形式引用類型:&狗T終身的。com -堆垛機確保參考(v,在我們前充足的)只有在生活——時間,再參照不習慣,直到生命結束。
在我們的例子中，生存期(都是由編譯器推斷出來的)分別只持續add _ something和Vec::push的持續時間。當上一個借位的生命周期仍在進行時，使用Never v。
相反，圖4顯示了從圖1推斷出的前一個示例的生命周期。vptr的borrow的生命周期a從第2行開始，一直持續到第4行。它不能再短了，因為vptr在第4行使用。然而，這意味著在第3行中，當存在未償還借款時使用了v，這是一個錯誤。
總而言之:無論什么東西是通過價值傳遞的(如在consume中)，Rust將其解釋為所有權轉移;當某個東西通過引用傳遞時(如在add_ something中)，Rust將其解釋為一個特定的生命周期。
共享引用。遵循可以使用別名或變異(但不能同時使用)的原則，可變引用是唯一指針:它們不允許別名。為了完成這幅圖，Rust有第二種引用，共享引用寫為&Vec或&'a Vec，它允許混列但不允許變異。共享引用的一個主要用例是在多個線程之間共享只讀數據，如圖5所示。
這里，我們創建了一個共享引用vptr，指向(并借用)v[1]。這里的豎線表示不帶任何參數的閉包函數(有時也稱為匿名函數或“lambda”)。這些閉包被傳遞給join，這是“并行組合”的Rust版本:它接收兩個閉包，并行運行它們，等待它們都完成，并返回它們的結果。當join返回時，借位結束，所以我們可以再次改變v。
就像可變引用一樣，共享引用也有生命周期。在底層，Rust編譯器使用一個生命周期來跟蹤v在兩個線程之間臨時共享的時間段;生命周期結束后(在第5行)，v的原始所有者重新獲得完全控制權。這里的關鍵區別是，在同一生命周期內允許多個共享引用共存，只要它們只用于讀，而不是寫。我們可以通過將示例中的兩個線程中的一個更改為|| v.push(12)來見證這一限制的實施:然后編譯器會抱怨不能同時擁有對Vec的可變引用和共享引用。實際上，該程序在讀取線程和推入向量的線程之間有一個致命的數據競爭，所以編譯器靜態地檢測這種情況是很重要的。
共享引用在序列代碼中也很有用;例如，在對vector對象進行共享迭代時，仍然可以將對整個vector對象的共享引用傳遞給另一個函數。但在本文中，我們將重點討論并發共享的使用。
總結。為了獲得安全性，Rust類型系統要求引用不能同時有別名和可變。擁有類型為T的值意味著您完全“擁有”它。類型T的值可以使用可變引用(&mut)或共享引用(&T)來“借用”。

通過安全的api放松Rust嚴格的所有權紀律

Rust的核心所有權規程足夠靈活，可以考慮許多低級編程習慣用法。但是對于實現特定的數據結構，它可能會有過多的限制。例如，如果沒有別名狀態的任何變化，則不可能實現雙重鏈表，因為每個節點都由它的下一個和前一個鄰居別名。
Rust采用了一種不同尋常的方法來解決這個問題。與其使其類型系統復雜化以考慮不符合它的數據結構實現，或引入動態檢查以在運行時加強安全性，Rust允許通過開發安全的api來放松自己的規則，這些api通過允許安全控制別名可變狀態的使用來擴展語言的表達能力。盡管這些api的實現不遵守Rust嚴格的所有權規則(這一點我們稍后再討論)，但api本身關鍵地利用了Rust的所有權和借用機制，以確保它們保持了Rust作為一個整體的安全保證。現在讓我們看幾個例子。
共享可變狀態。Rust的共享引用允許多個線程并發讀取共享數據。但是只讀數據的線程只是故事的一半，所以接下來我們將看看互斥鎖API是如何使一個人安全地跨線程邊界共享可變狀態的。起初，這似乎與我們迄今為止所說的關于Rust的安全性的所有內容相矛盾:Rust所有權原則的全部意義不就是防止共享狀態的突變嗎?確實如此，但我們將看到如何使用互斥鎖來充分限制這種變異，從而不破壞內存或線程安全。考慮圖6中的示例。
我們再次使用結構化并發和共享引用，但現在我們將vector封裝在一個互斥鎖中:變量mutex_v的類型為Mutex<Vec>。互斥鎖上的鍵操作是鎖，它會阻塞，直到它能獲得排他鎖為止。當變量超出作用域時，v的析構函數隱式地釋放鎖。最后，如果第一個線程首先獲得鎖，這個程序要么打印[10,11,12]，要么打印[10,11]，如果第二個線程獲得鎖。
為了理解我們的示例程序是如何進行類型檢查的，讓我們仔細看看鎖。它(幾乎)有類型fn(&'a Mutex) -> MutexGuard <'a, T>。這種說鎖可以被稱為共享引用μ- tex,這就是為什么生銹讓我們叫鎖在兩個線程:兩個閉包捕獲一個互斥< Vec <等> >,并與vptr捕獲的類型等,在我們的第一個并發的例子中,兩個線程同時可以使用引用。事實上，至關重要的是，鎖采用共享引用而不是muta- ble引用，否則，兩個線程無法同時嘗試獲取鎖，而且從一開始就不需要鎖。
鎖。此外，當它超出作用域時，它會自動釋放鎖(在c++世界中稱為rai31的習慣用法)。
在我們的示例中,這意味著兩個線程暫時的獨占訪問權向量,他們有一個可變參考,反映了事實,由于正確實現互斥鎖,他們永遠都有一個可變參考- ence同時,如此獨特的——洛克可變的屬性引用。換句話說，互斥可以安全地提供別名狀態的變化，因為它實現了運行時檢查，確保在每次變化期間，狀態沒有別名。
引用計數。我們已經看到，共享引用提供了一種在程序中的不同方之間共享數據的方法。但是，共享引用具有靜態確定的生存期，當該生存期結束時，數據又被唯一地擁有。這在結構化并行中工作得很好(如前面示例中的join)，但不適用于非結構化并行，在非結構化并行中，線程被派生出來并獨立于父線程運行。
在生銹,典型的在這種情況下共享數據的方法是使用一個atomi -卡莉采用引用計數的指針:弧T < T >是一個指針,但也多少存在這樣的指針和重新分配T(和釋放相關資源),最后一個指針是de -毀掉了。(這可以看作是一種輕量級庫實現的垃圾收集。)
由于數據是共享的，我們不能從Arc中獲得&mut T，但是我們可以獲得&T(其中編譯器確保在引用的生命周期內，Arc不會被銷毀)，如圖7中的示例所示。
我們首先創建一個指向通常向量的Arc。Arc_v2是通過克隆arc_v1獲得的，這意味著引用計數增加了1，但數據本身并不復制。然后生成一個使用arc_v2的線程;即使當我們在這里編寫的函數返回時，這個線程仍然在后臺運行。因為這是一種非結構化并行，所以我們必須顯式地將arc_v2的所有者轉移到另一個線程中運行的閉包中。Arc是一個“智能指針”(類似于c++中的shared_ptr)，所以我們幾乎可以把它當作&Vec來使用。特別地，在第3行和第4行中，我們可以使用索引來輸出位置為1的元素。隱式地，當arc_v1和arc_v2超出作用域時，會調用它們的析構函數，最后一個要銷毀的Arc會釋放vector對象。
線程安全。最后一個類型,我們想談談在這銹簡介:Rc < T >是一種采用引用計數的弧< T >非常相似,但由于電弧的關鍵區別< T >使用原子(抓取和-添加)指令更新- ence引用計數,而Rc < T >使用非原子內存操作。因此，Rc可能更快，但不是線程安全的。類型Rc在復雜的順序代碼中很有用，在這些代碼中，共享引用強制的靜態作用域不夠靈活，或者不能靜態地預測對象的最后一個引用何時會被銷毀，從而可以釋放對象本身。
因為Rc不是線程安全的，我們需要確保程序員不會在應該使用Arc時意外使用Rc。這是很重要的:如果我們以之前的Arc為例，用Rc替換所有的Arc，程序會有一個數據競爭，可能會過早地釋放內存或根本不釋放內存。然而，非常值得注意的是，Rust編譯器能夠捕捉到這個錯誤。它的工作方式是Rust em-使用了一種稱為Send trait的東西:一種類型的屬性，只有當類型T的元素可以安全地發送到另一個線程時，類型T才能使用這種屬性。類型為Arc是Send，類型為Rc不是。join和spawn都要求它們運行的閉包捕獲的所有內容都是Send，因此，如果我們在閉包中捕獲非Send類型Rc的值，編譯將失敗。
Rust對Send特性的使用說明，有時強靜態類型施加的限制可以導致更強的表達能力，而不是更弱。特別地，c++的智能引用計數指針，std::shared_ ptr，總是使用原子指令，因為使用像Rc這樣更高效的非線程安全的變量被認為風險太大。相比之下,生銹的特性允許發送到“黑客而不用擔心:“26日有兩個線程提供了一種方法——安全數據結構(如弧)和非線程安全的數據結構(如Rc)在相同的語言,同時確保到模塊化,這兩個不習慣不正確的方法。

不安全代碼，安全封裝

我們已經看到了像Arc和Mutex這樣的類型是如何讓Rust程序安全地使用引用計數和共享可變狀態等特性的。然而，有一個問題:這些類型實際上不能在Rust中實現。或者，更確切地說，它們不能在安全的Rust中實現:編譯器會因為可能違反混疊規則而拒絕Arc的實現。事實上，它甚至會拒絕Vec的實現來訪問可能未ini化的內存。為了提高效率，Vec手動管理底層緩沖區并跟蹤它的哪些部分被初始化。當然，Arc的實現實際上并沒有違反混淆規則，Vec實際上也沒有訪問未初始化的內存，但是建立這些事實所需的參數太微妙了，Rust編譯器無法推斷。為了解決這個問題，Rust有一個“出口”:Rust不僅包含我們目前討論過的安全語言——它還提供了一些不安全的特性，比如c風格的無限制指針。這些特性的安全性(內存安全性和/或線程安全性)無法由編譯器保證，因此它們只在標記為不安全關鍵字的語法塊中可用。這樣，就可以確保不會意外地離開安全的Rust領域。
例如，Arc的實現使用了不安全的代碼來實現一個模式，這個模式不能用安全的代碼來表達:Rust:共享沒有明確的own- er，由線程安全的引用計數管理。由于支持“弱引用”，情況變得更加復雜:這些引用不會使referent保持活動狀態，但可以原子性地檢查活動狀態并升級到完整的Arc。Arc的正確性依賴于相當微妙的并發推理，而Rust編譯器根本沒有辦法靜態地驗證，當引用計數達到0時，釋放內存實際上是安全的。
不安全塊的替代品。可以將Arc或Vec之類的東西轉換為語言原語。例如，Py- thon和Swift有內置的引用計數，Python有list作為Vec的內置等效物。然而，這些語言特性是用C或c++實現的，所以它們實際上并不比不安全的Rust實現更安全。除此之外，將不安全的操作限制在語言原語的實現中也嚴重限制了靈活性。例如，Firefox使用一個Rust庫實現了一個不支持弱引用的Arc變體，這就提高了不需要弱引用的代碼的空間利用率和性能。語言是否應該為任何內置類型的設計空間中的每一個可想到的地方提供原語?
另一個避免不安全代碼的選擇是使類型系統具有足夠的表現力，從而能夠實際驗證類型(如Arc)的安全性。然而,由于如何微妙的正確性的數據結構(事實上弧和簡化的變異作為主要案例研究在最近的一些正式的驗證papers9、12、18),這個基本上需要一種通用的定理prover-and研究員足夠的背景來使用它。定理證明社區離讓開發人員自己進行這種證明還有很長的路要走
安全的抽象。相反，Rust選擇允許程序員在必要時靈活地編寫不安全的代碼，盡管它應該由安全的api封裝。安全封裝意味著，不考慮像Arc或Vec這樣的Rust api是用不安全代碼實現的，這些api的用戶應該不會受到影響:只要用戶在Rust的安全片段中編寫了類型良好的代碼，他們就不應該能夠觀察到由于在api實現中使用不安全代碼而導致的異常行為。這與c++形成了鮮明的對比，后者的弱類型系統甚至缺乏強制api安全使用的能力。因此，像shared_ptr或vector這樣的c++ api很容易被誤用，導致引用計數錯誤和迭代器失效，而這些在Rust中不會出現。
編寫不安全代碼的能力就像一個杠桿，Rust程序員用它使類型系統更有用，而不用把它變成一個定理證明，事實上，我們相信這是Rust成功的關鍵因素。Rust社區正在開發一個安全可用的高性能庫的完整生態系統，使程序員能夠在這些庫之上構建安全高效的應用程序。
但是當然，沒有免費的午餐:這取決于Rust庫的作者以某種方式確保，如果他們編寫不安全的代碼，他們會非常小心，不破壞Rust的安全保證。一方面，這比在C/ c++中要好得多，因為絕大多數的Rust代碼是在該語言的安全片段中編寫的，所以Rust的“攻擊面”要小得多。另一方面，當需要不安全的代碼時，程序員如何知道他們是否足夠“小心”是很不明顯的。
為了保持對Rust生態系統安全性的信心，我們真的想要有一種方式，正式說明和驗證將不安全的代碼安全地封裝在一個安全的API后面意味著什么。這正是銹帶項目的目標。

Rustbelt：確保rust的基礎

驗證Rust的安全聲明的關鍵挑戰是解釋安全代碼和不安全代碼之間的交互。要了解這為什么具有挑戰性，讓我們簡要地看一看驗證編程語言安全性的標準技術—所謂的語法方法。使用這種技術，安全性用語法類型判斷來表示，語法類型判斷用一些數學推理規則來形式化地說明類型檢查器。
定理1(句法類型健全性)。如果一個程序e在語法類型判斷方面是良好類型的，那么e是安全的。
不幸的是，這個定理對于我們的目的來說太弱了，因為它只討論語法安全的程序，從而排除了使用不安全代碼的程序。例如，如果為真{e} else {crash()}不是語法良好的類型，但它仍然是安全的，因為crash()永遠不會執行。
關鍵的解決方案:語義類型的可靠性。為了說明安全代碼和不安全代碼之間的交互，我們轉而使用一種稱為語義類型可靠性的技術，它根據程序的“行為”而不是一組固定的推理規則來表達安全性。語義健全的關鍵因素是邏輯關系，它為每個API分配了一個安全契約。它表示，如果API中每個方法的輸入符合它們指定的類型，那么輸出也符合。使用來自正式驗證的技術，可以證明API的實現滿足分配的安全契約，如圖8所示。
語義類型健全性是推理使用安全代碼和不安全代碼組合的程序的理想選擇。對于任何使用不安全代碼的庫(如Arc、Mutex、Rc和Vec)，必須手工證明其實現滿足安全契約。例如:
定理2。Arc滿足其安全契約。
對于程序中安全的部分，驗證是自動的。這可以用下面的定理來表達，它說，如果一個組件寫在Rust的安全片段中，它通過構造來滿足其安全契約。
定理3(基本定理)。如果組件e在語法上是良好類型的，那么e滿足它的安全契約。
總之，這意味著如果不安全的塊只出現在已經手動驗證以滿足其安全契約的庫中，那么Rust程序就是安全的。
使用Iris邏輯對安全契約進行編碼。語義類型穩健性是一種古老的技術，至少可以追溯到Milner 1978年關于類型穩健性的開創性論文28，但將其擴展到現實的現代語言(如Rust)已被證明是一個困難的挑戰。事實上，將其擴展到具有可變狀態和高階函數的語言仍然是一個開放的問題，直到21世紀初，“步進索引Kripke邏輯關系”(SKLR)模型的開發，作為基本攜帶代碼證明項目的一部分。即使這樣，直接使用SKLR模型編碼的安全契約的驗證也變得非常乏味、低級，并且難以維護。
在銹帶中，我們建立在Iris的最新工作之上，Iris是一個用于高階、并發、強制程序的驗證框架，在Coq證明助手中實現。Iris為編碼和使用SKLR模型提供了更高級的語言，從而使我們能夠擴展這樣的模型來處理像Rust這樣復雜的語言。特別是，Iris是基于分離邏輯的，它是Hoare邏輯的擴展，專門針對指針操作程序的模塊化推理，并以所有權的概念為中心。這為我們提供了一種理想的語言，可以在Rust中對所有權類型的語義建模。
Iris擴展了傳統的分離邏輯，增加了幾個對Rust建模至關重要的特性:
?Iris支持用戶定義的虛狀態:定義自定義邏輯資源的能力，這些資源對于證明程序的正確性很有用，但并不直接對應于其物理狀態中的任何東西。Iris的用戶定義的ghost狀態使我們能夠驗證像Arc這樣的庫的合理性，對于這些庫，所有權并不對應于物理所有權(例如，兩個獨立擁有的Arc可能由相同的底層內存支持)——這是一種被稱為“虛擬分離”的現象。10,11通過(在Iris內)導出一個新的、領域特定的“生命周期邏輯”，它也使我們能夠在更高的抽象層次上對Rust的借用和生命周期進行推理。
Iris支持命令式不變量:程序狀態上的不變量，可以循環地指向其他不變量的存在謂詞不變量在建模中心類型系統特性(如遞歸類型和閉包)中扮演著重要的角色。
Rust的復雜性要求我們的語義合理性證明是機器檢查的，因為手工做證明太乏味且容易出錯。幸運的是，Iris提供了一套豐富的分離邏輯策略，這些策略是模仿標準Coq策略的，因此可以以Coq用戶熟悉的經過時間檢驗的方式交互式地開發機器檢查的語義合理性證明。

總結

以上是生活随笔為你收集整理的Rust的安全系统编程的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。