Towards a verified range analysis for JavaScript JITs
Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan
Abstract
We present VeRA, a system for verifying the range analysis pass in browser just-in-time (JIT) compilers. Browser developers write range analysis routines in a subset of C++, and verification developers write infrastructure to verify custom analysis properties. Then, VeRA automatically verifies the range analysis routines, which browser developers can integrate directly into the JIT. We use VeRA to translate and verify Firefox range analysis routines, and it detects a new, confirmed bug that has existed in the browser for six years.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 1e78a906-5b72-4698-b7f5-7190ca5ed4bfCited by top-tier papers11
- Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT CompilerAurèle Barrière, Sandrine Blazy, David PichardiePOPL 2023 · 27 citations
- Compiler Testing using Template Java ProgramsZhiqiang Zang, Nathan Wiatrek, Milos Gligoric, August ShiASE 2022 · 21 citations
- Translation Validation for JIT Compiler in the V8 JavaScript EngineSeungwan Kwon, Jaeseong Kwon, Wooseok Kang, Juneyoung Lee et al.ICSE 2024 · 19 citations
- Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-ExecutionNaomi Smith, Abhishek Sharma, John Renner, David Thien et al.SOSP 2024 · 17 citations
- Speeding up SMT Solving via Compiler OptimizationBenjamin Mikek, Qirun ZhangFSE 2023 · 11 citations
Builds on6
- HACL*: A Verified Modern Cryptographic LibraryJean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin BeurdoucheCCS 2017 · 258 citations
- CodeAlchemist: Semantics-Aware Code Generation to Find Vulnerabilities in JavaScript EnginesHyungSeok Han, DongHyeon Oh, Sang Kil ChaNDSS 2019 · 178 citations
- SoK: Computer-Aided CryptographyManuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet et al.S&P 2021 · 169 citations
- Site Isolation: Process Separation for Web Sites within the BrowserCharles Reis, Alexander Moshchuk, Nasko OskovUSENIX Security 2019 · 105 citations
- A Call to ARMs: Understanding the Costs and Benefits of JIT Spraying MitigationsWilson Lian, Hovav Shacham, Stefan SavageNDSS 2017 · 7 citations
Related papers
- Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernelLuke Nelson, Jacob Van Geffen, Emina Torlak, Xi WangOSDI 2020 · 72 citations
- Verifying the Verifier: eBPF Range Analysis VerificationHarishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, Santosh NagarakatteCAV 2023 · 37 citations
- Understanding and Finding JIT Compiler Performance BugsZijian Yi, Cheng Ding, August Shi, Milos GligoricOOPSLA 2026
- FUZZILLI: Fuzzing for JavaScript JIT Compiler VulnerabilitiesSamuel Groß, Simon Koch, Lukas Bernhard, Thorsten Holz et al.NDSS 2023
- FuzzJIT: Oracle-Enhanced Fuzzing for JavaScript Engine JIT CompilerJunjie Wang, Zhiyi Zhang, Shuang Liu, Xiaoning Du et al.USENIX Security 2023
