CapC: Capability C semantics, tools and 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.