A CompCert backend with symbolic encryption
Binary encryption can be used to strengthen a verified compilation toolchain, in order to protect executable code from malware attacks. We present IntrinSec, a C backend that extends RISC-V with binary encryption and our work on its formalization and verification as a CompCert backend.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
16:40 - 17:55
|A CompCert backend with symbolic encryptionRemote|
PriSCPre-print File Attached
|The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating codeRemote|