Skip to content

Commit fbfc201

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
fix(validator): enforce policy in production path; harden digests; add max_age freshness (#71)
Three real security gaps in the A2ML validator, closed with proofs: 1. validatePolicy was DEAD CODE in the production path: neither validateManifest nor validateManifestIO called it, so a manifest with require_sig=true and no attestation PASSED validation. It is now enforced in validateManifest (and hence validateManifestIO). 2. isValidHexString accepted '.' and empty strings with no length bound; it now requires exactly 64 hex chars (all supported algorithms emit 32-byte digests). 3. max_age freshness was never compared to a clock. validateManifestIO now fetches System.time and enforces it via a pure, total validatePolicyAt (clock passed as argument), backed by a minimal total ISO-8601 subset parser (YYYY-MM-DDTHH:MM:SSZ) with field range checks and epoch conversion. New machine-checked theorems (ValidatorProof.idr, %default total, no assert_total/believe_me): - requireSigNoAttestationRejected: require_sig without attestation is rejected by the pure validator (the gate is provably wired in) - staleManifestRejected: validatePolicyAt rejects a manifest older than max_age (end to end through the policy pipeline) - checkFreshnessRejectsStale / checkFreshnessAcceptsFresh - hexAcceptSound (strengthened): acceptance forces exact digest length AND hex-only content; hexWrongLengthRejected; hexEmptyRejected - parseTimestamp known-answer proofs (epoch, modern date, garbage, month 13) - validateManifestSound extended to a 4-tuple: accepted manifests also satisfy validatePolicy = Right () Tests updated for the stricter digest rule (hex64 padding helper in Property/Integration suites). Verified: ochrance.ipkg builds clean; ParserTests exit 0; PropertyTests 47/47; IntegrationTests 55 PASS. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent cc3a102 commit fbfc201

4 files changed

Lines changed: 391 additions & 70 deletions

File tree

‎ochrance-core/Ochrance/A2ML/Validator.idr‎

Lines changed: 215 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,15 @@
55
||| Ochrance.A2ML.Validator - Semantic validation of parsed manifests
66
|||
77
||| Checks that a parsed Manifest satisfies all semantic constraints:
8-
||| supported version, valid hash algorithms, valid base64, signature
9-
||| verification, and policy consistency.
8+
||| supported version, valid hash algorithms, well-formed digests,
9+
||| signature verification, and policy consistency (require_sig and
10+
||| max_age freshness).
1011

1112
module Ochrance.A2ML.Validator
1213

1314
import Data.Vect
1415
import Data.Maybe
16+
import System
1517
import Ochrance.A2ML.Types
1618
import Ochrance.Framework.Error
1719
import Ochrance.FFI.Crypto
@@ -51,13 +53,27 @@ isVersionSupported : String -> Bool
5153
isVersionSupported "0.1.0" = True
5254
isVersionSupported _ = False
5355

54-
||| Check if a hash value contains only valid hex characters
56+
||| Length, in hex characters, of a supported digest. All supported hash
57+
||| algorithms (BLAKE3, SHA-256, SHA3-256) produce 32-byte digests,
58+
||| i.e. exactly 64 hex characters.
59+
public export
60+
digestHexLength : Nat
61+
digestHexLength = 64
62+
63+
||| Check that a string consists of exactly `n` hex digits ([0-9a-fA-F]).
64+
||| Rejects the empty string whenever `n` is non-zero.
65+
public export
66+
isValidHexStringN : (n : Nat) -> String -> Bool
67+
isValidHexStringN n s =
68+
let cs = unpack s
69+
in length cs == n && all isHexDigit cs
70+
71+
||| Check if a hash value is a well-formed digest: exactly 64 hex characters.
72+
||| (An earlier version accepted '.' and imposed no length bound, so empty,
73+
||| truncated or padded "digests" passed validation.)
5574
public export
5675
isValidHexString : String -> Bool
57-
isValidHexString s = all isHexChar (unpack s)
58-
where
59-
isHexChar : Char -> Bool
60-
isHexChar c = isHexDigit c || c == '.'
76+
isValidHexString s = isValidHexStringN digestHexLength s
6177

6278
||| Validate a single reference's hash
6379
public export
@@ -67,8 +83,170 @@ validateRef ref =
6783
then Left (InvalidHashValue ref.hash.value)
6884
else Right ()
6985

70-
||| Validate a complete manifest (pure version, no signature verification).
71-
||| Use validateManifestIO for full validation including signatures.
86+
--------------------------------------------------------------------------------
87+
-- Timestamp Parsing (minimal total ISO-8601 subset)
88+
--------------------------------------------------------------------------------
89+
90+
||| Decimal value of a digit character. Public so proofs and tests can
91+
||| reduce `parseTimestamp` definitionally.
92+
public export
93+
digitVal : Char -> Maybe Integer
94+
digitVal c =
95+
if isDigit c
96+
then Just (cast (ord c - ord '0'))
97+
else Nothing
98+
99+
||| Read a fixed run of decimal digits as a non-negative Integer.
100+
public export
101+
readDigits : Integer -> List Char -> Maybe Integer
102+
readDigits acc [] = Just acc
103+
readDigits acc (c :: cs) = case digitVal c of
104+
Nothing => Nothing
105+
Just d => readDigits (acc * 10 + d) cs
106+
107+
||| Gregorian leap-year test.
108+
public export
109+
isLeapYear : Integer -> Bool
110+
isLeapYear y = (y `mod` 4 == 0 && y `mod` 100 /= 0) || y `mod` 400 == 0
111+
112+
||| Days in a month (1-12). Defensively 31 outside that range; callers
113+
||| range-check the month first.
114+
public export
115+
daysInMonth : (leap : Bool) -> (month : Integer) -> Integer
116+
daysInMonth leap 2 = if leap then 29 else 28
117+
daysInMonth _ 4 = 30
118+
daysInMonth _ 6 = 30
119+
daysInMonth _ 9 = 30
120+
daysInMonth _ 11 = 30
121+
daysInMonth _ _ = 31
122+
123+
||| Days before the first day of the given month (1-12) within one year.
124+
public export
125+
daysBeforeMonth : (leap : Bool) -> (month : Integer) -> Integer
126+
daysBeforeMonth leap m =
127+
let base : Integer = case m of
128+
1 => 0; 2 => 31; 3 => 59; 4 => 90
129+
5 => 120; 6 => 151; 7 => 181; 8 => 212
130+
9 => 243; 10 => 273; 11 => 304; _ => 334
131+
in if leap && m > 2 then base + 1 else base
132+
133+
||| Leap years strictly before the given year (counting from year 1;
134+
||| positive years only - truncating and floor division agree there).
135+
public export
136+
leapsBefore : Integer -> Integer
137+
leapsBefore y =
138+
let p = y - 1
139+
in p `div` 4 - p `div` 100 + p `div` 400
140+
141+
||| Days from 1970-01-01 to January 1st of the given year (year >= 1970).
142+
public export
143+
daysSinceEpochToYear : Integer -> Integer
144+
daysSinceEpochToYear y = 365 * (y - 1970) + (leapsBefore y - leapsBefore 1970)
145+
146+
||| Parse a manifest timestamp - the minimal total ISO-8601 subset
147+
||| YYYY-MM-DDTHH:MM:SSZ (UTC only, the format A2ML manifests carry) -
148+
||| into seconds since the Unix epoch. Rejects out-of-range date/time
149+
||| fields and years before 1970.
150+
public export
151+
parseTimestamp : String -> Maybe Integer
152+
parseTimestamp s = case unpack s of
153+
[y1,y2,y3,y4,'-',mo1,mo2,'-',d1,d2,'T',h1,h2,':',mi1,mi2,':',se1,se2,'Z'] => do
154+
year <- readDigits 0 [y1,y2,y3,y4]
155+
month <- readDigits 0 [mo1,mo2]
156+
day <- readDigits 0 [d1,d2]
157+
hour <- readDigits 0 [h1,h2]
158+
minute <- readDigits 0 [mi1,mi2]
159+
second <- readDigits 0 [se1,se2]
160+
let leap = isLeapYear year
161+
if year >= 1970
162+
&& month >= 1 && month <= 12
163+
&& day >= 1 && day <= daysInMonth leap month
164+
&& hour <= 23 && minute <= 59 && second <= 59
165+
then let days = daysSinceEpochToYear year
166+
+ daysBeforeMonth leap month
167+
+ (day - 1)
168+
in Just (((days * 24 + hour) * 60 + minute) * 60 + second)
169+
else Nothing
170+
_ => Nothing
171+
172+
--------------------------------------------------------------------------------
173+
-- Policy Validation
174+
--------------------------------------------------------------------------------
175+
176+
||| require_sig: a policy that requires a signature is violated by a
177+
||| manifest that carries no attestation.
178+
public export
179+
checkRequireSig : Policy -> Maybe Attestation -> Either ValidationError ()
180+
checkRequireSig p Nothing =
181+
if p.requireSig
182+
then Left (PolicyViolation "Policy requires signature but none present")
183+
else Right ()
184+
checkRequireSig _ (Just _) = Right ()
185+
186+
||| max_age: the constraint is only meaningful if the manifest carries a
187+
||| timestamp in the supported ISO-8601 subset. The freshness comparison
188+
||| itself needs a clock - see validatePolicyAt.
189+
public export
190+
checkMaxAgeShape : Policy -> Maybe String -> Either ValidationError ()
191+
checkMaxAgeShape p ts = case p.maxAge of
192+
Nothing => Right ()
193+
Just _ => case ts of
194+
Nothing =>
195+
Left (PolicyViolation "Policy specifies max_age but manifest has no timestamp")
196+
Just t => case parseTimestamp t of
197+
Nothing =>
198+
Left (PolicyViolation ("Policy specifies max_age but timestamp is not ISO-8601 YYYY-MM-DDTHH:MM:SSZ: " ++ t))
199+
Just _ => Right ()
200+
201+
||| Freshness: the manifest age (now - issued, both in seconds since the
202+
||| Unix epoch) must not exceed max_age seconds.
203+
public export
204+
checkFreshness : (now : Integer) -> (issued : Integer) -> (maxAge : Nat) ->
205+
Either ValidationError ()
206+
checkFreshness now issued maxAge =
207+
if now - issued > cast maxAge
208+
then Left (PolicyViolation ("Manifest age " ++ show (now - issued)
209+
++ "s exceeds policy max_age " ++ show maxAge ++ "s"))
210+
else Right ()
211+
212+
||| Validate the clock-free policy constraints of a manifest: require_sig
213+
||| demands an attestation, and max_age demands a parseable timestamp.
214+
||| Enforced by validateManifest (and hence validateManifestIO).
215+
public export
216+
validatePolicy : Manifest -> Either ValidationError ()
217+
validatePolicy m = case m.policy of
218+
Nothing => Right ()
219+
Just p => do
220+
checkRequireSig p m.attestation
221+
checkMaxAgeShape p m.manifestData.timestamp
222+
223+
||| Validate all policy constraints of a manifest at a given time (seconds
224+
||| since the Unix epoch): the clock-free constraints plus max_age
225+
||| freshness. Pure and total - the caller supplies `now`;
226+
||| validateManifestIO fetches it from the system clock.
227+
public export
228+
validatePolicyAt : (now : Integer) -> Manifest -> Either ValidationError ()
229+
validatePolicyAt now m = do
230+
validatePolicy m
231+
case m.policy of
232+
Nothing => Right ()
233+
Just p => case (p.maxAge, m.manifestData.timestamp) of
234+
(Just maxAge, Just ts) => case parseTimestamp ts of
235+
-- Unreachable after validatePolicy succeeds, but kept total
236+
-- and fail-closed rather than assuming reachability.
237+
Nothing =>
238+
Left (PolicyViolation ("Policy specifies max_age but timestamp is not ISO-8601 YYYY-MM-DDTHH:MM:SSZ: " ++ ts))
239+
Just issued => checkFreshness now issued maxAge
240+
_ => Right ()
241+
242+
--------------------------------------------------------------------------------
243+
-- Manifest Validation
244+
--------------------------------------------------------------------------------
245+
246+
||| Validate a complete manifest (pure version: no signature verification,
247+
||| no clock). Enforces the structural constraints and the clock-free
248+
||| policy constraints (require_sig, max_age shape). Use validateManifestIO
249+
||| for full validation including signatures and max_age freshness.
72250
public export
73251
validateManifest : Manifest -> Either ValidationError ValidManifest
74252
validateManifest m = do
@@ -82,8 +260,9 @@ validateManifest m = do
82260
else pure ()
83261
-- Validate all refs
84262
traverse_ validateRef m.refs
85-
-- Signature verification skipped in pure version
86-
-- Wrap in ValidManifest
263+
-- Enforce clock-free policy constraints (require_sig, max_age shape)
264+
validatePolicy m
265+
-- Signature verification and freshness are IO concerns - see validateManifestIO
87266
Right (MkValidManifest m)
88267

89268
--------------------------------------------------------------------------------
@@ -114,54 +293,36 @@ verifySignatureIO sigHex pubkeyHex hash = do
114293
Right Nothing => pure False -- Hex parsing failure => reject
115294
Right (Just ok) => pure ok
116295

117-
||| Validate a complete manifest with signature verification (IO version).
118-
||| This performs full validation including cryptographic signature checks.
296+
||| Validate a complete manifest with signature verification and policy
297+
||| freshness (IO version). This performs full validation including
298+
||| cryptographic signature checks and max_age enforcement against the
299+
||| system clock.
119300
export
120301
validateManifestIO : HasIO io => Manifest -> io (Either ValidationError ValidManifest)
121302
validateManifestIO m = do
122-
-- Run pure validation first
303+
-- Run pure validation first (structure + clock-free policy constraints)
123304
case validateManifest m of
124305
Left err => pure (Left err)
125306
Right _ => do
126-
-- If attestation present, verify signature
127-
case m.attestation of
128-
Nothing => pure (Right (MkValidManifest m))
129-
Just att => do
130-
-- Compute manifest hash for signature verification
131-
let manifestBytes = serializeForSigning m
132-
hashResult <- blake3 manifestBytes
133-
134-
case hashResult of
135-
Left _ => pure (Left SignatureVerificationFailed)
136-
Right manifestHash => do
137-
-- Verify signature (Ed25519 via FFI)
138-
signatureValid <- verifySignatureIO att.signature att.pubkey manifestHash
139-
140-
if signatureValid
141-
then pure (Right (MkValidManifest m))
142-
else pure (Left SignatureVerificationFailed)
307+
-- Enforce max_age freshness against the system clock
308+
now <- time
309+
case validatePolicyAt now m of
310+
Left err => pure (Left err)
311+
Right () =>
312+
-- If attestation present, verify signature
313+
case m.attestation of
314+
Nothing => pure (Right (MkValidManifest m))
315+
Just att => do
316+
-- Compute manifest hash for signature verification
317+
let manifestBytes = serializeForSigning m
318+
hashResult <- blake3 manifestBytes
143319

144-
--------------------------------------------------------------------------------
145-
-- Policy Validation
146-
--------------------------------------------------------------------------------
320+
case hashResult of
321+
Left _ => pure (Left SignatureVerificationFailed)
322+
Right manifestHash => do
323+
-- Verify signature (Ed25519 via FFI)
324+
signatureValid <- verifySignatureIO att.signature att.pubkey manifestHash
147325

148-
||| Validate that a manifest satisfies policy constraints
149-
export
150-
validatePolicy : Manifest -> Either ValidationError ()
151-
validatePolicy m =
152-
case m.policy of
153-
Nothing => Right ()
154-
Just p => do
155-
-- Check require_sig policy
156-
if p.requireSig && isNothing m.attestation
157-
then Left (PolicyViolation "Policy requires signature but none present")
158-
else Right ()
159-
-- Check max_age policy (requires timestamp)
160-
case (p.maxAge, m.manifestData.timestamp) of
161-
(Just _, Nothing) =>
162-
Left (PolicyViolation "Policy specifies max_age but manifest has no timestamp")
163-
_ => Right ()
164-
where
165-
isNothing : Maybe a -> Bool
166-
isNothing Nothing = True
167-
isNothing (Just _) = False
326+
if signatureValid
327+
then pure (Right (MkValidManifest m))
328+
else pure (Left SignatureVerificationFailed)

0 commit comments

Comments
 (0)