dan
/
rushby-noninterference
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cleanup

This commit is contained in:
Dan Frumin 2019-06-12 18:29:21 +02:00
parent 8601f7c673
commit 4dd4e4f383
9 changed files with 144 additions and 128 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

133
ArrayMachine.v
View File

@ -1,7 +1,8 @@
Require Import Rushby. (** Instantiation of the intransitive interference with an "array machine" *)
From stdpp Require Import list relations collections fin_collections. Require Import NI.Rushby.
From stdpp Require Import list relations gmap sets fin_sets.
Module ArrayMachine <: Mealy. Module ArrayMachine.
Definition state := nat -> nat. Definition state := nat -> nat.
Inductive command := Inductive command :=
@ -23,39 +24,51 @@ Definition preform (s : state) (a : action) : state * out :=
Definition step s a := fst (preform s a). Definition step s a := fst (preform s a).
Definition output s a := snd (preform s a). Definition output s a := snd (preform s a).
Definition initial (x : nat) := 0. Definition initial (x : nat) := 0.
End ArrayMachine.
End ArrayMachine.
Import ArrayMachine. Import ArrayMachine.
Module M := Rushby.Rushby ArrayMachine. Instance ArrayMealyMachine : Mealy state action out :=
Import M. { initial := initial;
step := step;
output := output }.
Eval compute in (do_actions [Write 1 1] 2). Eval compute in (do_actions [Write 1 1] 2).
(** ===> 0 *)
Definition domain := action. Definition domain := action.
Definition nameA := nat. Definition nameA := nat.
Definition valA := nat. Definition valA := nat.
Definition observeA (u : domain) : FinSet nameA := Definition observeA (u : domain) : gset nameA :=
match u with match u with
| Read i => {[ i ]} | Read i => {[ i ]}
| Write _ _ => ∅ | Write _ _ => ∅
end. end.
Definition alterA (u : domain) : FinSet valA := Definition alterA (u : domain) : gset valA :=
match u with match u with
| Read _ => ∅ | Read _ => ∅
| Write i _ => {[ i ]} | Write i _ => {[ i ]}
end. end.
Instance domain_dec : forall (u v : domain), Decision (u = v). Instance domain_dec : EqDecision domain.
Proof. intros. Proof. intros u v.
unfold Decision. unfold Decision.
repeat (decide equality). repeat (decide equality).
Defined. Defined.
Instance arraymachine_ss : StructuredState domain := Instance domain_countable : Countable domain.
refine (inj_countable' (λ x, match x with
| Write i1 i2 => (inl (i1, i2))
| Read i => (inr i)
end) (λ x, match x with
| inl (i1, i2) => Write i1 i2
| inr i => Read i
end) _); by intros [].
Defined.
Instance arraymachine_ss : StructuredState domain :=
{ name := nameA; value := valA; contents s n := s n { name := nameA; value := valA; contents s n := s n
; observe := observeA; alter := alterA }. ; observe := observeA; alter := alterA }.
Definition interference (u v : domain) := Definition interference (u v : domain) :=
(exists (n : nameA), n ∈ alterA u ∧ n ∈ observeA v). (exists (n : nameA), n ∈ alterA u ∧ n ∈ observeA v).
@ -64,59 +77,64 @@ Inductive interferenceR : relation domain :=
| interference_refl : forall (u : domain), interferenceR u u | interference_refl : forall (u : domain), interferenceR u u
| interference_step : forall (u v: domain), interference u v -> interferenceR u v. | interference_step : forall (u v: domain), interference u v -> interferenceR u v.
Instance policy_ss : Policy domain := Instance: Set_ nameA (gset nameA).
apply _.
Qed.
Instance policy_ss : Policy domain :=
{ policy := interferenceR { policy := interferenceR
; dom := fun (a : action) => (a : domain) }. ; dom := fun (a : action) => (a : domain) }.
Proof. Proof.
intros. unfold Decision. - intros v w.
destruct v as [i j | i]; destruct w as [m n | m]. destruct v as [i j | i]; destruct w as [m n | m].
- destruct (decide (i = m)). destruct (decide (j = n)); subst; auto. + destruct (decide (i = m)). destruct (decide (j = n)); subst; auto.
left. constructor. left. constructor.
right. intro I. inversion I; subst. apply n0. auto. right. intro I. inversion I; subst. apply n0. auto.
inversion H. unfold observeA in *. destruct H0 as [HH HHH]. inversion H. unfold observeA in *. destruct H0 as [HH HHH].
apply (not_elem_of_empty x); assumption. apply (not_elem_of_empty x HHH).
right. intro. inversion H; subst. apply n0. auto. right. intro. inversion H; subst. apply n0. auto.
inversion H0. unfold alterA, observeA in *. destruct H1. inversion H0. unfold alterA, observeA in *. destruct H1 as [HH HHH].
apply (not_elem_of_empty x); assumption. apply (not_elem_of_empty x HHH).
- destruct (decide (i = m)); subst. left. right. unfold interference. + destruct (decide (i = m)); subst. left. right. unfold interference.
simpl. exists m. split; apply elem_of_singleton; auto. simpl. exists m. split; apply elem_of_singleton; auto.
right. intro. inversion H; subst. inversion H0. simpl in H1. right. intro. inversion H; subst. inversion H0. simpl in H1.
destruct H1. apply elem_of_singleton in H1; apply elem_of_singleton in H2. subst. apply n;auto. destruct H1. apply elem_of_singleton in H1; apply elem_of_singleton in H2. subst. apply n;auto.
- right. intro. inversion H;subst. inversion H0; subst. + right. intro. inversion H;subst. inversion H0; subst.
simpl in H1; inversion H1. apply (not_elem_of_empty x); assumption. simpl in H1; inversion H1. eapply (not_elem_of_empty x); eassumption.
- destruct (decide (i = m)); subst. + destruct (decide (i = m)); subst.
left. constructor. left. constructor.
right. intro. inversion H; subst. auto. right. intro. inversion H; subst. auto.
inversion H0; subst. simpl in H1; inversion H1. eapply not_elem_of_empty. eassumption. inversion H0; subst. simpl in H1; inversion H1.
eapply (not_elem_of_empty x); eassumption.
- intro u. constructor. - intro u. constructor.
Defined. Defined.
Check RefMonAssumptions.
Instance rma_yay : RefMonAssumptions. Instance rma_yay : RefMonAssumptions.
Proof. split; simpl; unfold RMA_partition; intros; Proof.
unfold contents in *; simpl in H8. split; simpl; unfold RMA_partition.
unfold output. - intros a s t Hst;
unfold preform. destruct a as [i j | i]; simpl in *. reflexivity. unfold contents in *; simpl in *.
apply H8. apply elem_of_singleton. reflexivity. unfold output.
unfold preform. destruct a as [i j | i]; simpl in *. reflexivity.
unfold step, preform. destruct a as [i j | i]. simpl in *. apply Hst. eapply elem_of_singleton. reflexivity.
destruct (decide (i = n)); subst; unfold extendS; simpl. - intros a s t n Hst Hn.
replace (beq_nat n n) with true; auto. apply beq_nat_refl. unfold step, preform. destruct a as [i j | i]. simpl in *.
destruct H9. destruct (decide (i = n)); subst; unfold extendS; simpl.
unfold step in H9; simpl in H9. unfold extendS in H9; simpl in H9. replace (beq_nat n n) with true; auto. apply beq_nat_refl.
replace (beq_nat n i) with false in *; auto. destruct Hn as [Hn|Hn].
congruence. SearchAbout beq_nat false. symmetry. apply beq_nat_false_iff. omega. unfold step in Hn; simpl in Hn. unfold extendS in Hn; simpl in Hn.
unfold step in H9; simpl in H9. unfold extendS in H9; simpl in H9. replace (beq_nat n i) with false in *; auto.
replace (beq_nat n i) with false in *; auto. congruence. symmetry. apply beq_nat_false_iff. omega.
congruence. symmetry. apply beq_nat_false_iff. omega. unfold step in Hn; simpl in Hn. unfold extendS in Hn; simpl in Hn.
replace (beq_nat n i) with false in *; auto.
congruence. symmetry. apply beq_nat_false_iff. omega.
simpl. destruct H9; unfold step, preform in H9; simpl in H9; simpl. destruct Hn as [Hn|Hn]; unfold step, preform in Hn; simpl in Hn;
congruence. congruence.
- intros a s n Hst.
unfold step, preform in H8; simpl in H8. destruct a; simpl in *. unfold step, preform in Hst; simpl in Hst. destruct a; simpl in *.
unfold extendS in H8. destruct (decide (n = n0)); subst. unfold extendS in Hst. destruct (decide (n = n0)); subst.
apply elem_of_singleton; auto. replace (beq_nat n n0) with false in *; try (congruence). symmetry. apply beq_nat_false_iff. assumption. apply elem_of_singleton; auto. replace (beq_nat n n0) with false in *; try (congruence). symmetry. apply beq_nat_false_iff. assumption.
congruence. congruence.
Defined. Defined.
@ -125,4 +143,3 @@ Proof.
apply rma_secure_intransitive. apply rma_secure_intransitive.
intros u v n A1 A2. simpl. right. firstorder. intros u v n A1 A2. simpl. right. firstorder.
Qed. Qed.

136
Rushby.v
View File

@ -1,24 +1,11 @@
(** Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby (** Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby
www.csl.sri.com/papers/csl-92-2/ www.csl.sri.com/papers/csl-92-2/
*) *)
(** printing -> #→# *) (** printing -> #→# *)
(** printing (policy a b) #a ⇝ b# *) (** printing (policy a b) #a ⇝ b# *)
From stdpp Require Import list relations collections fin_collections. From stdpp Require Import list relations gmap sets fin_sets.
Parameter FinSet : Type -> Type.
(** begin hide **)
Context `{forall A, ElemOf A (FinSet A)}.
Context `{forall A, Empty (FinSet A)}.
Context `{forall A, Singleton A (FinSet A)}.
Context `{forall A, Union (FinSet A)}.
Context `{forall A, Intersection (FinSet A)}.
Context `{forall A, Difference (FinSet A)}.
Context `{forall A, Elements A (FinSet A)}.
Context `{forall A, Collection A (FinSet A)}.
(* TODO: i wrote this line down so that there is a Collection -> SimpleCollection -> JoinSemiLattice instance for FinSet; how come this is not automatically picked up by the next assumption? *)
Context `{forall A (H : EqDecision A), FinCollection A (FinSet A)}.
(** end hide **)
(** * Mealy machines *) (** * Mealy machines *)
@ -46,10 +33,10 @@ Fixpoint run `{Mealy state action out} (s : state) (ls : list action) : state :=
Definition do_actions `{Mealy state action out} : list action -> state := run initial. Definition do_actions `{Mealy state action out} : list action -> state := run initial.
(** The [test] function runs the required list of actions and examines the output of the resulting state on a specified action. *) (** The [test] function runs the required list of actions and examines the output of the resulting state on a specified action. *)
Definition test `{Mealy state action out} (ls : list action) : action -> out := output (do_actions ls). Definition test `{Mealy state action out} (ls : list action) : action -> out := output (do_actions ls).
Section Rushby. Section Rushby.
(** We assume for the rest of the formalisation that we have a Mealy (** We assume for the rest of the formalisation that we have a Mealy
machine [M]. Thus, we parameterize our main development module by a machine [M]. *) machine [M]. Thus, we parameterize our main development module by a machine [M]. *)
@ -73,6 +60,7 @@ Class Policy (domain : Type) := {
instances. *) instances. *)
domain_dec :> EqDecision domain; domain_dec :> EqDecision domain;
domain_countable :> Countable domain;
policy :> relation domain; policy :> relation domain;
policy_dec :> RelDecision policy; policy_dec :> RelDecision policy;
policy_refl :> Reflexive policy policy_refl :> Reflexive policy
@ -83,7 +71,7 @@ Delimit Scope policy_scope with P.
Open Scope policy_scope. Open Scope policy_scope.
Infix "⇝" := policy (at level 70) : policy_scope. Infix "⇝" := policy (at level 70) : policy_scope.
(** Quoting Rushby: (** Quoting Rushby:
<< <<
We wish to define security in terms of information flow, so the We wish to define security in terms of information flow, so the
@ -136,10 +124,10 @@ Section view_partitions.
(** Formally, a view partition is an assignment of an equivalence (** Formally, a view partition is an assignment of an equivalence
relation [≈{u}] for every domain [u] *) relation [≈{u}] for every domain [u] *)
Class ViewPartition (domain : Type) := { Class ViewPartition (domain : Type) := {
view_partition :> domain -> relation state; view_partition :> domain -> relation state;
view_partition_is_equiv :> forall v, Equivalence (view_partition v) view_partition_is_equiv :> forall v, Equivalence (view_partition v);
}. }.
Notation "S ≈{ U } T" := (view_partition U S T) Notation "S ≈{ U } T" := (view_partition U S T)
@ -149,7 +137,7 @@ Open Scope policy_scope.
states [s, t] that are indistinguishable w.r.t. the domain [dom a], states [s, t] that are indistinguishable w.r.t. the domain [dom a],
the output of the system [output s a] is the same as [output t a] *) the output of the system [output s a] is the same as [output t a] *)
Class OutputConsistent `{P : Policy domain} `(ViewPartition domain) := Class OutputConsistent `{P : Policy domain} `(ViewPartition domain) :=
output_consistent : (forall a s t, s ≈{dom a} t -> output s a = output t a). output_consistent : (forall a s t, s ≈{dom a} t -> output s a = output t a).
(** Our first lemma states that if we have a view partitioned system (** Our first lemma states that if we have a view partitioned system
@ -195,15 +183,15 @@ Theorem unwinding `{P: Policy domain} `{VP: ViewPartition domain} `{@OutputConsi
Proof. Proof.
intros LRP SC. apply output_consist_security. intros LRP SC. apply output_consist_security.
assert (forall ls u s t, view_partition u s t -> view_partition u (run s ls) (run t (purge ls u))) as General. (* TODO: a simple generalize would not suffice, because we actually need the s ≈ t assumption *) assert (forall ls u s t, view_partition u s t -> view_partition u (run s ls) (run t (purge ls u))) as General. (* TODO: a simple generalize would not suffice, because we actually need the s ≈ t assumption *)
induction ls; simpl; auto. induction ls; simpl; auto.
intros u s t HI. intros u s t HI.
destruct (decide (policy (dom a) u)). destruct (decide (policy (dom a) u)).
(* DOESNT WORK (Lexer) : destruct (decide ((dom a) ⇝ u)). *) (* DOESNT WORK (Lexer) : destruct (decide ((dom a) ⇝ u)). *)
(** Case [(dom a) ~> u] *) (** Case [(dom a) ~> u] *)
apply IHls. apply SC; assumption. apply IHls. apply SC; assumption.
(** Case [(dom a) ~/> u] *) (** Case [(dom a) ~/> u] *)
apply IHls. apply IHls.
transitivity s. symmetry. unfold locally_respects_policy in LRP. apply LRP; assumption. assumption. transitivity s. symmetry. unfold locally_respects_policy in LRP. apply LRP; assumption. assumption.
unfold do_actions. intros ls u. apply General. reflexivity. unfold do_actions. intros ls u. apply General. reflexivity.
Qed. Qed.
@ -213,7 +201,7 @@ End view_partitions.
Section ACI. Section ACI.
(** In this section we consider a formalisation of the access control mechansisms. (** In this section we consider a formalisation of the access control mechansisms.
We say that the machine has _structured state_ if we have a collection We say that the machine has _structured state_ if we have a collection
of [name]s and [value]s (the latter being decidable), and some sort of of [name]s and [value]s (the latter being decidable), and some sort of
@ -227,8 +215,10 @@ Class StructuredState (domain : Type) := {
value : Type; value : Type;
contents : state -> name -> value; contents : state -> name -> value;
value_dec :> EqDecision value; value_dec :> EqDecision value;
observe : domain -> FinSet name; name_dec :> EqDecision name;
alter : domain -> FinSet name name_countable :> Countable name;
observe : domain -> gset name;
alter : domain -> gset name
}. }.
(** This induces the view partition relation as follows: two state [s] (** This induces the view partition relation as follows: two state [s]
@ -240,13 +230,15 @@ Definition RMA_partition `{@StructuredState domain} (u : domain) s t := (forall
Transparent RMA_partition. Transparent RMA_partition.
Instance RMA `{@StructuredState domain} : ViewPartition domain := { view_partition := RMA_partition }. Instance RMA `{!StructuredState domain}
`{!EqDecision domain, !Countable domain}
: ViewPartition domain := { view_partition := RMA_partition }.
(* begin hide *) (* begin hide *)
intro u. split; unfold RMA_partition. intro u. split; try apply _; unfold RMA_partition.
(* Reflexivity *) unfold Reflexive. auto. (* Reflexivity *) - unfold Reflexive. auto.
(* Symmetry *) unfold Symmetric. intros x y Sy. (* Symmetry *) - unfold Symmetric. intros x y Sy.
symmetry. apply Sy. assumption. symmetry. apply Sy. assumption.
(* Transitivity *) unfold Transitive. intros x y z T1 T2 n. - (* Transitivity *) unfold Transitive. intros x y z T1 T2 n.
transitivity (contents y n); [apply T1 | apply T2]; assumption. transitivity (contents y n); [apply T1 | apply T2]; assumption.
Defined. (* We have to use 'Defined' here instead of 'Qed' so that we can unfold 'RMA' later on *) Defined. (* We have to use 'Defined' here instead of 'Qed' so that we can unfold 'RMA' later on *)
(* end hide *) (* end hide *)
@ -255,18 +247,20 @@ Hint Resolve RMA.
(** ** Reference monitor assumptions *) (** ** Reference monitor assumptions *)
(* TODO: explain those assumptions *) (* TODO: explain those assumptions *)
Class RefMonAssumptions `{Policy domain} `{StructuredState domain} := Class RefMonAssumptions `{!Policy domain, !StructuredState domain} :=
{ rma1 : forall (a : action) s t, { rma1 :
view_partition (dom a) s t -> output s a = output t a forall (a : action) s t,
; rma2 : forall a s t n, view_partition (dom a) s t -> output s a = output t a;
view_partition (dom a) s t -> rma2 :
((contents (step s a) n) ≠ (contents s n) forall a s t n,
∨ (contents (step t a) n) ≠ (contents t n)) view_partition (dom a) s t ->
-> contents (step s a) n = contents (step t a) n ((contents (step s a) n) ≠ (contents s n)
; rma3 : forall a s n, ∨ (contents (step t a) n) ≠ (contents t n))
contents (step s a) n ≠ contents s n -> n ∈ alter (dom a) -> contents (step s a) n = contents (step t a) n;
}. rma3 :
forall a s n, contents (step s a) n ≠ contents s n -> n ∈ alter (dom a)
}.
(** If the reference monitor assumptions are satisfied, then the system is output-consistent *) (** If the reference monitor assumptions are satisfied, then the system is output-consistent *)
Global Instance OC `{RefMonAssumptions}: OutputConsistent RMA. Global Instance OC `{RefMonAssumptions}: OutputConsistent RMA.
exact rma1. Defined. exact rma1. Defined.
@ -278,15 +272,15 @@ exact rma1. Defined.
*) *)
(* Theorem 2 *) (* Theorem 2 *)
Theorem RMA_secutity `{RefMonAssumptions} : Theorem RMA_secutity `{RefMonAssumptions} :
(forall u v, (policy u v) → observe u ⊆ observe v) (forall u v, (policy u v) → observe u ⊆ observe v)
-> (forall u v n, (n ∈ alter u) → (n ∈ observe v) → (policy u v)) -> (forall u v n, (n ∈ alter u) → (n ∈ observe v) → (policy u v))
-> security. -> security.
Proof. Proof.
intros Cond1 Cond2. apply unwinding. intros Cond1 Cond2. apply unwinding.
(** We apply the unwinding theorem, so we have to verify that (** We apply the unwinding theorem, so we have to verify that
we locally respect policy and that we have step-consistency *) we locally respect policy and that we have step-consistency *)
unfold locally_respects_policy. unfold locally_respects_policy.
intros a u s. intros a u s.
(** In order to prove that the system locally respects the policy (** In order to prove that the system locally respects the policy
@ -297,7 +291,7 @@ Proof.
intros opH. destruct opH as [n [??]]. intros opH. destruct opH as [n [??]].
eapply Cond2. eapply rma3. eauto. assumption. eapply Cond2. eapply rma3. eauto. assumption.
intros NPolicy. intros NPolicy.
unfold view_partition, RMA, RMA_partition. unfold view_partition, RMA, RMA_partition.
(* TODO: why can't decide automatically pick the instance value_dec? *) (* TODO: why can't decide automatically pick the instance value_dec? *)
intros. destruct (decide (contents s n = contents (step s a) n)) as [e|Ne]. assumption. exfalso. apply NPolicy. apply CP. intros. destruct (decide (contents s n = contents (step s a) n)) as [e|Ne]. assumption. exfalso. apply NPolicy. apply CP.
exists n; split; assumption. exists n; split; assumption.
@ -317,7 +311,7 @@ Proof.
(* We use the Second RM assmption to deal with this case *) (* We use the Second RM assmption to deal with this case *)
apply rma2. (* for this we have to show that s ~_(dom a) t *) apply rma2. (* for this we have to show that s ~_(dom a) t *)
unfold view_partition, RMA, RMA_partition. unfold view_partition, RMA, RMA_partition.
intros m L. apply A. intros m L. apply A.
apply Cond1 with (u:=dom a). apply Cond1 with (u:=dom a).
apply Cond2 with (n:=n); [eapply rma3 | ]; eassumption. apply Cond2 with (n:=n); [eapply rma3 | ]; eassumption.
assumption. assumption.
@ -326,7 +320,7 @@ Proof.
(* TODO: repetition *) (* TODO: repetition *)
apply rma2. (* for this we have to show that s ~_(dom a) t *) apply rma2. (* for this we have to show that s ~_(dom a) t *)
unfold view_partition, RMA, RMA_partition. unfold view_partition, RMA, RMA_partition.
intros m L. apply A. intros m L. apply A.
apply Cond1 with (u:=dom a). apply Cond1 with (u:=dom a).
apply Cond2 with (n:=n); [eapply rma3| ]; eassumption. apply Cond2 with (n:=n); [eapply rma3| ]; eassumption.
assumption. assumption.
@ -339,7 +333,7 @@ End ACI.
Section Intransitive. Section Intransitive.
(** Auxiliary definitions *) (** Auxiliary definitions *)
Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : FinSet domain := Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : gset domain :=
match ls with match ls with
| [] => {[ d ]} | [] => {[ d ]}
| a::tl => let src := sources tl d in | a::tl => let src := sources tl d in
@ -351,7 +345,7 @@ Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : FinSet domai
Lemma sources_mon `{Policy} : forall a ls d, sources ls d ⊆ sources (a::ls) d. Lemma sources_mon `{Policy} : forall a ls d, sources ls d ⊆ sources (a::ls) d.
Proof. Proof.
intros. simpl. intros. simpl.
destruct (decide _); [apply union_subseteq_l |]; auto. destruct (decide _); [apply union_subseteq_l |]; auto.
Qed. Qed.
Hint Resolve sources_mon. Hint Resolve sources_mon.
@ -360,12 +354,12 @@ Lemma sources_monotone `{Policy} : forall ls js d, sublist ls js → sources ls
Proof. Proof.
intros ls js d M. intros ls js d M.
induction M. simpl. reflexivity. induction M. simpl. reflexivity.
simpl. destruct (decide (∃ v : domain, v ∈ sources l1 d ∧ policy (dom x) v)); destruct (decide (∃ v : domain, v ∈ sources l2 d ∧ policy (dom x) v)). simpl. destruct (decide (∃ v : domain, v ∈ sources l1 d ∧ policy (dom x) v)); destruct (decide (∃ v : domain, v ∈ sources l2 d ∧ policy (dom x) v)).
- apply union_mono_r. assumption. - apply union_mono_r. assumption.
- exfalso. apply n. destruct e as [v [e1 e2]]. exists v; split; try (apply (IHM v)); assumption. - exfalso. apply n. destruct e as [v [e1 e2]]. exists v; split; try (apply (IHM v)); assumption.
- transitivity (sources l2 d). assumption. apply union_subseteq_l. - transitivity (sources l2 d). assumption. apply union_subseteq_l.
- assumption. - assumption.
- transitivity (sources l2 d); auto. - transitivity (sources l2 d); auto.
Qed. Qed.
Lemma sources_in `{Policy} : forall ls d, d ∈ sources ls d. Lemma sources_in `{Policy} : forall ls d, d ∈ sources ls d.
@ -408,9 +402,13 @@ Proof.
apply (H ls (dom a)). apply (H ls (dom a)).
Qed. Qed.
Definition view_partition_general `{ViewPartition domain} (C : FinSet domain) s t := forall (u: domain), u ∈ C -> view_partition u s t. Definition view_partition_general
`{!ViewPartition domain, !EqDecision domain, !Countable domain}
(C : gset domain) s t
:= forall (u: domain), u ∈ C -> view_partition u s t.
Global Instance view_partition_general_equiv `{ViewPartition domain}: Global Instance view_partition_general_equiv
`{ViewPartition domain, !EqDecision domain, !Countable domain}:
forall V, Equivalence (view_partition_general V). forall V, Equivalence (view_partition_general V).
Proof. Proof.
intro V. split. intro V. split.
@ -422,10 +420,10 @@ Qed.
Definition weakly_step_consistent `{Policy domain} `{ViewPartition domain} := Definition weakly_step_consistent `{Policy domain} `{ViewPartition domain} :=
forall s t u a, view_partition u s t -> view_partition (dom a) s t -> view_partition u (step s a) (step t a). forall s t u a, view_partition u s t -> view_partition (dom a) s t -> view_partition u (step s a) (step t a).
Ltac exists_inside v := Ltac exists_inside v :=
let H := fresh "Holds" in let H := fresh "Holds" in
let nH := fresh "notHolds" in let nH := fresh "notHolds" in
destruct (decide _) as [H | []]; destruct (decide _) as [H | []];
[ try reflexivity | exists v; try auto]. [ try reflexivity | exists v; try auto].
Local Hint Resolve sources_mon. Local Hint Resolve sources_mon.
@ -436,7 +434,7 @@ Local Hint Resolve elem_of_union.
(* Lemma 3 *) (* Lemma 3 *)
Lemma weakly_step_consistent_general `{Policy domain} `{ViewPartition domain} (s t : state) (a : action) ls (u: domain) : weakly_step_consistent -> locally_respects_policy -> Lemma weakly_step_consistent_general `{Policy domain} `{ViewPartition domain} (s t : state) (a : action) ls (u: domain) : weakly_step_consistent -> locally_respects_policy ->
view_partition_general (sources (a::ls) u) s t view_partition_general (sources (a::ls) u) s t
-> view_partition_general (sources ls u) (step s a) (step t a). -> view_partition_general (sources ls u) (step s a) (step t a).
Proof. Proof.
intros WSC LRP P v vIn. intros WSC LRP P v vIn.
@ -444,12 +442,12 @@ Proof.
unfold locally_respects_policy in LRP. unfold locally_respects_policy in LRP.
destruct (decide (policy (dom a) v)). destruct (decide (policy (dom a) v)).
(* Case [dom a ~> v] *) (* Case [dom a ~> v] *)
apply WSC; apply P. auto. apply WSC; apply P. auto.
(* we need to show that [dom a ∈ sources (a::ls) v] *) (* we need to show that [dom a ∈ sources (a::ls) v] *)
simpl. exists_inside v. apply elem_of_union. right. auto. apply elem_of_singleton; trivial. simpl. exists_inside v. apply elem_of_union. right. auto. apply elem_of_singleton; trivial.
(* Case [dom a ~/> v] *) (* Case [dom a ~/> v] *)
transitivity s. symmetry. apply LRP; assumption. transitivity s. symmetry. apply LRP; assumption.
transitivity t. apply P. auto. transitivity t. apply P. auto.
apply LRP; assumption. apply LRP; assumption.
Qed. Qed.
@ -476,14 +474,14 @@ Proof.
induction ls; intros s t. induction ls; intros s t.
simpl. intro A. apply (A u). apply elem_of_singleton; reflexivity. simpl. intro A. apply (A u). apply elem_of_singleton; reflexivity.
intro VPG. simpl. unfold sources. fold (sources (a::ls) u). intro VPG. simpl. unfold sources. fold (sources (a::ls) u).
destruct (decide _). destruct (decide _).
(** Case [dom a ∈ sources (a::ls) u] *) (** Case [dom a ∈ sources (a::ls) u] *)
simpl. apply IHls. apply weakly_step_consistent_general; auto. simpl. apply IHls. apply weakly_step_consistent_general; auto.
(** Case [dom a ∉ sources (a::ls) u] *) (** Case [dom a ∉ sources (a::ls) u] *)
apply IHls. symmetry. transitivity t. apply IHls. symmetry. transitivity t.
- intros v vIn. symmetry. apply VPG. apply sources_mon; exact vIn. - intros v vIn. symmetry. apply VPG. apply sources_mon; exact vIn.
- apply locally_respects_gen; try(assumption). - apply locally_respects_gen; try(assumption).
Qed. Qed.
@ -503,7 +501,7 @@ Proof. intro policyA.
unfold view_partition. unfold RMA_partition; simpl. intros n L. unfold view_partition. unfold RMA_partition; simpl. intros n L.
destruct (decide (contents (step s a) n = contents s n)) as [E1 | NE1]. destruct (decide (contents (step s a) n = contents s n)) as [E1 | NE1].
destruct (decide (contents (step t a) n = contents t n)) as [E2 | NE2]. destruct (decide (contents (step t a) n = contents t n)) as [E2 | NE2].
(* Case [contents (step s a) n = contents s n /\ contents (step t a) n = contents t n] *) (* Case [contents (step s a) n = contents s n /\ contents (step t a) n = contents t n] *)
rewrite E1, E2. apply A1; assumption. rewrite E1, E2. apply A1; assumption.
(* Case [contents (step t a) n ≠ contents t n] *) (* Case [contents (step t a) n ≠ contents t n] *)
apply rma2; [ | right]; assumption. apply rma2; [ | right]; assumption.

3
_CoqProject
View File

@ -1,2 +1,3 @@
-R . "" -R . NI
Rushby.v Rushby.v
ArrayMachine.v

0
Mealy.v → experimental/Mealy.v
View File

0
MealySync.v → experimental/MealySync.v
View File

0
Monoids.v → experimental/Monoids.v
View File

0
Policy.v → experimental/Policy.v
View File

0
Security.v → experimental/Security.v
View File

0
ViewPartition.v → experimental/ViewPartition.v
View File