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至少以两种新颖而令人兴奋的方式超越了之前工作的所有权类型系统:

Rust使用了借用和生存期机制，这使得表达通用c++风格的习惯用法更加容易，并确保它们被安全地使用。
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用户熟悉的经过时间检验的方式交互式地开发机器检查的语义合理性证明。