The project investigates techniques for scaling precise symbolic security analysis data-flow-based compliance checking for Java Web-applications. The project is based on Jaint, a JVM bytecode analysis framework combining multi-color taint analysis with dynamic symbolic execution for Java Web-applications.
We have demonstrated the effectiveness of Jaint in the past: the current prototypical implementation solves all tasks in the OWASP benchmark with perfect accuracy.
The scalability of the approach crucially depends on the capabilities of the Java virtual machine that is used for executing programs and requires four features of the virtual machine:
- symbolic annotation of bytecode instructions,
- annotation of values on the heap and stack,
- injection of mock implementations for certain methods, and
- notifications on method invocations and returns.
The first version of Jaint is built on top of the Java PathFinder virtual machine, a partial JVM implementation that is part of the Java PathFinder model checker. This VM served well for initial results, but missing features hamper application to industrial scale applications.
Hence, the project develops a scalable dynamic symbolic execution and taint analysis, GDart (Dart on GraalVM), for the Espresso Java virtual machine. Espresso is a full-fledged Java virtual machine that is implemented as a guest language for the polyglot Graal virtual machine.
- Amazon Research Award, Spring 2021