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.13 + AHUNTSIC [CC License]

info visites 3987930