CapC: Capability C semantics, tools and reasoning

我们解决了一个来自行业的技术难题：我们寻求C和C++编程语言标准中的基本问题的解决方案。C和C++代码不仅仅是流行的--它被用来形成我们系统的最低和最受信任的级别。每个主流操作系统的内核都使用了这两种操作系统的某种组合，包括Windows、MacOS、iOS、Android、Linux和Unix，以及一系列具有汽车发动机管理等基本功能的嵌入式控制器。有一个良好的语言规范是验证这些重要系统组件的正确性的第一步。--对抗软件故障--这项工作是通过开发技术来验证软件的正确性来对抗软件故障的更大努力的一部分。目前，计算机系统的开发人员主要依靠测试来确保系统按照他们应该的方式运行。系统在各种输入上运行了一段时间，并监控故障。他们希望这将暴露系统中足够多的缺陷，使其在部署后变得可靠。但要实现良好的覆盖成本越来越高：像汽车这样的系统经历了千变万化的输入，特定车型的车队集体运行的时间远远长于其计算机系统的测试时间。更糟糕的是，现代系统是并发的--使用多个通信处理器来完成一项任务。并发处理器之间微妙的相互作用使得系统的输出依赖于通信的时间，因此一些行为在数十亿次运行中只出现了几次，这使得测试几乎没有希望找到相关的错误。在审查安全属性时，人们面临的不是简单的情况，而是一个公认的对手，这些对手不是通过简单的测试就能复制的。有证据表明，通过测试验证软件正在崩溃，一些漏洞甚至在关键系统中也在逃避发现：例如，一个并发漏洞导致丰田的一些汽车突然无情加速，导致83人在10年内死亡。据美国国家标准与技术研究院估计，软件故障造成的更广泛的经济成本为每年600亿美元。改进对软件故障的处理将具有重大的经济和社会影响。验证提供了测试的另一种选择：一种定义系统的期望属性--它不会崩溃，燃料计量将与加速器输入成正比，等等--并且从数学上证明代码满足它们。在验证的理想中，没有错误潜入的空间，正确性的数学证明是绝对的。这对于安全物业尤其有价值。不幸的是，验证技术总是建立在计算机系统的理想化模型之上，例如，假设存储器访问以全局顺序进行，即所谓的顺序一致性(SC)。理想和现实之间的距离给虫子留下了足够的生存空间。事实上，现状要糟糕得多，因为我们没有系统行为的现实特征：我们最好的编程语言行为模型是已知被打破的，例如在C、C++和Java中。在这个广泛的上下文中，我们的项目将开发一种符合现实的C语言描述，允许编译器优化和底层并发处理器所隐藏的行为类型。同时，我们将在正确模拟现代语言微妙行为的环境中开发验证技术，与这些以前对系统的不同观点相吻合。我们的工作将使并发系统的验证变得更加可行，包括安全属性，有助于解决软件故障带来的经济和社会代价。

We address a difficult technical problem that is drawn from industry:we seek a solution to fundamental problems found in the standards ofthe C and C++ programming languages. C and C++ code is not justprevalent -- it is used to form the lowest and most trusted levels ofour systems. The kernel of every mainstream operating system uses somecombination of the two, including Windows, MacOS, iOS, Android, Linuxand Unix, as do the swathe of embedded controllers with essentialfunctions like automotive engine management. Having a goodspecification of the language is the first step in verifying thecorrectness of these vital system components.-- Combatting software failure --This work is part of a larger effort to combat software failure bydeveloping techniques to verify the correctness of software.Currently, developers of computer systems rely predominantly ontesting to ensure that systems behave as they should. The system isrun for some time over various inputs and monitored for failure. Thehope is that this will expose enough of the flaws in the system tomake it reliable once it is deployed. But it is increasinglyexpensive to achieve good coverage: systems like cars experiencewildly varied inputs, and a fleet of a particular model of car runscollectively for far longer than the time its computer systems aretested. Worse still, modern systems are concurrent -- using multiplecommunicating processors to complete a task. The delicate interplaybetween the concurrent processors makes the output of the systemdependent on the timing of communication, so that some behavioursoccur only a handful of times in billions of runs, leaving testinglittle hope of finding associated bugs. When scrutinising securityproperties, one is faced not with simple circumstance, but with acommitted adversary that cannot be replicated by simple testing.There is evidence that validating software through testing is breakingdown and some bugs are evading discovery even in critical systems: forexample a concurrency bug caused some of Toyota's cars to suddenly andrelentlessly accelerate, killing 83 over 10 years. The wider economiccost of software failure was estimated by the U.S. National Instituteof Standards and Technology to cost USD 60bn each year. Improving ourapproach to software failure would have substantial economic andsocietal impact.Verification offers an alternative to testing: one defines desirableproperties of the system -- it will not crash, fuel metering will beproportional to accelerator input, and so on -- and mathematicallyproves that the code satisfies them. In the ideal of verification,there is no space for bugs to creep in and the mathematical proof ofcorrectness is absolute. This is particularly valuable for securityproperties. Unfortunately, verification techniques are invariablybuilt above an idealised model of the computer system, e.g.\ theassumption that memory accesses take place in a global sequentialorder, so called sequential consistency (SC). The distance between theideal and the reality leaves ample space for bugs to persist. In factthe status quo is much worse because we do not have a characterisationof the reality of the system's behaviour: our best models ofprogramming-language behaviour are known to be broken, e.g.\ in C, C++and Java.In this broad context, our project will develop a description the Clanguage that matches the reality, permitting the sorts of behaviourexhibited by compiler optimisations and the underlying concurrentprocessors. At the same time, we will develop verification techniquesin a setting that correctly models the subtle behaviour of modernlanguages, dovetailing these previously disparate views of thesystem. Our work will make verification of concurrent systems moreviable, including security properties, helping to address the economicand social costs of software failure.