Anticipating all possible attacks on a system is hard work. Malicious actors seem to have an inherent advantage, since they can win by finding single vulnerabilities. In our MIT team within the DARPA SSITH program, we are exploring principled ways to rule out human error as a source of security issues in computer processors. A typical security audit involves prose arguments about attack models and why they are thwarted. We instead write down formal mathematical theorems about real digital hardware designs, and we build their formal proofs that can be checked algorithmically. That is, a program, rather than a potentially distracted human, confirms that the security argument is convincing.
After giving some background on the general technology, I would like to focus on two concrete uses in the SSITH program. First, we are exploring flexible tagging support, to flow additional security-relevant information through the microarchitectural state of a Linux-capable processor. Unusually, however, we propose to compile custom processor descriptions automatically from descriptions of security policies to be enforced. We aim to do this compilation in a way that gives formal theorems that the generated processors truly enforce the security policies. Second, we are tackling the issues with timing side channels exposed by the Spectre and Meltdown vulnerabilities. Through a synergistic connection with work funded by the National Science Foundation, we are able to prove security theorems for whole hardware-software system stacks. For instance, we can show that a compiled C program with a cryptographic function will run on a specific RISC-V processor, in a way where a secret input flowing into the function provably has no effect on timing of output events flowing out of the processor.