Nondeterministic Inputs and Transitions¶
Description of the Case Study¶
To evaluate how nondeterministic choices impact model checking performance, we extend a standard example in two ways.
We first change the high and low as integers ranging \(0 \ldots k\). Next, the model of #14.1 set the initial condition nondeterministically as a number from \(0 \ldots k\). Another model in #14.2, instead, have high initially as \(0\), but on the next transition, have high set to a number \(\le k\).
The HyperLTL formula used is the classic \(\forall\exists\) non-interference, but with arithmetic comparison instead of simply Boolean matching.
Benchmarks¶
The Model(s)
-- (hand-craft)
MODULE main
-- A simple program that violates non-interference
-- 1: LOW=0, HIGH={0....10}
-- 2: if(HIGH>5):
-- 3: LOW=HIGH
--
VAR
HIGH: 0..12;
LOW: 0..12;
PC: 1..3;
ASSIGN
-- Initial Conditions
init(HIGH):= {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12};
init(LOW):= {0};
init(PC):= 1; -- program counter starts at 1.
-- Transition Relations
next(HIGH) := HIGH;
next(LOW) :=
case
((PC=2) & (HIGH>6)): HIGH;
TRUE: LOW;
esac;
next(PC) :=
case
(PC=3): 3;
TRUE: PC+1;
esac;
DEFINE
Formula
forall A. exists B.
F~(*HIGH[A] = HIGH[B]*)
/\
G(*LOW[A] = LOW[B]*)
The Model(s)
-- (hand-craft)
MODULE main
-- A simple program that violates non-interference
--
-- 1: LOW=0, HIGH={0}
-- 2: HIGH={0...10}
-- 3: if(HIGH>5):
-- 4: LOW=HIGH
--
VAR
HIGH: 0..15;
LOW: 0..15;
PC: 1..4;
ASSIGN
-- Initial Conditions
init(HIGH):= {0};
init(LOW):= {0};
init(PC):= 1; -- program counter starts at 1.
-- Transition Relations
next(HIGH):=
case
(PC=2): {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
TRUE: HIGH;
esac;
next(LOW) :=
case
((PC=3) & (HIGH>7)): HIGH;
TRUE: LOW;
esac;
next(PC) :=
case
(PC=4): 4;
TRUE: PC+1;
esac;
DEFINE
Formula
forall A. exists B.
F~(*HIGH[A] = HIGH[B]*)
/\
G(*LOW[A] = LOW[B]*)