Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. However, black-box monitoring of HyperLTL is not possible in general.

In this talk, I will present an alternative approach called gray-box monitoring which combines runtime verification and static analysis to cover a wider class of hyperproperties.

I will start the talk by giving a brief recap of LTL, Hyper-LTL and some basic results about black-box monitoring. I will then sketch a proof that black-box monitoring of HyperLTL is in general unfeasible, and present our gray-box approach as an alternative to circumvent this limitation. Gray-box monitoring implies performing analysis of the system at run-time, which brings new limitations to monitorabiliy (the feasibility of solving the monitoring problem). Thus, I will present a refined notion of monitorability, both for trace properties and hyperproperties, that takes into account static knowledge and computability of the monitor.

In the last part of the talk, I will present a case study where we applied this approach to monitor a privacy hyperproperty called distributed data minimality. The case-study is supported by a proof-of-concept implementation that uses the KeY symbolic execution engine and the Z3 SMT solver to perform static analysis at runtime.

This talk is based on joint work with César Sánchez, Gerardo Schneider and Borzoo Bonakdarpour.

• FMSD paper (2021)
• Original FM'19 paper