More Like this

1. Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution

   Smith, Naomi ; Sharma, Abhishek ; Renner, John ; Thien, David ; Brown, Fraser ; Shacham, Hovav ; Jhala, Ranjit ; Stefan, Deian ( November 2024 , Association for Computing Machinery)

   Arpaci-Dusseau, Andrea ; Keeton, Kimberly (Ed.)

   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. 

   more » « less
2. Java JIT Testing with Template Extraction

   https://doi.org/10.1145/3643777  

   Zang, Zhiqiang ; Yu, Fu-Yao ; Thimmaiah, Aditya ; Shi, August ; Gligoric, Milos ( July 2024 , Proceedings of the ACM on Software Engineering)

   We present LeJit, a template-based framework for testing Java just-in-time (JIT) compilers. Like recent template-based frameworks, LeJit executes a template---a program with holes to be filled---to generate concrete programs given as inputs to Java JIT compilers. LeJit automatically generates template programs from existing Java code by converting expressions to holes, as well as generating necessary glue code (i.e., code that generates instances of non-primitive types) to make generated templates executable. We have successfully used LeJit to test a range of popular Java JIT compilers, revealing five bugs in HotSpot, nine bugs in OpenJ9, and one bug in GraalVM. All of these bugs have been confirmed by Oracle and IBM developers, and 11 of these bugs were previously unknown, including two CVEs (Common Vulnerabilities and Exposures). Our comparison with several existing approaches shows that LeJit is complementary to them and is a powerful technique for ensuring Java JIT compiler correctness.

    

   more » « less
3. Visualizing JIT Compiler Graphs

   Lim, HeuiChan ; Kobourov, Stephen ( September 2021 , 29th International Symposium on Graph Drawing and Network Visualization (GD 2021))

   null (Ed.)

   Just-in-time (JIT) compilers are used by many modern programming systems in order to improve performance. Bugs in JIT compilers provide exploitable security vulnerabilities and debugging them is difficult as they are large, complex, and dynamic. Current debugging and visualization tools deal with static code and are not suitable in this domain. We describe a new approach for simplifying the large and complex intermediate representation, generated by a JIT compiler and visualize it with a metro map metaphor to aid developers in debugging. 

   more » « less
4. Methodologies for Quantifying (Re-)randomization Security and Timing under JIT-ROP

   https://doi.org/10.1145/3372297  

   Salman Ahmed, Ya Xiao ( January 2020 , 2020 ACM SIGSAC Conference on Computer and Communications Security (CCS'20))

   null (Ed.)

   Just-in-time return-oriented programming (JIT-ROP) allows one to dynamically discover instruction pages and launch code reuse attacks, effectively bypassing most fine-grained address space layout randomization (ASLR) protection. However, in-depth questions regarding the impact of code (re-)randomization on code reuse attacks have not been studied. For example, how would one compute the re-randomization interval effectively by considering the speed of gadget convergence to defeat JIT-ROP attacks? ; how do starting pointers in JIT-ROP impact gadget availability and gadget convergence time? ; what impact do fine-grained code randomizations have on the Turing-complete expressive power of JIT-ROP payloads? We conduct a comprehensive measurement study on the effectiveness of fine-grained code randomization schemes, with 5 tools, 20 applications including 6 browsers, 1 browser engine, and 25 dynamic libraries. We provide methodologies to measure JIT-ROP gadget availability, quality, and their Turing-complete expressiveness, as well as to empirically determine the upper bound of re-randomization intervals in re-randomization schemes using the Turing-complete (TC), priority, MOV TC, and payload gadget sets. Experiments show that the upper bound ranges from 1.5 to 3.5 seconds in our tested applications. Besides, our results show that locations of leaked pointers used in JIT-ROP attacks have no impacts on gadget availability but have an impact on how fast attackers find gadgets. Our results also show that instruction-level single-round randomization thwarts current gadget finding techniques under the JIT-ROP threat model. 

   more » « less
5. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel

   Nelson, Luke ; Van Geffen, Jacob ; Torlak, Emina ; Wang, Xi ( January 2020 , 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20))

   This paper describes our experience applying formal meth- ods to a critical component in the Linux kernel, the just-in-time compilers (“JITs”) for the Berkeley Packet Filter (BPF) virtual machine. We verify these JITs using Jitterbug, the first frame- work to provide a precise specification of JIT correctness that is capable of ruling out real-world bugs, and an automated proof strategy that scales to practical implementations. Using Jitterbug, we have designed, implemented, and verified a new BPF JIT for 32-bit RISC-V, found and fixed 16 previously unknown bugs in five other deployed JITs, and developed new JIT optimizations; all of these changes have been upstreamed to the Linux kernel. The results show that it is possible to build a verified component within a large, unverified system with careful design of specification and proof strategy. 

   more » « less