Room 206 (2nd floor, badged access)
10 mars 2022 - 14h00
A CompCert Backend with Symbolic Encryption
par Paolo Torrini de Inria Sardes
Abstract: IntrinSec is a secure cryptoprocessor, designed by Oliver Savry's team of CEA-LETI, that extends RISC-V with hardware support to monitor control-flow hijacks. We present our CompCert formal model of its assembly language, the control-flow protections inserted by our CompCert backend, and their associated formal proofs of correctness.
