POPL 2023 (series) / PriSC 2023 (series) / PriSC 2023 /
FaJITa: Verifying Optimizations on Just-In-Time Programs
We introduce FaJITa: a translation validation tool for verifying semantic equivalence after optimizations. FaJITa combines symbolic execution with more traditional static analysis techniques to verify functions which have passed through Firefox’s optimizing JIT compiler. We are able to verify practically all JavaScript functions, without having to resort to dynamic techniques or branch pruning to decrease the state space. We additionally develop a fuzzing infrastructure to look for bugs in the Firefox JIT, as well as debugging tools for distinguishing true bugs from false positives.
| FaJITa PriSC 2023 Paper (fajita-prisc23-paper.pdf) | 318KiB |
| FaJITa PriSC 2023 Presentation (PriSC 2023 FaJITa .pdf) | 610KiB |
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 21 Jan
Displayed 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 | ||