|
|
|
|
@ -0,0 +1,717 @@
|
|
|
|
|
(*
|
|
|
|
|
* Copyright 2020, The University of Melbourne (ABN 84 002 705 224)
|
|
|
|
|
*
|
|
|
|
|
* SPDX-License-Identifier: BSD-2-Clause
|
|
|
|
|
*
|
|
|
|
|
* Developers of future substantial additions to this tutorial may wish to
|
|
|
|
|
* append their names to the author list in its document root.tex file.
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
theory EquivValidTutorial
|
|
|
|
|
imports Lib.EquivValid
|
|
|
|
|
begin
|
|
|
|
|
|
|
|
|
|
text \<open>
|
|
|
|
|
This tutorial provides a basic introduction to the seL4 verification repository's
|
|
|
|
|
EquivValid library, which formalises proof machinery first
|
|
|
|
|
introduced by the CPP'12 paper:
|
|
|
|
|
``Noninterference for Operating System Kernels''
|
|
|
|
|
by Murray, Matichuk, Brassil, Gammie, and Klein \cite{Murray_MBGK_12}.
|
|
|
|
|
This mostly comes in the form of worked examples.
|
|
|
|
|
|
|
|
|
|
EquivValid statements are used to phrase seL4's information-flow security lemmas,
|
|
|
|
|
because they can be used to assert that a function preserves (or establishes)
|
|
|
|
|
``observable equivalence'' of system state, as seen by some attacker model.
|
|
|
|
|
The ``Valid'' part of EquivValid is based on the fact that the Isabelle definition
|
|
|
|
|
for Hoare triples in the seL4 proof base is called \<open>valid\<close>. The EquivValid statements
|
|
|
|
|
\<open>equiv_valid\<close>, \<open>equiv_valid_2\<close> are therefore the ``equivalence'' versions of \<open>valid\<close>.
|
|
|
|
|
In \cite{Murray_MBGK_12},
|
|
|
|
|
EquivValid statements are referred to as ``ev'' or ``ev2'' statements.
|
|
|
|
|
These roughly (but not exactly) correspond to \<open>equiv_valid\<close> and \<open>equiv_valid_2\<close>
|
|
|
|
|
(resp.) in the Isabelle theories.
|
|
|
|
|
|
|
|
|
|
This tutorial will assume that the reader knows how to use the weakest precondition tool,
|
|
|
|
|
``wp'', to discharge Hoare triples. More information on this is available in the
|
|
|
|
|
Lib.WPTutorial theory in the seL4 verification repo.
|
|
|
|
|
\<close>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section \<open> Preliminaries \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> It will be best to think of an EquivValid statement as akin to a Hoare triple.
|
|
|
|
|
Recall that a Hoare triple consists of a precondition, function, and postcondition.
|
|
|
|
|
This following basic example of a Hoare triple asserts that, for any \<^emph>\<open>single\<close> run
|
|
|
|
|
of the function \<open>f\<close>, assuming the precondition \<open>P\<close> holds prior to that run,
|
|
|
|
|
the postcondition \<open>Q\<close> will hold afterwards. \<close>
|
|
|
|
|
|
|
|
|
|
term "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
|
|
|
|
|
thm valid_def
|
|
|
|
|
|
|
|
|
|
text \<open> Similarly to a Hoare triple, an EquivValid statement makes an assertion
|
|
|
|
|
about the possible executions (or ``runs'') of some function.
|
|
|
|
|
However, rather than making an assertion about single runs of the function,
|
|
|
|
|
it instead makes assertions about \<^emph>\<open>relations between\<close> runs of that function.
|
|
|
|
|
In this sense, EquivValid statements could be thought of as \<^emph>\<open>relational\<close> Hoare triples. \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> This tutorial will introduce some syntactic sugar to emphasise the similarity
|
|
|
|
|
between Hoare triples and EquivValid statements.
|
|
|
|
|
(Here, \<open>\<top>\<top>\<close> is an alias provided by Lib.NonDetMonad for the trivial binary predicate,
|
|
|
|
|
which always returns \<open>True\<close>; similarly, there is also \<open>\<bottom>\<bottom>\<close> for \<open>False\<close>.) \<close>
|
|
|
|
|
|
|
|
|
|
abbreviation
|
|
|
|
|
equiv_valid_sugar ::
|
|
|
|
|
"('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s,'b) nondet_monad \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
|
|
|
|
|
("\<lbrace>|_|, _\<rbrace>/ _ /\<lbrace>|_|\<rbrace>")
|
|
|
|
|
where
|
|
|
|
|
"\<lbrace>|A|, P\<rbrace> f \<lbrace>|B|\<rbrace> \<equiv> equiv_valid \<top>\<top> A B P f"
|
|
|
|
|
|
|
|
|
|
text \<open> This most basic form of an EquivValid statement asserts that,
|
|
|
|
|
for any \<^emph>\<open>pair\<close> of runs of the function \<open>f\<close>,
|
|
|
|
|
assuming the \<^emph>\<open>pre-equivalence\<close> \<open>A\<close> relates the initial states of the two runs
|
|
|
|
|
(and the precondition \<open>P\<close> holds initially for both runs),
|
|
|
|
|
the \<^emph>\<open>post-equivalence\<close> \<open>B\<close> will relate the final states of the two runs afterwards. \<close>
|
|
|
|
|
|
|
|
|
|
term "\<lbrace>|A|, P\<rbrace> f \<lbrace>|B|\<rbrace>"
|
|
|
|
|
term "equiv_valid \<top>\<top> A B P f"
|
|
|
|
|
|
|
|
|
|
text \<open> The following Isabelle theorem in the EquivValid library gives
|
|
|
|
|
a definition for \<open>equiv_valid\<close> that is closest to that of ``ev'' as presented in
|
|
|
|
|
\cite{Murray_MBGK_12};
|
|
|
|
|
this is what we will use to unfold \<open>equiv_valid\<close> statements in this tutorial: \<close>
|
|
|
|
|
|
|
|
|
|
thm equiv_valid_def2[simplified equiv_valid_2_def]
|
|
|
|
|
|
|
|
|
|
text \<open> In the seL4 EquivValid library, the \<open>equiv_valid\<close> definition also includes,
|
|
|
|
|
as a convenience, an \<^emph>\<open>invariant equivalence\<close> \<open>I\<close> that it asserts as both pre- and
|
|
|
|
|
post-equivalence. We will ignore this convenience for the rest of this tutorial. \<close>
|
|
|
|
|
|
|
|
|
|
lemma "equiv_valid I \<top>\<top> \<top>\<top> P f = equiv_valid \<top>\<top> I I P f"
|
|
|
|
|
unfolding equiv_valid_def2 equiv_valid_2_def
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> Furthermore, the library version of \<open>equiv_valid\<close> is defined in terms of a
|
|
|
|
|
version \<open>spec_equiv_valid\<close> that supports restricting the attention of the statement to
|
|
|
|
|
a particular initial state. We will avoid encountering \<open>spec_equiv_valid\<close> for the rest
|
|
|
|
|
of this tutorial, by unfolding \<open>equiv_valid_def2\<close> instead of \<open>equiv_valid_def\<close>. \<close>
|
|
|
|
|
|
|
|
|
|
\<comment> \<open>Specialised\<close>
|
|
|
|
|
thm equiv_valid_def
|
|
|
|
|
equiv_valid_def[simplified spec_equiv_valid_def equiv_valid_2_def]
|
|
|
|
|
|
|
|
|
|
text \<open> Finally, the library also contains both simplified and more general forms of
|
|
|
|
|
EquivValid statement; the more general forms allow proof engineers to specify the
|
|
|
|
|
equivalences and functions on which they are asserted in a more fine-grained fashion
|
|
|
|
|
than is allowed by \<open>equiv_valid\<close>. These will be addressed further later in this tutorial. \<close>
|
|
|
|
|
|
|
|
|
|
\<comment> \<open>Simplified for A = B.\<close>
|
|
|
|
|
lemma "equiv_valid_inv I A P f" unfolding equiv_valid_def2 oops
|
|
|
|
|
\<comment> \<open>Generalised to allow specifying equivalence R on return values.\<close>
|
|
|
|
|
lemma "equiv_valid_rv_inv I A R P f" unfolding equiv_valid_2_def oops
|
|
|
|
|
\<comment> \<open>Generalised further.\<close>
|
|
|
|
|
lemma "equiv_valid_rv I A B R P f" unfolding equiv_valid_2_def oops
|
|
|
|
|
lemma "equiv_valid_2 I A B R P P' f f'" unfolding equiv_valid_2_def oops
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section \<open> Example setting: a room with a view \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> EquivValid statements assert equivalences between system states in alternative runs
|
|
|
|
|
of a given program; for this tutorial we define a basic structure for the system state: \<close>
|
|
|
|
|
|
|
|
|
|
record 'val Room =
|
|
|
|
|
desk :: 'val
|
|
|
|
|
window :: 'val
|
|
|
|
|
outbox :: 'val
|
|
|
|
|
inbox :: 'val
|
|
|
|
|
job :: "'val \<Rightarrow> 'val"
|
|
|
|
|
|
|
|
|
|
text \<open> The state equivalences of interest will then be of the kind
|
|
|
|
|
``\<open>desk\<close> has the same value in both states'', and so forth.
|
|
|
|
|
We will typically use these to specify the attacker's assumed ability to make
|
|
|
|
|
observations of (or otherwise know) the contents of those parts of the state. \<close>
|
|
|
|
|
|
|
|
|
|
definition desk_equivalence :: "'val Room \<Rightarrow> 'val Room \<Rightarrow> bool"
|
|
|
|
|
where
|
|
|
|
|
"desk_equivalence r1 r2 \<equiv> desk r1 = desk r2"
|
|
|
|
|
|
|
|
|
|
definition window_equivalence :: "'val Room \<Rightarrow> 'val Room \<Rightarrow> bool"
|
|
|
|
|
where
|
|
|
|
|
"window_equivalence r1 r2 \<equiv> window r1 = window r2"
|
|
|
|
|
|
|
|
|
|
text \<open> We could just as well define equivalences similarly for
|
|
|
|
|
\<open>inbox\<close>, \<open>outbox\<close>, or \<open>job\<close> -- we omit these here. \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> Furthermore, you can use the \<open>And\<close> alias provided by Lib.NonDetMonad
|
|
|
|
|
to write the conjunction of two binary predicates.
|
|
|
|
|
(Similarly, there is also an \<open>Or\<close> alias for disjunction.)\<close>
|
|
|
|
|
|
|
|
|
|
thm bipred_conj_def bipred_disj_def
|
|
|
|
|
lemma
|
|
|
|
|
"(desk_equivalence And window_equivalence) r1 r2 =
|
|
|
|
|
(desk r1 = desk r2 \<and> window r1 = window r2)"
|
|
|
|
|
unfolding bipred_conj_def desk_equivalence_def window_equivalence_def
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> In this setting, we might consider a trivial program that just returns
|
|
|
|
|
the contents of \<open>desk\<close>; note, there is no difference between these two ways
|
|
|
|
|
of expressing it: \<close>
|
|
|
|
|
lemma "gets desk = do document \<leftarrow> gets desk; return document od"
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> Or, we might consider some programs that transfer values from one part
|
|
|
|
|
of the state to another, write constants to state, execute functions
|
|
|
|
|
that can themselves be found in state, or some combination of these: \<close>
|
|
|
|
|
|
|
|
|
|
definition reveal_desk_to_window :: "('val Room, unit) nondet_monad"
|
|
|
|
|
where
|
|
|
|
|
"reveal_desk_to_window \<equiv> modify (\<lambda>s. s\<lparr>window := desk s\<rparr>)"
|
|
|
|
|
|
|
|
|
|
definition sanitise_desk :: "('val::zero Room, unit) nondet_monad"
|
|
|
|
|
where
|
|
|
|
|
"sanitise_desk \<equiv> modify (\<lambda>s. s\<lparr>desk := 0\<rparr>)"
|
|
|
|
|
|
|
|
|
|
definition work_at_desk :: "('val Room, unit) nondet_monad"
|
|
|
|
|
where
|
|
|
|
|
"work_at_desk \<equiv>
|
|
|
|
|
do modify (\<lambda>s. s\<lparr>desk := inbox s\<rparr>);
|
|
|
|
|
modify (\<lambda>s. s\<lparr>desk := (job s) (desk s)\<rparr>);
|
|
|
|
|
modify (\<lambda>s. s\<lparr>outbox := desk s\<rparr>)
|
|
|
|
|
od"
|
|
|
|
|
|
|
|
|
|
definition work_sanitise_reveal :: "('val::zero Room, unit) nondet_monad"
|
|
|
|
|
where
|
|
|
|
|
"work_sanitise_reveal \<equiv>
|
|
|
|
|
do work_at_desk;
|
|
|
|
|
sanitise_desk;
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
od"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section \<open> Attacker models expressible using EquivValid statements \<close>
|
|
|
|
|
|
|
|
|
|
subsection \<open> An attacker with access to return values \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> The most basic form of \<open>equiv_valid\<close> asserts an information-flow security property
|
|
|
|
|
that would be appropriate against an attacker that can see only the program's return value:
|
|
|
|
|
that any two runs of this program will give the same return value.\footnote{If you think
|
|
|
|
|
this doesn't sound like a very useful program, you'd be spot on: Our goal here is
|
|
|
|
|
to prove that the program would be stubbornly uninformative to such an attacker.}
|
|
|
|
|
|
|
|
|
|
Of course, we will find that we can't expect to prove this unless we place some
|
|
|
|
|
restrictions on the runs under consideration.
|
|
|
|
|
Consider the case where we are maximally permissive with the pre- and post-equivalences
|
|
|
|
|
(by supplying \<open>\<top>\<top>\<close>) and precondition (by supplying \<open>\<top>\<close>): \<close>
|
|
|
|
|
|
|
|
|
|
lemma gets_desk_return_leak:
|
|
|
|
|
\<comment> \<open> No restrictions on pre-equivalence, precondition, or post-equivalence. \<close>
|
|
|
|
|
"\<lbrace>|\<top>\<top>|, \<top>\<rbrace> gets desk \<lbrace>|\<top>\<top>|\<rbrace>"
|
|
|
|
|
find_theorems intro
|
|
|
|
|
\<comment> \<open> There happens to be an applicable \<open>gets\<close> rule for \<open>equiv_valid_inv\<close>. \<close>
|
|
|
|
|
thm gets_ev''
|
|
|
|
|
apply(rule gets_ev'')
|
|
|
|
|
\<comment> \<open> \<open>equiv_valid\<close> requires the return value to be the same in both runs.
|
|
|
|
|
As expected, we are stuck, as we don't know that the contents of \<open>desk\<close>
|
|
|
|
|
were initially the same for both runs. \<close>
|
|
|
|
|
nitpick
|
|
|
|
|
oops
|
|
|
|
|
|
|
|
|
|
text \<open> How might we know that \<open>gets desk\<close> will return the same value for each of
|
|
|
|
|
a given pair of runs?
|
|
|
|
|
|
|
|
|
|
One way we might know this is if the pre-equivalence tells us that we can assume
|
|
|
|
|
that \<open>desk\<close> initially has the same value in both runs.
|
|
|
|
|
This might be appropriate to assume, for example:
|
|
|
|
|
(1) after executing some function that equalises the value of \<open>desk\<close> between
|
|
|
|
|
all runs under consideration, or
|
|
|
|
|
(2) when the attacker already knows the contents of \<open>desk\<close>.
|
|
|
|
|
Note that these are just two ways of saying that we consider it to be acceptable
|
|
|
|
|
for the attacker to know the initial contents of \<open>desk\<close>.
|
|
|
|
|
|
|
|
|
|
We can specify this formally by setting \<open>desk_equivalence\<close> as the pre-equivalence.%
|
|
|
|
|
\footnote{To avoid complicating things for now, we'll also set the post-equivalence
|
|
|
|
|
to be the same as the pre-equivalence. Examples of proving \<open>equiv_valid\<close> statements
|
|
|
|
|
with a different pre- and post-equivalence will be addressed later in this tutorial.}
|
|
|
|
|
The resulting EquivValid statement's demand for equal return values is easily provable
|
|
|
|
|
for \<open>gets desk\<close>, using the \<open>gets\<close> rule for \<open>equiv_valid\<close> we found earlier: \<close>
|
|
|
|
|
|
|
|
|
|
lemma gets_desk_equiv_return:
|
|
|
|
|
\<comment> \<open> Pre-equivalence (and post-equivalence):
|
|
|
|
|
The value of \<open>desk\<close> is equal initially (and finally) for both runs. \<close>
|
|
|
|
|
"\<lbrace>|desk_equivalence|, \<top>\<rbrace>
|
|
|
|
|
gets desk
|
|
|
|
|
\<lbrace>|desk_equivalence|\<rbrace>"
|
|
|
|
|
find_theorems intro
|
|
|
|
|
apply(rule gets_ev'')
|
|
|
|
|
unfolding desk_equivalence_def
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> Note that the \<open>equiv_valid_rv\<close> form of EquivValid allows you to customise the
|
|
|
|
|
relationship demanded between return values to be something other than equality: \<close>
|
|
|
|
|
lemma "\<lbrace>|\<top>\<top>|, \<top>\<rbrace> f \<lbrace>|\<top>\<top>|\<rbrace> = equiv_valid_rv \<top>\<top> \<top>\<top> \<top>\<top> (=) \<top> f"
|
|
|
|
|
by (simp add:equiv_valid_def2) \<comment> \<open> Try replacing the \<open>(=)\<close> here. \<close>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
subsection \<open> An attacker with a window into the system state \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> As a rule of thumb, we use an EquivValid statement's pre-equivalence to specify
|
|
|
|
|
the secrecy (or initial attacker knowledge) of values in system state, and use the
|
|
|
|
|
post-equivalence to specify the attacker's powers of observation.
|
|
|
|
|
|
|
|
|
|
Suppose now a scenario where the desk in our room initially contains secrets,
|
|
|
|
|
and we wish to prevent these secrets from affecting what is observable to an attacker
|
|
|
|
|
with binoculars pointed at the window. In this case:
|
|
|
|
|
\begin{enumerate}
|
|
|
|
|
\item We \<^emph>\<open>do not\<close> include \<open>desk_equivalence\<close> in the pre-equivalence, as we
|
|
|
|
|
do not consider it acceptable for the attacker to know the initial contents of \<open>desk\<close>.
|
|
|
|
|
|
|
|
|
|
\item Furthermore, we \<^emph>\<open>do\<close> include \<open>window_equivalence\<close> in the post-equivalence, as we
|
|
|
|
|
do consider that the attacker will be able to observe the final contents of \<open>window\<close>.
|
|
|
|
|
\end{enumerate}
|
|
|
|
|
|
|
|
|
|
Clearly, in this situation, using \<open>modify\<close> to transfer the contents of \<open>desk\<close>
|
|
|
|
|
to \<open>window\<close> would constitute an unacceptable information leak.
|
|
|
|
|
So we should be encouraged to see that the following \<open>equiv_valid\<close>
|
|
|
|
|
statement is not provable: \<close>
|
|
|
|
|
|
|
|
|
|
lemma reveal_desk_window_leak:
|
|
|
|
|
\<comment> \<open> Pre-equivalence and post-equivalence:
|
|
|
|
|
The value of \<open>window\<close> is equal initially and finally for both runs. \<close>
|
|
|
|
|
"\<lbrace>|window_equivalence|, \<top>\<rbrace>
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding reveal_desk_to_window_def
|
|
|
|
|
\<comment> \<open> We find an applicable \<open>modify\<close> rule for \<open>equiv_valid_inv\<close>. \<close>
|
|
|
|
|
find_theorems intro
|
|
|
|
|
apply(rule modify_ev'')
|
|
|
|
|
\<comment> \<open> Applying it, we see that it demands that \<open>window_equivalence\<close> holds
|
|
|
|
|
between the final states of both runs. \<close>
|
|
|
|
|
unfolding window_equivalence_def
|
|
|
|
|
apply clarsimp
|
|
|
|
|
\<comment> \<open> We should not expect to be able to prove this, because we have
|
|
|
|
|
said nothing about the initial value of desk in these runs. \<close>
|
|
|
|
|
oops (* Try: nitpick *)
|
|
|
|
|
|
|
|
|
|
text \<open> As before, however, we should expect this to hold with a pre-equivalence
|
|
|
|
|
that includes \<open>desk_equivalence\<close>. \<close>
|
|
|
|
|
|
|
|
|
|
lemma reveal_desk_equiv_window_equiv:
|
|
|
|
|
"\<lbrace>|desk_equivalence And window_equivalence|, \<top>\<rbrace>
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
\<lbrace>|desk_equivalence And window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding reveal_desk_to_window_def
|
|
|
|
|
apply(rule modify_ev'')
|
|
|
|
|
unfolding bipred_conj_def desk_equivalence_def window_equivalence_def
|
|
|
|
|
by clarsimp
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section \<open> The typical toolkit \<close>
|
|
|
|
|
|
|
|
|
|
subsection \<open> Using and customising the \<open>wp\<close> tool's rule set \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> Recall the lemma we proved for \<open>gets desk\<close>: \<close>
|
|
|
|
|
thm gets_desk_equiv_return
|
|
|
|
|
text \<open> Instead of using any of the \<open>gets\<close> rules for \<open>equiv_valid\<close> directly, we can
|
|
|
|
|
also try using the \<open>wp\<close> tool to see if it has any applicable rules in its rule set: \<close>
|
|
|
|
|
thm wp_ev
|
|
|
|
|
|
|
|
|
|
text \<open>Before applying \<open>wp\<close> to EquivValid statements in this fashion, we may need
|
|
|
|
|
to use the rule \<open>pre_ev\<close> to weaken their precondition.
|
|
|
|
|
This allows us to apply rules that are designed to be applied when the precondition
|
|
|
|
|
is a schematic variable, so as to infer a weakest precondition for the statement to hold.
|
|
|
|
|
It then leaves a goal for later to show that our original precondition implies
|
|
|
|
|
the weaker one that was inferred.\<close>
|
|
|
|
|
thm pre_ev
|
|
|
|
|
\<comment> \<open> Note: \<open>pre_ev\<close> is just the standard \<open>hoare_pre\<close> + \<open>equiv_valid_guard_imp\<close> \<close>
|
|
|
|
|
thm hoare_pre
|
|
|
|
|
thm equiv_valid_guard_imp
|
|
|
|
|
|
|
|
|
|
text \<open> Applying the \<open>wp\<close> tactic then works because the \<open>gets_ev\<close> rule happens to be
|
|
|
|
|
in the \<open>wp\<close> tool's rule set: \<close>
|
|
|
|
|
thm gets_ev
|
|
|
|
|
|
|
|
|
|
lemma gets_desk_equiv_return_using_wp:
|
|
|
|
|
"\<lbrace>|desk_equivalence|, \<top>\<rbrace>
|
|
|
|
|
gets desk
|
|
|
|
|
\<lbrace>|desk_equivalence|\<rbrace>"
|
|
|
|
|
\<comment> \<open> Use \<open>pre_ev\<close> to weaken the precondition of the \<open>equiv_valid\<close> statement
|
|
|
|
|
and make the \<open>wp\<close> method applicable. \<close>
|
|
|
|
|
apply(rule pre_ev)
|
|
|
|
|
apply wp
|
|
|
|
|
unfolding desk_equivalence_def
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> You can freely customise the \<open>wp\<close> rule set as needed, whether to
|
|
|
|
|
add new rules, or to replace rules with ones that are more applicable
|
|
|
|
|
in a given situation.
|
|
|
|
|
|
|
|
|
|
For example, the \<open>modify_ev\<close> rule is not part of the default \<open>wp\<close> rule set: \<close>
|
|
|
|
|
|
|
|
|
|
thm reveal_desk_equiv_window_equiv
|
|
|
|
|
modify_ev
|
|
|
|
|
|
|
|
|
|
lemma reveal_desk_equiv_window_equiv_using_wp:
|
|
|
|
|
"\<lbrace>|desk_equivalence And window_equivalence|, \<top>\<rbrace>
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
\<lbrace>|desk_equivalence And window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding reveal_desk_to_window_def
|
|
|
|
|
apply(rule pre_ev)
|
|
|
|
|
apply(wp add:modify_ev)
|
|
|
|
|
unfolding bipred_conj_def desk_equivalence_def window_equivalence_def
|
|
|
|
|
by clarsimp
|
|
|
|
|
|
|
|
|
|
text \<open> As another example:
|
|
|
|
|
It might be the \<^emph>\<open>precondition\<close> for both runs that tells us that \<open>desk\<close> has
|
|
|
|
|
a fixed initial constant value \<open>c\<close> that is common to both runs.
|
|
|
|
|
(This might be the case if, even if we might normally use \<open>desk\<close> for
|
|
|
|
|
secrets, we happen to have just executed a ``flush'' function that writes \<open>c\<close> to
|
|
|
|
|
\<open>desk\<close> before this point in the program, for all pairs of runs we care to compare.)
|
|
|
|
|
|
|
|
|
|
Here we can modify the wp rule set to invoke \<open>gets_ev''\<close> for \<open>equiv_valid\<close>,
|
|
|
|
|
which is better than the default \<open>gets_ev\<close> rule for situations like this
|
|
|
|
|
where we actually need to use the precondition: \<close>
|
|
|
|
|
thm gets_ev''
|
|
|
|
|
|
|
|
|
|
lemma example_precond_desk_return:
|
|
|
|
|
\<comment> \<open> Precondition: The value of desk is some fixed value \<open>c\<close>.
|
|
|
|
|
\<open>equiv_valid\<close> then assumes that this precondition applies to both runs. \<close>
|
|
|
|
|
"\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
|
|
|
|
|
gets desk
|
|
|
|
|
\<lbrace>|\<top>\<top>|\<rbrace>"
|
|
|
|
|
apply(wp del:gets_ev add:gets_ev'')
|
|
|
|
|
by force
|
|
|
|
|
|
|
|
|
|
text \<open> Relying on such a precondition, a similar argument is possible
|
|
|
|
|
when proving that \<open>reveal_desk_to_window\<close> preserves \<open>window_equivalence\<close>: \<close>
|
|
|
|
|
thm modify_ev''
|
|
|
|
|
|
|
|
|
|
lemma reveal_const_desk_preserves_window_equiv:
|
|
|
|
|
\<comment> \<open> Precondition: Desk initially has a fixed constant \<open>c\<close>.
|
|
|
|
|
\<open>equiv_valid\<close> then assumes that this precondition applies to both runs. \<close>
|
|
|
|
|
"\<lbrace>|window_equivalence|, (\<lambda>s. desk s = c)\<rbrace>
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding reveal_desk_to_window_def
|
|
|
|
|
apply(wp add:modify_ev'')
|
|
|
|
|
unfolding window_equivalence_def
|
|
|
|
|
by clarsimp
|
|
|
|
|
|
|
|
|
|
text \<open> Finally, new EquivValid rules that we expect to be exercised
|
|
|
|
|
often can be added to the \<open>wp\<close> rule set using a declaration: \<close>
|
|
|
|
|
declare modify_ev[wp]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
subsection \<open> Remainder of worked example using \<open>wp\<close> tool \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> Let's use all this to prove that our overarching program,
|
|
|
|
|
\<open>work_sanitise_reveal\<close>, is secure against the attacker at the window
|
|
|
|
|
with the binoculars (i.e. preserves \<open>window_equivalence\<close>). \<close>
|
|
|
|
|
|
|
|
|
|
thm work_sanitise_reveal_def
|
|
|
|
|
|
|
|
|
|
text \<open> First, we expect these two statements to be provable, because
|
|
|
|
|
\<open>work_at_desk\<close> and \<open>sanitise_desk\<close> have nothing to do with the window. \<close>
|
|
|
|
|
|
|
|
|
|
lemma work_at_desk_preserves_window_equiv:
|
|
|
|
|
"\<lbrace>|window_equivalence|, P\<rbrace>
|
|
|
|
|
work_at_desk
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding work_at_desk_def
|
|
|
|
|
apply wp \<comment> \<open> Instead of \<open>apply(wp add:modify_ev)\<close> \<close>
|
|
|
|
|
unfolding window_equivalence_def
|
|
|
|
|
by force
|
|
|
|
|
|
|
|
|
|
lemma sanitise_desk_preserves_window_equiv:
|
|
|
|
|
"\<lbrace>|window_equivalence|, P\<rbrace>
|
|
|
|
|
sanitise_desk
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding sanitise_desk_def
|
|
|
|
|
apply(rule pre_ev)
|
|
|
|
|
apply wp \<comment> \<open> Instead of \<open>apply(wp add:modify_ev)\<close> \<close>
|
|
|
|
|
unfolding window_equivalence_def
|
|
|
|
|
by force
|
|
|
|
|
|
|
|
|
|
text \<open> The consequence of all this is that \<open>work_at_desk\<close> might freely
|
|
|
|
|
shuttle secrets between \<open>inbox\<close> and \<open>outbox\<close> via \<open>desk\<close>, and execute
|
|
|
|
|
a secret \<open>job\<close> on them, but it does not allow any of these secrets
|
|
|
|
|
to affect what is visible at \<open>window\<close>.
|
|
|
|
|
|
|
|
|
|
The mere fact of \<^emph>\<open>excluding\<close> any equivalences on \<open>inbox\<close>, \<open>outbox\<close>, or
|
|
|
|
|
\<open>job\<close> from the pre- and post-equivalence of these statements
|
|
|
|
|
implies both:
|
|
|
|
|
\begin{enumerate}
|
|
|
|
|
\item We \<^emph>\<open>do not\<close> consider it acceptable for the attacker to know the
|
|
|
|
|
initial values of \<open>inbox\<close> and \<open>outbox\<close> in these locations;
|
|
|
|
|
even the \<open>job\<close> to be executed may differ between the runs.
|
|
|
|
|
All of these are therefore secrets to be protected by the property.
|
|
|
|
|
|
|
|
|
|
\item We \<^emph>\<open>do\<close> consider it acceptable for \<open>inbox\<close>, \<open>outbox\<close>, and \<open>job\<close>
|
|
|
|
|
to contain secret values after the program has finished executing.
|
|
|
|
|
\end{enumerate} \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> We will, however, need that \<open>sanitise_desk\<close> establishes the precondition
|
|
|
|
|
demanded by our recently proved lemma: that \<open>desk\<close> contains a constant. \<close>
|
|
|
|
|
thm reveal_const_desk_preserves_window_equiv
|
|
|
|
|
|
|
|
|
|
text \<open> Note that this is a regular (non-EquivValid) Hoare triple: \<close>
|
|
|
|
|
lemma sanitise_desk_sets_zero:
|
|
|
|
|
"\<lbrace>P\<rbrace> sanitise_desk \<lbrace>\<lambda>r s. desk s = 0\<rbrace>"
|
|
|
|
|
unfolding sanitise_desk_def
|
|
|
|
|
apply(rule pre_ev)
|
|
|
|
|
apply wp
|
|
|
|
|
by force
|
|
|
|
|
|
|
|
|
|
text \<open> We can now use all these lemmas to have \<open>wp\<close> discharge that
|
|
|
|
|
our overarching program \<open>work_sanitise_reveal\<close> preserves \<open>window_equivalence\<close>. \<close>
|
|
|
|
|
|
|
|
|
|
lemma work_sanitise_reveal_preserves_window_equiv:
|
|
|
|
|
"\<lbrace>|window_equivalence|, \<top>\<rbrace>
|
|
|
|
|
work_sanitise_reveal
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding work_sanitise_reveal_def
|
|
|
|
|
apply(wp add:reveal_const_desk_preserves_window_equiv[where c=0]
|
|
|
|
|
sanitise_desk_preserves_window_equiv
|
|
|
|
|
sanitise_desk_sets_zero
|
|
|
|
|
work_at_desk_preserves_window_equiv)
|
|
|
|
|
by force
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section \<open> The advanced toolkit \<close>
|
|
|
|
|
|
|
|
|
|
subsection \<open> More general forms of EquivValid statements \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> Lib.EquivValid provides rules for discharging \<open>equiv_valid_inv\<close> statements for
|
|
|
|
|
the basic monad primitives \<open>return\<close> and \<open>bind\<close>, and some of the more basic functions
|
|
|
|
|
like \<open>gets\<close> (already seen); potentially in a number of variants. \<close>
|
|
|
|
|
|
|
|
|
|
thm return_ev
|
|
|
|
|
bind_ev
|
|
|
|
|
gets_ev gets_ev' gets_ev''
|
|
|
|
|
modify_ev modify_ev' modify_ev''
|
|
|
|
|
|
|
|
|
|
text \<open> On rare occasions you may find a need to use some of the more general
|
|
|
|
|
forms of EquivValid. These are all defined in terms of the most general form,
|
|
|
|
|
\<open>equiv_valid_2\<close>, which allows full customisation of
|
|
|
|
|
(1) return value equivalence \<open>R\<close>,
|
|
|
|
|
(2) differing pre-equivalence \<open>A\<close> vs post-equivalence \<open>B\<close>, and even
|
|
|
|
|
(3) differing preconditions \<open>P,P'\<close> and functions \<open>f,f'\<close> for each run.
|
|
|
|
|
(In \cite{Murray_MBGK_12}, \<open>equiv_valid_2\<close> is referred to as ``ev2''.) \<close>
|
|
|
|
|
|
|
|
|
|
\<comment> \<open>Generalised to allow specifying equivalence R on return values.\<close>
|
|
|
|
|
lemma "equiv_valid_rv_inv I A R P f" unfolding equiv_valid_2_def oops
|
|
|
|
|
\<comment> \<open>Generalised further.\<close>
|
|
|
|
|
lemma "equiv_valid_rv I A B R P f" unfolding equiv_valid_2_def oops
|
|
|
|
|
lemma "equiv_valid_2 I A B R P P' f f'" unfolding equiv_valid_2_def oops
|
|
|
|
|
|
|
|
|
|
text \<open> If you ever have a need to unfold an \<open>equiv_valid\<close> statement to its
|
|
|
|
|
\<open>equiv_valid_2\<close> form -- perhaps as part of a more involved manual proof --
|
|
|
|
|
it is often better to unfold \<open>equiv_valid_def2\<close> rather than \<open>equiv_valid_def\<close>.
|
|
|
|
|
|
|
|
|
|
Lib.EquivValid also provides various rules for discharging \<open>equiv_valid_2\<close>
|
|
|
|
|
statements for the basic monad primitives. For example: \<close>
|
|
|
|
|
|
|
|
|
|
thm return_ev2
|
|
|
|
|
equiv_valid_2_bind equiv_valid_2_bind_pre equiv_valid_2_bind_general
|
|
|
|
|
modify_ev2
|
|
|
|
|
|
|
|
|
|
lemma reveal_desk_equiv_window_equiv_using_ev2:
|
|
|
|
|
"\<lbrace>|desk_equivalence And window_equivalence|, \<top>\<rbrace>
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
\<lbrace>|desk_equivalence And window_equivalence|\<rbrace>"
|
|
|
|
|
unfolding reveal_desk_to_window_def
|
|
|
|
|
apply(clarsimp simp:equiv_valid_def2)
|
|
|
|
|
\<comment> \<open> After peeling back to \<open>equiv_valid_2\<close> form, we can use its \<open>modify\<close> rule. \<close>
|
|
|
|
|
find_theorems intro
|
|
|
|
|
apply(rule modify_ev2)
|
|
|
|
|
unfolding desk_equivalence_def window_equivalence_def
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> The basic \<open>equiv_valid\<close> form and its rule set may sometimes
|
|
|
|
|
be too restrictive, due to their demand for return values to be equal.
|
|
|
|
|
|
|
|
|
|
For example, if we ever needed to prove an \<open>equiv_valid\<close> statement about
|
|
|
|
|
\<open>do s \<leftarrow> get; return (f s) od\<close>, we would need to unfold it to \<open>equiv_valid_2\<close> form.
|
|
|
|
|
This is because \<open>equiv_valid\<close> and its bind rule \<open>bind_ev_pre\<close> will both demand
|
|
|
|
|
that the return value of \<open>get\<close> (the entire state) be the same for both runs;
|
|
|
|
|
however, we might only need (or know) the parts of the state inspected
|
|
|
|
|
by the function \<open>f\<close> to be the same. Say \<open>f\<close> was \<open>desk\<close>: \<close>
|
|
|
|
|
|
|
|
|
|
thm bind_ev_pre
|
|
|
|
|
equiv_valid_def2[simplified equiv_valid_2_def]
|
|
|
|
|
|
|
|
|
|
lemma pitfall1_using_bind_ev:
|
|
|
|
|
"\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
|
|
|
|
|
do
|
|
|
|
|
s \<leftarrow> get;
|
|
|
|
|
return (desk s)
|
|
|
|
|
od
|
|
|
|
|
\<lbrace>|\<top>\<top>|\<rbrace>"
|
|
|
|
|
\<comment> \<open> Using the bind rule for \<open>equiv_valid\<close> splits the goal into
|
|
|
|
|
two \<open>equiv_valid\<close> statements, one for each of \<open>get\<close> and \<open>return\<close>.
|
|
|
|
|
It will ask us to prove them in reverse order. \<close>
|
|
|
|
|
apply(rule bind_ev_pre)
|
|
|
|
|
\<comment> \<open> The \<open>wp\<close> tool discharges the \<open>return (desk s)\<close> part trivially: \<close>
|
|
|
|
|
apply wp
|
|
|
|
|
\<comment> \<open> But the return value of \<open>get\<close> is the entire state: \<close>
|
|
|
|
|
apply(clarsimp simp:equiv_valid_def2 equiv_valid_2_def)
|
|
|
|
|
apply(clarsimp simp add:get_def)
|
|
|
|
|
\<comment> \<open> This causes us to get stuck, because we have no idea whether the state
|
|
|
|
|
is equivalent for parts of the room other than the desk. \<close>
|
|
|
|
|
oops
|
|
|
|
|
|
|
|
|
|
text \<open> Therefore we need to use \<open>equiv_valid_2\<close> and its bind rule \<open>equiv_valid_2_bind_pre\<close>;
|
|
|
|
|
these will allow us to specify the equivalence \<open>R\<close> to be asserted between
|
|
|
|
|
the return values of the \<open>get\<close>. \<close>
|
|
|
|
|
|
|
|
|
|
thm equiv_valid_2_bind_pre
|
|
|
|
|
equiv_valid_2_def
|
|
|
|
|
|
|
|
|
|
text \<open> Another anti-pattern to avoid when applying the bind rules directly is leaving
|
|
|
|
|
intermediate preconditions unspecified; the automation is liable to guess \<open>False\<close>,
|
|
|
|
|
which will later be unprovable.
|
|
|
|
|
|
|
|
|
|
Here, the \<open>force\<close> tactic correctly infers that \<open>desk_equivalence\<close> is the equivalence \<open>R\<close>
|
|
|
|
|
that we need between the return values from \<open>get\<close>.
|
|
|
|
|
However, it guesses an incorrect postcondition: \<close>
|
|
|
|
|
|
|
|
|
|
lemma pitfall2_using_bind_ev2:
|
|
|
|
|
"\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
|
|
|
|
|
do
|
|
|
|
|
s \<leftarrow> get;
|
|
|
|
|
return (desk s)
|
|
|
|
|
od
|
|
|
|
|
\<lbrace>|\<top>\<top>|\<rbrace>"
|
|
|
|
|
\<comment> \<open> First we need to peel it back to \<open>equiv_valid_2\<close> form, so we can apply its bind rule. \<close>
|
|
|
|
|
apply(clarsimp simp:equiv_valid_def2)
|
|
|
|
|
apply(rule equiv_valid_2_bind_pre)
|
|
|
|
|
\<comment> \<open> Here \<open>wp\<close> infers correctly that the equivalence between the
|
|
|
|
|
intermediate return values needs to be \<open>\<lambda>rv rv'. desk rv = desk rv'\<close>,
|
|
|
|
|
i.e. that \<open>desk\<close> has the same value in the state returned by \<open>get\<close> in both runs. \<close>
|
|
|
|
|
apply(wp add:return_ev2)
|
|
|
|
|
apply(clarsimp simp:equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)
|
|
|
|
|
\<comment> \<open> The \<open>force\<close> tactic just guesses \<open>False\<close> for the postcondition for both steps. \<close>
|
|
|
|
|
apply(force simp add:get_def)
|
|
|
|
|
\<comment> \<open> As these next two goals are Hoare triples, we use the \<open>wp\<close> tool, as usual for
|
|
|
|
|
Hoare triples in the seL4 proof base. See Lib.WPTutorial for more information. \<close>
|
|
|
|
|
apply wp
|
|
|
|
|
apply wp
|
|
|
|
|
\<comment> \<open> Now we are stuck because \<open>force\<close> guessed \<open>False\<close> as a premise
|
|
|
|
|
to discharge the goal earlier, giving us an unsatisfiable goal here. \<close>
|
|
|
|
|
oops
|
|
|
|
|
|
|
|
|
|
text \<open> We can avoid this by giving \<open>equiv_valid_2\<close>'s bind rule a little more information. \<close>
|
|
|
|
|
|
|
|
|
|
lemma precond_get_return_desk:
|
|
|
|
|
"\<lbrace>|\<top>\<top>|, (\<lambda>s. desk s = c)\<rbrace>
|
|
|
|
|
do
|
|
|
|
|
s \<leftarrow> get;
|
|
|
|
|
return (desk s)
|
|
|
|
|
od
|
|
|
|
|
\<lbrace>|\<top>\<top>|\<rbrace>"
|
|
|
|
|
apply(clarsimp simp:equiv_valid_def2)
|
|
|
|
|
\<comment> \<open> We want to use the fact that \<open>desk\<close> contains \<open>c\<close> initially for both runs.
|
|
|
|
|
So we give it here. \<close>
|
|
|
|
|
apply(rule_tac P="(\<lambda>s. desk s = c)" and P'="(\<lambda>s. desk s = c)" in equiv_valid_2_bind_pre)
|
|
|
|
|
apply(wp add:return_ev2)
|
|
|
|
|
apply(clarsimp simp:equiv_valid_def2 equiv_valid_2_def)
|
|
|
|
|
\<comment> \<open> No need to guess anything. \<close>
|
|
|
|
|
apply(force simp add:get_def)
|
|
|
|
|
\<comment> \<open> Use \<open>wp\<close> tactic to discharge the two Hoare triples; see Lib.WPTutorial for more info. \<close>
|
|
|
|
|
apply wp
|
|
|
|
|
apply wp
|
|
|
|
|
apply force
|
|
|
|
|
apply force
|
|
|
|
|
done
|
|
|
|
|
|
|
|
|
|
subsection \<open> A note on what is currently available and why \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> As noted in \cite{Murray_MBGK_12}, the machinery developed of this kind
|
|
|
|
|
(available in Lib.EquivValid's default \<open>wp\<close> rule set) is mostly geared
|
|
|
|
|
towards \<open>equiv_valid_inv\<close>; this is an abbrevation for the simplified case of
|
|
|
|
|
\<open>equiv_valid\<close> where the post-equivalence is the same as the pre-equivalence: \<close>
|
|
|
|
|
|
|
|
|
|
lemma "equiv_valid_inv I A P f" unfolding equiv_valid_def2 equiv_valid_2_def oops
|
|
|
|
|
|
|
|
|
|
text \<open> The reason for this is that the seL4 infoflow proofs take the approach of defining an
|
|
|
|
|
\emph{unwinding} relation \cite{Goguen_Meseguer_84}: an equivalence relation
|
|
|
|
|
flexible enough to describe what we think ought to continue to look the same between
|
|
|
|
|
all possible pairs of executions as seen by a given attacker model.%
|
|
|
|
|
\footnote{If every pair of executions being compared is like a wound-up rope ladder thrown
|
|
|
|
|
over the side of a ship, then the rungs of those ladders would be the unwinding relation.}
|
|
|
|
|
|
|
|
|
|
However, the EquivValid library merely provides a way to reason about equivalences,
|
|
|
|
|
so it is not prescriptive about taking this approach.
|
|
|
|
|
|
|
|
|
|
Furthermore, the overall unwinding relation for a system may be composed from a number of
|
|
|
|
|
equivalences, which may each hold or not at different times, in a manner that depends on
|
|
|
|
|
where we are in the system.%
|
|
|
|
|
\footnote{This is like saying that the first six rungs of the ladder may be made of wood,
|
|
|
|
|
but the next seven rungs may be made of aluminium, and so on.}
|
|
|
|
|
As it happens, this is the case for seL4's unwinding relation, but the number of ev sub-lemmas
|
|
|
|
|
needing to be proved for differing pre-/post-equivalences is rather limited at current time of
|
|
|
|
|
writing, hence the lack of machinery.%
|
|
|
|
|
\footnote{This may perhaps be the lemma covering the step between the sixth and seventh
|
|
|
|
|
rung of our imaginary wood-and-aluminium--runged ladder.} \<close>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
subsection \<open> Proving EquivValid with differing pre- and post-equivalences \<close>
|
|
|
|
|
|
|
|
|
|
text \<open> So far we have only proved \<open>equiv_valid\<close> statements
|
|
|
|
|
whose pre-equivalence is the same as their post-equivalence.
|
|
|
|
|
|
|
|
|
|
We will now attempt to prove an \<open>equiv_valid\<close> statement where they differ.
|
|
|
|
|
|
|
|
|
|
This allows us to say, for example, that although usually we use the desk
|
|
|
|
|
for secrets:
|
|
|
|
|
(1) at this point in the program we happened to make sure that
|
|
|
|
|
desk contains the same value for any two runs we care to check, and
|
|
|
|
|
(2) we don't care if desk contains the same value for both runs afterwards. \<close>
|
|
|
|
|
|
|
|
|
|
lemma reveal_desk_equiv_to_window_equiv:
|
|
|
|
|
"\<lbrace>|desk_equivalence|, \<top>\<rbrace> \<comment> \<open> Pre-equivalence: The value of \<open>desk\<close> is
|
|
|
|
|
the same initially in both runs. \<close>
|
|
|
|
|
reveal_desk_to_window
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>" \<comment> \<open> Post-equivalence: The value of \<open>window\<close> is required to be
|
|
|
|
|
the same at the end of both runs; no longer so for \<open>desk\<close>. \<close>
|
|
|
|
|
unfolding reveal_desk_to_window_def
|
|
|
|
|
apply(rule modify_ev'')
|
|
|
|
|
unfolding window_equivalence_def desk_equivalence_def
|
|
|
|
|
by simp
|
|
|
|
|
|
|
|
|
|
text \<open> This is handy, because we might subsequently copy secrets into the desk,
|
|
|
|
|
in which case \<open>desk_equivalence\<close> would no longer hold in the post-equivalence.
|
|
|
|
|
|
|
|
|
|
As before, the mere fact of \<^emph>\<open>excluding\<close> any equivalence on \<open>inbox\<close> from the
|
|
|
|
|
pre-equivalence implies we \<^emph>\<open>do not\<close> consider it acceptable for the attacker
|
|
|
|
|
to know \<open>inbox\<close>'s initial value; it is therefore a secret to be protected by this property.
|
|
|
|
|
Conversely, the absence of \<open>desk_equivalence\<close> from the post-equivalence implies
|
|
|
|
|
that we \<^emph>\<open>do\<close> consider it acceptable for the desk to contain secrets after the program
|
|
|
|
|
has finished executing.
|
|
|
|
|
|
|
|
|
|
Consequently, this \<open>equiv_valid\<close> statement is provable: \<close>
|
|
|
|
|
|
|
|
|
|
lemma desk_equiv_no_longer_needed:
|
|
|
|
|
"\<lbrace>|desk_equivalence|, \<top>\<rbrace>
|
|
|
|
|
do reveal_desk_to_window;
|
|
|
|
|
modify (\<lambda>r. r\<lparr>desk := inbox r\<rparr>)
|
|
|
|
|
od
|
|
|
|
|
\<lbrace>|window_equivalence|\<rbrace>"
|
|
|
|
|
\<comment> \<open> Use \<open>pre_ev\<close> to weaken the precondition of the \<open>equiv_valid\<close> statement. \<close>
|
|
|
|
|
apply(rule pre_ev)
|
|
|
|
|
\<comment> \<open> Use \<open>bind_ev_general\<close> to split the goal into \<open>equiv_valid\<close> statements for
|
|
|
|
|
each of the two \<open>modify\<close> commands. It will ask us to prove them in reverse order. \<close>
|
|
|
|
|
apply(rule bind_ev_general)
|
|
|
|
|
\<comment> \<open> Prove \<open>equiv_valid\<close> for \<open>desk := inbox\<close> manually. \<close>
|
|
|
|
|
apply clarsimp
|
|
|
|
|
apply(rule modify_ev'')
|
|
|
|
|
\<comment> \<open> The \<open>force\<close> tactic has enough information here to figure out that
|
|
|
|
|
the intermediate equivalence \<open>B\<close> needs to be \<open>window_equivalence\<close>. \<close>
|
|
|
|
|
apply(force simp:window_equivalence_def desk_equivalence_def)
|
|
|
|
|
\<comment> \<open> This happens to be the post-equivalence for the \<open>equiv_valid\<close> lemma
|
|
|
|
|
we just proved for \<open>window := desk\<close>, so we can reuse that lemma here. \<close>
|
|
|
|
|
using reveal_desk_equiv_to_window_equiv
|
|
|
|
|
unfolding window_equivalence_def
|
|
|
|
|
apply force
|
|
|
|
|
apply wp
|
|
|
|
|
apply force
|
|
|
|
|
done
|
|
|
|
|
|
|
|
|
|
end
|
Robert Sison