llStar's theory is based on separation logic, and performs symbolic execution on bitcode programs given as input. To perform this task, it interfaces with the coreStar tool. More precisely, the architecture of the tool is as follows, where wavy boxes indicate user input.
Given a bitcode program and specs for its functions as input, llStar attempts to formally prove it correct. Its output is either "yes" is it finds a proof, or "no" if it cannot. The existence of a proof guarantees that formal correctness has been established (the program satisfies its specs, and is memory safe). Its absence, however, can be due either to a real bug in the program, or a weakness of llStar's proof system. In the latter scenario, the user may refine both the specs it wants to prove and llStar's internal logic to get a proof.
The program to verify, in the form of
a bitcode module. llStar uses
LLVM to parse this file, and to retrieve the memory layout of the data
structures defined on the file (e.g. offsets and padding of
Specifications for the functions defined and used in the bitcode module.
coreStar is an open-source symbolic execution and frame inference engine f or separation logic. Bitcode programs are translated into coreStar's generic language of assignments (defined by their specs), gotos and labels. We include the latest development version of coreStar in llStar.
Rules generated by llStar
When performing symbolic execution
of programs, coreStar needs to manipulate the formula describing the
current state. The base theory of coreStar is agnostic in the
predicates used to describe symbolic states. To cope with user-defined
predicates (such as our
additional logic rules have to be given to coreStar. llStar
generates the rules needed to analyse a bitcode module automatically,
for instance to unfold pointers to a structure into pointers to each
field of the structure. Some of these rules will be the same for every
module, and can be found in the
Rules provided by the user
Users of llStar may define their own set of rules on top of llStar. Two examples are included in the distribution: rules to reason about singly-linked lists ( rules/lseg.logic and rules/lseg.abs ) and rules to reason about binary directed acyclic graphs ( rules/dags_const_pointers.logic ). The soundness and termination of the system of rules are currently the responsibility of the user.
At many points during the symbolic execution, queries have to be made to an SMT solver by coreStar. Our SMT solver of choice is z3.