Détails sur le séminaire


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.




Contact | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4199681