Verifiably Secure Systems with Universal Contracts and Secure Compilation. KU Leuven
One of the driving ambitions of my research is to make it possible and affordable to construct systems with a rigorous proof of important security properties. Imagine, for example, constructing the software for a smart device with a computer-verified guarantee that it will only ever communicate with servers at example.com, or software for an industrial controller that can be proven to never send out-of-range parameters to a physical actuator. ...