A CompCert backend with symbolic encryption
summary
A verified C backend called IntrinSec extends CompCert’s RISC-V backend with instruction-level symbolic encryption: new mask registers, four crypto instructions (load destination mask, load runtime mask, store/load return mask), and a stack-frame redesign. Forward/backward simulation proofs are refactored so compiled encrypted binaries preserve source behaviors; implementation adds about 6000 LOC and took ~seven person-months. Security relies on an unguessable next-mask function and protected mask storage; the stack remains unencrypted. Ongoing work adds far pointers, a pseudo-assembly stage, and finer security proofs.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:47Motivation
- 2:35Background
- 4:03Encryption
- 6:02Encryption Diagram
- 8:53The problem
- 9:34The solution
- 10:49Development overview
- 12:09Verification overview
- 13:10Encryption protocol
- 14:39Masks
- 16:13Assembly code
- 17:15Verification
- 18:46Forward Simulation Theorem
- 20:16Security aspects
- 21:38Work in progress
- 23:09Conclusion
- 24:54Security properties
related talks
15mMy Journey in Secure Compilation
24mA CompCert Compiler that Preserves Cryptographic Constant-time
18mCPU Security in the Context of RISC-V
28mMemory simulations, security and optimization in a verified compiler
28mSECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M...
58mFast Cryptographic Code via Partial Evaluation
52mEnabling New Security Frontiers: Deep-Dive Into Implementing Confidential Computing on RISC-V
19mAn Open Source Approach to System Security