CapC: Capability C semantics, tools and reasoning

CapC：Capability C 语义、工具和推理

基本信息

批准号：
EP/V000470/1
负责人：
Mark Batty
金额：
$ 61.82万
依托单位：
University of Kent
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2020
资助国家：
英国
起止时间：
2020 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FV000470%2F1
关键词：
CapC Capability semantics tools reasoning

项目摘要

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.

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