Computing has been massively successful, and we routinely trust computer systems with our personal, financial, medical, commercial, and governmental information. But at the same time, these systems are pervasively prone to security flaws and subject to malicious attacks. We have to trust them, but they are not trustworthy.
There are two root causes. First, the pan-industry computing infrastructure, of processors, programming languages, and operating systems, is based on designs from a more forgiving time, with simpler systems and little incentive to design-in strong security protection. Second, the conventional engineering techniques we use (prose specifications, manually written tests, and test-and-debug development) are good enough to make systems work in common cases, but cannot exclude all errors - and a single coding error can lead to a devastating exploit.
Are we doomed? Perhaps not. This talk will highlight the sorry state of the art and then draw on cutting-edge research, from the University of Cambridge, SRI International, ARM, and other partners, to show some ways we can do better. First, we'll show how it's become possible to build and use rigorous models for key existing interfaces to improve engineering: for the ARMv8-A and RISC-V architectures, and the C language, in the REMS project. Then we'll describe a principled but pragmatic path to build in more hardware and software security protection to future systems, as developed in the CHERI project. These are joint work by many people over the last 10 years.