From generalized non-interference to properties of the shape ∀*∃*Φ for safe Φ

RM/AVM Information flow properties
1

Generalized noninterference properties[1]

Mclean [42] reformulates generalized noninterference as a policy requiring a system to contain, for any traces t₁ and t₂, an interleaved trace t₃ whose high inputs are the same as t₁ and whose low events are the same as t₂.

Formally, the set of generalized non-interference properties T is defined as follows.

{T ∈ Prop | ∀t₁, t₂ ∈ T. ∃t₃ ∈ T. hi(t₃) = hi(t₁) ∧ low(t₃)= low(t₂)}

So, a given property T—i.e., a set of traces T={t₁, t₂ , t₃,…}—is a generalized non-interference property (GNI) when the following is true.

∀t₁, t₂ ∈ T. ∃t₃ ∈ T. hi(t₃) = hi(t₁) ∧ low(t₃) = low(t₂)

From GNI to properties of the shape ∀*∃*Φ for safe Φ

Now, if we look at the above formula, we first have the ∀ and the ∃ quantification over traces, and then a formula that can be interpreted as predicate over three traces. In more detail, if we define

Φ(t₁, t₂ , t₃) ≔ hi(t₃) = hi(t₁) ∧ low(t₃) = low(t₂)

then a non-interference property boils down to a specific formula of the shape ∀t₁, t₂. ∃t₃. Φ(t₁, t₂ , t₃). Moreover, the property Φ(t₁, t₂ , t₃) is true iff it is true for all finite prefixes of t₁, t₂ , t₃. Thus it is a special case of a safe property as defined in the paper Coinductive Proofs for Temporal Hyperliveness, in which the authors introduce

HyCo, a coinductive relation to reason about the difficult class of hyperproperties of the form ∀∗∃∗𝜓 , where 𝜓 is a safety relation between traces. Importantly, HyCo is language agnostic: it does not commit to a specific programming language to model systems, nor to a particular logic to specify trace relations.

We can take away a couple of points:

  • we are in the land of co-inductive proofs, but that’s part and parcel of a message-oriented take on objects, which is almost inherently co-algebraic
  • the proof technique is language agnostic (that’s my emphasis)
  • we probably don’t need to look for more complicated properties (in the short and mid term)

In the paper, we also can find written:

Interaction Trees (ITrees) [41] have recently been introduced as a general-purpose coinductive structure to model potentially non-terminating computations within the Coq proof assistant. Several approaches have been developed to establish trace inclusion (resp. equivalence) between ITrees using simulation (resp. bisimulation) techniques [15, 43]. Similar to the framework presented in this paper, these approaches are based on variants of parameterized coinduction. However, they do not support temporal reasoning. An interesting and natural direction would be to apply our approach to the verification of temporal hyperproperties of programs modeled as ITrees.

As a consequence, if we follow through with the idea of programs as ITrees[2], then we can in principle apply these proof techniques to information flow properties for dapps. The generality of the shape of properties makes hope; also, note that we could actually have application specific properties.

  1. https://dl.acm.org/doi/abs/10.5555/1891823.1891830 ↩︎

  2. This is the framework under consideration to formalize the Anoma Virtual Machine programs. ↩︎

1 Like