Skip to content

Home

Jump to bottom
Christoph Matheja edited this page Mar 21, 2018 · 29 revisions

Contents

What is Attestor?

Pointers constitute an essential concept in modern programming languages, and are used for implementing dynamic data structures like lists, trees etc. However, many software bugs can be traced back to the erroneous use of pointers by e.g. dereferencing null pointers or accidentally pointing to wrong parts of the heap. Due to the resulting unbounded state spaces, pointer errors are hard to detect. Automated tool support for validation of pointer programs that provides meaningful debugging information in case of violations is therefore highly desirable.

Attestor is a verification tool that attempts to achieve both of these goals. To this aim, it first constructs an abstract state space of the input program by means of symbolic execution. Each state depicts both links between heap objects and values of program variables using a graph representation. Abstraction is performed on state level by means of graph grammars. They specify the data structures maintained by the program, and describe how to summarise substructures of the heap in order to obtain a finite representation. After labelling each state with propositions that provide information about structural properties such as reachability or heap shapes, the actual verification task is performed in a second step. To this aim, the abstract state space is checked against a user-defined LTL specification. In case of violations, a counterexample is provided.

In summary, Attestor's main features can be characterized as follows:

  • It employs context-free graph grammars as a formal underpinning for defining heap abstractions.These grammars enable local heap concretisation and thus naturally provide implicit abstract semantics.
  • The full instruction set of Java bytecode is handled. Program actions that are outside the scope of our analysis, such as arithmetic operations or Boolean tests on payload data, are handled by (safe) over-approximation.
  • Specifications are given by linear-time temporal logic (LTL) formulae which support a rich set of program properties, ranging from memory safety over shape, reachability or balancedness to properties such as full traversal or preservation of the exact heap structure.
  • Except for expecting a graph grammar that specifies the data structures handled by a program, the analysis is fully automated. In particular, no program annotations are required.
  • Modular reasoning is supported in the form of contracts that summarise the effect of executing a (recursive) procedure. These contracts can be automatically derived or manually specified.
  • Feedback is provided through a comprehensive report including (minimal) non-spurious counterexamples in case of property violations.
  • Its functionality is made accessible through the command line as well as a graphical user and an application programming interface.

System Requirements

The following software has to be installed prior to the installation of Attestor:

Installation

$ git clone https://github.com/moves-rwth/attestor.git
$ mvn install

Please note that the installation requires an internet connection as maven will install additional dependencies.

Clone this wiki locally