We will present the Phasar framework at the PLDI 2018 conference held in Philadelphia, Pennsylvania, United States.
We have implemented Phasar, a novel static-analysis framework on top of LLVM. Phasar provides various solvers that allow the solving of arbitrary monotone data-flow problems (distributive or not) in a fully automated manner. A user just has to provide the specific description of the problem to solve.
Phasar’s solver supports a context and flow-sensitive analysis, which is notoriously hard to scale.
Also, the C and C++ programming languages make it especially hard to statically analyze. This is due to their deliberately unsafe type system, function pointers and in case of C++ virtual dispatch and other powerful language constructs.
We will explain how Phasar uses summaries, tabulation and a compositional analysis approach to nevertheless scale to actual applications with millions of lines of code.
We will give an introduction to the framework, explain its relationship to LLVM, its architecture, and give hands-on examples of how to implement useful example analyses with Phasar. For the examples we will focus on security applications.
Before the tutorial, we will release Phasar as a well documented open-source project on Github.