1111||| - Origin reflection without validation
1212||| - Overly permissive method/header lists
1313||| - Missing Vary: Origin header
14+ |||
15+ ||| All proofs are constructive. Zero believe_me. Zero postulates.
1416module Boj.SafeCORS
1517
1618import Data.List
1719import Data.Nat
1820import Data.String
21+ import Boj.SafetyLemmas
1922
2023%default total
2124
@@ -30,6 +33,14 @@ isOriginChar c =
3033 isAlphaNum c || c == ' -' || c == ' .' || c == ' :' || c == ' /' ||
3134 c == ' [' || c == ' ]'
3235
36+ ||| Predicate: an origin character list contains only valid characters.
37+ public export
38+ data OriginCharsValid : List Char -> Type where
39+ MkOriginCharsValid : (cs : List Char) ->
40+ {auto nonEmpty : NonEmpty cs} ->
41+ {auto prf : all isOriginChar cs = True} ->
42+ OriginCharsValid cs
43+
3344||| Predicate: an origin string contains only valid characters.
3445public export
3546data OriginValid : String -> Type where
@@ -50,6 +61,30 @@ data NotWildcard : String -> Type where
5061 {auto prf : (s == wildcardOrigin) = False} ->
5162 NotWildcard s
5263
64+ ||| Theorem: origin char validity implies no spaces (prevents header injection).
65+ export
66+ originCharsNoSpace : OriginCharsValid cs -> Not (Elem ' ' cs)
67+ originCharsNoSpace (MkOriginCharsValid cs {prf}) elemPrf =
68+ let charFails : isOriginChar ' ' = True
69+ charFails = allTrueElem prf elemPrf
70+ in absurd charFails
71+
72+ ||| Theorem: origin char validity implies no newlines (prevents response splitting).
73+ export
74+ originCharsNoNewline : OriginCharsValid cs -> Not (Elem '\n' cs)
75+ originCharsNoNewline (MkOriginCharsValid cs {prf}) elemPrf =
76+ let charFails : isOriginChar '\n' = True
77+ charFails = allTrueElem prf elemPrf
78+ in absurd charFails
79+
80+ ||| Theorem: origin char validity implies no carriage returns.
81+ export
82+ originCharsNoCR : OriginCharsValid cs -> Not (Elem '\r' cs)
83+ originCharsNoCR (MkOriginCharsValid cs {prf}) elemPrf =
84+ let charFails : isOriginChar '\r' = True
85+ charFails = allTrueElem prf elemPrf
86+ in absurd charFails
87+
5388-- ------------------------------------------------------------------------------
5489-- CORS Policy Types
5590-- ------------------------------------------------------------------------------
@@ -74,18 +109,22 @@ data CORSHeader : Type where
74109public export
75110record SafeCORSPolicy where
76111 constructor MkSafeCORSPolicy
77- allowedOrigins : List String
78- allowedMethods : List CORSMethod
79- allowedHeaders : List CORSHeader
112+ allowedOrigins : List String
113+ allowedMethods : List CORSMethod
114+ allowedHeaders : List CORSHeader
80115 allowCredentials : Bool
81- maxAge : Nat -- Preflight cache seconds
116+ maxAge : Nat -- Preflight cache seconds
82117
83118-- ------------------------------------------------------------------------------
84119-- Safety Predicates
85120-- ------------------------------------------------------------------------------
86121
87122||| Predicate: a CORS policy does not combine wildcard origin with credentials.
88123||| This is the most critical CORS misconfiguration to prevent.
124+ |||
125+ ||| Constructors encode the two safe cases:
126+ ||| - NoCredentials: credentials is False, so wildcard is harmless
127+ ||| - NoWildcard: wildcard is not in origins, so credentials are safe
89128public export
90129data CORSCredentialSafe : SafeCORSPolicy -> Type where
91130 NoCredentials : (p : SafeCORSPolicy) ->
@@ -95,7 +134,7 @@ data CORSCredentialSafe : SafeCORSPolicy -> Type where
95134 {auto prf : not (elem wildcardOrigin p.allowedOrigins) = True} ->
96135 CORSCredentialSafe p
97136
98- ||| Predicate: all origins in the policy are valid (no wildcards with credentials) .
137+ ||| Predicate: all origins in the policy are valid character-wise .
99138public export
100139data AllOriginsValid : List String -> Type where
101140 NilOrigins : AllOriginsValid []
@@ -106,23 +145,65 @@ public export
106145data ReasonableMaxAge : Nat -> Type where
107146 MkReasonableMaxAge : (n : Nat ) -> {auto prf : LTE n 86400} -> ReasonableMaxAge n
108147
148+ ||| A fully validated CORS policy: credential-safe, valid origins, bounded max-age.
149+ public export
150+ record ValidatedCORSPolicy where
151+ constructor MkValidatedCORSPolicy
152+ policy : SafeCORSPolicy
153+ 0 credSafe : CORSCredentialSafe policy
154+ 0 originsValid : AllOriginsValid policy.allowedOrigins
155+ 0 maxAgeBounded : ReasonableMaxAge policy.maxAge
156+
109157-- ------------------------------------------------------------------------------
110158-- Core Theorems
111159-- ------------------------------------------------------------------------------
112160
113161||| Theorem: a policy with credentials=False is always credential-safe,
114162||| regardless of origin list contents.
163+ ||| Proof: directly construct NoCredentials with the Refl witness.
115164export
116165noCredsAlwaysSafe : (p : SafeCORSPolicy) ->
117166 {auto prf : p.allowCredentials = False} ->
118167 CORSCredentialSafe p
119168noCredsAlwaysSafe p = NoCredentials p
120169
121170||| Theorem: the empty origin list is valid.
171+ ||| Proof: NilOrigins constructor directly.
122172export
123173emptyOriginsValid : AllOriginsValid []
124174emptyOriginsValid = NilOrigins
125175
176+ ||| Theorem: credential safety is decidable for any policy.
177+ ||| Proof: case split on allowCredentials; if False, NoCredentials;
178+ ||| if True, check for wildcard in origins.
179+ export
180+ decideCredentialSafe : (p : SafeCORSPolicy) ->
181+ Either (CORSCredentialSafe p)
182+ (p. allowCredentials = True , elem wildcardOrigin p. allowedOrigins = True )
183+ decideCredentialSafe p with (p. allowCredentials) proof credPrf
184+ decideCredentialSafe p | False = Left (NoCredentials p {prf = credPrf})
185+ decideCredentialSafe p | True with (elem wildcardOrigin p. allowedOrigins) proof elemPrf
186+ decideCredentialSafe p | True | False =
187+ Left (NoWildcard p {prf = rewrite elemPrf in Refl })
188+ decideCredentialSafe p | True | True =
189+ Right (credPrf, elemPrf)
190+
191+ ||| Theorem: adding a valid origin to valid origins preserves validity.
192+ ||| Proof: ConsOrigins constructor.
193+ export
194+ consOriginsValid : OriginValid o -> AllOriginsValid os -> AllOriginsValid (o :: os)
195+ consOriginsValid = ConsOrigins
196+
197+ ||| Theorem: max-age of 0 is always reasonable.
198+ export
199+ zeroMaxAgeReasonable : ReasonableMaxAge 0
200+ zeroMaxAgeReasonable = MkReasonableMaxAge 0
201+
202+ ||| Theorem: max-age of 3600 (1 hour) is reasonable.
203+ export
204+ oneHourMaxAgeReasonable : ReasonableMaxAge 3600
205+ oneHourMaxAgeReasonable = MkReasonableMaxAge 3600
206+
126207-- ------------------------------------------------------------------------------
127208-- Default Policies
128209-- ------------------------------------------------------------------------------
@@ -139,6 +220,12 @@ bojDefaultCORS = MkSafeCORSPolicy
139220 , maxAge = 3600
140221 }
141222
223+ ||| Theorem: the default CORS policy is credential-safe.
224+ ||| Proof: credentials is False, so NoCredentials applies.
225+ export
226+ bojDefaultCORSIsSafe : CORSCredentialSafe SafeCORS.bojDefaultCORS
227+ bojDefaultCORSIsSafe = NoCredentials bojDefaultCORS
228+
142229||| The BoJ production CORS policy: specific origins, with credentials.
143230public export
144231bojProductionCORS : SafeCORSPolicy
@@ -150,6 +237,12 @@ bojProductionCORS = MkSafeCORSPolicy
150237 , maxAge = 7200
151238 }
152239
240+ ||| Theorem: the production CORS policy is credential-safe.
241+ ||| Proof: allowedOrigins is empty, so wildcard cannot be an element.
242+ export
243+ bojProductionCORSIsSafe : CORSCredentialSafe SafeCORS.bojProductionCORS
244+ bojProductionCORSIsSafe = NoWildcard bojProductionCORS
245+
153246-- ------------------------------------------------------------------------------
154247-- FFI Bridge Declarations
155248-- ------------------------------------------------------------------------------
@@ -173,19 +266,24 @@ boj_safety_check_cors_policy : (originsPtr : AnyPtr) -> (methodsPtr : AnyPtr) ->
173266||| Summary of CORS safety properties proven in this module:
174267|||
175268||| 1. **Credential/Wildcard Exclusion**: Credentials=True and Origin=* are
176- ||| mutually exclusive. Proof: CORSCredentialSafe is a sum type requiring
177- ||| either credentials=False OR wildcard not in origins .
269+ ||| mutually exclusive. Proof: CORSCredentialSafe sum type; decideCredentialSafe
270+ ||| provides a decision procedure that returns evidence for either case .
178271|||
179272||| 2. **Origin Validation**: All origin strings validated against character set.
180- ||| Proof: OriginValid requires all chars pass isOriginChar.
273+ ||| Proofs: originCharsNoSpace, originCharsNoNewline, originCharsNoCR use
274+ ||| allTrueElem to derive contradiction from isOriginChar.
181275|||
182276||| 3. **Method Restriction**: Only GET/POST/OPTIONS allowed — no PUT/DELETE
183- ||| from cross-origin contexts by default.
277+ ||| from cross-origin contexts by default. Proof: CORSMethod ADT.
184278|||
185279||| 4. **Max-Age Bounds**: Preflight cache capped at 24 hours to limit
186- ||| stale policy window.
280+ ||| stale policy window. Proof: ReasonableMaxAge carries LTE witness.
187281|||
188282||| 5. **Default Policies**: Pre-built safe policies for dev and production.
283+ ||| Proofs: bojDefaultCORSIsSafe and bojProductionCORSIsSafe are witnesses.
284+ |||
285+ ||| 6. **Composition**: ValidatedCORSPolicy bundles all safety properties
286+ ||| into a single record with erased proofs.
189287public export
190288corsSafetyGuarantees : String
191- corsSafetyGuarantees = " BoJ SafeCORS: 5 proven properties preventing CORS misconfiguration"
289+ corsSafetyGuarantees = " BoJ SafeCORS: 6 proven properties preventing CORS misconfiguration"
0 commit comments