Sat 22 Jan 2022 16:40 - 17:05 at Independence - Secure systems Chair(s): Marco Guarnieri

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.

A CompCert backend with symbolic encryption (prisc22_revised.pdf)324KiB
A CompCert Backend with Symbolic Encryption (slides, revised) (prisc_slides1.pdf)113KiB

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:40 - 17:55
Secure systemsPriSC at Independence
Chair(s): Marco Guarnieri IMDEA Software Institute
16:40
25m
Talk
A CompCert backend with symbolic encryptionRemote
PriSC
Paolo Torrini INRIA, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
File Attached
17:05
25m
Talk
Effect-Oblivious EquivalenceRemote
PriSC
Yao Li University of Pennsylvania, Stephanie Weirich University of Pennsylvania
Pre-print File Attached
17:30
25m
Talk
The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating codeRemote
PriSC
Dominic Mulligan Arm Research, Nick Spinale Arm Research
File Attached