Wiki

Clone wiki

llStar / Architecture

Overview

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.

llStar architecture

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.

Bitcode

bitcode 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 fields inside structs).

Specifications

specs Specifications for the functions defined and used in the bitcode module.

coreStar

coreStar 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

bitcode rules 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 pointer and malloced above), 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/ directory.

Rules provided by the user

user rules 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.

SMT solver

SMT solver 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.

Updated