Seminar details


Room 206 (2nd floor, badged access)

10 March 2022 - 14h00
A CompCert Backend with Symbolic Encryption
by Paolo Torrini from 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.




Contact | Site Map | Site powered by SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4125120