HoRSt

Horn clause based sound static analysis

HoRSt is a novel language and framework to help designers of static analyses. HoRSt was first developed to be used in eThor, a sound static analyzer for Ethereum smart contracts.

Try HoRSt

You can get either build HoRSt from the latest sources (follow the instructions in README.md) or download a precompiled jar.

Documentation

HoRSt (short for Horn clause Reasoning for Static analysis) is a specification language for defining static analyzers based on Horn clauses.

Who should use HoRSt?

We intended HoRSt to be a tool for researchers and industry that want to design static analysis tools for programming languages. One approach to static analysis that proved to be very successful in the last years is to model (an abstraction of) the semantics of a programming language in Horn clauses and to then to leverage exiting SMT solvers with reachability engines (in particular z3) to answer reachability queries on this semantics. However, programming such an analysis from scratch, turned to be error-prone: The input to SMT-solvers needed to be created either via specific APIs or by generating smt-lib output - the low-level standardized input format for SMT-solvers. As a consequence, analysis specification and implementation were usually intermingled. This resulted in lacking

  • readability and compliance: Either no formal (readable) specification of the static analysis was provided in the end, or there were huge gaps between an existing pen and paper formalization and the final implementation.
  • variability: Little changes in the analysis specification required major reworking of the whole analyzer. This is particularly problematic since designing a performant static analysis is an iterative process with many evolution steps.
  • re-usability: Many optimizations needed to be reimplemented for each static analysis.

HoRSt aims at tackling these issues by providing a high-level specification format for Horn clauses that compiles to z3-compatible smt-lib format. The language provides high-level language constructs (such as custom data types, pattern matching, user-defined functions and bounded iteration) that makes specification convenient and readable. It allows for the specification of a neat interface with domain-specific components (for e.g., interfacing with parsers or pre-analysis engines) and hence provides flexibility to be used in different domains.

The HoRSt language

For a brief introduction to the HoRSt language, we refer the reader to our current research paper:

Interfaces

A key concept of HoRSt are the user defined interfaces called selector functions that can be used in the Horn Clause definitions and that are implemented by Java functions. The idea of selector functions is that the general semantics of a programming language needs to be ultimately indexed by a concrete program in order to analyze this specific program. This indexing can be done in manifold ways: Either just a set of Horn clauses that corresponds to a program-specific initialization needs to be produced, or the Horn clauses to be generated in the first place depend on the program itself (e.g. individual horn clauses are produced for each program location). For a flexible and generic way of interfacing, we allow for the specification of indexed relations over the base types int and bool. These indexed relations are defined by functions taking as input a tuple of base values and returning a relation (a set of tuples) of base values. A very simple example is the following interval selector function as it would be declared in HoRSt:

sel interval: int * int -> [int];

This function takes as argument two integer values (representing lower bound l and the upper bound u of an interval) and returns a set of numbers - the numbers from l to u-1. This functionality, however, needs to be implemented first. This is done by a so called selector function provider. A selector function provider is a Java source code file (class) that implements public methods matching the selector functions declared in the HoRSt file. Matching in this case means that it needs to have the same name and a fitting type: where int is represented by BigInteger in Java, bool is represented by Boolean, and tuples of int and bool are represented by the classes in wien.secpriv.horst.data.tuples, e.g. Tuple2<BigInteger, Boolean> for int*bool. A corresponding method implementing the interval function could look as follows:

    public Iterable<BigInteger> interval(BigInteger start, BigInteger end) {
        return new Iterable<BigInteger>() {
            @Override
            public Iterator<BigInteger> iterator() {
                return new Iterator<BigInteger>() {
                    BigInteger state = start;

                    @Override
                    public boolean hasNext() {
                        return state.compareTo(end) < 0;
                    }

                    @Override
                    public BigInteger next() {
                        BigInteger ret = state;
                        state = state.add(BigInteger.ONE);
                        return ret;
                    }
                };
            }
        };
    }

Generating an analyzer using HoRSt

HoRSt is meant to be used as a component of a (program) analyzer which provides the infrastructure for parsing a program and potentially conducting pre-analyses.

It can be used in two different ways. The simplest one (best suited for ad-hoc developments and experiments) is to build HoRSt and to execute it from the command line as follows:

java -jar horst.jar <options> -s <HoRSt specification> -f <selector function providers>

  • The flag -s allows for providing several HoRSt files (in .txt format). Those can contain rules as well as queries and will simply be concatenated in the given order.

  • The flag -f allows for providing several selector function providers (.java files) that are required to implement the selector functions declared in the provided HoRSt specification. Non.java parameters following the -f flag are interpreted as arguments to the preceding .java file. These arguments (containing e.g. the program to be analyzed) can be accessed in the selector function provider by implementing a constructor taking a single List<String> as argument. This mechanism can hence be used to prototype simple analyzers in a single .java file: The constructor of the contained class (either the default one or, if available, a constructor taking List<String> as argument) is executed before the HoRSt compiler. In this way, state accessed by the actual selector functions can be initialized depending on the input (e.g. the program can be parsed and selector functions can access the resulting program information). This approach of course only scales for very simple developments since it requires all functionality to be implemented in a single file.

For more involved projects we recommend to use HoRSt as a dependency and to use the corresponding HorSt methods to invoke the HoRSt compilation pipeline from within the project as needed. For an example of such an integration, we refer the reader to the eThor project (in particular the EvmHostCompiler class).