VEX, as part of Valgrind, is well-established in the world of dynamic analysis. However, there are certain questions that are best answered by symbolic analyses. In this talk I will describe the ideas behind symbolic analysis, detail challenges frequently faced when attempting to implement it, and introduce the work ongoing at UC Santa Barbara to use VEX to address these challenges, and implement a large-scale symbolic analysis system.
VEX is designed and widely used in dynamic analysis, in the form of Valgrind. Barring some implementation issues, VEX's side-effects-free, mostly-architecture-independent implementation provides an effective base on which to build non-dynamic analyses, as well. Specifically, we have used VEX to implement architecture-independent static and symbolic analyses.
Symbolic analysis is an active area of research, and many challenges are faced when attempting to implement it. These challenges include tradeoffs between tractability and precision when reasoning about symbolic memory, the NP-completeness of the underlying SMT-solving algorithms, difficult-to-analyze program actions, and many others. Some of these challenges are unsolveable, but compromises can be made to achieve useful results with symbolic analysis. This talk attempts to outline these challenges, describe some solutions, and provide a guide for parties interested in symbolic analysis with VEX.
Speakers: Yan Shoshitaishvili