Intransitive Non-interference

Description of the Case Study

[RG99]. Intransitivity down-grades non-interference (NI) in the cases that the systems secure correct information flow with a thirdparty. Formally, given three parties \(A\), \(B\) and \(C\), while the flow \(A\) to \(C\) is uncertain, intransitive NI permitted such flow if \(A \rightsquigarrow B \land B \rightsquigarrow C\), then \(A \rightsquigarrow C\). In this case we investigate a shared buffer model [WGW10], which contains a secret (S) process, an unclassified (U) process, and a scheduler (sched). The main idea is to prevent U from gaining secret information about S by speculating sched, but imposing that this potential flow is allowable via identical sched. That is, if the two executions agree on sched, the flow from S to U is considered safe. We apply this concept together with classic hyperproperties observational determinism (OD) and non-interference (NI), and wrote two variations that consider intransitivity:

\[\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. \Box \left( \left( in^{S}_{\pi_A} = \epsilon \right) \land \left( out^{U}_{\pi_A} \leftrightarrow out^{U}_{\pi_B} \right) \right) \lor \Box \left( sched_{\pi_A} \leftrightarrow sched_{\pi_B} \right)\]

Benchmarks

Case #9.1Case #9.2Case #9.3

The Model(s)

Unscheduled Buffer

--BUFFER
--(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_Mode: 0..1; -- 0: secure, 1: unclassified
  -- P2_Mode: 0..1; -- 0: secure, 1: unclassified
  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 ;

Formula

forall A. forall B.
G((*P2_unclass_in[A]=P2_unclass_in[B]*)
->
(*P2_unclass_out[A]=P2_unclass_out[B]*))