CapC: Capability C semantics, tools and reasoning

我们解决了一个来自工业界的技术难题：我们寻求解决C和C++编程语言标准中的基本问题。C和C++代码不仅仅是流行的--它被用来构成我们系统的最低和最可信的级别。每一个主流操作系统的内核都使用这两种操作系统的结合，包括Windows、MacOS、iOS、Android、Linux和Unix，以及一系列具有汽车发动机管理等基本功能的嵌入式控制器。有一个良好的语言规范是验证这些重要系统组件正确性的第一步。对抗软件故障--这项工作是通过开发技术来验证软件正确性来对抗软件故障的更大努力的一部分。目前，计算机系统的开发人员主要依靠测试来确保系统按其应有的方式运行。系统在各种输入上运行一段时间，并监视故障。他们希望这将暴露出系统中足够多的缺陷，使其在部署后变得可靠。但是，要达到良好的覆盖率，成本越来越高：像汽车这样的系统会经历各种各样的输入，一个特定型号的汽车车队选择性地运行的时间远远超过其计算机系统测试的时间。更糟糕的是，现代系统是并发的--使用多个并行处理器来完成一项任务。并发处理器之间微妙的相互作用使得系统的输出依赖于通信的时间，因此某些行为在数十亿次运行中只发生少数几次，使得测试几乎没有希望找到相关的错误。在审查安全属性时，人们面临的不是简单的情况，而是无法通过简单测试复制的特定对手。有证据表明，通过测试验证软件正在崩溃，甚至在关键系统中也有一些错误无法被发现：例如，一个并发错误导致丰田的一些汽车突然无情地加速，在10年内造成83人死亡。据美国国家标准与技术研究所估计，软件故障造成的更广泛的经济损失每年为600亿美元。改进我们对软件故障的处理方法将产生巨大的经济和社会影响。验证提供了一种替代测试的方法：一种方法是定义系统的合理属性--它不会崩溃，燃料计量将与加速器输入成比例，等等--并最终证明代码满足这些属性。在理想的验证中，没有漏洞的空间，正确性的数学证明是绝对的。这对于安全属性特别有价值。不幸的是，验证技术总是建立在计算机系统的理想模型之上，例如，存储器访问以全局顺序顺序发生的假设，即所谓的顺序一致性（SC）。理想和现实之间的距离为bug留下了足够的生存空间。事实上，现状要糟糕得多，因为我们没有一个系统行为的现实特征：我们最好的编程语言行为模型被打破了，例如。在这个广泛的背景下，我们的项目将开发一种描述与现实相匹配的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.