Skip to content

Commit 40d8e9f

Browse files
sjqtentaclescursoragent
sjqtentacles
and
cursoragent
committed
Add record-layer protection, cert-chain validation, extension codecs, and HOL4 spec scaffolding
Track A1 - TlsRecordProtect: per-record nonce (IV XOR seq), AEAD encrypt/decrypt with content-type hiding + padding, 2^14 size limit. RFC 8448 encrypted-record vectors verified. 14 tests. Track A2 - TlsCertVerify: chain building to trust anchors, RSA-PSS/PKCS1 signature verification, validity dates, hostname/SAN matching with wildcard rules, BasicConstraints/pathLen, KeyUsage/EKU enforcement. ECDSA hook for sml-p256. 18 tests with deterministic openssl fixtures. Track A3 - TlsExtensions: parse/build for key_share (CH+SH), supported_versions, supported_groups, signature_algorithms, SNI, ALPN. Negotiation helpers. Downgrade sentinels. All decoders total. 65 tests. Track B1 - HOL4 formal spec: wire structure datatypes + encode/decode relations, key schedule functions, handshake transition relation, and safety invariants. Round-trip theorems stated; RFC 8448 vectors as theorem goals. Awaiting HOL4 build for Holmake validation. Phase 0 scaffolding: INTEGRATION.md (J1 contract), cakeml/README.md, proof/Holmakefile. 136 tests pass on MLton + Poly/ML, byte-identical. Co-authored-by: Cursor <cursoragent@cursor.com>
1 parent bb503b6 commit 40d8e9f

40 files changed

Lines changed: 3903 additions & 0 deletions

‎INTEGRATION.md‎

Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
# Integration contract (J1 integrator's checklist)
2+
3+
This document is the **J1 join-point checklist**: exactly where each
4+
parallel track's deliverable plugs into the `TlsClient.step` /
5+
`TlsServer.step` state machine in
6+
[`lib/github.com/sjqtentacles/sml-tls/tls.sml`](lib/github.com/sjqtentacles/sml-tls/tls.sml),
7+
and which state fields each adds. It was frozen in Phase 0 so the
8+
integrator does not re-discover the seams.
9+
10+
The Phase 0 stubs (`TlsRecordProtect`, `TlsCertVerify`, `TlsExtensions`)
11+
are wired into the build ([`sources.mlb`](lib/github.com/sjqtentacles/sml-tls/sources.mlb))
12+
and the test suite ([`test/sources.mlb`](test/sources.mlb),
13+
[`test/entry.sml`](test/entry.sml)) but their bodies currently `raise
14+
Fail "todo: A1|A2|A3"`. The J1 integrator replaces the seams below with
15+
real calls once each track's TDD work is green.
16+
17+
## Current state machine (pre-J1)
18+
19+
`TlsClient` / `TlsServer` carry:
20+
21+
- `x25519PrivateKey`, `clientRandom` / `serverRandom`, `legacySessionId`,
22+
`cipherSuites` / `cipherSuite`, `extensions` (a `TlsHandshake.extension list`).
23+
- The negotiated `keySchedule` (all seven secrets from `TlsKeySchedule.schedule`)
24+
after the ServerHello is processed.
25+
- Traffic-key accessors (`serverHandshakeKey`, `clientHandshakeKey`,
26+
`serverAppKey`, `clientAppKey`) that return `(key, iv)` options.
27+
- A `transcript` accumulator (concatenated wire-form handshake messages).
28+
29+
**Gap the J1 integrator closes:** record AEAD is currently *offloaded to
30+
the caller* (see `tls.sig` lines 422-440 — "the caller does that using
31+
traffic keys extracted from the state"). There is no HelloRetryRequest,
32+
no extension negotiation/enforcement, no certificate-chain validation,
33+
no KeyUpdate / NewSessionTicket / resumption, and only limited alert-on-error.
34+
35+
## A1 — Record-layer protection (`TlsRecordProtect`) → into `step`
36+
37+
**Seam:** every place `TlsClient.step` / `TlsServer.step` currently hands
38+
the caller a plaintext record to AEAD-protect/decrypt, the state machine
39+
instead calls `TlsRecordProtect`.
40+
41+
**New state fields** (added to `clientState` / `serverState`):
42+
43+
- `serverWriteProtect : TlsRecordProtect.state option`
44+
— initialised with `TlsRecordProtect.init {key, iv}` from the server
45+
handshake-traffic key once the ServerHello is processed; re-initialised
46+
from the server application-traffic key after the server Finished.
47+
- `clientWriteProtect : TlsRecordProtect.state option`
48+
— same, for the client's write direction (handshake then application).
49+
- `serverReadProtect : TlsRecordProtect.state option`
50+
— the peer's write direction seen from our side (the inverse).
51+
- `clientReadProtect : TlsRecordProtect.state option`
52+
53+
**Call sites in `step`:**
54+
55+
- **Outbound:** before emitting any post-ServerHello record, the state
56+
machine calls
57+
`TlsRecordProtect.protect {state, innerType, plaintext, pad}`
58+
to produce the `TLSCiphertext` body, then `TlsRecord.encodeCiphertext`
59+
for the 5-byte header. `innerType` is `Handshake` during the handshake,
60+
`ApplicationData` afterwards, `Alert` for alerts.
61+
- **Inbound:** `TlsRecord.decodeCiphertext` parses the 5-byte header, then
62+
`TlsRecordProtect.unprotect {state, record}` authenticates and strips
63+
padding. `NONE` → emit `bad_record_mac` (fatal); plaintext longer than
64+
`TlsRecordProtect.maxPlaintext` → `record_overflow` (fatal).
65+
66+
**Replaces:** the `trafficKeys` accessor pattern and the "caller does
67+
record decryption" note in `tls.sig` (the accessor stays for
68+
inspection/testing, but `step` no longer requires the caller to AEAD).
69+
70+
## A3 — Extension negotiation (`TlsExtensions`) → into `step` + CH/SH build
71+
72+
**Seam:** `TlsClient.startHandshake` / `TlsServer.produceServerHello`
73+
build the ClientHello/ServerHello extension lists; `step` parses the
74+
peer's extensions and enforces negotiation.
75+
76+
**New state fields:**
77+
78+
- `negotiatedGroup : Word16.word option` — the selected key-share group
79+
(X25519 today, P-256 after A4).
80+
- `negotiatedSigAlg : Word16.word option` — the selected signature
81+
algorithm for CertificateVerify.
82+
- `downgradeChecked : bool` — set once the ServerHello.random is
83+
confirmed free of the `downgradeSentinelTls12` / `downgradeSentinelTls11`
84+
sentinels (§4.1.3).
85+
86+
**Call sites:**
87+
88+
- **CH build:** `TlsExtensions.encodeSupportedVersionsCH`,
89+
`encodeSupportedGroups`, `encodeKeyShareCH`, `encodeSignatureAlgorithms`,
90+
`encodeServerName`, `encodeAlpn` produce the ClientHello extension
91+
bodies (currently the state machine builds these inline).
92+
- **SH parse:** `TlsExtensions.decodeSelectedVersionSH`,
93+
`decodeKeyShareSH` parse the ServerHello extensions; `negotiateGroup`
94+
/ `negotiateSigAlg` / `negotiateVersion` pick the agreed parameters.
95+
- **Enforcement:** if negotiation yields `NONE` → `handshake_failure` /
96+
`illegal_parameter` as appropriate; if a downgrade sentinel is present
97+
in `ServerHello.random` → `illegal_parameter`.
98+
- **HelloRetryRequest (new):** if the server rejects the client's
99+
`key_share` / `supported_groups`, it emits an HRR with a `cookie`
100+
extension; the client's `step` must handle the synthetic
101+
`MessageHash` transcript reset (§4.1.3) using
102+
`TlsKeySchedule` + the HRR message.
103+
104+
## A2 — Certificate-chain validation (`TlsCertVerify`) → at the Certificate step
105+
106+
**Seam:** when `step` receives the server's `Certificate` message (client
107+
side) or the client's `Certificate` (server side, if requested).
108+
109+
**New state fields:**
110+
111+
- `trustStore : string list` — caller-supplied DER trust anchors (passed
112+
in via `clientConfig` / `serverConfig`).
113+
- `now : int` — injected unix time (caller-supplied, keeps the library pure).
114+
- `sigAlgs : Word16.word list` — acceptable signature algorithms.
115+
116+
**Call site in `step` (client side):** after parsing the server
117+
`Certificate` and `CertificateVerify`:
118+
119+
1. `TlsCertVerify.verifyChain {chain, trust, hostname, now, sigAlgs}`
120+
→ `Valid` continues the handshake; `Invalid desc` → emit `desc`
121+
(fatal) and abort.
122+
2. The `CertificateVerify` signature itself is verified separately
123+
(RSA-PSS via `Rsa`, ECDSA via A4 `P256` once wired). A failed
124+
signature → `decrypt_error`.
125+
126+
**Hostname:** comes from the caller (a new `clientConfig` field); matched
127+
via `TlsCertVerify.matchHostname` against the leaf's SAN/CN.
128+
129+
## A4 — `sml-p256` (NIST P-256) → `key_share` + `signature_algorithms`
130+
131+
**Seam:** once `sml-p256` is vendored into `lib/github.com/sjqtentacles/`,
132+
it adds a second key-share group and ECDSA signature scheme.
133+
134+
**New constants** (in `TlsHandshake`):
135+
136+
- `groupSecp256r1 : Word16.word` = `0x0017` (§4.2.7) — alongside
137+
`groupX25519` (`0x001d`).
138+
- `sigEcdsaSecp256r1Sha256 : Word16.word` = `0x0403` (already present).
139+
140+
**New state fields:**
141+
142+
- `p256PrivateKey : string option` — caller-supplied 32-byte scalar
143+
(alongside `x25519PrivateKey`).
144+
145+
**Call sites:**
146+
147+
- `key_share`: the client may now offer both X25519 and P-256 entries;
148+
the server's `negotiateGroup` picks one. ECDH uses
149+
`P256.ecdh {privateKey, peerPublic}`.
150+
- `CertificateVerify`: ECDSA signatures (`sigEcdsaSecp256r1Sha256`)
151+
verified via `P256.ecdsaVerify {publicKey, message, signatureDer}`.
152+
153+
## Alert state machine (J1)
154+
155+
J1 also wires the full alert mapping: every protocol violation in `step`
156+
that currently raises `Tls` instead emits the correct fatal `TlsAlert`
157+
(record-wrapped under the current traffic key via `TlsRecordProtect`)
158+
and transitions to a terminal `Error` state. This is the single biggest
159+
behavioural change for the integrator.
160+
161+
## Out of scope for J1
162+
163+
- A5 conformance/fuzz harnesses (those run at J2 against the J1 result).
164+
- B1 HOL4 spec and B2 CakeML port (parallel; feed J3/J4, not J1).
165+
- Revocation via CRL (OCSP stapling parsing is in A2; CRL deferred).

‎cakeml/README.md‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# `cakeml/` — CakeML crypto-tower port (Track B2)
2+
3+
This directory holds the **CakeML subset/basis port** of the sjqtentacles
4+
crypto tower (Track B2, Phase 6). It starts at Phase 0 and runs in
5+
parallel with all functional work, because the crypto libraries are
6+
already stable — only the TLS-specific code waits for J2 (then it ports
7+
at J3).
8+
9+
## What goes here
10+
11+
One `<lib>.sml` port per library, fanned out by the dependency DAG:
12+
13+
- **L0 (no deps, 5 parallel workers):** `sml-codec` (SHA-256),
14+
`sml-bigint`, `sml-aes`, `sml-chacha20`, `sml-x25519`.
15+
- **L1 (after L0):** `sml-pem`, `sml-crypto` (HMAC), `sml-asn1`, `sml-aead`.
16+
- **L2 (after L1):** `sml-kdf`, `sml-rsa`.
17+
- **L3:** `sml-x509`.
18+
- **L4 (J3, after J2 stabilises the functional code):** the `sml-tls`
19+
sources themselves.
20+
21+
Each port is a *separate file* from the original SML — never edit the
22+
originals. The MLton/Poly build stays green in parallel as the porting
23+
oracle.
24+
25+
## Spike first
26+
27+
The **SHA-256 spike** (L0) is the go/no-go gate for the CakeML dialect
28+
before fanning out the rest of the tower: port it, build it under
29+
CakeML, and diff its output against the MLton `sml-codec` vectors.
30+
31+
## Toolchain to pin
32+
33+
- **CakeML:** pin a tagged release (record the exact commit in
34+
`cakeml/CAKEML_VERSION` once the spike lands).
35+
- **HOL4:** the CakeML translator (`ml_translatorLib` / `cv` tooling)
36+
requires a matching HOL4 build (record in `cakeml/HOL4_VERSION`).
37+
38+
These are added by the B2 sub-agent; this README is the Phase 0
39+
placeholder.

‎lib/github.com/sjqtentacles/sml-tls/certverify.sig‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
(* certverify.sig
2+
3+
Certificate-chain validation for TLS 1.3 (RFC 8446 §4.4.2), built on
4+
sml-x509 + sml-rsa (+ sml-p256 ECDSA, wired at J1).
5+
6+
Pure and deterministic: the trust store, hostname, current time, and
7+
acceptable signature algorithms are all passed in as parameters, so
8+
the same inputs always produce the same accept/alert outcome on both
9+
MLton and Poly/ML. No network access at test time.
10+
11+
This is the frozen contract for Track A2 (Phase 3). The Phase 0 stub
12+
raises `Fail "todo: A2"` from every function; the A2 subagent fills
13+
in the bodies against golden-chain fixtures. *)
14+
15+
signature TLS_CERT_VERIFY =
16+
sig
17+
(* DER-encoded trust anchors (one string per anchor certificate). *)
18+
type trustStore = string list
19+
20+
(* The outcome of chain validation. `Invalid` carries the alert the
21+
caller should send (and that the J1 integrator wires into the
22+
handshake state machine). *)
23+
datatype result = Valid | Invalid of TlsAlert.alertDescription
24+
25+
(* Validate a leaf-first DER certificate chain to a trust anchor:
26+
- chain building to a caller-supplied trust store,
27+
- signature verification up the chain (RSA-PSS/PKCS1; ECDSA via
28+
A4 `sml-p256` once wired, otherwise `Invalid UnsupportedCertificate`),
29+
- validity dates against the injected `now`,
30+
- hostname/SAN matching incl. wildcard rules (RFC 6125),
31+
- KeyUsage / EKU / BasicConstraints / pathLenConstraint (RFC 5280),
32+
- `sigAlgs` enforcement (§4.2.3). *)
33+
val verifyChain : {chain : string list, (* leaf-first DER *)
34+
trust : trustStore,
35+
hostname : string,
36+
now : int, (* injected unix time *)
37+
sigAlgs : Word16.word list} -> result
38+
39+
(* RFC 6125 hostname / SAN matching, including wildcard rules:
40+
`*.a.com` matches `x.a.com`, not `a.com`, not `x.y.a.com`. *)
41+
val matchHostname : {host : string, certName : string} -> bool
42+
end

0 commit comments

Comments
 (0)