Access-Controlled Database: Observational Equivalence (NuSMV)¶

Description of the Case Study¶

The access-controlled database (ACDB) benchmark models two processes that coordinate via locks to print records labelled according to the current access level. Process proc1 is authorised to produce entries A and B; the second, proc2, emits either C or D depending on whether the system is in high-security mode. We analyse the flattened composition produced by asynchronous scheduling and require that observers cannot distinguish executions based solely on the visible outputs. The HyperLTL property demands that for every trace there exists an observationally equivalent one, ensuring that the print sequence never reveals the secret bit controlling the high-mode branch.

The NuSMV model(s)¶

acdb_flattened.smv captures the composed system after encoding the scheduler, while acdb_composed.smv retains the modular structure for reference. The benchmark instantiates the flattened variant for verification.

Note

The flattened model omits the scheduling nondeterminism present in the composed description, enabling HyperQB to explore the reachable state space within the configured bound while preserving the observable traces.

MODULE main
VAR
    -- original globals
	-- use two modules to perform async-composition
	SCHEDULE: 0..1; -- 0:p1 moves, 1:p2 moves
	ID_one: 0..1;
	ID_two: 0..1;
    LOCKED   : boolean;
    in_HIGH  : boolean;

    -- flattened program instances
    proc1.line : 1..5;
    proc2.line : 6..11;

ASSIGN
    init(SCHEDULE) := 0;
    next(SCHEDULE) := 0;

    init(in_HIGH) := {TRUE, FALSE};
    next(in_HIGH) := in_HIGH;

	init(ID_one) := 0;
	next(ID_one) := 0;
	init(ID_two) := 1;
	next(ID_two) := 1;

    init(LOCKED):= FALSE;
    next(LOCKED) :=
        case
            (proc1.line=2): TRUE;
            (proc1.line=5): FALSE;
            (proc2.line=9): TRUE;
            (proc2.line=10): FALSE;
            TRUE: LOCKED;
        esac;

    ----------------------------------------------------------------
    -- proc1 instance (ID_one, initial line = 1)
    ----------------------------------------------------------------
    init(proc1.line) := 1;

    next(proc1.line) := 1;
    ----------------------------------------------------------------
    -- proc2 instance (ID_two, initline = 6)
    ----------------------------------------------------------------
    init(proc2.line) := 6;

    next(proc2.line) := 6;

	DEFINE
        obs_printA := (proc1.line=3);
		obs_printB := (proc1.line=4);
		obs_printC := (proc2.line=6);
		obs_printD := (proc2.line=11);

		-- halting condition
		halt := ((proc1.line=5) & (proc2.line=11));
	

MODULE main
	VAR
		LOCKED: boolean; -- semaphore
		in_HIGH: boolean; -- in_HIGH-value

		-- use two modules to perform async-composition
		SCHEDULE: 0..1; -- 0:p1 moves, 1:p2 moves
		ID_one: 0..1;
		ID_two: 0..1;

		proc1: programs(ID_one, SCHEDULE, LOCKED, in_HIGH, 1);
		proc2: programs(ID_two, SCHEDULE, LOCKED, in_HIGH, 6);

	ASSIGN
		init(ID_one) := 0;
		next(ID_one) := 0;
		init(ID_two) := 1;
		next(ID_two) := 1;
		init(LOCKED):= FALSE;
		next(LOCKED) :=
			case
				(proc1.line=2 | proc1.line=3 | proc1.line=4 | proc2.line=2 | proc2.line=3 | proc2.line=4 ) : TRUE;
				(proc1.line=9 | proc2.line=9) : TRUE;
				TRUE: FALSE;
			esac;
		init(SCHEDULE) := {0,1};
		next(SCHEDULE) :=
			case
				(proc1.line=5): 1;
				(proc2.line=11): 0;
				TRUE: {0,1};
			esac;

		init(in_HIGH):= {TRUE, FALSE};
		next(in_HIGH):= in_HIGH;

	DEFINE
		-- halting condition
		halt := ((proc1.line=5) & (proc2.line=11));
		obs_printA := (proc1.line=3);
		obs_printB := (proc1.line=4);
		obs_printC := (proc2.line=6);
		obs_printD := (proc2.line=11);


MODULE programs(ID, SCHEDULE, LOCKED, in_HIGH, initline)
	VAR
		line: 1..11;

	ASSIGN
		init(line) := initline;
		next(line) :=
			case
				(!(SCHEDULE=ID)) : line;
				-- program1,diameter=4
				(line=1 & LOCKED) : {1}; -- wait if LOCKED
				(line=1 & !LOCKED) : {2}; -- else go to 2
				(line=2) : {3}; -- LOCK it
				(line=3) : {4}; -- print A
				(line=4) : {5}; -- print B
				(line=5) : {5}; -- UNLOCK, END
				-- program2,diameter==5
				(line=6) : {7}; -- print C
				(line=7 & in_HIGH) : {8}; -- if in_HIGH, proceed
				(line=7 & !in_HIGH) : {11}; -- if !in_HIGH, skip to end
				(line=8 & LOCKED) : {8}; -- wait if LOCKED
				(line=8 & !LOCKED) : {9}; -- else, proceed
				(line=9) : {10}; -- LOCK
				(line=10) : {11}; -- UNLOCKEd
				(line=11) : {11}; -- print D, END
				TRUE: line;
			esac;

The HyperLTL formula(s)¶

The equivalence requirement states that every observable event emitted by proc1 and proc2 must match across the original trace \(\pi_A\) and the witness \(\pi_B\) at each time instant \(t\). HyperQB solves the model under halting pessimistic semantics, confirming that the database preserves confidentiality with respect to the four published outputs.

\[\varphi_{\text{ACDB}} = \forall \pi_A . \exists \pi_B . \exists t . \Box\Big( obs\_printA_{\pi_A}[t] = obs\_printA_{\pi_B}[t] \land obs\_printB_{\pi_A}[t] = obs\_printB_{\pi_B}[t] \land obs\_printC_{\pi_A}[t] = obs\_printC_{\pi_B}[t] \land obs\_printD_{\pi_A}[t] = obs\_printD_{\pi_B}[t] \Big)\]

Forall A . Exists B . E t .  
G(
    (obs_printA[A][t] = obs_printA[B][t])
    &
    (obs_printB[A][t] = obs_printB[B][t])
    &
    (obs_printC[A][t] = obs_printC[B][t])
    &
    (obs_printD[A][t] = obs_printD[B][t])
)