Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution
Pages 473 - 487
Abstract
Just-in-time (JIT) compilers make JavaScript run efficiently by replacing slow JavaScript interpreter code with fast machine code. However, this efficiency comes at a cost: bugs in JIT compilers can completely subvert all language-based (memory) safety guarantees, and thereby introduce catastrophic exploitable vulnerabilities. We present Icarus: a new framework for implementing JIT compilers that are automatically, formally verified to be safe, and which can then be converted to C++ that can be linked into browser runtimes. Crucially, we show how to build a JIT with Icarus such that verifying the JIT implementation statically ensures the security of all possible programs that the JIT could ever generate at run-time, via a novel technique called symbolic meta-execution that encodes the behaviors of all possible JIT-generated programs as a single Boogie meta-program which can be efficiently verified by SMT solvers. We evaluate Icarus by using it to re-implement components of Firefox's JavaScript JIT. We show that Icarus can scale up to expressing complex JITs, quickly detects real-world JIT bugs and verifies fixed versions, and yields C++ code that is as fast as hand-written code.
References
[1]
Jason Ansel, Petr Marchenko, Úlfar Erlingsson, Elijah Taylor, Brad Chen, Derek L. Schuff, David Sehr, Cliff L. Biffle, and Bennet Yee. 2011. Language-Independent Sandboxing of Just-in-Time Compilation and Self-Modifying Code. In PLDI. ACM.
[2]
Abhishek Arya and Cris Neckar. 2012. Fuzzing for Security. Online: https://blog.chromium.org/2012/04/fuzzing-for-security.html.
[3]
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek. 2021. Formally Verified Speculation and Deoptimization in a JIT Compiler. In POPL. ACM.
[4]
Aurèle Barrière, Sandrine Blazy, and David Pichardie. 2020. Towards Formally Verified Just-in-Time Compilation. In CoqPL.
[5]
Aurèle Barrière, Sandrine Blazy, and David Pichardie. 2023. Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. In POPL. ACM.
[6]
Lukas Bernhard, Tobias Scharnowski, Moritz Schloegel, Tim Blazytko, and Thorsten Holz. 2022. JIT-picking: Differential fuzzing of JavaScript engines. In CCS. ACM.
[7]
Fraser Brown, John Renner, Andres Noetzli, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020. Towards a Verified Range Analysis for JavaScript JITs. In PLDI. ACM.
[8]
Craig Chambers, David Ungar, and Elgin Lee. 1989. An Efficient Implementation of SELF, a Dynamically-Typed Object-Oriented Language based on Prototypes. ACM SIGPLAN Notices 24, 10 (1989).
[9]
Chromium Issue Tracker 2023. Security: [0-day] Bug in the Handling of the Arguments Object. Online: https://issues.chromium.org/issues/40065138.
[10]
Willem De Groef, Nick Nikiforakis, Yves Younan, and Frank Piessens. 2010. JITSec: Just-in-time Security for Code Injection Attacks. In WISSEC.
[11]
Jan de Mooij, Matthew Gaudet, Iain Ireland, Nathan Henderson, and J Nelson Amaral. 2023. CacheIR: The Benefits of a Structured Representation for Inline Caches. In MPLR. ACM.
[12]
L Peter Deutsch and Allan M Schiffman. 1984. Efficient Implementation of the Smalltalk-80 System. In POPL. ACM.
[13]
Sung Ta Dinh, Haehyun Cho, Kyle Martin, Adam Oest, Kyle Zeng, Alexandros Kapravelos, Gail-Joon Ahn, Tiffany Bao, Ruoyu Wang, Adam Doupé, et al. 2021. Favocado: Fuzzing the Binding Code of JavaScript Engines Using Semantically Correct Test Cases. In NDSS. Internet Society.
[14]
Stefano Dissegna, Francesco Logozzo, and Francesco Ranzato. 2016. An Abstract Interpretation-Based Model of Tracing Just-in-Time Compilation. ACM TOPLAS 38, 2 (2016).
[15]
Jeremy Fetiveau. 2019. Circumventing Chrome's Hardening of Typer Bugs. Online: https://doar-e.github.io/blog/2019/05/09/circumventing-chromes-hardening-of-typer-bugs/.
[16]
Tommaso Frassetto, David Gens, Christopher Liebchen, and Ahmad-Reza Sadeghi. 2017. JITGuard: Hardening Just-in-Time Compilers with SGX. In CCS. ACM.
[17]
Matthew Gaudet. 2023. An Inline Cache isn't Just a Cache. https://www.mgaudet.ca/technical/2018/6/5/an-inline-cache-isnt-just-a-cache.
[18]
Sergei Glazunov. 2021. In-the-Wild Series: Chrome Infinity Bug. Online: https://googleprojectzero.blogspot.com/2021/01/in-wild-series-chrome-infinity-bug.html.
[19]
Samuel Groß. 2024. The V8 Sandbox. Online: https://v8.dev/blog/sandbox.
[20]
Samuel Groß, Simon Koch, Lukas Bernhard, Thorsten Holz, and Martin Johns. 2023. FUZZILLI: Fuzzing for JavaScript JIT Compiler Vulnerabilities. In NDSS. Internet Society.
[21]
Shu-yu Guo and Jens Palsberg. 2011. The Essence of Compiling with Traces. In POPL. ACM.
[22]
HyungSeok Han, DongHyeon Oh, and Sang Kil Cha. 2019. CodeAlchemist: Semantics-Aware Code Generation to Find Vulnerabilities in JavaScript Engines. In NDSS. Internet Society.
[23]
Renáta Hodován and Ákos Kiss. 2016. Fuzzing JavaScript engine APIs. In Integrated Formal Methods. Springer.
[24]
Christian Holler, Kim Herzig, and Andreas Zeller. 2012. Fuzzing with code fragments. In USENIX Security. USENIX.
[25]
Gary Kwong. 2017. JavaScript Fuzzing in Mozilla, 2017. Slides online: https://nth10sd.github.io/js-fuzzing-in-mozilla/.
[26]
Akash Lal and Shaz Qadeer. 2013. Reachability Modulo Theories. In Reachability Problems. Springer.
[27]
K. Rustan M. Leino. 2008. This is Boogie 2. Online: https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2.
[28]
Sorin Lerner, Todd Millstein, and Craig Chambers. 2003. Automatically Proving the Correctness of Compiler Optimizations. In PLDI. ACM.
[29]
Xavier Leroy. 2006. Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant. In POPL. ACM.
[30]
Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2018. Practical Verification of Peephole Optimizations with Alive. Commun. ACM 61, 2 (2018), 84--91.
[31]
Mozilla. 2020. Security Severity Ratings/Client. Online: https://wiki.mozilla.org/Security_Severity_Ratings/Client.
[32]
Mozilla Bugzilla 2021. Crash [@ ??] or Assertion failure: Expecting length to fit in int32, at jit/VMFunctions.cpp:2789. Online: https://bugzilla.mozilla.org/show_bug.cgi?id=1685925.
[33]
Magnus O. Myreen. 2010. Verified Just-in-Time Compiler on x86. In POPL. ACM.
[34]
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. In SOSP. ACM.
[35]
Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In OSDI. USENIX.
[36]
Ben Niu and Gang Tan. 2014. RockJIT: Securing Just-in-Time Compilation using Modular Control-Flow Integrity. In CCS. ACM.
[37]
Soyeon Park, Wen Xu, Insu Yun, Daehee Jang, and Taesoo Kim. 2020. Fuzzing JavaScript Engines with Aspect-Preserving Mutation. In S&P. IEEE.
[38]
Taemin Park, Karel Dhondt, David Gens, Yeoul Na, Stijn Volckaert, and Michael Franz. 2020. NoJITsu: Locking down JavaScript Engines. In NDSS. Internet Society.
[39]
Boris Shingarov. 2019. Formal Verification of JIT by Symbolic Execution. In VMIL. ACM.
[40]
Window Snyder and Mike Shaver. 2007. Building and Breaking the Browser. Black Hat. Slides online: https://www.blackhat.com/presentations/bh-usa-07/Snyder_and_Shaver/Presentation/bh-usa-07-snyder_and_shaver.pdf.
[41]
Maddie Stone and Jared Semrau an James Sadowski. 2024. We're All in this Together: A Year in Review of Zero-Days Exploited In-the-Wild in 2023. Online: https://storage.googleapis.com/gweb-uniblog-publish-prod/documents/Year_in_Review_of_ZeroDays.pdf.
[42]
Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. 2020. Synthesizing JIT Compilers for In-Kernel DSLs. In CAV. Springer.
[43]
Junjie Wang, Bihuan Chen, Lei Wei, and Yang Liu. 2019. Superion: Grammar-Aware Greybox Fuzzing. In ICSE. IEEE.
[44]
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In OSDI. USENIX.
[45]
David Williams-King, Graham Gobieski, Kent Williams-King, James P. Blake, Xinhao Yuan, Patrick Colp, Michelle Zheng, Vasileios P. Kemerlis, Junfeng Yang, and William Aiello. 2016. Shuffler: Fast and Deployable Continuous Code Re-Randomization. In OSDI. USENIX.
[46]
Chao Zhang, Mehrdad Niknami, Kevin Zhijie Chen, Chengyu Song, Zhaofeng Chen, and Dawn Song. 2015. JITScope: Protecting Web Users from Control-Flow Hijacking Attacks. In INFOCOM. IEEE.
[47]
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In POPL. ACM.
Index Terms
- Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution
Index terms have been assigned to the content through auto-classification.
Recommendations
Surgical precision JIT compilers
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationJust-in-time (JIT) compilation of running programs provides more optimization opportunities than offline compilation. Modern JIT compilers, such as those in virtual machines like Oracle's HotSpot for Java or Google's V8 for JavaScript, rely on dynamic ...
Surgical precision JIT compilers
PLDI '14Just-in-time (JIT) compilation of running programs provides more optimization opportunities than offline compilation. Modern JIT compilers, such as those in virtual machines like Oracle's HotSpot for Java or Google's V8 for JavaScript, rely on dynamic ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
November 2024
765 pages
ISBN:9798400712517
DOI:10.1145/3694715
- Chair:
- Emmett Witchel,
- Co-chair:
- Christopher J Rossbach,
- Program Chair:
- Andrea Arpaci-Dusseau,
- Program Co-chair:
- Kimberly Keeton
Copyright © 2024 Copyright held by the owner/author(s).
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).
Sponsors
In-Cooperation
- USENIX
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 November 2024
Check for updates
Qualifiers
- Research-article
Funding Sources
Conference
SOSP '24
Sponsor:
SOSP '24: ACM SIGOPS 30th Symposium on Operating Systems Principles
November 4 - 6, 2024
TX, Austin, USA
Acceptance Rates
SOSP '24 Paper Acceptance Rate 43 of 245 submissions, 18%;
Overall Acceptance Rate 174 of 961 submissions, 18%
Upcoming Conference
SOSP '25
- Sponsor:
- sigops
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 21Total Downloads
- Downloads (Last 12 months)21
- Downloads (Last 6 weeks)21
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in