Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Just-in-time (JIT) compilers face a tough task: chewing up potentially-untrusted input and spitting out machine code that’s at once fast, correct, and secure, working close-to-the-metal with low-level primitives in a tight time budget. Developers juggle complex invariants which generated code must respect, which can easily shatter the system’s security model when broken. Cachet, our domain-specific language for JIT implementation, makes these invariants explicit and statically-verified. Our toolchain compiles Cachet code both to the SMT-solvable Boogie verification language and to C++ suitable for embedding in host applications and language runtimes. We are evaluating Cachet by reimplementing and verifying components of Firefox’s JavaScript JIT.
| Extended Abstract (prisc23-paper10.pdf) | 372KiB |
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:30 | |||
16:00 25mTalk | Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers PriSC Michael Smith UC San Diego, Abhishek Sharma UC San Diego, John Renner University of California at San Diego, USA, David Thien UC San Diego, Sorin Lerner University of California at San Diego, Fraser Brown CMU, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego File Attached | ||
16:25 25mTalk | FaJITa: Verifying Optimizations on Just-In-Time Programs PriSC David Thien UC San Diego, Michael Smith UC San Diego, Evan Johnson University of California at San Diego; Arm, Sorin Lerner University of California at San Diego, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego, Fraser Brown CMU Pre-print File Attached | ||
16:50 25mTalk | Universally Composable Security for Program Partitioning PriSC Coşku Acay Cornell University, Joshua Gancher Carnegie Mellon University, Rolph Recto Cornell University, Andrew Myers Cornell University File Attached | ||