Main
Set Implicit Arguments.
Require Import Coq.Arith.PeanoNat Strings.String Lists.List Lia Program.Equality.
Ltac inv H := (inversion H; subst; clear H).
Section Compositionality.
Require Import Coq.Arith.PeanoNat Strings.String Lists.List Lia Program.Equality.
Ltac inv H := (inversion H; subst; clear H).
Section Compositionality.
Definition el { A } (x : A) (C : A → Prop) := C x.
Notation "x '∈' A" := (el x A) (at level 50).
Definition subset { A } (C1 C2 : A → Prop) := ∀ x, x ∈ C1 → x ∈ C2.
Notation "A '⊆' B" := (subset A B) (at level 50).
Notation "A '≡' B" := (A ⊆ B ∧ B ⊆ A) (at level 50).
Axiom set_ext : ∀ A, ∀ (X Y : A → Prop), X ≡ Y → X = Y.
Definition intersect { A } (C1 C2 : A → Prop) := ∀ x, x ∈ C1 ∧ x ∈ C2.
Axiom Intersection : ∀ A, ∀ (C1 C2 : A → Prop), A → Prop.
Notation "A '∩' B" := (Intersection A B) (at level 50).
Axiom IntroIntersect : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ X → x ∈ Y → x ∈ (X ∩ Y).
Axiom ElimIntersect : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ (X ∩ Y) → x ∈ X ∧ x ∈ Y.
Definition union { A } (C1 C2 : A → Prop) := ∀ x, x ∈ C1 ∨ x ∈ C2.
Axiom Union : ∀ A, ∀ (C1 C2 : A → Prop), A → Prop.
Notation "A '∪' B" := (Union A B) (at level 50).
Axiom IntroUnion : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ X ∨ x ∈ Y → x ∈ (X ∪ Y).
Axiom ElimUnion : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ (X ∪ Y) → x ∈ X ∨ x ∈ Y.
Lemma self_intersect { A } (C : A → Prop) :
C ∩ C = C.
Lemma self_union { A } (C : A → Prop) :
C ∪ C = C.
Notation "x '∈' A" := (el x A) (at level 50).
Definition subset { A } (C1 C2 : A → Prop) := ∀ x, x ∈ C1 → x ∈ C2.
Notation "A '⊆' B" := (subset A B) (at level 50).
Notation "A '≡' B" := (A ⊆ B ∧ B ⊆ A) (at level 50).
Axiom set_ext : ∀ A, ∀ (X Y : A → Prop), X ≡ Y → X = Y.
Definition intersect { A } (C1 C2 : A → Prop) := ∀ x, x ∈ C1 ∧ x ∈ C2.
Axiom Intersection : ∀ A, ∀ (C1 C2 : A → Prop), A → Prop.
Notation "A '∩' B" := (Intersection A B) (at level 50).
Axiom IntroIntersect : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ X → x ∈ Y → x ∈ (X ∩ Y).
Axiom ElimIntersect : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ (X ∩ Y) → x ∈ X ∧ x ∈ Y.
Definition union { A } (C1 C2 : A → Prop) := ∀ x, x ∈ C1 ∨ x ∈ C2.
Axiom Union : ∀ A, ∀ (C1 C2 : A → Prop), A → Prop.
Notation "A '∪' B" := (Union A B) (at level 50).
Axiom IntroUnion : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ X ∨ x ∈ Y → x ∈ (X ∪ Y).
Axiom ElimUnion : ∀ A, ∀ (X Y : A → Prop), ∀ x, x ∈ (X ∪ Y) → x ∈ X ∨ x ∈ Y.
Lemma self_intersect { A } (C : A → Prop) :
C ∩ C = C.
Lemma self_union { A } (C : A → Prop) :
C ∪ C = C.
Axiom Trace : Set.
(* Set of traces *)
Definition Property := Trace → Prop.
(* Set of sets of traces *)
Definition Hyperproperty := Property → Prop.
(* Sets of hyperproperties *)
Definition PClass := Hyperproperty → Prop.
Abstract description of a Programming Language
- A set of (admissible) partial programs. Basically, partial programs are syntactically and semantically correct.
- A judgement that checks whether a partial program is partial or not. Only whole programs can be executed.
- The linker is self-explanatory.
- The step relation, as mentioned before, works on whole programs and emits their behaviour. Behaviours are, like properties, just sets of traces. For languages with deterministic semantics, these are singleton sets that contain just one trace.
Record Language : Type :=
{
Partials : Set;
whole : Partials → Prop;
link : Partials → Partials → Partials;
step : ∀ (p : Partials), whole p → Property;
}.
Notation "C '⋈' P" := (link _ P C) (at level 50).
Definition SumLanguage (L0 L1 : Language)
(cross_linker : Partials L0 → Partials L1 → Partials L0 + Partials L1)
:=
{|
Partials := Partials L0 + Partials L1 ;
whole := fun (p : Partials L0 + Partials L1) ⇒
match p with
| inl p0 ⇒ whole L0 p0
| inr p1 ⇒ whole L1 p1
end
;
link := fun (p0 p1 : Partials L0 + Partials L1) ⇒
match p0, p1 with
| inl pa, inl pb ⇒ inl(link L0 pa pb)
| inr pa, inr pb ⇒ inr(link L1 pa pb)
| inl pa, inr pb ⇒ cross_linker pa pb
| inr pa, inl pb ⇒ cross_linker pb pa
end
;
step := fun (p : Partials L0 + Partials L1) ⇒
match p with
| inl p0 ⇒ fun (H0 : whole L0 p0) ⇒ step L0 p0 H0
| inr p1 ⇒ fun (H1 : whole L1 p1) ⇒ step L1 p1 H1
end
;
|}.
{
Partials : Set;
whole : Partials → Prop;
link : Partials → Partials → Partials;
step : ∀ (p : Partials), whole p → Property;
}.
Notation "C '⋈' P" := (link _ P C) (at level 50).
Definition SumLanguage (L0 L1 : Language)
(cross_linker : Partials L0 → Partials L1 → Partials L0 + Partials L1)
:=
{|
Partials := Partials L0 + Partials L1 ;
whole := fun (p : Partials L0 + Partials L1) ⇒
match p with
| inl p0 ⇒ whole L0 p0
| inr p1 ⇒ whole L1 p1
end
;
link := fun (p0 p1 : Partials L0 + Partials L1) ⇒
match p0, p1 with
| inl pa, inl pb ⇒ inl(link L0 pa pb)
| inr pa, inr pb ⇒ inr(link L1 pa pb)
| inl pa, inr pb ⇒ cross_linker pa pb
| inr pa, inl pb ⇒ cross_linker pb pa
end
;
step := fun (p : Partials L0 + Partials L1) ⇒
match p with
| inl p0 ⇒ fun (H0 : whole L0 p0) ⇒ step L0 p0 H0
| inr p1 ⇒ fun (H1 : whole L1 p1) ⇒ step L1 p1 H1
end
;
|}.
Definition Compiler (L0 L1 : Language) := Partials L0 → Partials L1.
Definition seqcomp {L0 L1 L2 : Language} (f : Compiler L1 L2) (g : Compiler L0 L1) := fun x ⇒ f (g x).
Notation "f '∘' g" := (seqcomp g f) (at level 50).
Section Satisfaction.
Definition seqcomp {L0 L1 L2 : Language} (f : Compiler L1 L2) (g : Compiler L0 L1) := fun x ⇒ f (g x).
Notation "f '∘' g" := (seqcomp g f) (at level 50).
Section Satisfaction.
Context {K : Language}.
Definition sat (p : Partials K) (π : Property) : Prop := ∀ (H : whole K p), ∀ t, step K p H t → t ∈ π.
Definition rsat (p : Partials K) (π : Property) : Prop := ∀ (c : Partials K), sat (c ⋈ p) π.
Definition behaviour (p : Partials K) (H : whole K p) : Property := fun b ⇒ step K p H b.
Definition hsat (p : Partials K) (Π : Hyperproperty) : Prop := ∀ (H : whole K p), behaviour p H ∈ Π.
Definition rhsat (p : Partials K) (Π : Hyperproperty) : Prop := ∀ (c : Partials K), hsat (c ⋈ p) Π.
Definition csat (p : Partials K) (C : PClass) : Prop := ∀ Π, Π ∈ C → hsat p Π.
Definition rcsat (p : Partials K) (C : PClass) : Prop := ∀ Π, Π ∈ C → rhsat p Π.
End Satisfaction.
Notation "p '|-' C" := (rcsat p C) (at level 50).
Notation "p '|=' Π" := (rhsat p Π) (at level 50).
Section Main.
Variable S I T : Language.
Variable linkSI : Partials S → Partials I → Partials S + Partials I.
Definition RC { L0 L1 : Language } (γ : Compiler L0 L1) (C : PClass) :=
∀ Π, Π ∈ C → ∀ (p : Partials L0), p |= Π → γ p |= Π.
Notation "'pres|-' γ ':' C" := (RC γ C) (at level 50, γ at next level).
Definition sat (p : Partials K) (π : Property) : Prop := ∀ (H : whole K p), ∀ t, step K p H t → t ∈ π.
Definition rsat (p : Partials K) (π : Property) : Prop := ∀ (c : Partials K), sat (c ⋈ p) π.
Definition behaviour (p : Partials K) (H : whole K p) : Property := fun b ⇒ step K p H b.
Definition hsat (p : Partials K) (Π : Hyperproperty) : Prop := ∀ (H : whole K p), behaviour p H ∈ Π.
Definition rhsat (p : Partials K) (Π : Hyperproperty) : Prop := ∀ (c : Partials K), hsat (c ⋈ p) Π.
Definition csat (p : Partials K) (C : PClass) : Prop := ∀ Π, Π ∈ C → hsat p Π.
Definition rcsat (p : Partials K) (C : PClass) : Prop := ∀ Π, Π ∈ C → rhsat p Π.
End Satisfaction.
Notation "p '|-' C" := (rcsat p C) (at level 50).
Notation "p '|=' Π" := (rhsat p Π) (at level 50).
Section Main.
Variable S I T : Language.
Variable linkSI : Partials S → Partials I → Partials S + Partials I.
Definition RC { L0 L1 : Language } (γ : Compiler L0 L1) (C : PClass) :=
∀ Π, Π ∈ C → ∀ (p : Partials L0), p |= Π → γ p |= Π.
Notation "'pres|-' γ ':' C" := (RC γ C) (at level 50, γ at next level).
Lemma sequential_composition (γ0 : Compiler S I) (γ1 : Compiler I T) (C0 C1 : PClass) :
pres|- γ0 : C0 → pres|- γ1 : C1 → pres|- (γ0 ∘ γ1) : (C0 ∩ C1).
Proof.
intros H0 H1 Π H2 p H3.
apply ElimIntersect in H2 as [H2a H2b].
apply H1; trivial.
apply H0; trivial.
Qed.
Corollary swappable (γ0 γ1 : Compiler I I) (C0 C1 : PClass) :
pres|- γ0 : C0 → pres|- γ1 : C1 → pres|- (γ0 ∘ γ1) : (C0 ∩ C1) ∧ pres|- (γ1 ∘ γ0) : (C0 ∩ C1).
Proof.
intros H0 H1; split.
all:
intros Π H2 p H3;
apply ElimIntersect in H2 as [H2a H2b];
(apply H1, H0 || apply H0, H1); trivial.
Qed.
Definition UpperComposition { L0 L1 L2 : Language } { cross_link }
(γ0 : Compiler L0 L2) (γ1 : Compiler L1 L2)
: Partials (SumLanguage L0 L1 cross_link) → Partials L2
:=
fun (pab : Partials (SumLanguage L0 L1 cross_link)) ⇒
match pab with
| inl p ⇒ γ0 p
| inr p ⇒ γ1 p
end
.
Lemma upper_compose (γ0 : Compiler S T) (γ1 : Compiler I T) (C0 C1 : PClass) :
pres|- γ0 : C0 → pres|- γ1 : C1 → pres|- (@UpperComposition S I T linkSI γ0 γ1) : (C0 ∩ C1).
Proof.
intros H0 H1 Π H2 [pS | pI] H3; apply ElimIntersect in H2 as [H2a H2b].
- apply H0; try easy.
intros Cs Hw; specialize (H3 (inl Cs) Hw); assumption.
- apply H1; try easy.
intros Cs Hw; specialize (H3 (inr Cs) Hw); assumption.
Qed.
(* Secure Enforcements *)
Definition enforcement { L0 L1 : Language } (γ : Compiler L0 L1) (C : PClass) := ∀ (p : Partials L0), rcsat (γ p) C.
Notation "'enf|-' γ '--≻' C" := (enforcement γ C) (at level 80).
Definition secure_enforcement { L0 L1 : Language } (γ : Compiler L0 L1) (C0 C1 : PClass) :=
pres|- γ : C0 ∧ enf|- γ --≻ C1.
Notation "'senf|-' γ '-[' C0 ']-≻' C1" := (secure_enforcement γ C0 C1) (at level 50).
Lemma senf_and_rc (γ0 : Compiler S I) (γ1 : Compiler I T) (C0 C1 : PClass) :
pres|- γ0 : C0 → senf|- γ1 -[ C0 ]-≻ C1 → pres|- (γ0 ∘ γ1) : (C0 ∪ C1).
Proof.
intros H0 [H1a H1b] Π H2 p H3.
apply ElimUnion in H2 as [H2a|H2b].
- apply H1a; trivial. apply H0; trivial.
- apply H1b; trivial.
Qed.
Lemma rc_and_senf (γ0 : Compiler S I) (γ1 : Compiler I T) (C0 C1 : PClass) :
senf|- γ0 -[ C0 ]-≻ C1 → pres|- γ1 : C0 → pres|- (γ0 ∘ γ1) : (C0 ∪ C1).
Proof.
intros [H0a H0b] H1 Π H2 p H3.
apply ElimUnion in H2 as [H2a|H2b].
- apply H1; trivial. apply H0a; trivial.
- (* This is where things go wrong. We can only apply H1, but this means
we need to prove that our pi is in C0, which it isn't...! *)
Abort.
Lemma join_sinstrus (γ1 : Compiler S I) (γ2 : Compiler I T) (C0 C1 C2 : PClass) :
senf|- γ1 -[C0]-≻ C1 → senf|- γ2 -[C1]-≻ C2 → senf|- (γ1 ∘ γ2) -[C0 ∩ C1]-≻ (C1 ∪ C2).
Proof.
intros [H0a H0b] [H1a H1b]; split.
- intros Π H2 p H3; apply ElimIntersect in H2 as [H2a H2b].
apply H1a; trivial; apply H0a; trivial.
- intros p Π H2; apply ElimUnion in H2 as [H2a|H2b].
+ apply H1a; trivial; now apply H0b.
+ now apply H1b.
Qed.
Lemma instru_union (γ : Compiler S T) (C0 C1 : PClass) :
senf|- γ -[C0]-≻ C1 → pres|- γ : (C0 ∪ C1).
Proof.
intros [H0a H0b] Π H2 p H3.
apply ElimUnion in H2 as [H2a|H2b].
- apply H0a; assumption.
- apply H0b; assumption.
Qed.
Lemma instru_cap (γ : Compiler S T) (C0 C1 : PClass) :
senf|- γ -[C0]-≻ C1 → pres|- γ : (C0 ∩ C1).
Proof.
intros [H0a H0b] Π H2 p H3.
apply ElimIntersect in H2 as [H2a H2b].
now apply H0a.
Qed.
Lemma join_instrus (γ0 : Compiler S I) (γ1 : Compiler I T) (C0 C1 : PClass) :
senf|- γ0 -[C1]-≻ C0 → senf|- γ1 -[C0]-≻ C1 → senf|- (γ0 ∘ γ1) -[C1]-≻ C0 ∧ senf|- (γ0 ∘ γ1) -[C0]-≻ C1.
Proof.
intros [H0a H0b] [H1a H1b]; repeat split.
- intros Π H2 p H3. now apply H1b.
- intros p Π H2. apply H1a; try assumption. now apply H0b.
- intros Π H2 p H3. apply H1a; try assumption. now apply H0b.
- intros p Π H2. now apply H1b.
Qed.
Lemma swappable_instrus (γ0 : Compiler I I) (γ1 : Compiler I I) (C0 C1 : PClass) :
senf|- γ0 -[C0]-≻ C1 → senf|- γ1 -[C1]-≻ C0 → senf|- (γ0 ∘ γ1) -[C0 ∪ C1]-≻ (C0 ∪ C1) ∧
senf|- (γ1 ∘ γ0) -[C0 ∪ C1]-≻ (C0 ∪ C1).
Proof.
intros [H0a H0b] [H1a H1b]; repeat split.
- intros Π H2 p H3; apply ElimUnion in H2 as [H2a|H2b].
+ now apply H1b.
+ apply H1a; trivial; now apply H0b.
- intros p Π H2; apply ElimUnion in H2 as [H2a|H2b].
+ now apply H1b.
+ apply H1a; trivial; now apply H0b.
- intros Π H2 p H3; apply ElimUnion in H2 as [H2a|H2b].
+ apply H0a; trivial; now apply H1b.
+ now apply H0b.
- intros p Π H2; apply ElimUnion in H2 as [H2a|H2b].
+ apply H0a; trivial; now apply H1b.
+ now apply H0b.
Qed.
Definition ProdLanguage (L0 L1 : Language) :=
{|
Partials := (Partials L0) × (Partials L1) ;
whole := fun (p : (Partials L0) × (Partials L1)) ⇒
match p with
| (p0, p1) ⇒ whole L0 p0 ∧ whole L1 p1
end
;
link := fun (p0 p1 : (Partials L0) × (Partials L1)) ⇒
match p0, p1 with
| (pa0, pa1), (pb0, pb1) ⇒
(link L0 pa0 pb0, link L1 pa1 pb1)
end
;
step := fun (p : (Partials L0) × (Partials L1)) ⇒
let '(p0, p1) := p in
fun H ⇒
match H with
| conj H0 H1 ⇒ fun (τ : Trace) ⇒ step L0 p0 H0 τ ∧ step L1 p1 H1 τ
end
;
|}.
Notation "L0 'L*' L1" := (ProdLanguage L0 L1) (at level 80).
(* Lower Composition *)
Definition LowerComposition { L0 L1 L2 : Language } (γ0 : Compiler L0 L1) (γ1 : Compiler L0 L2)
: Partials L0 → Partials (ProdLanguage L1 L2)
:=
fun (p : Partials L0) ⇒ (γ0 p, γ1 p)
.
Definition subset_closed (Π : Hyperproperty) :=
∀ (π : Property), π ∈ Π → ∀ (π' : Property), π' ⊆ π → π' ∈ Π.
Definition ssc_class (C : PClass) :=
∀ (Π : Hyperproperty), Π ∈ C → subset_closed Π.
Lemma lowercomp_compose (γ0 : Compiler S I) (γ1 : Compiler S T) (C0 C1 : PClass) :
ssc_class C0 →
pres|- γ0 : C0 → pres|- γ1 : C1 → pres|- (LowerComposition γ0 γ1) : (C0 ∩ C1).
Proof.
intros SSC0 H0 H1 Π H2 p H3; apply ElimIntersect in H2 as [H2a H2b].
intros [Ci Ct] Hw. unfold LowerComposition in ×.
apply H0 in H3 as H3a; apply H1 in H3 as H3b; trivial.
unfold "_ |= _" in ×. unfold behaviour; cbn; destruct Hw as [Hw0 Hw1].
specialize (H3a Ci Hw0); specialize (H3b Ct Hw1).
unfold behaviour in H3a, H3b.
change (fun b ⇒ ?h b) with h in H3a, H3b.
apply SSC0 in H2a as SSPi. eapply SSPi in H3a, H3b.
apply H3a. intros τ H4.
change (τ ∈ (fun b : Trace ⇒ ?h b)) with (τ ∈ h) in H4.
unfold "_ ∈ _" in ×. destruct H4 as [H4a H4b]. assumption.
Qed.
Lemma enforcement_implies_robustness (γ : Compiler S I) (C : PClass) :
enf|- γ --≻ C → pres|- γ : C.
Proof.
intros H0 Π H1 p H2; now apply H0.
Qed.
Lemma enforcements_are_secure_for_fixed_class (γ : Compiler S I) (C : PClass) :
enf|- γ --≻ C → senf|- γ -[C]-≻ C.
Proof.
intros H0; split.
- intros H1 Π H2 p; now apply H0.
- exact H0.
Qed.
End Main.
End Compositionality.