Formal Processor Model Providing Provably Secure Speculation For The Constant-Time Policy


A new technical paper titled "ProSpeCT: Provably Secure Speculation for the Constant-Time Policy" was published by researchers at imec-DistriNet, KU Leuven, CEA, and INRIA. This paper was included at the recent 32nd USENIX Security Symposium. Abstract: "We propose ProSpeCT, a generic formal processor model providing provably secure speculation for the constant-time policy. For constant-tim... » read more

Formal Processor Model Providing Secure Speculation For The Constant-Time Policy


A technical paper titled "ProSpeCT: Provably Secure Speculation for the Constant-Time Policy (Extended version)" was published by researchers at imec-DistriNet at KU Leuven, CEA, List, Université Paris Saclay and INRIA. Abstract: "We propose ProSpeCT, a generic formal processor model providing provably secure speculation for the constant-time policy. For constant-time programs under a no... » read more