Nondeterministic Inputs and Transitions (NuSMV)¶

Description of the Case Study¶

To assess how nondeterminism affects non-interference verification, we extend the standard information-flow example by allowing integer secrets and observables in the range \(0 \ldots k\). The first variant draws the secret nondeterministically at initialisation, while the second keeps the initial secret fixed but introduces nondeterministic updates on the next transition. HyperQB checks whether these variations still satisfy non-interference, using arithmetic comparisons rather than Boolean equality. Exploring the search space reveals how additional nondeterminism impacts solver performance.

The NuSMV model(s)¶

-- A simple program that violates non-interference
-- 1: LOW=0, HIGH={0....10}
-- 2: if(HIGH>5):
-- 3:   LOW=HIGH
MODULE main
VAR
  HIGH: 0..12;
  LOW: 0..12;
  PC: 1..3;
ASSIGN
  -- Initial Conditions
  init(HIGH):= {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12};
  init(LOW):= {0};
  init(PC):= 1; -- program counter starts at 1.

  -- Transition Relations
  next(HIGH) := HIGH;
  next(LOW) :=
    case
      ((PC=2) & (HIGH>6)): HIGH;
      TRUE: LOW;
    esac;
  next(PC) :=
    case
      (PC=3): 3;
      TRUE: PC+1;
    esac;
DEFINE

-- 1: LOW=0, HIGH={0}
-- 2: HIGH={0...10}
-- 3: if(HIGH>5):
-- 4:   LOW=HIGH
MODULE main
VAR
  HIGH: 0..15;
  LOW: 0..15;
  PC: 1..4;
ASSIGN
  -- Initial Conditions
  init(HIGH):= {0};
  init(LOW):= {0};
  init(PC):= 1; -- program counter starts at 1.

  -- Transition Relations
  next(HIGH):=
    case
      (PC=2): {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
      TRUE: HIGH;
    esac;

  next(LOW) :=
    case
      ((PC=3) & (HIGH>7)): HIGH;
      TRUE: LOW;
    esac;
  next(PC) :=
    case
      (PC=4): 4;
      TRUE: PC+1;
    esac;
DEFINE

The HyperLTL formula(s)¶

Both variants are analysed with the classic \(\forall\exists\) non-interference property, adapted to compare integer values. The existential trace must reproduce the public behaviour of the original run while allowing a different secret.

\[\varphi_{\text{NI}} = \forall \pi_A . \exists \pi_B . \Box \big( \mathit{low}_{\pi_A} = \mathit{low}_{\pi_B} \big) \land \Box \big( \mathit{high}_{\pi_A} \neq \mathit{high}_{\pi_B} \big)\]

Forall A . Exists B .
F~(HIGH[A] = HIGH[B])
&
G(LOW[A] = LOW[B])