Non-interference: Multi-threaded Programs (NuSMV)

Description of the Case Study

Non-interference [GM82] demands that changes to confidential inputs cannot be observed through public outputs. We analyse the concurrent program introduced by Smith and Volpano [SV98], where the high-security input PIN controls whether the low-security output Result reveals sensitive information. The benchmark includes both the original, vulnerable implementation and the repaired version proposed in the paper. Using HyperQB under halting pessimistic semantics we obtain a satisfying witness for the buggy program—demonstrating that two runs differing only in PIN can expose the secret via Result. Switching to the fixed implementation and halting optimistic semantics, HyperQB proves unsatisfiability, confirming that the repaired program enforces non-interference.

The NuSMV model(s)

--(adopted from: Geoffrey Smith and Dennis M. Volpano. Secure information flow in a multithreaded imperative language. In Proc. of the 25th ACM Symposium on Principles of Programming Languages (POPL’98))
-- //// TRIGGER 0
-- // 0   trigger0 loops if (mask != 0) else go to line25
-- // 1        - while (trigger0 == 0) do nothing
-- // 2		- result = result OR mask
-- // 3		- trigger0 = 0
-- // 4		- maintrigger = matrigger + 1
-- // 5 		- if maintrigger = 1, then trigger1 = 1
-- // 6 		- if (mask != 0 and trigger0 = 0) back to line 1
-- //// TRIGGER 1
-- // 8	trigger1 loops if (mask != 0) else go to line25
-- // 9		- while (trigger1 == 0) do nothing
-- // 10		- result = result AND compliment(mask)
-- // 11		- trigger1 = 0
-- // 12   	- maintrigger = maintriger + 1
-- // 13       - if maintrigger = 1, then trigger0 = 1
-- // 14		- if (mask != 0 and trigger1 = 0) back to line 9
-- //// MAIN TRIGGER
-- // 16	maintrigger starts:
-- // 17		- while (mask != 0) // Hm mm
-- // 18		- maintrigger = 0
-- // 19		- if (PIN & Mask = 0)
-- // 20		- trigger0 = 1
-- // 21		- else    trigger1 = 1
-- // 22		while (maintrigger != 2) loop
-- // 23		mask = mask / 2


MODULE main
VAR
	PIN_0 : 0..1;
    PIN_1 : 0..1;
    PIN_2 : 0..1;

    MASK_0 : 0..1;
    MASK_1 : 0..1;
    MASK_2 : 0..1;

    RESULT_0 : 0..1;
    RESULT_1 : 0..1;
    RESULT_2 : 0..1;
    
	main_trigger: 0..2;
	trigger_alpha: boolean;
	trigger_beta: boolean;

	alpha_line: 0..6;
	beta_line: 0..6;
	theta_line: 0..6;

	halt : boolean;

ASSIGN

	init(halt) := FALSE;
	next(halt) :=
	case
		((theta_line=0) & (MASK_2=0) & (MASK_1=0) & (MASK_0=0)) : TRUE;
		TRUE: halt;
	esac;
	-- when PIN is arbitrary, small PINs such as 001, is leaking information
	init(PIN_2) := {1,0}; init(PIN_1) := {1,0}; init(PIN_0) := {1,0};
	init(MASK_2) := 1; init(MASK_1) := 0; init(MASK_0) := 0;
	-- the lines of each process
	init(alpha_line) := 0;
	init(beta_line) := 0;
	init(theta_line) := 0;

	init(RESULT_0) := 0; init(RESULT_1) := 0; init(RESULT_2) := 0;

	init(main_trigger) := 0;
	init(trigger_alpha) := FALSE;
	init(trigger_beta) := FALSE;

	next(PIN_2) := PIN_2;
	next(PIN_1) := PIN_1;
	next(PIN_0) := PIN_0;

	next(RESULT_2) :=
		case
			((alpha_line = 2) &  ((RESULT_2 = 1) | (MASK_2 = 1))) : 1;
			((alpha_line = 2) & !((RESULT_2 = 1) | (MASK_2 = 1))) : 0;
			((beta_line = 2)  &  ((RESULT_2 = 1) & (MASK_2 = 0))) : 1;
			((beta_line = 2)  & !((RESULT_2 = 1) & (MASK_2 = 0))) : 0;
			TRUE: RESULT_2;
		esac;

	next(RESULT_1) :=
		case
			((alpha_line = 2) &  ((RESULT_1 = 1) | (MASK_1 = 1))) : 1;
			((alpha_line = 2) & !((RESULT_1 = 1) | (MASK_1 = 1))) : 0;
			((beta_line = 2)  &  ((RESULT_1 = 1) & (MASK_1 = 0))) : 1;
			((beta_line = 2)  & !((RESULT_1 = 1) & (MASK_1 = 0))) : 0;
			TRUE: RESULT_1;
		esac;

	next(RESULT_0) :=
		case
			((alpha_line = 2) & ((RESULT_0 = 1) | (MASK_0 = 1))) : 1;
			((alpha_line = 2) & !((RESULT_0 = 1) | (MASK_0 = 1))) : 0;
			((beta_line = 2) & ((RESULT_0 = 1) & (MASK_0 = 0))) : 1;
			((beta_line = 2) & !((RESULT_0 = 1) & (MASK_0 = 0))) : 0;
			TRUE: RESULT_0;
		esac;

	next(MASK_2) :=
		case
			((theta_line = 6) & (MASK_2 = 1)) : 0;
			TRUE: MASK_2;
		esac;

	next(MASK_1) :=
		case
			((theta_line = 6) & (MASK_2 = 1)) : 1; -- divided by 2
			((theta_line = 6) & (MASK_1 = 1)) : 0;
			TRUE: MASK_1;
		esac;

	next(MASK_0) :=
		case
			((theta_line = 6) & (MASK_1 = 1)) : 1; -- divided by 2
			((theta_line = 6) & (MASK_0 = 1)) : 0;
			TRUE: MASK_0;
		esac;


	next(main_trigger) :=
		case
			(theta_line = 1) : 0;
			((alpha_line = 4) & (main_trigger = 0)) : 1;
			((alpha_line = 4) & (main_trigger = 1)) : 2;
			((beta_line = 4) & (main_trigger = 0)) : 1;
			((beta_line = 4) & (main_trigger = 1)) : 2;
			TRUE : main_trigger;
		esac;

	next(trigger_alpha) :=
		case
			(theta_line = 3) : TRUE;
			((beta_line = 5) & (main_trigger = 1)) : TRUE;
			(alpha_line = 3) : FALSE;
			TRUE: trigger_alpha;
		esac;

	next(trigger_beta) :=
		case
			(theta_line = 4) : TRUE;
			((alpha_line = 5) & (main_trigger = 1)) : TRUE;
			(beta_line = 3) : FALSE;
			TRUE: trigger_beta;
		esac;

	next(alpha_line) :=
		case
			((alpha_line = 0) & ((MASK_2 = 0) & (MASK_1 = 0) & (MASK_0 = 0))) : {0}; -- END
			((alpha_line = 0) & !((MASK_2 = 0) & (MASK_1 = 0) & (MASK_0 = 0))) : {1};
			((alpha_line = 1) & (trigger_alpha = FALSE)) : {1};
			((alpha_line = 1) & (trigger_alpha = TRUE)) : {2};
			(alpha_line = 2) : {3}; -- result = result OR mask
			(alpha_line = 3) : {4}; -- trigger0 = 0
			(alpha_line = 4) : {5}; -- maintrigger = matrigger + 1
			(alpha_line = 5) : {6}; -- if maintrigger = 1, then trigger1 = 1
			(alpha_line = 6) : {0}; -- if (mask != 0 and trigger0 = 0) back to line 1
		esac;

	next(beta_line) :=
		case
			((beta_line = 0) & ((MASK_2 = 0) & (MASK_1 = 0) & (MASK_0 = 0))) : {0}; -- END
			((beta_line = 0) & !((MASK_2 = 0) & (MASK_1 = 0) & (MASK_0 = 0))) : {1};
			((beta_line = 1) & (trigger_beta = FALSE)) : {1};
			((beta_line = 1) & (trigger_beta = TRUE)) : {2};
			(beta_line = 2) : {3}; -- result = result AND complement(mask)
			(beta_line = 3) : {4}; -- trigger1 = 0
			(beta_line = 4) : {5}; -- maintrigger = maintrigger + 1
			(beta_line = 5) : {6}; -- if maintrigger = 1, then trigger0 = 1
			(beta_line = 6) : {0}; -- if (mask != 0 and trigger1 = 0) back to line 1
		esac;

	next(theta_line) :=
		case
			((theta_line = 0) & ((MASK_2 = 0) & (MASK_1 = 0) & (MASK_0 = 0))) : {0};
			((theta_line = 0) & !((MASK_2 = 0) & (MASK_1 = 0) & (MASK_0 = 0))) : {1};
			(theta_line = 1) : {2}; -- maintrigger = 0
			((theta_line = 2) & ((PIN_2 = MASK_2) & (PIN_1 = MASK_1) & (PIN_0 = MASK_0))) : {3}; -- if (PIN & Mask = 0)
			(theta_line = 3) : {5}; -- trigger_alpha = 1
			((theta_line = 2) & !((PIN_2 = MASK_2) & (PIN_1 = MASK_1) & (PIN_0 = MASK_0))) : {4}; -- if !(PIN & Mask = 0)
			(theta_line = 4) : {5}; -- trigger_beta = 1
			((theta_line = 5) & !(main_trigger = 2)) : {5}; -- while (maintrigger != 2) loop
			((theta_line = 5) & (main_trigger = 2)) : {6}; -- proceed
			(theta_line = 6) : {0}; -- mask = mask / 2
		esac;

The HyperLTL formula(s)

The property below captures termination-sensitive non-interference. Two executions must agree on the publicly observable output Result whenever both runs terminate, even if they start with different secret inputs. The until operator constrains the traces until simultaneous halting, ensuring observable equivalence once both executions finish.

\[\begin{split}\begin{aligned} \varphi_{\text{NI}} = {} & \forall \pi_A . \exists \pi_B . (\mathit{PIN}_{\pi_A} \neq \mathit{PIN}_{\pi_B}) \land \\ & \big( (\neg \mathit{halt}_{\pi_A} \lor \neg \mathit{halt}_{\pi_B}) \ \mathcal{U} \ ((\mathit{halt}_{\pi_A} \land \mathit{halt}_{\pi_B}) \land (\mathit{Result}_{\pi_A} = \mathit{Result}_{\pi_B})) \big) \end{aligned}\end{split}\]
Forall A . Exists B . F~((PIN_2[A] = PIN_2[B]) & (PIN_1[A] = PIN_1[B]) & (PIN_0[A] = PIN_0[B])) & ( (~halt[A] | ~halt[B]) U ((halt[A] & halt[B]) & ((RESULT_2[A] = RESULT_2[B]) & (RESULT_1[A] = RESULT_1[B]) & (RESULT_0[A] = RESULT_0[B]))))

References