Secrecy-preserving Refinement (NuSMV)

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\).

The NuSMV model(s)

--(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);

The HyperLTL formula(s)

The synthesis specification nests quantifiers to ensure that every abstract/concrete execution pair can be related by some mapping trace \(\pi_M\) that preserves non-interference. HyperQB searches for a witness mapping, increasing complexity by one alternation over the underlying security requirement.

\[\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)\]
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])
    )
  )
)