Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
summary
Cachet is a DSL that compiles Cachet to Boogie and C++ and encodes JIT invariants so the verifier proves generated code never violates them. The toolchain uses Boogie + Corral to check pipelines and supports translation validation of real SpiderMonkey stubs; 67 of 333 CacheIR ops are implemented, a fixed-slot generator verifies in 4s, dynamic slots in 39s, combined in 63s. Firefox stubs (159 deduped, 70 fully supported) have median verification 27s with some heavy cases up to ~4 hours. verifies generated stubs end-to-end
AI-written summary · about
chapters (14)
- 0:00Cachet and verified JIT compilers
- 1:50JavaScript JIT compilation challenges
- 4:37Inline caching security
- 7:04Cachet design goals
- 9:11Cachet as a DSL for JITs
- 10:35Incremental adoption in SpiderMonkey
- 13:45Verification pipeline and Boogie
- 16:56Verified inline cache system
- 19:45Optimizing with symbolic execution
- 21:11Cachet performance evaluation
- 22:35Future plans with Firefox
- 23:22Collaboration with SpiderMonkey
- 24:25New language vs existing tools
- 25:49Q&A: Boogie and trusted code
related talks
22mGigue: A JIT Code Binary Generator for Hardware Testing
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
29mTowards Formally Verified Just-In-Time Compilation
14mCollapsing Towers for Side-Channel Security
17mOvercoming Restraint: Composing Verification of Foreign Functions with Cogent
15mAmalgamating Different JIT Compilations in a Meta-tracing JIT Compiler Framework
20mCacheIR: The Benefits of a Structured Representation for Inline Caches
15mAutomatically Reasoning About How Systems Code Uses the CPU Cache