Non-interference in multi-threaded programs (NuSMV)

Description of the Case Study

The hyperproperty of non-interference [GM82] states that low-security variables are independent from the high-security variables, thus preserving secure information flow. We consider the concurrent program example in [SV98], where PIN is high security input and Result is low security output. HyperQB returns SAT in the halting pessimistic semantics, indicating that there is a trace that we can spot the difference of high-variables by observing low variables, that is, violating non-interference. With HyperQB we also verified the correctness of a fix to this algorithm, proposed in [SV98] as well. In this case, HyperQB uses the UNSAT results from the solver (with halting optimistic semantics) to infer the absence of a violation.

\[\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} \\ &\qquad ((\mathit{halt}_{\pi_A} \land \mathit{halt}_{\pi_B}) \land (\mathit{Result}_{\pi_A} = \mathit{Result}_{\pi_B})) \big) \end{aligned}\end{split}\]

Benchmarks

The Model(s)

--MULTI-THREADED PROGRAM
--(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
	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;
-- DEFINE
-- 		halt := ((theta_line=0) & (MASK_2=0) & (MASK_1=0) & (MASK_0=0));

Formula

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