Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification

Potential supervisors: 
Description: 

Many properties of programs can be characterized by good and bad traces. For example, terminating executions can be marked as good executions, and runs that do not hit a division by zero as bad executions.

However, some advanced properties simultaneously reason about sets of traces, which are known as hyperproperties.  Examples of hyperproperties include information-flow security properties, properties of coding/decoding systems, linearizability and other consistency criteria, most concurrency properties, as well as privacy properties like data minimality. The analysis of such properties is difficult given that (1) in general one cannot verify these properties statically, and (2) at runtime one needs to observe more than one execution trace. Many of such properties are in fact non-monitorable in the sense that there is no runtime monitor that correctly answers Yes/No to the question on whether the property is satisfied or not.

To manage this problem, we propose to use a combination of static verification with runtime verification. By using static verification, one typically obtains a model of the system that allows to limit the source of search for “hypothetical” traces to a sound over-approximation of the runs of the system [1]. The model crafted in this manner is simpler than the system itself. Then, at runtime, the monitor matches observed trace agains the traces from the model to try to decide the hyperproperty.  The goal is to extend the effective
monitorability of hyperproperties to a larger class of systems and
properties.

The main objectives of this master thesis are manifold, and the proposal may be split among many different student projects:
(1) to re-define concurrent properties as relevant hyperproperties;
(2) to design a combined analyser based on static and runtime verification techniques (based on [1]); 
(3) to implement the solution and apply it to suitable case studies.

Practical examples include monitoring the execution of concurrent datatypes [2], which are datatypes that implement simple abstractions like sets or stacks, but are executed by multiple threads simulatenously. The monitor would decide linearizability by matching an observed concurrent execution and compare it against the possible executions of a model (an ideal atomic set or stack).

These objective may be pursued as a result of more than one thesis.

Related courses: Formal Methods, Language-Based Security and Programming Languages

Prerequisites: Programming (Python, Java, C,…), and (basic) knowledge of language-based security.

Contact: Gerardo Schneider (gersch@chalmers.se)

References and Further Reading:
[1] B. Bonakdarpour, C. Sánchez, and G. Schneider. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. In ISoLA’18, LNCS, 2018 (http://www.cse.chalmers.se/~gersch/isola2018-hyperproperties.pdf)
[2] M. Herlihy and N. Shavit. "The Art of Multiprocessor Programming”, Morgan Kaufmann, 2008.

Date range: 
October, 2018 to October, 2023