Secrecy-preserving Refinement

Description of the Case Study

Relating programs at different levels (e.g., high vs. low, abstract vs. concrete) is often involved in system design. For example, secure compilation specifies that when the compiler transforms the code (e.g., for optimization purposes), the compiled code should still satisfy the intended security property. For instance, to preserve the classic \(\forall \exists\) non-interference property during compilation, an \(\exists \forall \forall \exists \exists\) formula must be verified. That is, there exists a mapping \(M\) that preserves NI from code \(A\) to code \(B\), as follows:

\[\Phi_{\text{NI--ABM}} = \exists \pi_M . \forall \pi_{A_1} . \forall \pi_{B_1} . \exists \pi_{A_2} . \exists \pi_{B_2} . \left( \varphi_{\mathit{map}_1} \rightarrow \left( \varphi_{\mathit{map}_2} \land \psi_{\text{NI}} \right) \right)\]

HyperQB is able to correctly synthesize a correct mapping (i.e., the leading \(\exists\)) if one exists. Such a formula with multiple quantifier alternations bumps up the complexity of model checking by one step in the polynomial hierarchy compared to the original non-interference formula.

Benchmarks

The Model(s)

--MAPSYNTH
--(adopted from: Tzu-Han Hsu, Borzoo Bonakdarpour, Eunsuk Kang, and Stavros Tripakis. Mapping synthesis for hyperproperties. In 2022 IEEE 35th Computer Security Foundations Symposium (CSF))
MODULE main

VAR
  atom_p: boolean;
  atom_q: boolean;
  PC: 0..3;

ASSIGN
  -- Initial Conditions
  init(atom_p):= FALSE;
  init(atom_q):= FALSE;
  init(PC) := 0;

  -- Transition Relations
  next(atom_p) :=
    case
      (PC=0): {TRUE,  FALSE};
      (PC=1): {TRUE,  FALSE};
      (PC=2): FALSE;
      TRUE: atom_p;
    esac;

  next(atom_q) :=
    case
      (PC=0): {TRUE,  FALSE};
      (PC=1): {TRUE,  FALSE};
      (PC=2): FALSE;
      TRUE: atom_q;
    esac;

  next(PC) :=
    case
      (PC=3): 3;
      TRUE: PC+1;
    esac;

DEFINE
  fAIL := (atom_p & atom_q);

Formula

Exists A . Forall B . Forall C . Exists D . Exists E .
G 
(
  (pr[A]&~ps[A] & ~qr[A]&qs[A]) 
  | 
  (~pr[A]&ps[A] & qr[A]&~qs[A])
)
&
(
  G (
      ((pr[A]) -> ((atom_p[B]) -> (atom_r[C]))) &
      ((ps[A]) -> ((atom_p[B]) -> (atom_s[C]))) &
      ((qr[A]) -> ((atom_q[B]) -> (atom_r[C]))) &
      ((qs[A]) -> ((atom_q[B]) -> (atom_s[C]))) &
      (~fAIL[B] & ~fAIL[C])
  )
  ->
  (
  G ( 
      ((pr[A]) -> ((atom_p[D]) -> (atom_r[E]))) &
      ((ps[A]) -> ((atom_p[D]) -> (atom_s[E]))) &
      ((qr[A]) -> ((atom_q[D]) -> (atom_r[E]))) &
      ((qs[A]) -> ((atom_q[D]) -> (atom_s[E]))) &
      (~fAIL[D] & ~fAIL[E])
  )
  &
  G (
      (atom_p[B]) -> (~atom_p[D])
    )
  )
)