(** Verified pure functions for Content-Security-Policy header construction.
Extracted to Haskell for use in the DarcsWeb application.
Security property: the builder ensures no raw semicolons appear within
individual directive values, preventing CSP injection attacks where
an attacker-controlled value could introduce new directives. *)
From Stdlib Require Import Ascii String Bool List.
From Stdlib Require Import ExtrHaskellString.
Import ListNotations.
Open Scope string_scope.
Open Scope bool_scope.
(** -- Helper: check if a character appears in a string -- *)
Fixpoint string_contains (needle : ascii) (haystack : string) : bool :=
match haystack with
| EmptyString => false
| String c rest => Ascii.eqb c needle || string_contains needle rest
end.
(** -- Helper: remove all occurrences of a character -- *)
Fixpoint strip_char (c : ascii) (s : string) : string :=
match s with
| EmptyString => EmptyString
| String h rest =>
if Ascii.eqb h c then strip_char c rest
else String h (strip_char c rest)
end.
(** Sanitize a single CSP directive value by stripping semicolons. *)
Definition sanitize_value (v : string) : string :=
strip_char ";"%char v.
(** Build a single CSP directive: "name value".
The value is sanitized to strip any embedded semicolons. *)
Definition build_directive (name : string) (value : string) : string :=
String.append name (String.append " " (sanitize_value value)).
(** Join a list of strings with "; " separator. *)
Fixpoint join_directives (ds : list string) : string :=
match ds with
| nil => EmptyString
| d :: nil => d
| d :: rest => String.append d (String.append "; " (join_directives rest))
end.
(** Build a complete CSP header from a list of (name, value) pairs. *)
Definition build_csp (directives : list (string * string)) : string :=
let ds := List.map (fun p => build_directive (fst p) (snd p)) directives in
join_directives ds.
(* -- Extraction setup -- *)
Set Extraction Output Directory "../gen".
Extraction Language Haskell.
Extract Inlined Constant String.append => "(Prelude.++)".
Extraction "CspPure"
sanitize_value
build_directive
build_csp.
