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.
Soundness
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.
Automation
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.
Reusability
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.
Main directions of our research include:
- Cryptography for Privacy
Zero-knowledge proofs and blockchains - Provably secure and efficient cryptography
Design of cryptographic schemes and optimization for specific applications - Scalability and Interoperability of Blockchains
Payment channels and blockchain protocols - Web security
Formal verification of web protocols and standards - Secure Systems Lab
Applied systems security (mobiles, IoT) and malware analysis and detection