Theory Second_Example
chapter ‹Second Example›
theory %invisible Second_Example
imports Main
begin
text ‹\label{chap:exampleII}›
text ‹Pop-refinement is illustrated via a simple derivation,
in Isabelle/HOL,
of a non-deterministic program that satisfies a hyperproperty.›
section ‹Hyperproperties›
text ‹\label{sec:hyper}›
text ‹Hyperproperties are predicates over sets of traces~%
\<^cite>‹"ClarksonSchneiderHyperproperties"›.
Hyperproperties capture security policies
like non-interference~\<^cite>‹"GoguenMeseguerNonInterference"›,
which applies to deterministic systems,
and generalized non-interference (GNI)~\<^cite>‹"McCulloughSpecificationsMLS"›,
which generalizes non-interference to non-deterministic systems.›
text ‹The formulation of GNI in~\<^cite>‹"ClarksonSchneiderHyperproperties"›,
which is derived from~\<^cite>‹"McLeanPossibilisticProperties"›,
is based on:
\begin{itemize}
\item
A notion of traces as infinite streams of abstract states.
\item
Functions that map each state to low and high inputs and outputs,
where `low' and `high' have the usual security meaning
(e.g.\ `low' means `unclassified' and `high' means `classified').
These functions are homomorphically extended to map each trace
to infinite streams of low and high inputs and outputs.
\end{itemize}
The following formulation is slightly more general,
because the functions that return low and high inputs and outputs
operate directly on abstract traces.›
text ‹GNI says that for any two traces @{term τ⇩1} and @{term τ⇩2},
there is always a trace @{term τ⇩3} with
the same high inputs as @{term τ⇩1}
and the same low inputs and low outputs as @{term τ⇩2}.
Intuitively, this means that a low observer
(i.e.\ one that only observes low inputs and low outputs of traces)
cannot gain any information about high inputs
(i.e.\ high inputs cannot interfere with low outputs)
because observing a trace @{term τ⇩2}
is indistinguishable from observing some other trace @{term τ⇩3}
that has the same high inputs as an arbitrary trace @{term τ⇩1}.›
locale generalized_non_interference =
fixes low_in :: "'τ ⇒ 'i"
fixes low_out :: "'τ ⇒ 'o"
fixes high_in :: "'τ ⇒ 'i"
fixes high_out :: "'τ ⇒ 'o"
definition (in generalized_non_interference) GNI :: "'τ set ⇒ bool"
where "GNI 𝒯 ≡
∀τ⇩1 ∈ 𝒯. ∀τ⇩2 ∈ 𝒯. ∃τ⇩3 ∈ 𝒯.
high_in τ⇩3 = high_in τ⇩1 ∧ low_in τ⇩3 = low_in τ⇩2 ∧ low_out τ⇩3 = low_out τ⇩2"
section ‹Target Programming Language›
text ‹\label{sec:targetII}›
text ‹In the target language used in this example,%
\footnote{Even though this language has many similarities
with the language in \secref{sec:targetI},
the two languages are defined separately
to keep \chapref{chap:exampleI} simpler.}
a program consists of
a list of distinct state variables
and a body of statements.
The statements modify the variables
by deterministically assigning results of expressions
and by non-deterministically assigning random values.
Expressions are built out of
non-negative integer constants,
state variables,
and addition operations.
Statements are combined
via conditionals, whose tests compare expressions for equality,
and via sequencing.
Each variable stores a non-negative integer.
Executing the body in a state yields a new state.
Because of non-determinism, different new states are possible,
i.e.\ executing the body in the same state
may yield different new states at different times.›
text ‹For instance, executing the body of the program
\begin{verbatim}
prog {
vars {
x
y
}
body {
if (x == y + 1) {
x = 0;
} else {
x = y + 3;
}
randomize y;
y = y + 2;
}
}
\end{verbatim}
in the state where \verb|x| contains 4 and \verb|y| contains 7,
yields a new state where
\verb|x| always contains 10
and \verb|y| may contain any number in $\{2,3,\ldots\}$.›
subsection ‹Syntax›
text ‹\label{sec:syntaxII}›
text ‹Variables are identified by names.›
type_synonym name = string
text ‹Expressions are built out of
constants, variables, and addition operations.›