Towards a verified range analysis for JavaScript JITs
Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan
2020年份
28被引次数
11顶会引用
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式，引用它的顶会 Paper 也一样。你提问，回答直接引用原文。
引用它的顶会 Paper11
- 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 次
- Compiler Testing using Template Java ProgramsZhiqiang Zang, Nathan Wiatrek, Milos Gligoric, August ShiASE 2022 · 被引用 21 次
- Translation Validation for JIT Compiler in the V8 JavaScript EngineSeungwan Kwon, Jaeseong Kwon, Wooseok Kang, Juneyoung Lee 等ICSE 2024 · 被引用 19 次
- Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-ExecutionNaomi Smith, Abhishek Sharma, John Renner, David Thien 等SOSP 2024 · 被引用 17 次
- Speeding up SMT Solving via Compiler OptimizationBenjamin Mikek, Qirun ZhangFSE 2023 · 被引用 11 次
它引用的顶会 Paper6
- HACL*: A Verified Modern Cryptographic LibraryJean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin BeurdoucheCCS 2017 · 被引用 258 次
- CodeAlchemist: Semantics-Aware Code Generation to Find Vulnerabilities in JavaScript EnginesHyungSeok Han, DongHyeon Oh, Sang Kil ChaNDSS 2019 · 被引用 178 次
- SoK: Computer-Aided CryptographyManuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet 等S&P 2021 · 被引用 169 次
- Site Isolation: Process Separation for Web Sites within the BrowserCharles Reis, Alexander Moshchuk, Nasko OskovUSENIX Security 2019 · 被引用 105 次
- A Call to ARMs: Understanding the Costs and Benefits of JIT Spraying MitigationsWilson Lian, Hovav Shacham, Stefan SavageNDSS 2017 · 被引用 7 次
相关 Paper
- 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 次
- Verifying the Verifier: eBPF Range Analysis VerificationHarishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, Santosh NagarakatteCAV 2023 · 被引用 37 次
- 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 等NDSS 2023
- FuzzJIT: Oracle-Enhanced Fuzzing for JavaScript Engine JIT CompilerJunjie Wang, Zhiyi Zhang, Shuang Liu, Xiaoning Du 等USENIX Security 2023
