Termination-sensitive/-insensitive Non-interference

Description of the Case Study

It is a classic definition [CS10] of whether leaking the information via termination channels is allowed, which derives two notions of non-interference (NI). For termination-insensitive, if one trace terminates, then there must exists another trace that either (1) terminates and obeys NI, or (2) not terminate. That is,

\[\varphi_{\text{tini}} = \forall \pi_A. \exists \pi_B. \Diamond(\mathit{halt}_{\pi_A}) \rightarrow \Box \left( \mathit{halt}_{\pi_B} \rightarrow \left( \left( \mathit{high}_{\pi_A} \neq \mathit{high}_{\pi_B} \right) \land \left( \mathit{low}_{\pi_A} = \mathit{low}_{\pi_B} \right) \right) \right)\]

Termination-sensitive strengthens the property by asking there must exists another trace that terminates and obeys NI. We verify a program from [UTK21] with respect to termination sensitivity. By using optimistic semantics, both return UNSAT, meaning no bugs can be found in the finite exploration. Hence, the program satisfies the properties

Benchmarks

Case #10.1Case #10.2

The Model(s)

NI Example

--NI
--(adpted from: Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Computer Aided Verification: 33rd International Conference, CAV 2021)
MODULE main
-- 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;
-- }

 VAR
	location: 1..7;
	x: 0..10;
	nondet: boolean;
	high: boolean;
	low: 0..5;

--  FROZENVAR
	-- high: boolean;
	-- low: 0..5;

 ASSIGN
	init(location) := 1 ;
	init(nondet) := {TRUE, FALSE};
	init(x) := {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
	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 ;

Formula

forall A. exists B.
F(halt[A]) ->
G(~halt[B] \/ ((halt[B])->((~(high[A]<->high[B])) /\ (*x[A]=x[B]*))))