Gray-box Monitoring of Hyperproperties (Extended Version)

TL;DR

This paper introduces a gray-box runtime verification approach for hyperproperties like HyperLTL, refining monitorability notions and applying it to privacy properties using SMT-based verification.

Contribution

It proposes a feasible gray-box monitoring framework for hyperproperties, refining monitorability concepts and demonstrating practical application to privacy hyperproperties.

Findings

Gray-box monitoring is feasible where black-box is not.

Refined notions of monitorability for hyperproperties.

Successful runtime verification of a privacy hyperproperty.

Abstract

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. We first show that black-box monitoring of HyperLTL is in general unfeasible, and suggest a gray-box approach. 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, as another contribution of this paper we refine the classic notions of monitorability, both for trace properties and hyperproperties, taking into account the computability of the monitor. We then apply our approach to monitor a privacy hyperproperty called distributed data minimality, expressed as a HyperLTL property, by using an SMT-based static verifier at runtime.

Equations

$$\phi$$

$$\begin{array}[]{l@{\hspace{2em}}c@{\hspace{2em}}l}t\models p\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&p\in t[0]\\ t\models\neg\varphi\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&t\not\models\varphi\\ t\models\varphi_{1}\mathrel{\vee}\varphi_{2}\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&t\models\varphi_{1}\text{ or }t\models\varphi_{2}\\ t\models\LTLcircle\varphi\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&t[1,..]\models\varphi\\ t\models\varphi_{1}\mathbin{\mathcal{U}}\varphi_{2}\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&\text{for some $i$, }t[i,..]\models\varphi_{2}\text{ and }\text{for all $j<i$, }t[j,..]\models\varphi_{1}\\ \end{array}$$

$$\phi$$

$$\begin{array}[]{l@{\hspace{2em}}c@{\hspace{2em}}l}T,\Pi\models\forall\pi.\varphi\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&\text{for all }t\in T\text{ the following holds }T,\Pi[\pi\rightarrow t]\models\varphi\phantom{aaaaaaaaaaaaaaa}\\ T,\Pi\models\exists\pi.\varphi\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&\text{there exists }t\in T\text{ such that }T,\Pi[\pi\rightarrow t]\models\varphi\\ T,\Pi\models\psi\hfil\hskip 20.00003pt&\text{iff}\hfil\hskip 20.00003pt&\Pi\models\psi\end{array}$$

$$\begin{array}[]{l@{\hspace{1em}}c@{\hspace{2em}}l}\Pi\models a_{\pi}\hfil\hskip 10.00002pt&\text{iff}\hfil\hskip 20.00003pt&a\in\Pi(\pi)[0]\\ \Pi\models\psi_{1}\mathrel{\vee}\psi_{2}\hfil\hskip 10.00002pt&\text{iff}\hfil\hskip 20.00003pt&\Pi\models\psi_{1}\text{ or }\Pi\models\psi_{2}\\ \Pi\models\neg\psi\hfil\hskip 10.00002pt&\text{iff}\hfil\hskip 20.00003pt&\Pi\not\models\psi\\ \Pi\models\LTLcircle\psi\hfil\hskip 10.00002pt&\text{iff}\hfil\hskip 20.00003pt&\Pi[1..]\models\psi\\ \Pi\models\psi_{1}\mathbin{\mathcal{U}}\psi_{2}\hfil\hskip 10.00002pt&\text{iff}\hfil\hskip 20.00003pt&\text{for some $i$, }\Pi[i,..]\models\psi_{2}\text{, and }\text{for all $j<i$ }T,\Pi[j,..]\models\psi_{1}\end{array}$$

$$O{\models }^s\phi \text{iff}\text{for all }B\in \mathcal{B}\text{ such that }O⪯B\text{, }B\models \phi$$

$$O{\models }^v\phi \text{iff}\text{for all }B\in \mathcal{B}\text{ such that }O⪯B\text{, }B/\models \phi$$

$$O{\models }_{\mathcal{S}}^s\phi$$

$$O{\models }_{\mathcal{S}}^v\phi$$

$$\mathrm{output}(\pi ,{\pi }^{\prime })$$

$${\mathrm{same}}_i(\pi ,{\pi }^{\prime })$$

$${\mathrm{almost}}_i(\pi ,{\pi }^{\prime })$$

$${\phi }_i$$

$${\phi }_{\mathsf{dm}}=\underset{i=1}{\overset{n}{\bigwedge }}{\phi }_i.$$

$${\phi }_f(i,x,y)=\exists z\in I.f(z[i\mapsto x])\ne f(z[i\mapsto y]),$$

$$N_{f,i}(x,y)=\{\begin{array}{ll}\top \text{ or }?& \text{if φf(i,x,y) holds},\\ \perp \text{ or }?& \text{otherwise.}\end{array}$$

$$M_{\text{dm}}(U)=\{\begin{array}{ll}?& \text{if }f(u_{\text{in}})\ne u_{\text{out}}\text{ for some }u\in U,\\ ?& \text{if }{\bigwedge }_{i=1}^n{\bigwedge }_{u,u^{\prime }\in U}{N}_{f,i}({\mathrm{proj}}_i(u_{\text{in}}),{\mathrm{proj}}_i(u_{\text{in}}^{\prime }))\ne \perp ,\\ \perp & \text{otherwise.}\end{array}$$

$$M_{\text{dm}}(U)=\perp$$

$${\bigvee }_{i=1}^n{\bigvee }_{u,u^{\prime }\in U}{N}_{f,i}({\mathrm{proj}}_i(u_{\text{in}}),{\mathrm{proj}}_i(u_{\text{in}}^{\prime }))=\perp$$

$$\iff$$

$$\Rightarrow$$

$${\bigvee }_i\exists u,u^{\prime }\in V.\forall w\in V.f(w_{\text{in}}[i\mapsto {\mathrm{proj}}_i(u)])=f(w_{\text{in}}[i\mapsto {\mathrm{proj}}_i(u^{\prime })])$$

$$\iff$$

Full text

1 Introduction

Consider a confidentiality policy $\varphi$ that requires that every pair of separate executions of a system agree on the position of occurrences of some proposition $a$. Otherwise, an external observer may learn some sensitive information about the system. We are interested in studying how to build runtime monitors for properties like $\varphi$, where the monitor receives independent executions of the system under scrutiny and intend to determine whether or not the system satisfies the property. While no such monitor can determine whether the system satisfies $\varphi$ — as it cannot determine whether it has observed the whole (possibly infinite) set of traces — it may be able to detect violations. For example, if the monitor receives finite executions $t_{1}=\{a\}\{\}\{\}\{a\}\{\}$ and $t_{2}=\{a\}\{a\}\{\}\{\}\{a\}$, then it is straightforward to see that the pair $(t_{1},t_{2})$ violates $\varphi$ (the traces do not agree on the truth value of $a$ in the second, fourth, and fifth positions).

Now, if we change the policy to $\varphi^{\prime}$ requiring that, for every execution, there must exist a different one that agrees with the first execution on the position of occurrences of $a$, the monitor cannot even detect violations of $\varphi^{\prime}$. Indeed, it is not possible to tell at run-time whether or not for each execution (from a possibly infinite set), there exists a related one. Such properties for which no monitor can detect satisfaction or violation are known as non-monitorable.

Monitorability was first defined in [pnueli06psl] as the problem of deciding whether any extension of an observed trace would violate or satisfy a property expressed in LTL. We call this notion semantic black-box monitorability. It is semantic because it defines a decision problem (the existence of a satisfying or violating trace extension) without requiring a corresponding decision procedure. In settings like LTL the problem is decidable and the decision procedures are well-studied, but in other settings, a property may be semantically monitorable even though no algorithm to monitor it exists. This notion of monitorability is “black-box” because it only considers the temporal logic formula to determine the plausibility of an extended observation that violates or satisfies the formula. This is the only sound assumption without looking inside the system. Many variants of this definition followed, mostly for trace logics [havelund18runtime] (see also [bartocci18introduction]).

The definition of semantic monitorability is extended in [agrawal16runtime] to the context of hyperproperties [cs10]. A hyperproperty is essentially a set of sets of traces, so monitoring hyperproperties involves reasoning about multiple traces simultaneously. The confidentiality example discussed above is a hyperproperty. The notion of monitorability for hyperproperties in [agrawal16runtime] also considers whether extensions of an observed trace, or of other additional observed traces, would violate or satisfy the property. An important drawback of these notions of monitorability is that they completely ignore the role of the system being monitored and the possible set of executions that it can exhibit to compute a verdict of a property.

In this paper, we consider a landscape of monitorability aspects along three dimensions, as depicted in Fig. 1. We explore the ability of the monitor to reason about multiple traces simultaneously (the trace/hyper dimension). We first show that a large class of hyperproperties that involve quantifier alternations are non-monitorable. That is, no matter the observation, no verdict can ever be declared. We then propose a solution based on a combination of static analysis and runtime verification. If the analysis of the system is completely precise, we call it white-box monitoring. Black-box monitoring refers to the classic approach of ignoring the system and crafting general monitors that provide sound verdicts for every system. In gray-box monitoring, the monitor uses an approximate set of executions, given for example as a model, in addition to the observed finite execution. The combination of static analysis and runtime verification allows to monitor hyperproperties of interest, but it involves reasoning about possible executions of the system (the black/gray dimension in Fig. 1). This, in turn, forces us to consider the computability limitations of the monitors themselves as programs (the computability dimension).

We apply this approach to monitoring a complex hyperproperty of interest in privacy, namely, data minimization. The principle of data minimization (introduced in Article 5 of the EU General Data Protection Regulation [gdpr2012]) from a software perspective requires that only data that is semantically used by a program should be collected and processed. When data is collected from independent sources, the property is called distributed data minimization (DDM) [ASS17dm, PSS18rvh]. Our approach for monitoring DDM is as follows. We focus on detecting violations of DDM (which we express in HyperLTL using one quantifier alternation). We then create a gray-box monitor that collects dynamically potential witnesses for the existential part. The monitor then invokes an oracle (combining symbolic execution trees and SMT solving) to soundly decide the universally quantified inner sub-formula. Our approach is sound but approximated, so the monitor may give an inconclusive answer, depending on the precision of the static verification.

Contributions.

In summary, the contributions of this paper are the following:

1. $(1)$

Novel richer definitions of monitorability that consider trace and hyper-properties, and the possibility of analyzing the system (gray-box monitoring). This enables the monitoring, via the combination of static analysis and runtime verification, of properties that are non-monitorable in a black-box manner. Our novel notions of monitorability also cover the computability limitations of monitors as programs, which is inevitable once the analysis is part of the monitoring process. 2. $(2)$

We express DDM as a hyperproperty and study its monitorability within the richer landscape defined above. We then apply the combined approach where the static analysis in this case is based on symbolic execution (Sect. 4). 3. $(3)$

We describe a proof-of-concept implementation of our gray-box monitor for DDM, apply it to some representative examples, and present empirical evaluation (Sect. 5).

The source code of our implementation is freely available online.222At https://github.com/sstucki/minion/

2 Background

Let $\mathsf{AP}$ be a finite set of atomic propositions and $\mathrm{\Sigma}=2^{\mathsf{AP}}$ be the finite alphabet. We call each element of $\mathrm{\Sigma}$ a letter (or an event). Throughout the paper, $\mathrm{\Sigma}^{\omega}$ denotes the set of all infinite sequences (called traces) over $\mathrm{\Sigma}$, and $\mathrm{\Sigma}^{*}$ denotes the set of all finite traces over $\mathrm{\Sigma}$. For a trace $t\in\mathrm{\Sigma}^{\omega}$ (or $t\in\mathrm{\Sigma}^{*}$), $t[i]$ denotes the $i^{th}$ element of $t$, where $i\in\mathbb{N}$. We use $|t|$ to denote the length (finite or infinite) of trace $t$. Also, $t[i,j]$ denotes the subtrace of $t$ from position $i$ up to and including position $j$ (or $\epsilon$ if $i>j$ or if $i>|t|$). In this manner $t[0,i]$ denotes the prefix of $t$ up to and including $i$ and $t[i,..]$ denotes the suffix of $t$ from $i$ (including $i$).

Given a set $X$, we use $\mathcal{P}(X)$ for the set of subsets of $X$ and $\mathcal{P}_{\textit{fin}}(X)$ for the set of finite subsets of $X$. Let $u$ be a finite trace and $t$ a finite or infinite trace. We denote the concatenation of $u$ and $t$ by $ut$. Also, $u\preceq t$ denotes the fact that $u$ is a prefix of $t$. Given a finite set $U$ of finite traces and an arbitrary set $W$ of finite or infinite traces, we say that $W$ extends $U$ (written $U\preceq W$) if, for all $u\in U$, there is a $v\in W$, such that $u\preceq v$. Note that every trace in $U$ is extended by some trace in $W$ (we call these trace extensions), and that $W$ may also contain additional traces with no prefix in $U$ (we call these set extensions).

2.1 LTL and HyperLTL

We now briefly introduce LTL and HyperLTL. The syntax of LTL [pnueli77temporal] is:

[TABLE]

where $a\in\mathsf{AP}$. The semantics of LTL is given by associating to a formula the set of traces $t\in\Sigma^{\omega}$ that it accepts:

[TABLE]

We will also use the usual derived operators $(\LTLdiamond\varphi\equiv\textit{true}\,\mathbin{\mathcal{U}}\varphi)$ and $(\LTLsquare\varphi\equiv\neg\LTLdiamond\neg\varphi)$. All properties expressible in LTL are trace properties (each individual trace satisfies the property or not, independently of any other trace). Some important properties, such as information-flow security policies (including confidentiality, integrity, and secrecy), cannot be expressed as trace properties but require reasoning about two (or more) independent executions (perhaps from different inputs) simultaneously. Such properties are called hyperproperties [cs10]. HyperLTL [cfkmrs14] is a temporal logic for hyperproperties that extends LTL by allowing explicit quantification over execution traces. The syntax of HyperLTL is:

[TABLE]

A trace assignment $\Pi:\mathcal{V}\rightarrow\mathrm{\Sigma}^{\omega}$ is a partial function mapping trace variables in $\mathcal{V}$ to infinite traces. We use $\Pi_{\varnothing}$ to denote the empty assignment, and $\Pi[\pi\rightarrow t]$ for the same function as $\Pi$, except that $\pi$ is mapped to trace $t$. The semantics of HyperLTL is defined by associating formulas with pairs $(T,\Pi)$, where $T$ is a set of traces and $\Pi$ is a trace assignment:

[TABLE]

The semantics of the temporal inner formulas is defined in terms of the traces associated with each path (here $\Pi[i,..]$ denotes the map that assigns $\pi$ to $t[i,..]$ if $\Pi(\pi)=t$):

[TABLE]

We say that a set $T$ of traces satisfies a HyperLTL formula $\varphi$ (denoted $T\models\varphi$) if and only if $T,\Pi_{\varnothing}\models\varphi$.

Example 1

Consider the HyperLTL formula $\varphi=\forall\pi.\forall\pi^{\prime}.\LTLsquare(a_{\pi}\mathrel{\leftrightarrow}a_{\pi^{\prime}})$ and $T=\{t_{1},t_{2},t_{3}\}$, where $t_{1}=\{a,b\}\{a,b\}\{\}\{b\}\cdots$, $t_{2}=\{a\}\{a\}\{b\}\cdots$ and $t_{3}=\{\}\{a\}\{b\}\cdots$ Although traces $t_{1}$ and $t_{2}$ together satisfy $\varphi$, $t_{3}$ does not agree with the other two, i.e., $a\in t_{1}(0),a\in t_{2}(0)$, but $a\notin{}t_{3}(0)$. Hence, $T\not\models\varphi$.

2.2 Semantic Monitorability

Runtime verification (RV) is concerned with (1) generating a monitor from a formal specification $\varphi$, and (2) using the monitor to detect whether or not $\varphi$ holds by observing events generated by the system at run time. Monitorability refers to the possibility of monitoring a property. Some properties are non-monitorable because no finite observation can lead to a conclusive verdict. We now present some abstract definitions to encompass previous notions of monitorability in a general way. These definitions are made concrete by instantiating them for example to traces (for trace properties) or sets of traces (for hyperproperties), see Ex. 2 below.

• •

Observation. We refer to the finite information provided dynamically to the monitor up to a given instant as an observation. We use $O$ and $P$ to denote individual observations and $\mathcal{O}$ to denote the set of all possible observations, equipped with an operator $O\preceq P$ that captures the extension of an observation.

• •

System behavior. We use $\mathcal{B}$ to denote the universe of all possible behaviors of a system. A behavior $B\in\mathcal{B}$ may, in general, be an infinite piece of information. By abuse of notation, $O\preceq B$ denotes that observation $O\in\mathcal{O}$ can be extended to a behavior $B$.

Example 2

When monitoring trace properties such as LTL, we have $\mathcal{O}=\Sigma^{*}$, an observation is a finite trace $O\in\Sigma^{*}$, $O\preceq O^{\prime}$ is the prefix relation on finite strings, and $\mathcal{B}=\mathrm{\Sigma}^{\omega}$. When monitoring hyperproperties such as HyperLTL, an observation is a finite set of finite traces $O\subset\Sigma^{*}$, that is, $\mathcal{O}=\mathcal{P}_{\textit{fin}}(\mathrm{\Sigma}^{*})$. The relation $\preceq$ is the prefix for finite sets of finite traces defined above. That is, $O\preceq P$ whenever for all $t\in O$ there is a $t^{\prime}\in P$ such that $t\preceq t^{\prime}$. Finally, $\mathcal{B}=\mathcal{P}(\mathrm{\Sigma}^{\omega})$.

We say that an observation $O\in\mathcal{O}$ permanently satisfies a formula $\varphi$, if every $B\in\mathcal{B}$ that extends $O$ satisfies $\varphi$:

[TABLE]

where $\models$ denotes the satisfaction relation in the semantics of the logic. Similarly, we say that an observation $O\in\mathcal{O}$ permanently violates a formula $\varphi$, if every extension $B\in\mathcal{B}$ violates $\varphi$:

[TABLE]

Monitoring a system for satisfaction (or violation) of a formula $\varphi$ is to decide whether a finite observation permanently satisfies (resp. violates) $\varphi$.

Definition 1 (Semantic Monitorability)

A formula $\varphi$ is (semantically) monitorable if every observation $O$ has an extended observation $P\succeq O$, such that $P\models^{s}\varphi$ or $P\models^{v}\varphi$.

A similar definition of monitorability only for satisfaction or only for violation can be obtained by considering only $P\models^{s}\varphi$ or only $P\models^{v}\varphi$. Instantiating this definition of monitorability for LTL and finite traces as observations ($\mathcal{O}=\Sigma^{*}$ and $\mathcal{B}=\Sigma^{\omega}$) leads to the classic definitions of monitorability for LTL by Pnueli and Zaks [pnueli06psl] (see also [havelund18runtime]). Similarly, instantiating the definitions for HyperLTL and observations as finite sets of finite traces leads to monitorability as introduced by Agrawal and Bonakdarpour [agrawal16runtime].

Example 3

The LTL formula $\LTLsquare\LTLdiamond a$ is not (semantically) monitorable since it requires an infinite-length observation, while formulas $\LTLsquare a$ and $\LTLdiamond a$ are monitorable. Similarly, $\forall\pi.\forall\pi.\LTLsquare(a_{\pi}\leftrightarrow\neg a_{\pi^{\prime}})$ is monitorable, but $\forall\pi.\exists\pi.\LTLsquare(a_{\pi}\leftrightarrow\neg a_{\pi^{\prime}})$ is not, as it requires an observation set of infinite size. We will prove this claim in detail in Sect. 3.

3 The Notion of Gray-box Monitoring

Most of the previous definitions of monitorability make certain assumptions:

(1) the logics are trace logics, i.e. do not cover hyperproperties,

(2) the system under analysis is black-box in the sense that every further observation is possible,

(3) the logics are tractable, in that the decision problems of satisfiability, liveness, etc. are decidable.

We present here a more general notion of monitorability by challenging these assumptions.

3.1 The Limitations of Monitoring Hyperproperties

Earlier work on monitoring hyperproperties is restricted to the quantifier alternation-free fragment, that is either $\forall^{*}.\psi$ or $\exists^{*}.\psi$ properties. We establish now an impossibility result about the monitorability of formulas of the form $\forall\pi.\exists\pi^{\prime}.\LTLsquare F$, where $F$ is a state predicate. That is, $F$ is formed by atomic propositions, $a_{\pi}$ or $a_{\pi^{\prime}}$ and Boolean combinations thereof, and can be evaluated given two valuations of the propositions from $\mathsf{AP}$, one from each path $\pi$ and $\pi^{\prime}$ at the current position. For example, the predicate $F=(a_{\pi}\leftrightarrow\neg a_{\pi^{\prime}})$ for $\mathsf{AP}=\{a\}$ depends on the valuation of $a$ at the first state of paths $\pi$ and $\pi^{\prime}$. We use $v$ and $v^{\prime}$ in $F(v,v^{\prime})$ to denote that $F$ uses two copies of the variables $v$ (one copy from $\pi$ and another from $\pi^{\prime}$). A predicate $F$ is reflexive if for all valuations $v\in 2^{\mathsf{AP}}$, $F(v,v)$ is true. A predicate $F$ is serial if, for all $v$, there is a $v^{\prime}$ such that $F(v,v^{\prime})$ is true.

Theorem 3.1

A HyperLTL formula of the form $\psi=\forall\pi.\exists\pi^{\prime}.\LTLsquare F$ is non-monitorable if and only if $F$ is non-reflexive and serial.

Proof

Let $\varphi$ be $\forall\pi\exists\pi^{\prime}.\LTLsquare F$. We first observe that if $F$ is serial, then the universal set $\Sigma^{\omega}$ is a model of $\varphi$, i.e. $\Sigma^{\omega}\models\varphi$. We show the two directions separately.

• •

“$\Leftarrow$”. Assume that $F$ is non-reflexive and serial, and let $U$ be an arbitrary observation. We show an infinite extension of $U$ that violates $\varphi$ and another infinite extension of $U$ that satisfies $\varphi$, concluding that no observation has a finite extension that permanently satisfies or violates $\varphi$, that is, $\varphi$ is not monitorable. As mentioned above, since $F$ is serial, $\Sigma^{\omega}$ is a model of $\varphi$ and $\Sigma^{\omega}$ extends $U$. Now, assume that all traces in $U$ have the same length (otherwise, extend the shorter traces arbitrarily). Then, pick $v$ such that $F(v,v)$ is false (recall that $F$ is non-reflexive so such a $v$ must exist), and consider the set of infinite observations $V=\{uvt\;|\;u\in U,t\in\Sigma^{\omega}\}$. Since $v$ appears at the same position in all strings in $B$, it follows that $B\not\models\varphi$.

• •

“$\Rightarrow$”. If $F$ is reflexive then $\varphi$ holds for every non-empty set of infinite words by picking the same trace for $\pi$ and $\pi^{\prime}$. Therefore $\varphi$ is monitorable (in fact, guaranteed to be permanently satisfied for any observation). Otherwise, assume that $F$ is not serial, so for some $v$ and for all $v^{\prime}$, $F(v,v^{\prime})$ is false. Consider an arbitrary observation $U$ and extend one $u\in U$ into $uv$. The observation obtained permanently violates $\varphi$ because taking $\pi$ to be $uv$ cannot be matched at the position where $v$ occurs by any trace for $\pi^{\prime}$.

This finishes the proof. ∎

The fragment of $\forall\exists$ properties captured by Theorem 3.1 is very general (and this result can be easily generalized to $\forall^{+}\exists^{+}$ hyperproperties). First, the temporal operator is just safety (the result can be generalized for richer temporal formulas). Also, every binary predicate can be turned into a non-reflexive predicate by distinguishing the traces being related. Moroever, many relational properties, such as non-interference and DDM, contain a tacit assumption that only distinct traces are being related. Seriality simply establishes that $F$ cannot be falsified by only observing the local valuation of one of the traces. Intuitively, a predicate that is not serial can be falsified by looking only at one of the traces, so the property is not a proper hyperproperty. The practical consequence of Theorem 3.1 is that many hyperproperties involving one quantifier alternation cannot be monitored.

3.2 Gray-box Monitoring. Sound and Perfect Monitors

To overcome the negative non-monitorability result, we exploit knowledge about the set of traces that the system can produce (gray-box or white-box monitoring). Given a system that can produce the set of system behaviors $\mathcal{S}\subseteq\mathcal{B}$, we parametrize the notions of permanent satisfaction and permanent violation to consider only behaviors in $\mathcal{S}$:

[TABLE]

First, we extend the definition of monitorability (Def. 1 above) to consider the system under observation.

Definition 2 (Semantic Gray-Box Monitorability)

A formula $\varphi$ is semantically gray-box monitorable for a system $\mathcal{S}$ if every observation $O$ has an extended observation $P\succeq O$ in $\mathcal{S}$, such that $P\models^{s}_{\mathcal{S}}\varphi$ or $P\models^{v}_{\mathcal{S}}\varphi$.

In this definition, monitors must now analyze and decide properties of extended observations which is computationally not possible with full precision for sufficiently rich system descriptions.

We now introduce a novel notion of monitors that consider $\mathcal{S}$ and the computational power of monitors (the diagonal dimension in Fig. 1). A monitor for a property $\varphi$ and a set of traces $\mathcal{S}$ is a computable function $M_{\mathcal{S}}\colon\mathcal{O}\rightarrow\{\top,\bot,?\}$ that, given a finite observation $O$, decides a verdict for $\varphi$: $\top$ indicates success, $\bot$ indicates failure, and $?$ indicates that the monitor cannot declare a definite verdict given only $u$. To avoid clutter, we write $M$ instead of $M_{\mathcal{S}}$ when the system is clear from the context. The following definition captures when a monitor for a property $\varphi$ can give a definite answer.

Definition 3 (Sound monitor)

Given a property $\varphi$ and a set of behaviors $\mathcal{S}$, a monitor $M$ is sound whenever, for every observation $O\in\mathcal{O}$,

if $O\models^{s}_{\mathcal{S}}\varphi$, then $M(O)=\top$ or $M(O)={}?$, 2. 2.

if $O\models^{v}_{\mathcal{S}}\varphi$, then $M(O)=\bot$ or $M(O)={}?$, 3. 3.

otherwise $M(O)={}?$.

If a monitor is not sound then it is possible that an extension of $O$ forces $M$ to change a $\top$ to a $\bot$ verdict, or vice-versa. The function that always outputs $?$ is a sound monitor for any property, but this is the least informative monitor. A perfect monitor precisely outputs whether satisfaction or violation is inevitable, which is the most informative monitor.

Definition 4 (Perfect Monitor)

Given a property $\varphi$ and a set of traces $\mathcal{S}$, a monitor $M$ is perfect whenever, for every observation $O\in\mathcal{O}$,

if $O\models^{s}_{\mathcal{S}}\varphi$ then $M(O)=\top$, 2. 2.

if $O\models^{v}_{\mathcal{S}}\varphi$ then $M(O)=\bot$, 3. 3.

otherwise $M(O)={}?$.

Obviously, a perfect monitor is sound. Similar definitions of perfect monitor only for satisfaction (resp. violation) can be given by forcing the precise outcome only for satisfaction (resp. violation).

A black-box monitor is one where every behavior is potentially possible, that is $\mathcal{S}=\mathcal{B}$. If the monitor uses information about the actual system, then we say it is gray-box (and we use white-box when the monitor can reason with absolute precision about the set of traces of the system). In some cases, for example to decide instantiations of a $\forall$ quantifier, a satisfaction verdict that is taken from $\mathcal{S}$ can be concluded for all over-approximations (dually under-approximations for violation and for $\exists$). For space limitations, we do not give the formal details here.

Using Defs. 3 and 4, we can add the computability aspect to capture a stronger definition of monitorability. Abusing notation, we use $O\in\mathcal{S}$ to say that the observation $O$ can be extended to a trace allowed by the system.

Definition 5 (Strong Monitorability)

A property $\varphi$ is strongly monitorable for a system $\mathcal{S}$ if there is a sound monitor $M$ s.t. for all observations $O\in\mathcal{O}$, there is an extended observation $P\in\mathcal{S}$ for which either $M(P)=\top$ or $M(P)=\bot$.

A property is strongly monitorable for satisfaction if the extension with $M(P)=\top$ always exists (and analogously for violation). In what follows we will use the term monitorability to refer to strong monitorability whenever no confusion may arise. It is easy to see that if a property is not semantically monitorable, then it is not strongly monitorable, but in rich domains, some semantically monitorable properties may not be strongly monitorable. One trivial example is termination for deterministic programs (that is, the halting problem). Given a prefix of the execution of a deterministic program, either the program halts or it does not, so termination is monitorable in the semantics sense. However, it is not possible to build a monitor that decides the halting problem.

Lemma 1

If $\varphi$ is strongly monitorable, then $\varphi$ is semantically monitorable.

A property may not be monitorable in a black-box manner, but monitorable in a gray-box manner. In the realm of monitoring of LTL properties, strong and semantic monitorability coincide for finite state systems (see [zhang12runtime]) both black-box and gray-box (for finite state systems), because model-checking and the problem of deciding whether a state of a Büchi automaton is live are decidable.

Following [bss18] we propose to use a combination of static analysis and runtime verification to monitor violations of $\forall^{+}\exists^{+}$ properties (or dually, satisfactions of $\exists^{+}\forall^{+}$). The main idea is to collect candidates for the outer $\exists$ part dynamically and use static analysis at runtime to over-approximate the inner $\forall$ quantifiers.

4 Monitoring Distributed Data Minimality

In this section, we describe how to monitor DDM, which can be expressed as a hyperproperty of the form $\forall^{+}\exists^{+}$. The negative non-monitotabiliy result from Sect. 3.1 can be generalized to $\forall^{+}\exists^{+}$ hyperproperties. In the particular case of DDM, although we mainly deal with the input/output relation of functions and are not concerned with infinite temporal behavior, we still need to handle possibly infinite set extensions $\mathcal{S}$ for black-box monitoring. In the remainder of this section, we discuss the following, seemingly contradictory aspects of DDM:

1. (P1)

DDM is not semantically black-box monitorable, 2. (P2)

DDM is semantically white-box monitorable (for programs that are not DDM), 3. (P3)

checking DDM statically is undecidable, 4. (P4)

DDM is strongly gray-box monitorable for violation, and we give a sound monitor.

The apparent contradictions are resolved by careful analysis of DDM along the different dimensions of the monitorability cube (Fig. 1).

We will show how to monitor DDM and similar hyperproperties using a gray-box approach. In our approach, a monitor can decide at run time the existence of traces using a limited form of static analysis. The static analyzer receives the finite observation $O$ collected by the monitor, but not the future system behavior. Instead it must reason under the assumption that any system behavior in $\mathcal{S}$ that is compatible with $O$, may eventually occur. For example, given an $\exists\forall$ formula, the outer existential quantifier is instantiated with a concrete set $U$ of runtime traces, while possible extensions of $U$ provided by static analysis can be used to instantiate the inner universal quantifier.

4.1 DDM Preliminaries

We briefly recapitulate the formal notion of data-minimality from [ASS17dm]. Given a function $f\colon I\rightarrow O$, the problem of data minimization consists in finding a preprocessor function $p\colon I\rightarrow I$, such that $f=f\operatorname*{\circ}p$ and $p=p\operatorname*{\circ}p$. The goal of $p$ is to limit the information available to $f$ while preserving the behavior of $f$.

There are many possible such preprocessors (e.g. the identity function), which can be ordered according to the information they disclose, that is, according to the subset relation on their kernels. The kernel $\ker(p)$ of a function $p$ is defined as the equivalence relation $(x,y)\in\ker(p)\text{ iff }p(x)=p(y)$. The smaller $\ker(p)$ is, the more information $p$ discloses. The identity function is the worst preprocessor since it discloses all information (its kernel is equality — the least equivalence relation). An optimal preprocessor, or minimizer, is one that discloses the least amount of information.

A function $f$ is monolithic data-minimal (MDM), if it fulfills either of the following equivalent conditions:

the identity function is a minimizer for $f$, 2. 2.

$f$ is injective.

Condition 1. is an information-flow-based characterization that can be generalized to more complicated settings in a straightforward fashion. Condition 2. is a purely logical or data-based characterization more suitable for implementation in e.g. a monitor.

MDM is the strongest form of data minimality, where one assumes that all input data is provided by a single source and thus a single preprocessor can be used to minimize the function. If inputs are provided by multiple sources (called a distributed setting) and access to the system implementing $f$ is restricted, it might be impossible to use a single preprocessor. For example, consider a web-based auction system that accepts bids from $n$ bidders, represented by distinct input domains $I_{1},\dotsc,I_{n}$, and where concrete bids $x_{k}\in I_{k}$ are submitted remotely. The auction system must compute the function $m(x_{1},\dotsc,x_{n})=\max_{k}\{x_{k}\}$, which is clearly non-injective and, hence, non-MDM. In this case, a single, monolithic minimizer cannot be used since different bidders need not have any knowledge of each other’s bids. Instead, bidders must try to minimize the information contained in their bid locally, in a distributed way, before submitting it to the auction.

The problem of distributed data minimization consists in building a collection $p_{1},\dotsc,p_{n}$ of $n$ independent preprocessors $p_{k}\colon I_{k}\rightarrow I_{k}$ for a given function $f\colon I_{1}\times\dotsm\times I_{n}\rightarrow O$, such that their parallel composition $p(x_{1},\dotsc,x_{n})=(p_{1}(x_{1}),\dotsc,p(x_{n}))$ is a preprocessor for $f$. Such composite preprocessors are called distributed, and a distributed preprocessor for $f$ that discloses the least amount of information is called a distributed minimizer for $f$. Then, one can generalize the (information-flow) notion of data-minimality to the distributed setting as follows. The function $f$ is distributed data-minimal (DDM) if the identity function is a distributed minimizer for $f$. Returning to our example, the maximum function $m$ defined above is DDM. As for MDM, there is an equivalent, data-based characterization of DDM defined next.

Definition 6 (distributed data minimality [ASS17dm, PASS18corr])

A function $f$ is distributed data-minimal (DDM) if, for all input positions $k$ and all $x,y\in I_{k}$ such that $x\neq y$, there is some $z\in I$, such that $f(z[k\mapsto x])\neq f(z[k\mapsto y])$.

We use Def. 6 to explore how to monitor DDM. In the following, we assume that the function $f\colon I_{1}\times\dotsm\times I_{n}\rightarrow O$ has at least two arguments ($n\geq 2$). Note that for unary functions, DDM coincides with MDM. Since MDM is a $\forall^{+}$-property (involving no quantifier alternations), most of the challenges to monitorability discussed here do not apply [PSS18rvh]. We also assume, without loss of generality, that the function $f$ being monitored has only nontrivial input domains, i.e. $\lvert I_{k}\rvert\geq 2$ for all $k=1,\dotsc n$. If $I_{k}$ is trivial then this constant input can be ignored. Finally, note that checking DDM statically is undecidable (P3) for sufficiently rich programming languages [ASS17dm].

4.2 DDM as a Hyperproperty

We consider data-minimality for total functions $f\colon I\rightarrow O$. Our alphabet, or set of events, is the set of possible input-output (I/O) pairs of $f$, i.e. $\mathrm{\Sigma}_{f}=I\times O$. Since a single I/O pair $u=(u_{\textit{in}},u_{\textit{out}})\in\mathrm{\Sigma}_{f}$ captures an entire run of $f$, we restrict ourselves to observing singleton traces, i.e. traces of length $\lvert u\rvert=1$. In other words, we ignore any temporal aspects associated with the computation of $f$. This allows us to use first-order predicate logic — without any temporal modalities — as our specification logic.

DDM is a hyperproperty, expressed as a predicate over sets of traces, even though the traces are I/O pairs. The set of observable behaviors $\mathcal{O}_{f}$ of a given $f$ consists of all finite sets of I/O pairs $\mathcal{O}_{f}=\mathcal{P}_{\textit{fin}}(\mathrm{\Sigma}_{f})$. The set of all possible system behaviors $\mathcal{B}_{f}=\mathcal{P}(\mathrm{\Sigma}_{f})$ additionally includes infinite sets of I/O pairs.

Example 4

Let $f\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ be the addition function on natural numbers, $f(x,y)=x+y$. Then $I=\mathbb{N}\times\mathbb{N}$, $O=\mathbb{N}$, and a valid trace $u\in\mathrm{\Sigma}_{f}$ takes the form $u=((x,y),z)$, where $x$, $y$ and $z$ are all naturals. Both $U=\{((1,2),3),((2,1),3)\}$ and $V=\{((1,1),3)\}$ are considered observable behaviors $U,V\in\mathcal{O}_{f}$, even though $V$ does not correspond to a valid system behavior since $f(1,1)\neq 3$. Remember that we do not discriminate between valid and invalid system behaviors in a black-box setting.

We now express DDM as a hyperproperty, using HyperLTL, but with only state predicates (no temporal operators). Given a tuple $x=(x_{1},x_{2},\dotsc,x_{n})$, we write $\operatorname{proj}_{i}(x)$ or simply $x_{i}$ for its $i$-th projection. Given an I/O pair $u=(x,y)$ we use $u_{\textit{in}}$ for the input component and $u_{\textit{out}}$ for the output component (that is $u_{\textit{in}}=x$ and $u_{\textit{out}}=y$). Given trace variables $\pi,\pi^{\prime}$, we define

[TABLE]

Example 5

Let $u=((1,2),3)$, $u^{\prime}=((2,1),3)$, and $\Pi=\{\pi\mapsto u,\pi^{\prime}\mapsto u^{\prime}\}$. Then $\Pi\models\operatorname{output}(\pi,\pi^{\prime})$, but $\Pi\not\models\operatorname{same}_{1}(\pi,\pi^{\prime})$ and $\Pi\not\models\operatorname{almost}_{1}(\pi,\pi^{\prime})$.

We define DDM for input argument $i$ as follows:

[TABLE]

In words: given any pair of traces $\pi$ and $\pi^{\prime}$, if $\pi_{\textit{in}}$ and $\pi^{\prime}_{\textit{in}}$ differ in their $i$-th position, then there must be some common values $z$ for the remaining inputs, such that the outputs of $f$ for $\tau_{\textit{in}}=z[i\mapsto\operatorname{proj}_{i}(\pi_{\textit{in}})]$ and $\tau^{\prime}_{\textit{in}}=z[i\mapsto\operatorname{proj}_{i}(\pi^{\prime}_{\textit{in}})]$ differ. Note that $z$ does not appear in $\varphi_{i}$ directly, instead it is determined implicitly by the (existentially quantified) traces $\tau$ and $\tau^{\prime}$. Finally, distributed data minimality for $f$ is defined as

[TABLE]

The property $\varphi_{\mathsf{dm}}$ follows the same structure as the logical characterization of DDM from Sect. 4.1. The universally quantified variables range over the possible inputs at position $i$, while the existentially quantified variables $\tau$ and $\tau^{\prime}$ range over the other inputs and the outputs. Note also that, given the input coordinates of $\pi$, $\pi^{\prime}$, and $\tau$, all the output coordinates, as well as the input coordinates of $\tau^{\prime}$, are uniquely determined.333For simplicity, even though $\varphi_{\mathsf{dm}}$ is not in prenex normal form, it is a finite conjunction of $\forall\forall\exists\exists$ formulas in prenex normal form so a finite number of monitors can be built and executed in parallel, one per input argument.

Example 6

Consider again $U=\{((1,2),3),((2,1),3)\}$ and $V=\{((1,1),3)\}$ from Ex. 4. Then, $V\models\varphi_{\mathsf{dm}}$ trivially holds, but $U\not\models\varphi_{\mathsf{dm}}$ because when $\Pi(\pi)\neq\Pi(\pi^{\prime})$ there is no choice of $\Pi(\tau),\Pi(\tau^{\prime})\in U$ for which $\Pi\models\neg\operatorname{output}(\tau,\tau^{\prime})$ holds.

Note that, in the above example, $V\models\varphi_{\mathsf{dm}}$ holds despite the fact that $V$ is not a valid behavior of the example function $f(x,y)=x+y$. Indeed, whether or not $U\models\varphi_{\mathsf{dm}}$ holds for a given $U$ is independent of the choice of $f$. In particular, $\mathrm{\Sigma}_{f}\models\varphi_{\mathsf{dm}}$, for any choice of $f$ regardless of whether $f$ is data-minimal or not. This is already a hint that the notion of semantic black-box monitorability is too weak to be useful when monitoring $\varphi_{\mathsf{dm}}$. Since $\mathrm{\Sigma}_{f}$ is a model of $\varphi_{\mathsf{dm}}$, no observation $U$ can have an extension that permanently violates $\varphi_{\mathsf{dm}}$. As we will see shortly, gray-box monitoring does not suffer from this limitation. Monitorability of DDM for violations becomes possible once we exclude potential models such as $\mathrm{\Sigma}_{f}$ which do not correspond to valid system behaviors.

Remark.

Note that though our definition and approach work for general (reactive) systems, the DDM example is admittedly a non-reactive system with traces of length 1. This, however, is not a limitation of the approach. Extending DDM for reactive systems is left as future work.

4.3 Properties of DDM

Since $\varphi_{\mathsf{dm}}$ is a $\forall^{+}\exists^{+}$ property, it should not come as a surprise that it is not semantically black-box monitorable in general (P1).

Lemma 2 (black-box non-monitorability)

Assume $f\colon I\rightarrow O$, then $\varphi_{\mathsf{dm}}$ is semantically black-box monitorable iff $I$ is finite.

Proof

We first treat the case where $I$ is finite. Assume $I$ and $O$ each contain at least two elements. Smaller I/O domains correspond to degenerate cases for which semantic black-box monitorability is easy to show, so we omit them here.

Let $U\subseteq\mathcal{O}$ be a finite set of traces. We need to show that there is a finite extension $V\succeq U$ that permanently satisfies or violates $\varphi_{\mathsf{dm}}$. Pick $V=\mathrm{\Sigma}_{f}=I\times O$. Clearly, this is the largest observation in $\mathcal{O}$, so any property satisfied by $V$ is also permanently satisfied by $V$. Hence it suffices to show that $V\models^{s}\varphi_{\mathsf{dm}}$.

Let $u$, $u^{\prime}$, $w$ be arbitrary I/O pairs, $o\neq o^{\prime}\in O$ a pair of distinct outputs, and $i$ an arbitrary input position. Define $v=(w_{\textit{in}}[i\mapsto\operatorname{proj}_{i}(u_{\textit{in}})],o)$ and $v^{\prime}=(w_{\textit{in}}[i\mapsto\operatorname{proj}_{i}(u^{\prime}_{\textit{in}}),o^{\prime})$. Then $u$, $u^{\prime}$ and $v$, $v^{\prime}$ are all in $V$, and it is easy to check that $\varphi_{i}$ holds if the quantified variables are instantiated to these traces in the given order. In other words $V\models^{s}\varphi_{i}$ for all $i$, and hence $V$ permanently satisfies $\varphi_{\mathsf{dm}}$.

Conversely, assume that $I$ is infinite, and let $U$ again be a finite set of traces. To show that $U$ neither permanently satisfies nor permanently violates $\varphi_{\mathsf{dm}}$, it is sufficient to exhibit a pair of extensions $T_{s},T_{v}\succeq U$ that satisfy and violate $\varphi_{\mathsf{dm}}$, respectively. For $T_{s}$, we pick $T_{s}=\mathrm{\Sigma}_{f}=I\times O$. By the same argument as given above (for the finite case), we have $T_{s}\models^{s}\varphi_{\mathsf{dm}}$.

We have to work slightly harder to construct $T_{v}$. Since $I$ is infinite but $U$ is finite, there must be an input position $i$ and a pair of distinct elements $x\neq x^{\prime}\in I_{i}$ such that no trace in $U$ has $x$ or $x^{\prime}$ as its $i$-th input. Pick some arbitrary trace $w\in\mathrm{\Sigma}_{f}$, and let $v=w[i\mapsto x]$ and $v^{\prime}=w[i\mapsto x^{\prime}]$. By construction, $v,v^{\prime}\notin U$, so $T_{v}=U\cup\{v,v^{\prime}\}$ is a strict extension of $U$. To show that $T_{v}$ does indeed violate $\varphi_{\mathsf{dm}}$, it is sufficient to show that $T_{v}\models^{v}\varphi_{i}$. Pick $v,v^{\prime}$ to instantiate $\pi$ and $\pi^{\prime}$. Then $\operatorname{proj}_{i}(w_{\textit{in}})=x\neq x^{\prime}=\operatorname{proj}_{i}(w^{\prime}_{\textit{in}})$ by construction, but there is no way to instantiate $\tau$ and $\tau^{\prime}$: since they have to agree with $\pi$ and $\pi^{\prime}$ on the $i$-th input position, the only candidates are $v$ and $v^{\prime}$, but $v_{\textit{out}}=v^{\prime}_{\textit{out}}$ by construction. ∎

Perhaps surprisingly, $\varphi_{\mathsf{dm}}$ is semantically white-box monitorable for violations (P2). That is, if $f$ is not DDM, there is hope to detect it. To make this statement more precise, we first need to identify the set of valid system behaviors $\mathcal{S}_{f}$ of $f$. We define $\mathrm{\Sigma}_{f}^{\#}=\{(x,y)\mid f(x)=y\}$ to be the set of I/O pairs that correspond to executions of $f$. Then $\mathcal{S}_{f}=\mathcal{P}(\mathrm{\Sigma}_{f}^{\#})$ precisely characterizes the set of valid system behaviors.

Example 7

Define $g\colon\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ as $g(x,y)=x$, i.e. $g$ simply ignores its second argument. Then $\mathrm{\Sigma}_{g}^{\#}=\{((x,y),x)\mid x,y\in\mathbb{N}\}$. It is easy to show that DDM is white-box monitorable for $g$. Any finite set of valid traces $U$ can be extended to include a pair of traces $u,u^{\prime}$ that only differ in their second input value, e.g. $u=((1,1),1)$ and $u^{\prime}=((1,2),1)$. Now, consider any $T\in\mathcal{S}_{f}$ that extends $U\cup\{u,u^{\prime}\}$. Clearly, $T$ cannot contain any trace $v$ for which $\operatorname{proj}_{1}(v_{\textit{in}})=1$ but $v_{\textit{out}}\neq 1$ as that would constitute an invalid system behavior. But $T$ would have to contain such a trace to be a model of $\varphi_{2}$. Hence, $T\not\models\varphi_{\mathsf{dm}}$ for any such $T$, which means $U\cup\{u,u^{\prime}\}$ permanently violates $\varphi_{\mathsf{dm}}$.

Note the crucial use of information about $g$ in the above example: it is the restriction to valid extensions $T\in\mathcal{S}_{f}$ that excludes trivial models such as $\mathrm{\Sigma}_{f}$ and thereby restores (semantic) monitorability for violations. The apparent conflict between (P1) and (P2) is thus resolved.

With the extra information that gray-box monitoring affords, we can make more precise claims about properties like DDM: whether or not a property is monitorable may, for instance, depend on whether the property actually holds for the system under scrutiny. Concretely, for the case of DDM, we show the following.

Theorem 4.1

Given a function $f\colon I\rightarrow O$, the formula $\varphi_{\mathsf{dm}}$ is semantically gray-box monitorable in $\mathcal{S}_{f}$ if and only if either $f$ is distributed non-minimal or the input domain $I$ is finite.

Theorem 4.1 follows from the following two auxiliary lemmas.

Lemma 3 (semantic violation)

If $f$ is not DDM, then $\varphi_{\mathsf{dm}}$ is semantically monitorable for violation (in $\mathcal{S}_{f}$).

Proof

Assume a finite set of traces $U\in\mathcal{S}_{f}$. We need to show that there is a finite extension $V\succeq U$ permitted by $\mathcal{S}_{f}$ that permanently violates $\varphi_{\mathsf{dm}}$. First, note that the task is trivial if $I$ is finite: we simply pick $V=\mathrm{\Sigma}_{f}^{\#}$, i.e. the set of all possible executions, which is also finite. The only finite extension of $V$ permitted by $\mathcal{S}_{f}$ is the complete set of traces $\mathrm{\Sigma}_{f}^{\#}$ itself, and since $f$ is not distributed minimal, $\varphi_{\mathsf{dm}}$ cannot hold for $\mathrm{\Sigma}_{f}^{\#}$.

Assume instead that $I$ is infinite. Since $f$ is distributed non-minimal, there must be some input position $i$ and some pair of distinct inputs $x\neq x^{\prime}\in I_{i}$, such that $f(z[i\mapsto x])=f(z[i\mapsto x^{\prime}])$ for any choice of $z\in I$. Let $y=z[i\mapsto x]$ and $y^{\prime}=z[i\mapsto x^{\prime}]$ for an arbitrary $z\in I$. Then any set $W\in\mathcal{S}_{f}$ that contains the traces $u=(y,f(y))$ and $u^{\prime}=(y^{\prime},f(y^{\prime}))$ violates $\varphi_{\mathsf{dm}}$. To see this, assume instead that $W\models^{s}_{\mathcal{S}_{f}}\varphi_{\mathsf{dm}}$. Then there must be traces $v,v^{\prime}\in W$ that agree on all but the $i$-th input, such that $f(v_{\textit{in}}[i\mapsto x])\neq f(v^{\prime}_{\textit{in}}[i\mapsto x^{\prime}])$, thus contradicting non-minimality of $f$. Hence, by picking $V=U\cup\{u,u^{\prime}\}$, we have $V\models^{v}_{f}\varphi_{\mathsf{dm}}$. ∎

Lemma 4 (Semantic satisfaction)

If $f\colon I\rightarrow O$ is DDM, then $\varphi_{\mathsf{dm}}$ is semantic monitorable for satisfaction (in $\mathcal{S}_{f}$) if and only if $I$ is finite.

Proof

First, if $I$ is finite the result follows by picking $V=\mathrm{\Sigma}_{f}^{\#}$. Assume now that $f$ is distributed minimal, $\varphi_{\mathsf{dm}}$ is semantically monitorable for satisfaction, and $I$ is infinite. Let $U\in\mathcal{S}_{f}$ be some non-empty, finite set of traces with some distinguished element $u\in U$. Since $\varphi_{\mathsf{dm}}$ is monitorable for satisfaction, there must be a finite extension $V\succeq U$ that permanently satisfies $\varphi_{\mathsf{dm}}$. To arrive at a contradiction, it suffices to construct a finite extension $W\succeq V$ that does not satisfy $\varphi_{\mathsf{dm}}$.

Pick an input position $i$ for which $I_{i}$ is infinite. Such an $i$ must exist because otherwise $I$ would be the Cartesian product of finite sets, and $I$ is infinite by assumption. Next, pick a pair of distinct element $x\neq x^{\prime}\in I_{i}$ such that there are no traces in $V$ with $x$ or $x^{\prime}$ as their $i$-th input. Such $x,x^{\prime}$ must also exist because $I_{i}$ is infinite but $V$ is finite. Finally, pick an input position $j\neq i$, and a $y\in I_{j}$ such that $y\neq\operatorname{proj}_{j}(u_{\textit{in}})$. Such a $y$ must exist for $I_{j}$ to be non-trivial.

Now let $z=u_{\textit{in}}[i\mapsto x]$, $z^{\prime}=u_{\textit{in}}[i\mapsto z^{\prime},j\mapsto y]$ and $w=(z,f(z))$, $w^{\prime}=(z^{\prime},f(z^{\prime}))$. Then $w$ and $w^{\prime}$ are clearly valid traces, i.e. $w,w^{\prime}\in\mathrm{\Sigma}_{f}^{\#}$, but $w,w^{\prime}\notin V$ since $w$ and $w^{\prime}$ have $x$ and $x^{\prime}$ as their $i$-th inputs, respectively. Let $W=V\cup\{w,w^{\prime}\}$. By construction, $\neg\operatorname{same}_{i}(\pi,\pi^{\prime})$ holds if we instantiate $\pi$ and $\pi^{\prime}$ to $w$ and $w^{\prime}$, respectively, but there is no pair of traces $v,v^{\prime}\in W$ to instantiate $\tau,\tau^{\prime}$ in such a way that $\operatorname{same}_{i}(\pi,\tau)$, $\operatorname{same}_{i}(\pi^{\prime},\tau^{\prime})$ and $\operatorname{almost}_{i}(\tau,\tau^{\prime})$ all hold simultaneously. The former force the choice $\tau\mapsto w$ and $\tau^{\prime}\mapsto w^{\prime}$ but, by construction, $\operatorname{proj}_{j}(w_{\textit{in}})\neq\operatorname{proj}_{j}(w^{\prime}_{\textit{in}})$. Hence $W\not\models^{s}\varphi_{\mathsf{dm}}$ and we arrive at a contradiction. ∎

Intuitively, Theorem 4.1 means that $f$ cannot be monitored for satisfaction. Note that the semantic monitorability property established by Theorem 4.1 is independent of whether we can actually decide DDM for the given $f$. We address the question of strong monitorability later on in this section.

If $I$ is finite, it is easy to strengthen Theorem 4.1 by providing a perfect monitor $M_{\textsf{dm}}$ for $\varphi_{\mathsf{dm}}$. Since $f$ is assumed to be a total function with a finite domain, we can simply check the validity of $\varphi_{\mathsf{dm}}$ for every trace $U\subseteq\mathrm{\Sigma}_{f}^{\#}$ and tabulate the result. To do so, the $\exists$ and $\forall$ quantifiers in $\varphi_{\mathsf{dm}}$ can be converted into conjunctions and disjunctions over $U$.

Corollary 1

For $f:I\mathrel{\rightarrow}O$ with finite $I$, $\varphi_{\mathsf{dm}}$ is strongly monitorable in $\mathcal{S}_{f}$.

If $I$ is infinite, then $\varphi_{\mathsf{dm}}$ is not semantically monitorable for satisfaction, but we can still hope to build a sound monitor for violation of $\varphi_{\mathsf{dm}}$.

4.4 Building a Gray-box Monitor for DDM

In what follows, we assume a computable function capable of deciding DDM only for some instances. This function, which we call oracle, will serve as the basis for a sound monitor for DDM (P4). This monitor will detect some, but not all, violations of DDM when given sets of observed traces, thus resolving the apparent tension between (P3) and (P4).

Given $f\colon I_{1}\times\dotsm\times I_{n}\rightarrow O$, we define the predicate $\varphi_{f}$ as

[TABLE]

and assume a total computable function $N_{f,i}\colon I_{i}\times I_{i}\rightarrow\{\top,\bot,?\}$ such that

[TABLE]

The function $N_{f,i}$ acts as our oracle to instantiate the existential quantifiers in $\varphi_{\mathsf{dm}}$. As discussed earlier, such oracles may be implemented by statically analyzing the system under observation (here, the function $f$). In our proof-of-concept implementation, we extract $\varphi_{f}(i,x,y)$ from $f$ using symbolic execution, and use an SMT solver to compute $N_{f,i}(x,y)$.

We now define a monitor $M_{\textsf{dm}}$ for $\varphi_{\mathsf{dm}}$ as follows:

[TABLE]

Intuitively, the monitor $M_{\textsf{dm}}(U)$ checks the set of traces $U$ for violations of DDM by verifying two conditions: the first condition ensures the consistency of $U$, i.e. that every trace in $U$ does in fact correspond to a valid execution of $f$; the second condition is necessary for $U$ not to permanently violate $\varphi_{\mathsf{dm}}$. Hence, if it fails, $U$ must permanently violate $\varphi_{\mathsf{dm}}$. Since $N_{f,i}$ is computable, so is $M_{\textsf{dm}}$. Note that $M_{\textsf{dm}}$ never gives a positive verdict $\top$. This is a consequence of Theorem 4.1: if $f$ is DDM, then $\varphi_{\mathsf{dm}}$ is not monitorable in $\mathcal{S}_{f}$. In other words, DDM is not monitorable for satisfaction.

The second condition in the definition of $M_{\textsf{dm}}$ is an approximation of $\varphi_{\mathsf{dm}}$: the universal quantifiers are replaced by conjunctions over the finite set of input traces $U$, while the existential quantifiers are replaced by a single quantifier ranging over all of $\mathrm{\Sigma}_{f}^{\#}$ (not just $U$). This approximation is justified formally by the following theorem.

Theorem 4.2 (soundness)

The monitor $M_{\textsf{dm}}$ is sound. Formally,

$U\models^{s}_{\mathcal{S}_{f}}\varphi_{\mathsf{dm}}$* if $M_{\textsf{dm}}(U)=\top$, and* 2. 2.

$U\models^{v}_{\mathcal{S}_{f}}\varphi_{\mathsf{dm}}$* if $M_{\textsf{dm}}(U)=\bot$.*

Proof

The monitor never gives a $\top$ verdict, so the first half of the theorem (satisfaction) holds vacuously. For the second part (violation), we have

[TABLE]

and

[TABLE]

∎

We describe a prototype implementation of $M_{\textsf{dm}}$ in Sect. 5.

5 Implementation and Prototype

We have implemented the ideas described in Sect. 4 in a proof-of-concept monitor for DDM called minion. The monitor uses the symbolic execution API and the SMT backend of the KeY deductive verification system [ahrendt16deductive, KeYproject] to extract logical characterizations of Java programs (their symbolic execution trees). It then extends them to first-order formulas over sets of observed traces, and checks the result using the state-of-the-art SMT solver Z3 [DeMouraB08tacas, Z3github]. The minion monitor is written in Scala and provides a simple command-line interface (CLI). Its source code is freely available online at https://github.com/sstucki/minion/.

Before we describe minion in more detail, we introduce a running example illustrating the principles of both monolithic and distributed data minimality. For an example of monolithic data minimization, first consider the method rate shown in Fig. 2. The purpose of this method is to compute the baseline rate to be paid by the driver of a vehicle on a toll road. The rate depends on the time of day and the number of passengers in the vehicle. The range of the output is $\{56,70,72,90\}$, and consequently the data processor does not need to know the precise hour of the day, nor the exact number of passengers. A vehicle might pass a toll station at any time between 9pm and 5am to be subject to a the higher daytime rates (72, 90), and at any other time to benefit from the lower nighttime rates (56, 70). Also, any vehicle occupied by three or more passengers is eligible for a 20% carpool discount. Giving the actual hour and number of passengers violates the principle of data minimality because more information than necessary is collected. Data minimization is the process of ensuring that the range of inputs provided is reduced, such that different inputs result in different outputs.

In a distributed setting, the concept of minimization is more complex as input data may be collected from multiple independent sources. Consider the method fee in Fig. 2. This method computes the total fee for a trip on a toll road, based on the hours at which a vehicle passes three consecutive toll stations, and on the number of passengers in the vehicle. The overall fee depends on the total time spent on the toll road, which is data collected from all three toll stations. In particular, if a vehicle enters a section of the toll road during a low-rate early morning hour, but fails to reach the next station before 9pm, the driver will be charged the more expensive daytime rate for the entire section. DDM requires minimizing each input parameter (i.e. the information collected at separate toll stations) individually. A preprocessor or data minimizer [ASS17dm] located at any given toll station can easily minimize the individual inputs (hour, passengers) at that station. But an individual minimizer cannot guarantee minimization with respect to the overall fee since it has no information about the input data collected at the other stations. DDM therefore constitutes merely a “best effort” to minimize inputs given the inherently distributed nature of the system.

When running minion on the fee method of the class Toll, the tool builds first the symbolic execution tree. Then, the monitor reads and parses traces from an input file or standard input. Whenever minion parses a new trace, it rechecks the entire set of traces read thus far for violation, thereby supporting both online and offline monitoring. Traces are read from CSV files, where the number and format of the inputs is determined automatically from the method signature. Fig. 3a shows example traces for the fee method. Columns 1–4 correspond to the parameters h1, h2, h3 and p, respectively, while column 5 contains the result computed by fee for the given values.

By default, minion monitors traces for DDM. Thus, when processing the traces given in Fig. 3a, it signals a violation after reading the second line because fee$(20,h_{2},h_{3},p)={}$fee$(2,h_{2},h_{3},p)$ irrespective of the choice of $h_{2}$, $h_{3}$, and $p$. In contrast, all traces listed in Fig. 3b are accepted by minion since they have been preprocessed by a distributed minimizer. Alternatively, minion can be instructed to monitor traces for monolithic data minimality (MDM) in which case a violation is signaled when processing the last line of Fig. 3b, whereas all traces in Fig. 3c are accepted.

5.1 Lazy vs. Eager Monitoring

Perhaps surprisingly, there are cases where minion will detect a violation of DDM whereas it will not detect a violation of MDM. Consider the function $f(x,y)=x$. Since $f$ simply ignores its second argument, it is clearly neither distributed nor monolithic minimal. When monitoring the pair of traces $(1,2,1)$ and $(3,4,3)$ for DDM, minion detects a violation because $f(x,2)=f(x,4)$ for any choice of $x$. Note, however, that this situation does not appear among the observed traces since the two values for $y$ in the respective traces differ. The tool reports a violation because a common value for $x$ is found by our oracle when monitoring for DDM. When monitoring for MDM minion does not detect the violation, because in this case there is no need to invoke the oracle.

Whether or not this is the intended behavior of the monitor depends on the assumption of whether the traces are collected from a program $f$ or from the combined program $f\operatorname*{\circ}p$ ($p$ being a minimizer). In the latter case, some combinations of inputs may never be observed as the inputs have been minimized. On the other hand, if traces are not considered preprocessed, we may wish to explore the behavior of $f$ more exhaustively. For this purpose, minion can be instructed to monitor a set of traces eagerly for MDM, resp. lazily for DDM. For the former, minion considers not just the observed traces, but any combination of observed input values—even if that combination does not actually correspond to an observed trace. For the latter, minion only considers combinations of inputs originating from traces with the same result value. For example, for the pair of input traces $(1,2,1)$ and $(3,4,3)$, minion is able to find a violation in eager MDM mode since $f(1,2)=f(1,4)$, but not in lazy DDM mode since $f(1,2)\neq f(3,4)$.