Open Profile for DICE in OCaml: the CDI derivation of each boot layer, the CBOR or X.509 certificates a layer issues for the next one, the verification of a DICE chain, and the Android handover object that carries the CDIs and the chain from one boot stage to the next.

A Device Identifier Composition Engine (DICE) measures the next program before it runs and mixes the measurements into a secret only the current layer holds, the Compound Device Identifier (CDI). The first layer holds the Unique Device Secret (UDS) of the hardware instead. From each attestation CDI a key pair is derived, and each layer certifies the next layer's public key, with the measurements, in a CBOR Web Token signed as a COSE_Sign1 or in an X.509 certificate. A verifier walks the resulting chain back to the device's root key and reads every layer's measurements from it.

dice implements the Open Profile for DICE v2.6 and the CBOR side of its Android Profile:

Dice.Cdi: the attestation and sealing CDIs, held in Secret.t values that are never printed and that Cdi.destroy erases.
Dice.Key_pair and Dice.Public_key: the key pair of a layer, Ed25519 by default, ECDSA on P-256 or P-384, or ML-DSA-65 or ML-DSA-87, and the identifiers derived from public keys.
Dice.Certificate: CBOR and X.509 UDS and CDI certificates, issued byte for byte as the reference implementation, open-dice, writes them, and read back. The X.509 form carries the measurements in the profile's extension 1.3.6.1.4.1.11129.2.1.24.
Dice.Chain: DICE chains, a root public key and one certificate per layer, verified against an allowlist of signature algorithms that defaults to Ed25519. The certificates may mix the two forms; the CBOR encoding the Android Profile uses holds CBOR certificates.
Dice.Config: the Android Profile's configuration descriptor.
Dice.Handover: the Android DICE handover object, {1: CDI_Attest, 2: CDI_Seal, ? 3: DiceCertChain}, read and written as a Secret.t in the deterministic encoding of CBOR, and the boot stage that turns one handover into the next.

The derivations use SHA-512 and HKDF-SHA512, as the profile recommends. ECDSA signatures are deterministic (RFC 6979) and ML-DSA signatures use the deterministic variant of FIPS 204, where open-dice's are random, so an ECDSA or ML-DSA certificate matches open-dice's bytes everywhere but its signature. An ML-DSA public key is an AKP COSE_Key (RFC 9964).

Installation #

opam install dice

Usage #

The first layer derives its CDIs from the UDS, measures the next layer and issues its certificate. The UDS public key is the root of the chain, so the chain verifies from it.

# let uds =
    let s = Secret.v 32 in
    Secret.fill s '\x01';
    s;;
val uds : Secret.t = <abstr>
# let layer0 = Result.get_ok (Dice.Cdi.of_uds uds);;
val layer0 : Dice.Cdi.t = <abstr>
# let input =
    Result.get_ok
      (Dice.Input.v ~code_hash:(String.make 64 'c') ~mode:Dice.Mode.Normal ());;
val input : Dice.Input.t = <abstr>
# let layer1, cert = Dice.main_flow layer0 input;;
val layer1 : Dice.Cdi.t = <abstr>
val cert : Dice.Certificate.t = <abstr>
# let root = Dice.Key_pair.public_key (Dice.Key_pair.of_cdi layer0);;
val root : Dice.Public_key.t = <abstr>
# Dice.Cdi.destroy layer0;;
- : unit = ()
# let chain = Result.get_ok (Dice.Chain.v root [ cert ]);;
val chain : Dice.Chain.t = <abstr>
# Dice.Certificate.mode cert = Some Dice.Mode.Normal;;
- : bool = true
# String.equal (Dice.Certificate.issuer cert) (Dice.Public_key.id_hex root);;
- : bool = true

The next layer may certify its successor in X.509, and the chain mixes the two forms:

# let layer2, x509 = Dice.main_flow ~format:X509 layer1 input;;
val layer2 : Dice.Cdi.t = <abstr>
val x509 : Dice.Certificate.t = <abstr>
# Dice.Certificate.format x509;;
- : Dice.Certificate.format = Dice.Certificate.X509
# Result.is_ok (Dice.Chain.v root [ cert; x509 ]);;
- : bool = true

The CDIs print without their contents:

# Fmt.pr "%a@." Dice.Cdi.pp layer1;;
(cdi attest=<secret 32 bytes> seal=<secret 32 bytes>)
- : unit = ()

Under the Android Profile a stage hands the next its CDIs and the chain in a handover object. Dice.Handover.main_flow is one stage: it derives the next CDIs, certifies the next key and appends the certificate to the chain, which it starts from the stage's own public key when the handover has none. The encoded handover holds the CDIs, so it is a Secret.t too:

# let stage0 = Result.get_ok (Dice.Handover.v layer1);;
val stage0 : Dice.Handover.t = <abstr>
# let stage1 = Dice.Handover.main_flow stage0 input;;
val stage1 : Dice.Handover.t = <abstr>
# Fmt.pr "%a@." Dice.Handover.pp stage1;;
(handover (cdi attest=<secret 32 bytes> seal=<secret 32 bytes>)
 chain=<487 bytes>)
- : unit = ()
# let encoded = Dice.Handover.to_secret stage1;;
val encoded : Secret.t = <abstr>
# let received = Result.get_ok (Dice.Handover.of_secret encoded);;
val received : Dice.Handover.t = <abstr>
# Secret.destroy encoded; Dice.Handover.destroy stage0;;
- : unit = ()

Dice.Chain.of_string reads a chain from its CBOR encoding, and the dice command prints one, or, with --root, verifies certificate files of either form under a root COSE_Key:

$ dice chain --algorithm p256 valid_p256.chain
root: p256:1e7854194d6bc87c8c1ef36a53ce192c7aeba23d
certificate 0:
  issuer: Entity:0
  subject: Entity:1
  ...

dice handover reads a handover, prints its CDIs' sizes and never their contents, and verifies and prints its chain.

Testing #

The CDIs and certificates are checked against the known test values of open-dice (include/dice/known_test_values.h) for its three input sets: the CBOR certificates of its Ed25519, P-256, P-384, ML-DSA-65 and ML-DSA-87 configurations and the X.509 ones of its Ed25519, P-256, ML-DSA-65 and ML-DSA-87 configurations. The chain reader is checked against the DICE chain samples of AOSP's hwtrust, and the handover against the inputs of open-dice's handover tests (src/android_test.cc) and the CDIs and chain of AOSP's sample DICE inputs (libs/dice/sample_inputs), which three handover stages reproduce byte for byte. All are committed traces; REGEN=1 dune build @traces fetches them again at their pinned commits.

Not implemented #

The DRBG, OpenTitan and SP800-108 key derivation functions, and hashes other than SHA-512 for the CDI derivation.

open-dice, the reference implementation in C, which these derivations and certificates match.
hwtrust, AOSP's Rust tool for checking DICE chains.
tpm covers TPM 2.0 measured boot; DICE is the layered alternative for devices without a TPM.