Termination-sensitive/-insensitive Non-interference (NuSMV)

Description of the Case Study

Termination channels allow secrets to leak by influencing whether a program halts. Clarkson and Schneider [CS10] distinguish between termination-insensitive non-interference (TINI) and termination-sensitive non-interference (TSNI). We study the example from Unno, Terauchi, and Koskinen [UTK21], checking both notions with HyperQB. Under optimistic semantics the solver returns UNSAT for both properties, indicating no finite counterexample exists—thus the program satisfies both TINI and TSNI.

The NuSMV model(s)

--(adpted from: Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Computer Aided Verification: 33rd International Conference, CAV 2021)

-- gniEx(bool high, int low) {
--   1 if (high)
--      { int x = ndet_int ; // here we assign at the beginning
--   2    if (x >= low)
--   3      { return x; }
--   4    else { while (true) {} } }
--     else {
--   5   int x = low;
--       while ( ndet_bool ) {
--   6        x++; }
--       return x;
-- }

MODULE main
 VAR
	location: 1..7;
	x: 0..10;
	nondet: boolean;
	high: boolean;
	low: 0..5;
 ASSIGN
	init(location) := 1 ;
	init(nondet) := {TRUE, FALSE};
	init(x) := {0, 1, 2, 3, 4, 5};
	init(low) := {0, 1, 2, 3, 4, 5};
	next(low) := low;
	init(high) := {TRUE, FALSE};
	next(high) := high;

	next(location) := case
		((location = 1) & high): 2;
		((location = 1) & !high): 5;
		((location = 2) & (x >= low)) : 3;
		((location = 2) & (x < low)) : 4;
		((location = 5) & !nondet) : 3;
		((location = 5) & nondet) : 6;
		((location = 6) & !nondet) : 3;
		((location = 6) & nondet & (x < 10)) : 6;
		((location = 6) & nondet & (x = 10)) : 7;
		TRUE: location ;
	esac;

	next(x) := case
		(location = 5): low;
		((location = 6) & (x < 10)): x + 1;
		TRUE: x;
	esac;

	next(nondet) := case
		((location = 5) | (location = 6)): {TRUE, FALSE};
		TRUE: nondet;
	esac;

DEFINE
	halt := (location = 3) ;

The HyperLTL formula(s)

The two properties differ in how they treat the halting trace. TINI allows the witness trace to diverge, while TSNI insists on matching termination. HyperQB evaluates both specifications to confirm the absence of termination leaks.

\[\varphi_{\text{TINI}} = \forall \pi_A . \exists \pi_B . \Big( \Diamond \mathit{halt}_{\pi_A} \rightarrow \Box \big( \mathit{halt}_{\pi_B} \rightarrow (\mathit{high}_{\pi_A} \neq \mathit{high}_{\pi_B} \land \mathit{low}_{\pi_A} = \mathit{low}_{\pi_B}) \big) \Big)\]
\[\varphi_{\text{TSNI}} = \forall \pi_A . \exists \pi_B . \Box \big( \mathit{halt}_{\pi_A} \leftrightarrow \mathit{halt}_{\pi_B} \big) \land \Box \big( \mathit{high}_{\pi_A} \neq \mathit{high}_{\pi_B} \rightarrow \mathit{low}_{\pi_A} = \mathit{low}_{\pi_B} \big)\]
Forall A . Exists B .
F(halt[A]) ->
G(~halt[B] | ((halt[B])->((~(high[A]=high[B])) & (x[A]=x[B]))))

References