Spectres, Meltdowns, Zombies, Orcs: Can formal methods banish the ghosts that haunt our computing systems?

Abstract: In spite of growing efforts to integrate security-specific features into the hardware of modern processors and SoCs, HW security violations continue to be reported at an alarming rate. This has created high alertness among professionals and in the general public. Seemingly innocuous design decisions, like chip designers make them every day, such as adding or removing a buffer, can introduce covert channels with serious consequences. Similarly, subtle bugs that easily escape conventional flows can devastate the security of the entire hardware/software stack. Understanding the intricate implications of microarchitectural design decisions on system security remains a great challenge and calls for new formal-driven design methodologies.

This talk addresses these challenges at the microarchitectural level and discusses the threats related to transient execution side channels, such as Spectre and Meltdown, security-violating design bugs and HW weaknesses violating data-obliviousness. We present a formal method called Unique Program Execution Checking (UPEC) to detect such vulnerabilities. UPEC does not require a priori knowledge on possible attacks and detects HW vulnerabilities systematically without demanding the clever thinking of a human attacker.

The talk presents several case studies on open-source RISC-V systems and gives perspectives of new secure-by-construction design practices driven by formal methods.