darcsweb - verified/html_pure_proofs.v

(** Correctness proofs for HTML escaping functions. *)

From Stdlib.Strings Require Import Byte.
From Stdlib Require Import Ascii String Bool.
Require Import html_pure.

Open Scope string_scope.

(** -- Concrete correctness for esc_char -- *)

Lemma esc_char_lt : esc_char "<"%char = "&lt;".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_char_gt : esc_char ">"%char = "&gt;".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_char_amp : esc_char "&"%char = "&amp;".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_char_quot : esc_char dquote = "&quot;".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_char_apos : esc_char squote = "&#39;".
Proof. vm_compute. reflexivity. Qed.

(** Safe characters pass through unchanged *)

Lemma esc_char_a : esc_char "a"%char = "a".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_char_space : esc_char " "%char = " ".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_char_zero : esc_char "0"%char = "0".
Proof. vm_compute. reflexivity. Qed.

(** -- String-level escaping -- *)

Lemma esc_empty : esc EmptyString = EmptyString.
Proof. reflexivity. Qed.

Lemma esc_safe_string : esc "hello" = "hello".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_lt_string : esc "<" = "&lt;".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_mixed : esc "<b>" = "&lt;b&gt;".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_amp_in_text : esc "a&b" = "a&amp;b".
Proof. vm_compute. reflexivity. Qed.

Lemma esc_script_tag : esc "<script>alert(1)</script>" =
  "&lt;script&gt;alert(1)&lt;/script&gt;".
Proof. vm_compute. reflexivity. Qed.

(** -- Security property: esc output contains no raw '<' -- *)

Fixpoint string_mem (c : ascii) (s : string) : bool :=
  match s with
  | EmptyString => false
  | String c' rest => Ascii.eqb c c' || string_mem c rest
  end.

Lemma string_mem_append : forall c a b,
  string_mem c (String.append a b) = string_mem c a || string_mem c b.
Proof.
  intros c a. induction a as [| c' a' IH]; intros b.
  - reflexivity.
  - simpl. rewrite IH. rewrite Bool.orb_assoc. reflexivity.
Qed.

(** No esc_char output contains a raw '<' character. *)
Lemma esc_char_no_raw_lt : forall c, string_mem "<"%char (esc_char c) = false.
Proof.
  intro c.
  destruct c as [[] [] [] [] [] [] [] []]; vm_compute; reflexivity.
Qed.

(** The key security theorem: escaping eliminates all raw '<' characters. *)
Theorem esc_no_raw_lt : forall s, string_mem "<"%char (esc s) = false.
Proof.
  induction s as [| c rest IH].
  - reflexivity.
  - simpl. rewrite string_mem_append.
    rewrite esc_char_no_raw_lt. simpl. exact IH.
Qed.

(** No esc_char output contains a raw '>' character. *)
Lemma esc_char_no_raw_gt : forall c, string_mem ">"%char (esc_char c) = false.
Proof.
  intro c.
  destruct c as [[] [] [] [] [] [] [] []]; vm_compute; reflexivity.
Qed.

(** Escaping eliminates all raw '>' characters. *)
Theorem esc_no_raw_gt : forall s, string_mem ">"%char (esc s) = false.
Proof.
  induction s as [| c rest IH].
  - reflexivity.
  - simpl. rewrite string_mem_append.
    rewrite esc_char_no_raw_gt. simpl. exact IH.
Qed.

(** No esc_char output contains a raw double-quote character. *)
Lemma esc_char_no_raw_quot : forall c, string_mem dquote (esc_char c) = false.
Proof.
  intro c.
  destruct c as [[] [] [] [] [] [] [] []]; vm_compute; reflexivity.
Qed.

(** Escaping eliminates all raw double-quote characters. *)
Theorem esc_no_raw_quot : forall s, string_mem dquote (esc s) = false.
Proof.
  induction s as [| c rest IH].
  - reflexivity.
  - simpl. rewrite string_mem_append.
    rewrite esc_char_no_raw_quot. simpl. exact IH.
Qed.