More Like this

1. 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
2. Automated bug localization in JIT compilers

   https://doi.org/10.1145/3453933.3454021  

   Lim, HeuiChan ; Debray, Saumya ( April 2021 , Proceedings of the 17th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments (VEE ’21))

   null (Ed.)

   Many widely-deployed modern programming systems use just-in-time (JIT) compilers to improve performance. The size and complexity of JIT-based systems, combined with the dynamic nature of JIT-compiler optimizations, make it challenging to locate and fix JIT compiler bugs quickly. At the same time, JIT compiler bugs can result in exploitable security vulnerabilities, making rapid bug localization important. Existing work on automated bug localization focuses on static code, i.e., code that is not generated at runtime, and so cannot handle bugs in JIT compilers that generate incorrect code during optimization. This paper describes an approach to automated bug localization in JIT compilers, down to the level of distinct optimization phases, starting with a single initial Proof-of-Concept (PoC) input that demonstrates the bug. Experiments using a prototype implementation of our ideas on Google’s V8 JavaScript interpreter and TurboFan JIT compiler demonstrates that it can successfully identify buggy optimization phases. 

   more » « less
3. A Framework for Automatic Exploit Generation for JIT Compilers

   https://doi.org/10.1145/3465413.3488573  

   Kang, Xiyu ; Debray, Saumya ( November 2021 , Checkmate '21: Proceedings of the 2021 Research on offensive and defensive techniques in the Context of Man At The End (MATE) Attacks)

   Kwon, Yonghwi ; Banescu, Sebastian (Ed.)

   This paper proposes a framework for automatic exploit generation in JIT compilers, focusing in particular on heap corruption vulnerabilities triggered by dynamic code, ie, code generated at runtime by the JIT compiler. The purpose is to help assess the severity of vulnerabilities and thereby assist with vulnerability triage. The framework consists of two components: the first extracts high-level representations of exploitation primitives from existing exploits, and the second uses the primitives so extracted to construct exploits for new bugs. We are currently building a prototype implementation of the framework focusing on JavaScript JIT compilers. To the best of our knowledge, this is the first proposal to consider automatic exploit generation for code generated dynamically by JIT compilers. 

   more » « less
4. Modeling code manipulation in JIT compilers

   https://doi.org/10.1145/3520313.3534656  

   Lim, HeuiChan ; Kang, Xiyu ; Debray, Saumya ( June 2022 , Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis)

   Gonnord, Laure ; Titolo, Laura (Ed.)

   Just-in-Time (JIT) compilers are widely used to improve the performance of interpreter-based language implementations by creating optimized code at runtime. However, bugs in the JIT compiler’s code manipulation and optimization can result in the generation of incorrect code. Such bugs can be difficult to diagnose and fix, and can result in exploitable vulnerabilities. Unfortunately, existing approaches to automatic bug localization do not carry over well to such bugs. This paper discusses a different approach to analyzing JIT compiler optimization behaviors, based on using dynamic analysis to construct abstract models of the JIT compiler’s optimizer and back end. By comparing the models obtained for buggy and non-buggy executions of the JIT compiler, we can pinpoint the components of the JIT compiler’s internal representation that have been affected by the bug; this can then be mapped back to identify the buggy code. Our ex- periments with two real bugs for Google V8 JIT compiler, TurboFan, show the utility and practicality of our approach. 

   more » « less
5. Enhanced compiler bug isolation via memoized search

   https://doi.org/10.1145/3324884.3416570  

   Chen, Junjie ; Ma, Haoyang ; Zhang, Lingming ( December 2020 , IEEE/ACM International Conference on Automated Software Engineering)

   null (Ed.)

   Compiler bugs can be disastrous since they could affect all the software systems built on the buggy compilers. Meanwhile, diagnosing compiler bugs is extremely challenging since usually limited debugging information is available and a large number of compiler files can be suspicious. More specifically, when compiling a given bug-triggering test program, hundreds of compiler files are usually involved, and can all be treated as suspicious buggy files. To facilitate compiler debugging, in this paper we propose the first reinforcement compiler bug isolation approach via structural mutation, called RecBi. For a given bug-triggering test program, RecBi first augments traditional local mutation operators with structural ones to transform it into a set of passing test programs. Since not all the passing test programs can help isolate compiler bugs effectively, RecBi further leverages reinforcement learning to intelligently guide the process of passing test program generation. Then, RecBi ranks all the suspicious files by analyzing the compiler execution traces of the generated passing test programs and the given failing test program following the practice of compiler bug isolation. The experimental results on 120 real bugs from two most popular C open-source compilers, i.e., GCC and LLVM, show that RecBi is able to isolate about 23%/58%/78% bugs within Top-1/Top-5/Top-10 compiler files, and significantly outperforms the state-of-the-art compiler bug isolation approach by improving 92.86%/55.56%/25.68% isolation effectiveness in terms of Top-1/Top-5/Top-10 results. 

   more » « less