Model-Based Static Source Code Analysis of Java Programs with Applications to Android Security

We combine static analysis techniques with model- based deductive verification using SMT solvers to provide a framework that, given an analysis aspect of the source code, automatically generates an analyzer capable of inferring information about that aspect. The analyzer is generated by translating the collecting semantics of a program to a "marked" formula in first order logic over multiple underlying theories. The "marking" can be thought of as a set of holes or contexts corresponding to the "uninterpreted" APIs invoked in the program. Just as a program imports packages and uses methods from classes in those packages, we import the semantics of the API invocations as first order logic assertions. These assertions constitute the models used by the analyzer. Logical specification of the desired program behavior (rather its negation) is incorporated as a first order logic formula. An SMT-LIB formula solver treats the combined formula as a "constraint" and "solves" it. The "solved form" can be used to identify logical (security) errors in Java (Android) programs. Security properties of Android are represented as constraints and the analysis aims to show that these constraints are respected.