Intransitive Non-interference (NuSMV)

Description of the Case Study

Intransitive non-interference [RG99] relaxes classic information-flow guarantees by allowing certain flows only when an intermediary participates. We study the shared buffer model of Whalen, Greve, and Wagner [WGW10], featuring a secret process (S), an unclassified process (U), and a scheduler (sched). The scheduler can legitimately relay information from S to U, so observations are considered secure provided two runs use identical scheduling choices. HyperQB evaluates both observational determinism and Goguen–Meseguer non-interference under this intransitive policy, comparing scenarios with and without explicit scheduling control.

The NuSMV model(s)

--(adopted from: Michael W Whalen, David A Greve, and Lucas G Wagner. Model checking information flow. In Design and verification of microprocessor systems for high-assurance applications)
MODULE main
VAR
  P1_sec_in: 0..3;
  P2_unclass_in: 0..3;
  P1_sec_out: 0..3;
  P2_unclass_out: 0..3;

  shared_buffer: 0..3;

  sec_write: boolean;
  sec_read: boolean;

  unclass_write: boolean;
  unclass_read: boolean;

  PC: 1..3;
ASSIGN
  -- Initial Conditions
  init(P1_sec_in):= {0,1,2,3};
  init(P1_sec_out):= 0;
  init(P2_unclass_in):= {0,1,2,3};
  init(P2_unclass_out):= 0;
  init(shared_buffer) := 0;
  init(sec_write):= {TRUE, FALSE};
  init(sec_read):= {TRUE, FALSE};
  init(unclass_write):= {TRUE, FALSE};
  init(unclass_read):= {TRUE, FALSE};
  init(PC) := 1;

  -- Transition Relations
  next(P1_sec_in) := P1_sec_in;
  next(P2_unclass_in) := P2_unclass_in;
  next(sec_write) := sec_write;
  next(sec_read) := sec_read;
  next(unclass_write) := unclass_write;
  next(unclass_read) := unclass_read;

  next(shared_buffer) :=
    case
      ((PC=2) & (sec_write)): P1_sec_in;
      ((PC=2) & (unclass_write)): P2_unclass_in;
      TRUE: shared_buffer;
    esac;

  next(P1_sec_out) :=
    case
      ((PC=3) & (sec_read)) : shared_buffer;
      TRUE: P1_sec_out;
    esac;

  next(P2_unclass_out) :=
    case
      ((PC=3) & (unclass_read)) : shared_buffer;
      TRUE: P2_unclass_out;
    esac;

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

DEFINE
  halt := PC = 3 ;

The HyperLTL formula(s)

Two HyperLTL specifications capture the intransitive variants. The first adapts observational determinism, requiring equal outputs for U whenever both runs observe the same inputs and scheduler decisions. The second expresses intransitive non-interference, insisting that either the secret input is absent or scheduling remains identical across traces.

\[\varphi_{\text{OD}_{\text{intra}}} = \forall \pi_A . \forall \pi_B . \Box \left( in^{U}_{\pi_A} \leftrightarrow in^{U}_{\pi_B} \right) \rightarrow \left( \left( sched_{\pi_A} \leftrightarrow sched_{\pi_B} \right) \mathcal{R} \left( out^{U}_{\pi_A} \leftrightarrow out^{U}_{\pi_B} \right) \right)\]
\[\varphi_{\text{NI}_{\text{intra}}} = \forall \pi_A . \exists \pi_B . \left( \Box \left( (in^{S}_{\pi_A} = \epsilon) \land (out^{U}_{\pi_A} \leftrightarrow out^{U}_{\pi_B}) \right) \lor \Box \left( sched_{\pi_A} \leftrightarrow sched_{\pi_B} \right) \right)\]
Forall A . Forall B .
G((P2_unclass_in[A]=P2_unclass_in[B])
->
(P2_unclass_out[A]=P2_unclass_out[B]))

References