/attestor

A Shape Analysis Tool based on Graph Grammars

Primary LanguageJavaGNU General Public License v3.0GPL-3.0

Build Status Attestor Benchmarks Status Attestor on Maven Central License: GPL v3 Languages Last update

Attestor is a graph-based tool for analysing Java programs operating on dynamic data structures. It involves the generation of an abstract state space employing user-supplied graph grammars or, alternatively, formulas in a fragment of symbolic heap separation logic. LTL model checking is then applied to the generated state space, supporting both structural and functional correctness properties. The analysis is fully automated, procedure-modular, and provides visual feedback including counterexamples in case of property violations. As an alternative to graphs, Attestor also supports a fragment of symbolic heap separation logic with user-supplied inductive predicate definitions as an input.

Contents

Quickstart

Documentation

People & Publications

Quickstart

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 unbounded state spaces arising from dynamic data structures, 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 automatically 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 characterised 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.
  • Alternatively to graph grammars, a fragment of symbolic heap separation logic with inductive predicate definitions is supported as an input language.
  • 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 exact preservation of the 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.
  • Tool 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:

  • Java JDK 1.8
  • Apache Maven
  • Since Attestor uses soot, please make sure that rt.jar is in your CLASSPATH and that JAVA_HOME is set correctly.

Both the README and the Wiki cover Attestor version 0.4.0. Please confer previous revisions for documentation of older versions.

Reproducing Benchmarks

We distribute executable bundles consisting of the latest stable Attestor version together will all benchmarks on maven central. To run benchmarks on the latest version of Attestor, please proceed as follows.

Unix-based operating systems
 $ git clone https://github.com/moves-rwth/attestor-examples.git
 $ chmod +x run.sh
 $ ./run.sh
All operating systems
 $ git clone https://github.com/moves-rwth/attestor-examples.git
 $ mvn clean install exec:exec@run

Given the system requirements, no installation of Attestor is required to reproduce and comprehend previously reported benchmark results. We collect all benchmarks in a separate repository including auxiliary scripts to install, run and evaluate all benchmarks. Please confer the documentation in the benchmark repository for further details.

Installation

We distribute executable .jar files of stable Attestor releases on maven central. To install the latest version of Attestor, please proceed as follows:

$ 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.

Getting Started

After installation, an executable jar file is created in the directory target within the cloned repository. The name of executable jar is of the form

 attestor-<VERSION>-jar-with-dependencies.jar

where <VERSION> is the previously cloned version of the Attestor repository. To execute Attestor, it suffices to run

 $ java -jar attestor-<VERSION>-jar-with-dependencies.jar

from within the target directory. This should display a help page explaining all available command line options. Since the above jar file contains all dependencies, it is safe to rename it and move the file to a more convenient directory.

A Guided Tour

An instructive example with step-by-step instructions on using Attestor to analyze Java programs is found in our Wiki.

Furthermore, we maintain a collection of running examples (including source code, user-defined graph grammars, and configuration files) in a separate repository. All of these examples can be directly executed using provided auxiliary scripts. Please confer the documentation in the examples repository for further details.

Documentation

Options & Settings

Attestor can be configured using various command line options. Alternatively, it is possible to store such a configuration in a dedicated settings file. In particular, the options allow to pass linear temporal logic specifications to be verified for the provided Java program.

It is possible to manually supply graph grammars, initial heaps, and contracts to Attestor.

Since version 0.4.0, it is also possible to provide specifications in a restricted fragment of symbolic heap separation logic with inductive predicate definitions. This means that a symbolic heap can be supplied as an initial heap. Moreover, a system of inductive predicate definitions may be supplied instead of a graph grammar.

Please confer the respective page for further details on all options.

Graphical User Interface

State spaces, counterexamples, contracts, and graph grammars can be exported by Attestor to a webpage for graphical exploration. The corresponding export options are found here.

A brief explanation of our graphical notation for heap configurations is found here. Please confer the manual for further information on the features of the graphical user interface.

We provide a small online demo of the graphical user interface for state space exploration. Details about the underlying case study are found in the guided tour. The demo state space is found here.

Architecture

Attestor is organised in modular phases, for example marking generation, state space generation, and model-checking. Please confer our Wiki page on Attestor's architecture for further details.

Glossary

A glossary providing brief explanations of most technical terms is found in our Wiki.

People & Publications

People

Attestor is developed by the Chair for Software Modeling and Verification at RWTH Aachen University by

Publications