Theory Small_Step

(*  Title:       Extension of Stateful Intransitive Noninterference with Inputs, Outputs, and Nondeterminism in Language IMP
    Author:      Pasquale Noce
                 Senior Staff Firmware Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Extension of language IMP with inputs, outputs, and nondeterminism"

theory Small_Step
  imports
    "HOL-IMP.BExp"
    "HOL-IMP.Star"
begin

text ‹
\null

In a previous paper of mine \<^cite>‹"Noce24"›, the notion of termination-sensitive information flow
security with respect to a level-based interference relation, as studied in \<^cite>‹"Volpano96"›,
\<^cite>‹"Volpano97"› and formalized in \<^cite>‹"Nipkow23"›, is generalized to the notion of
termination-sensitive information flow correctness with respect to an interference function mapping
program states to (generally) intransitive interference relations. Moreover, a static type system is
specified and is proven to be capable of enforcing such information flow correctness policies.

The present paper extends both the aforesaid information flow correctness criterion and the related
static type system to the case of an imperative programming language supporting inputs, outputs, and
nondeterminism. Regarding inputs and nondeterminism, \<^cite>‹"Volpano96"›, section 7.1, observes that
``if we try to extend the core language with a primitive random number generator \emph{rand( )} and
allow an assignment such as \emph{z := rand( )} to be well typed when \emph{z} is low, then the
soundness theorem no longer holds'', and from this infers that ``new security models [...] should be
explored as potential notions of type soundness for new type systems that deal with nondeterministic
programs''. The present paper shows that this difficulty can be solved by extending the inductive
definition of the programming language's operational semantics so as to reflect the fact that, even
though the input instruction \emph{z := rand( )} may set \emph{z} to an arbitrary input value, the
same program state is produced whenever the input value is the same. As shown in this paper, this
enables to apply a suitably extended information flow correctness criterion based on stateful
intransitive noninterference, as well as an extended static type system enforcing this criterion, to
such an extended programming language.

The didactic imperative programming language IMP employed in \<^cite>‹"Nipkow23"›, extended with an
input instruction, an output instruction, and a control structure allowing for nondeterministic
choice, will be used for this purpose. Yet, in the same way as in my previous paper \<^cite>‹"Noce24"›,
the introduced concepts are applicable to larger, real-world imperative programming languages, too,
by just affording the additional type system complexity arising from richer language constructs.

For further information about the formal definitions and proofs contained in this paper, refer to
Isabelle documentation, particularly \<^cite>‹"Paulson24"›, \<^cite>‹"Nipkow24-4"›, \<^cite>‹"Krauss24"›,
\<^cite>‹"Nipkow11"›, and \<^cite>‹"Ballarin24"›.

As mentioned above, the first task to be tackled, which is the subject of this section, consists of
extending the original syntax, big-step operational semantics, and small-step operational semantics
of language IMP, as formalized in \<^cite>‹"Nipkow24-1"›, \<^cite>‹"Nipkow24-2"›, and \<^cite>‹"Nipkow24-3"›,
respectively.
›


subsection "Extended syntax"

text ‹
The starting point is extending the original syntax of language IMP with the following additional
constructs.

  ▪ An input instruction @{text "IN x"}, which sets variable \emph{x} to an input value.

  ▪ An output instruction @{text "OUT x"}, which outputs the current value of variable \emph{x}.

  ▪ A control structure @{text "c⇩1 OR c⇩2"}, which allows for a nondeterministic choice between
commands @{text "c⇩1"} and @{text "c⇩2"}.

\null
›

declare [[syntax_ambiguity_warning = false]]

datatype com =
  SKIP |
  Assign vname aexp  ("_ ::= _" [1000, 61] 70) |
  Input vname  ("(IN _)" [61] 70) |
  Output vname  ("(OUT _)" [61] 70) |
  Seq com com  ("_;;/ _" [61, 61] 70) |
  Or com com  ("(_ OR _)" [61, 61] 70) |
  If bexp com com  ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 70) |
  While bexp com  ("(WHILE _/ DO _)" [0, 61] 70)


subsection "Extended big-step semantics"

text ‹
The original big-step semantics of language IMP associates a pair formed by a command and an initial
\emph{program execution stage}, consisting of a program state, with a corresponding final program
execution stage, consisting of a program state as well. The extended big-step semantics defined here
below extends such program execution stage notion by considering, in addition to a program state,
the following additional parameters.

  ▪ A \emph{stream of input values}, consisting of a function @{text f} mapping each pair formed by
a variable and a natural number with an integer value, where @{text "f x n"} is the input value
assigned to variable @{text x} by an input instruction @{term "IN x"} after @{text n} previous such
assignments to @{text x}.

  ▪ A \emph{trace of inputs}, consisting of a list @{text vs} of pairs formed by a variable and an
integer value, to which a further element @{text "(x, i)"} is appended as a result of the execution
of an input instruction @{term "IN x"}, where @{text i} is the input value assigned to variable
@{text x}.

  ▪ A \emph{trace of outputs}, consisting of a list @{text ws} of pairs formed by a variable and an
integer value, to which a further element @{text "(x, i)"} is appended as a result of the execution
of an output instruction @{term "OUT x"}, where @{text i} is the current value of variable @{text x}
being output.

Unlike the other components of a program execution stage, the stream of input values is an
\emph{invariant} of the big-step semantics, and then also of the small-step semantics defined
subsequently, in that any two program execution stages associated with each other by either
semantics share the same stream of input values.

\null
›

type_synonym stream = "vname ⇒ nat ⇒ val"
type_synonym inputs = "(vname × val) list"
type_synonym outputs = "(vname × val) list"
type_synonym stage = "state × stream × inputs × outputs"


inductive big_step :: "com × stage ⇒ stage ⇒ bool"
  (infix "⇒" 55) where
Skip:
 "(SKIP, p) ⇒ p" |
Assign:
 "(x ::= a, s, p) ⇒ (s(x := aval a s), p)" |
Input:
 "n = length [p←vs. fst p = x] ⟹ (IN x, s, f, vs, ws) ⇒
    (s(x := f x n), f, vs @ [(x, f x n)], ws)" |
Output:
 "(OUT x, s, f, vs, ws) ⇒ (s, f, vs, ws @ [(x, s x)])" |
Seq:
 "⟦(c⇩1, p⇩1) ⇒ p⇩2; (c⇩2, p⇩2) ⇒ p⇩3⟧ ⟹ (c⇩1;; c⇩2, p⇩1) ⇒ p⇩3" |
Or1:
 "(c⇩1, p) ⇒ p' ⟹ (c⇩1 OR c⇩2, p) ⇒ p'" |
Or2:
 "(c⇩2, p) ⇒ p' ⟹ (c⇩1 OR c⇩2, p) ⇒ p'" |
IfTrue:
 "⟦bval b s; (c⇩1, s, p) ⇒ p'⟧ ⟹
    (IF b THEN c⇩1 ELSE c⇩2, s, p) ⇒ p'" |
IfFalse:
 "⟦¬ bval b s; (c⇩2, s, p) ⇒ p'⟧ ⟹
    (IF b THEN c⇩1 ELSE c⇩2, s, p) ⇒ p'" |
WhileFalse:
 "¬ bval b s ⟹ (WHILE b DO c, s, p) ⇒ (s, p)" |
WhileTrue:
 "⟦bval b s⇩1; (c, s⇩1, p⇩1) ⇒ (s⇩2, p⇩2);
    (WHILE b DO c, s⇩2, p⇩2) ⇒ (s⇩3, p⇩3)⟧ ⟹
  (WHILE b DO c, s⇩1, p⇩1) ⇒ (s⇩3, p⇩3)"


declare big_step.intros [intro]

inductive_cases SkipE [elim!]: "(SKIP, p) ⇒ p'"

inductive_cases AssignE [elim!]: "(x ::= a, p) ⇒ p'"

inductive_cases InputE [elim!]: "(IN x, p) ⇒ p'"

inductive_cases OutputE [elim!]: "(OUT x, p) ⇒ p'"

inductive_cases SeqE [elim!]: "(c⇩1;; c⇩2, p) ⇒ p'"

inductive_cases OrE [elim!]: "(c⇩1 OR c⇩2, p) ⇒ p'"

inductive_cases IfE [elim!]: "(IF b THEN c⇩1 ELSE c⇩2, p) ⇒ p'"

inductive_cases WhileE [elim]: "(WHILE b DO c, p) ⇒ p'"


subsection "Extended small-step semantics"

text ‹
The original small-step semantics of language IMP associates a pair formed by a command and a
program execution stage, which consists of a program state, with another such pair, formed by a
command to be executed next and a resulting program execution stage, which consists of a program
state as well. The extended small-step semantics defined here below rather uses the same extended
program execution stage notion as the extended big-step semantics specified above, and is defined
accordingly.

\null
›

inductive small_step :: "com × stage ⇒ com × stage ⇒ bool"
  (infix "→" 55) where
Assign:
 "(x ::= a, s, p) → (SKIP, s(x := aval a s), p)" |
Input:
 "n = length [p←vs. fst p = x] ⟹ (IN x, s, f, vs, ws) →
    (SKIP, s(x := f x n), f, vs @ [(x, f x n)], ws)" |
Output:
 "(OUT x, s, f, vs, ws) → (SKIP, s, f, vs, ws @ [(x, s x)])" |
Seq1:
 "(SKIP;; c⇩2, p) → (c⇩2, p)" |
Seq2:
 "(c⇩1, p) → (c⇩1', p') ⟹ (c⇩1;; c⇩2, p) → (c⇩1';; c⇩2, p')" |
Or1:
 "(c⇩1 OR c⇩2, p) → (c⇩1, p)" |
Or2:
 "(c⇩1 OR c⇩2, p) → (c⇩2, p)" |
IfTrue:
 "bval b s ⟹ (IF b THEN c⇩1 ELSE c⇩2, s, p) → (c⇩1, s, p)" |
IfFalse:
 "¬ bval b s ⟹ (IF b THEN c⇩1 ELSE c⇩2, s, p) → (c⇩2, s, p)" |
WhileFalse:
 "¬ bval b s ⟹ (WHILE b DO c, s, p) → (SKIP, s, p)" |
WhileTrue:
 "bval b s ⟹ (WHILE b DO c, s, p) → (c;; WHILE b DO c, s, p)"


declare small_step.intros [simp, intro]

inductive_cases skipE [elim!]: "(SKIP, p) → cf"

inductive_cases assignE [elim!]: "(x ::= a, p) → cf"

inductive_cases inputE [elim!]: "(IN x, p) → cf"

inductive_cases outputE [elim!]: "(OUT x, p) → cf"

inductive_cases seqE [elim!]: "(c⇩1;; c⇩2, p) → cf"

inductive_cases orE [elim!]: "(c⇩1 OR c⇩2, p) → cf"

inductive_cases ifE [elim!]: "(IF b THEN c⇩1 ELSE c⇩2, p) → cf"

inductive_cases whileE [elim]: "(WHILE b DO c, p) → cf"


abbreviation small_steps :: "com × stage ⇒ com × stage ⇒ bool"
  (infix "→*" 55) where
"cf →* cf' ≡ star small_step cf cf'"

function small_stepsl ::
 "com × stage ⇒ (com × stage) list ⇒ com × stage ⇒ bool"
  ("(_ →*'{_'} _)" [51, 51] 55)
where
"cf →*{[]} cf' = (cf = cf')" |
"cf →*{cfs @ [cf']} cf'' = (cf →*{cfs} cf' ∧ cf' → cf'')"

by (atomize_elim, auto intro: rev_cases)
termination by lexicographic_order


subsection "Equivalence of big-step and small-step semantics"

lemma star_seq2:
 "(c⇩1, p) →* (c⇩1', p') ⟹ (c⇩1;; c⇩2, p) →* (c⇩1';; c⇩2, p')"
proof (induction rule: star_induct)
  case refl
  thus ?case
    by simp
next
  case step
  thus ?case
    by (blast intro: star.step)
qed

lemma seq_comp:
 "⟦(c⇩1, p⇩1) →* (SKIP, p⇩2); (c⇩2, p⇩2) →* (SKIP, p⇩3)⟧ ⟹
    (c⇩1;; c⇩2, p⇩1) →* (SKIP, p⇩3)"
by (blast intro: star.step star_seq2 star_trans)

lemma big_to_small:
 "cf ⇒ p ⟹ cf →* (SKIP, p)"
proof (induction rule: big_step.induct)
  fix c⇩1 c⇩2 p⇩1 p⇩2 p⇩3
  assume "(c⇩1, p⇩1) →* (SKIP, p⇩2)" and "(c⇩2, p⇩2) →* (SKIP, p⇩3)"
  thus "(c⇩1;; c⇩2, p⇩1) →* (SKIP, p⇩3)"
    by (rule seq_comp)
next
  fix c⇩1 c⇩2 p p'
  assume "(c⇩1, p) →* (SKIP, p')"
  thus "(c⇩1 OR c⇩2, p) →* (SKIP, p')"
    by (blast intro: star.step)
next
  fix c⇩1 c⇩2 p p'
  assume "(c⇩2, p) →* (SKIP, p')"
  thus "(c⇩1 OR c⇩2, p) →* (SKIP, p')"
    by (blast intro: star.step)
next
  fix b c⇩1 c⇩2 s p p'
  assume "bval b s"
  hence "(IF b THEN c⇩1 ELSE c⇩2, s, p) → (c⇩1, s, p)"
    by simp
  moreover assume "(c⇩1, s, p) →* (SKIP, p')"
  ultimately show
   "(IF b THEN c⇩1 ELSE c⇩2, s, p) →* (SKIP, p')"
    by (simp add: star.step)
next
  fix b c⇩1 c⇩2 s p p'
  assume "¬ bval b s"
  hence "(IF b THEN c⇩1 ELSE c⇩2, s, p) → (c⇩2, s, p)"
    by simp
  moreover assume "(c⇩2, s, p) →* (SKIP, p')"
  ultimately show
   "(IF b THEN c⇩1 ELSE c⇩2, s, p) →* (SKIP, p')"
    by (simp add: star.step)
next
  fix b c s⇩1 s⇩2 s⇩3 p⇩1 p⇩2 p⇩3
  assume "bval b s⇩1"
  hence "(WHILE b DO c, s⇩1, p⇩1) →* (c;; WHILE b DO c, s⇩1, p⇩1)"
    by simp
  moreover assume
   "(c, s⇩1, p⇩1) →* (SKIP, s⇩2, p⇩2)" and
   "(WHILE b DO c, s⇩2, p⇩2) →* (SKIP, s⇩3, p⇩3)"
  hence "(c;; WHILE b DO c, s⇩1, p⇩1) →* (SKIP, s⇩3, p⇩3)"
    by (rule seq_comp)
  ultimately show "(WHILE b DO c, s⇩1, p⇩1) →* (SKIP, s⇩3, p⇩3)"
    by (blast intro: star_trans)
qed fastforce+

lemma small1_big_continue:
 "⟦cf → cf'; cf' ⇒ p⟧ ⟹ cf ⇒ p"
by (induction arbitrary: p rule: small_step.induct, force+)

lemma small_to_big:
 "cf →* (SKIP, p) ⟹ cf ⇒ p"
by (induction cf "(SKIP, p)" rule: star.induct,
 auto intro: small1_big_continue)

lemma big_iff_small:
 "cf ⇒ p = cf →* (SKIP, p)"
by (blast intro: big_to_small small_to_big)

end