(** Correctness proofs for CSP header construction functions.
Key security theorem: sanitize_value eliminates all semicolons,
so no injected value can break out of its directive. *)
From Stdlib Require Import Ascii String Bool List.
Require Import csp_pure.
Import ListNotations.
Open Scope string_scope.
Open Scope bool_scope.
(** -- strip_char correctness -- *)
Lemma strip_char_empty : forall c, strip_char c "" = "".
Proof. reflexivity. Qed.
Lemma strip_char_removes : strip_char ";"%char "a;b" = "ab".
Proof. vm_compute. reflexivity. Qed.
Lemma strip_char_noop : strip_char ";"%char "abc" = "abc".
Proof. vm_compute. reflexivity. Qed.
Lemma strip_char_all : strip_char ";"%char ";;;" = "".
Proof. vm_compute. reflexivity. Qed.
(** -- Security theorem: sanitize_value strips all semicolons -- *)
Lemma strip_char_no_target : forall c s,
string_contains c (strip_char c s) = false.
Proof.
intros c s. induction s as [| h rest IH].
- reflexivity.
- simpl. destruct (Ascii.eqb h c) eqn:Heq.
+ exact IH.
+ simpl. rewrite Heq. simpl. exact IH.
Qed.
(** The key security property: sanitized values contain no semicolons. *)
Theorem sanitize_value_no_semicolons : forall v,
string_contains ";"%char (sanitize_value v) = false.
Proof.
intro v. unfold sanitize_value. apply strip_char_no_target.
Qed.
(** -- build_directive correctness -- *)
Lemma build_directive_simple :
build_directive "default-src" "'none'" = "default-src 'none'".
Proof. vm_compute. reflexivity. Qed.
Lemma build_directive_sanitizes :
build_directive "style-src" "'self'; script-src 'unsafe-inline'" =
"style-src 'self' script-src 'unsafe-inline'".
Proof. vm_compute. reflexivity. Qed.
(** -- build_csp correctness -- *)
Lemma build_csp_empty : build_csp nil = "".
Proof. reflexivity. Qed.
Lemma build_csp_single :
build_csp (("default-src", "'none'") :: nil) =
"default-src 'none'".
Proof. vm_compute. reflexivity. Qed.
Lemma build_csp_two :
build_csp (("default-src", "'none'") :: ("style-src", "'self'") :: nil) =
"default-src 'none'; style-src 'self'".
Proof. vm_compute. reflexivity. Qed.
Lemma build_csp_three :
build_csp (("default-src", "'none'") ::
("style-src", "'self'") ::
("img-src", "'self'") :: nil) =
"default-src 'none'; style-src 'self'; img-src 'self'".
Proof. vm_compute. reflexivity. Qed.
(** Injection attempt: semicolons in values are stripped. *)
Lemma build_csp_injection_attempt :
build_csp (("default-src", "'none'; script-src 'unsafe-inline'") :: nil) =
"default-src 'none' script-src 'unsafe-inline'".
Proof. vm_compute. reflexivity. Qed.
