Static Analysis

Contemporary programs are complex systems whose implicit behaviors are not necessarily known to the program’s developers. This can lead to severe consequences when attackers exploit these implicit and unintended behaviors to steal financial assets or confidential data. Static analysis is a family of techniques to assess the presence or absence of certain program behaviors by examining the program source code. It can thus increase the trust developers have in their systems and prevent harm from happening to users.


The scope of static analysis spans from simple style checkers to complex models of program behavior—the solutions developed in the “Security and Privacy” group fall in the second category. In particular, we are interested in sound static analysis, meaning that we can give guarantees on the absence of vulnerabilities.

This involves formally modeling or over-approximating all possible program behaviors, which requires a deep understanding of the program’s execution environment—may it be a website, a smart contract, or a mobile device.


The tools we are developing are intended to be used by practitioners that may not be experts in static analysis. Therefore, we strive to minimize the amount of input that has to be provided to our analyses and achieve complete automation in most cases.

Soundness, automation, and performance are at odds with each other, so achieving all three of them is challenging.


Since the implementation of and experimentation with automated sound static analysis tools has recurring patterns, we developed the HoRSt framework to take care of those. HoRSt provides a uniform, high-level and declarative language to specify Horn-clause-based static analyses. It can target multiple backends (SMT-engines like z3 or the datalog engine souffle) and offers generic optimizations from which all analyses using HoRSt can profit.

eThor is a sound static reentrancy analyzer for the Ethereum Virtual Machine and the first tool to use HoRSt.