This work aims to implement a type based analysis based on the Checker Framework (https://checkerframework.org). The project consists of two components.
Some relatively complete Java syntax can be found at (https://users-cs.au.dk/amoeller/RegAut/JavaBNF.html) or (http://homepage.cs.uiowa.edu/~fleck/JavaBNF.htm), as specified in BNF.
The analysis produces a mapping that assigns a reference-typed variable to a set of heap objects, usually indicated by their creation sites in the program. We focus on two categories of variables --- local variables and fields. The initial type can be either null, as indicated by an empty set, or be a new statement "var = new C(...)" at line number abc which gives a singleton set {abc}. This set of points-to is propagated through assignments, as method call parameters, or as method call return values. We join the types in spirit of Andersen's subset based construction. This computes the may points-to information for all reference-typed local variables and fields as a result.
The algorithm for information flow analysis is based on the Dual-Access Labels (DAL), so that an object o can be labelled by a pair of access privileges (Acc, Cap), specifying the accessiblity (the privilege required to access o) and the capability (the privilege that is owned by o). When two labels (Acc1, Cap1) and (Acc2, Cap2) are joined, the combined accessibility may become larger (practically, it may be defined as the set union of Acc1 and Acc2), while the combined capability may shrink (may be defined as the set intersection of Cap1 and Cap2).
When computing the DAL on referenced heap objects, the algorithm collects points-to information for a given reference typed variable as computed in the previous step, and applies the join operation on all the objects that may be pointed-to as a conservative approximation. The initial security requirement is given in the form of annotations. For the details we refer to the technical report that is being developed in this repo.