gazagnaire.org
TPM 2.0 command/response wire codec (TCG TPM 2.0 Library)
tpm: add a deployment security review packet
A reviewer-facing REVIEW.md: scope, threat model, the security properties the
code enforces (with source references), the audit trail of issues found and
fixed, the independent-audit result, the residual limitations, and the
evidence (tests, fuzz, live swtpm smoke, merlint). It is written to make an
independent human security review fast and is explicit that it does not
replace one.
author
Thomas Gazagnaire
date
(May 30, 2026, 2:04 AM -0700)
commit
3a21b1e1
3a21b1e1d30ce58a213cca53747cc0a7c3ef1e9a
parent
3f0f1e03
3f0f1e03000e77c1d5df140720e052f96593dc44
+138
+138
REVIEW.md
+138
REVIEW.md
···
1
+
# ocaml-tpm — security review packet
2
+
3
+
This document is for a reviewer deciding whether to deploy `ocaml-tpm`. It
4
+
states the scope, the threat model, the security properties the code enforces
5
+
(with source references), the audit trail of issues found and fixed, the
6
+
residual limitations, and the evidence available. It is written to make an
7
+
independent human security review fast; it is **not** a substitute for one.
8
+
9
+
## Scope
10
+
11
+
A native, pure-OCaml TPM 2.0 client: it marshals the TCG TPM 2.0
12
+
command/response stream directly, with no FFI to `tpm2-tss`, so it links into a
13
+
statically-linked binary or a unikernel-style space-init where a C TSS cannot.
14
+
15
+
- `tpm` — the pure codec and protocol library. No I/O, no clock, no ambient
16
+
randomness. Depends on `wire` (byte layout), `digestif` (hash/HMAC), `eqaf`
17
+
(constant-time compare), `nox-crypto`/`nox-crypto-ec` (AES-CFB, P-256).
18
+
- `tpm-eio` — an Eio transport carrying packets over a Unix/TCP socket (swtpm)
19
+
or a `/dev/tpm*` character device.
20
+
21
+
## Threat model
22
+
23
+
The client talks to a TPM across a bus a malicious host may sit on. Therefore:
24
+
25
+
- **Every response byte is attacker-controlled.** Unauthenticated commands
26
+
(GetRandom, GetCapability, StartAuthSession, PCR_Read) carry no HMAC, so their
27
+
responses are fully forgeable by a bus interposer.
28
+
- **Authenticated responses are parsed before the HMAC is verified**, so a
29
+
malformed authenticated response is also reachable by a MITM.
30
+
- The client may link into a PID-1-like process, so an uncaught exception or a
31
+
memory-exhaustion read is an availability concern, not just a correctness one.
32
+
33
+
Out of scope: physical attacks on the TPM itself; the correctness of the
34
+
underlying crypto primitives in `digestif`/`nox-crypto`/`nox-crypto-ec`;
35
+
side-channel resistance of those primitives (see Residuals).
36
+
37
+
## Security properties enforced
38
+
39
+
- **Authenticated responses are authenticated before they are trusted.** The
40
+
response HMAC is checked with `Eqaf.equal` (constant-time) *before* any
41
+
response parameter is decoded or decrypted and *before* `nonceTPM` is rolled
42
+
(`lib/session.ml`, `verify_response_entry` / `parse_response`). A mismatch
43
+
fails loud and propagates; there is no path that accepts a forged HMAC.
44
+
- **Anti-replay / anti-structure-confusion on attestation.** `Quote.verify`
45
+
(`lib/quote.ml`) confirms the signed structure is a quote (`TPM_GENERATED`
46
+
magic, `TPM_ST_ATTEST_QUOTE` type) committing to the caller's challenge nonce
47
+
*before* validating the ECDSA signature. A replayed quote, or a validly signed
48
+
non-quote (e.g. a `TPM2_Certify` attest), is rejected — proven end-to-end with
49
+
a real P-256 signature in `test/test_quote.ml`.
50
+
- **Sealed secrets stay off the bus.** AES-128-CFB parameter encryption is keyed
51
+
by `sessionValue = sessionKey || authValue` (Part 1 sec 21.2), so an unsealed
52
+
value is encrypted to the session even on a snooped bus
53
+
(`lib/session.ml`, `cfb_transform`).
54
+
- **Framing is bounded and exact.** `response_length` caps the advertised
55
+
`responseSize` at 64 KiB and rejects sub-header sizes; `unframe` requires
56
+
`responseSize == bytes received`, so a padded/truncated packet cannot smuggle
57
+
trailing bytes through as parameters (`lib/marshal.ml`).
58
+
- **No silent integer truncation.** `Marshal.u8`/`u16`/`u32` reject
59
+
out-of-range values rather than masking to the low bits (`lib/marshal.ml`).
60
+
- **Bounds-checked decoding.** The `Marshal.Reader` cursor bound-checks every
61
+
read; a hostile count-prefixed list cannot pre-allocate or loop forever
62
+
(every element codec has a strictly positive minimum size, and the buffer is
63
+
capped at 64 KiB), and an oversized `TPM2B` raises rather than reading out of
64
+
bounds (CVE-2023-1018 regression).
65
+
- **Total response-code decoding.** `Rc.decode`/`name`/`pp` are total over all
66
+
32-bit codes (CVE-2023-22745 regression).
67
+
- **Weak-nonce rejection.** `nonceCaller` and `nonceTPM` below 16 octets are
68
+
rejected (`lib/session.ml`).
69
+
- **Key hygiene.** The session key, the salt, and the bind authorization value
70
+
are held in `Tpm.Secret` — an abstract wipeable buffer — and `Session.destroy`
71
+
zeros the key; `Secret.destroy` zeros the salt/bind-auth once the session key
72
+
is derived (`lib/secret.ml`, `lib/session.ml`).
73
+
74
+
## Audit trail (issues found and fixed)
75
+
76
+
Each was found by adversarial review and fixed with a regression/hostile test.
77
+
78
+
| Issue | Fix |
79
+
|---|---|
80
+
| `response_length` returned the raw UINT32 `responseSize` → a hostile bus announcing 4 GiB causes a memory-exhaustion read | cap at 64 KiB, reject sub-header sizes |
81
+
| `unframe` ignored `responseSize` → padded/truncated packet smuggles trailing bytes as parameters | require `responseSize == bytes received` |
82
+
| `Marshal.u16 70000` silently packed as 4464; `Rand.command` count was the live exposure | `u8`/`u16`/`u32` reject out-of-range |
83
+
| Session key (and the salt/bind-auth that derive it) sat in GC-managed strings for the session lifetime | wipeable `Secret` + `Session.destroy` |
84
+
| `Quote.verify` had no real-signature test; risk of replay / structure confusion regressions | end-to-end ECDSA test (valid quote accepted; replay, validly-signed non-quote, tamper, wrong-AK rejected) |
85
+
| Quote previously checked only the signature, not magic/type/nonce | check magic + type + nonce before the signature |
86
+
| CFB parameter encryption keyed by `sessionKey` alone | key by `sessionKey || authValue` |
87
+
| Weak/short nonces accepted | reject `< 16` octets on caller and TPM nonces |
88
+
89
+
## Independent audit
90
+
91
+
A separate adversarial reviewer was tasked to find exploitable bugs in the
92
+
current tree (integer/length overflow, false-accept paths, crypto-check
93
+
ordering, resource exhaustion, secret leaks), with instructions not to invent
94
+
findings. It traced every untrusted byte through every decoder and returned
95
+
**no real findings**, confirming the bounds arithmetic, the no-false-accept
96
+
property of `Quote.verify` and the response-HMAC path, and the fail-closed
97
+
behaviour of the structure walks.
98
+
99
+
## Residual limitations (read before deploying)
100
+
101
+
- **Transient secret copies are not scrubbed.** `Secret.destroy` wipes the
102
+
long-lived buffers (session key, salt, bind-auth), but the short-lived copies
103
+
a hash or a string concatenation makes internally are left to the GC, and
104
+
OCaml's moving collector may leave stale copies. A deployment needing hard
105
+
guarantees should run in a process whose memory is itself protected/locked.
106
+
- **Decoders fail loud, not soft.** Malformed input raises
107
+
(`Wire.Parse_error` / `Invalid_argument` / `Failure`) rather than returning a
108
+
`result`. This is intentional and fail-closed (no wrong value is ever
109
+
accepted), but a caller embedding this in a critical process must wrap TPM
110
+
I/O in exception handling so a hostile/desynchronised peer cannot crash it.
111
+
- **Scheme coverage.** `Public.ecc_point` parses the schemes this client uses
112
+
(ECDSA, NULL). A TPMT_PUBLIC using ECDAA (which carries an extra count field)
113
+
would misparse — but fail-closed to `None`/`false`, never a wrong accepted
114
+
point.
115
+
- **Crypto primitives are trusted.** Side-channel resistance of the AES/SHA/
116
+
P-256 implementations in `digestif`/`nox-crypto`/`nox-crypto-ec` is their
117
+
responsibility, not audited here. Elliptic-curve point validation (rejecting
118
+
off-curve keys) is delegated to `nox-crypto-ec`.
119
+
120
+
## Evidence
121
+
122
+
- `dune test ocaml-tpm` — 40 unit tests (spec-anchored vectors, the CVE
123
+
regressions, the end-to-end quote verify), 2 eio transport tests, 2 go-tpm
124
+
cross-implementation interop tests.
125
+
- `dune exec ocaml-tpm/fuzz/fuzz.exe` — 5 fuzz properties (decoders never crash
126
+
on hostile bytes; `Quote.verify` never false-accepts; encode/decode
127
+
round-trips; RC decoding total).
128
+
- `dune exec ocaml-tpm/eio/test/*_smoke.exe` — live verification against swtpm
129
+
(seal/unseal, PCR-policy sealing, salted sessions, parameter encryption, NV
130
+
counter, quote).
131
+
- `dune exec -- merlint ocaml-tpm` — 0 issues.
132
+
133
+
## Deployment recommendation
134
+
135
+
The code meets a thorough automated adversarial bar. Before production
136
+
deployment, an independent human security review is recommended — this packet
137
+
exists to make that review fast. Run the live `*_smoke` executables against the
138
+
target TPM (or swtpm) as an acceptance gate.