391 lines
35 KiB
Markdown
391 lines
35 KiB
Markdown
# Device identity
|
||
|
||
What a machine is, said by a chain of signed statements that anyone checks offline: who made it, which firmware it runs, who owns
|
||
it, what it may do, whether it is still in service, and what it says about itself right now. Every link is signed with a
|
||
post-quantum signature and bound to the link before it. One verifier judges the whole chain, names every rule that refused, and
|
||
says VALID, PARTIAL or INVALID.
|
||
|
||
Node.js 24 only (`node:crypto`: Ed25519 and ML-DSA-65, FIPS 204), no dependencies. It imports the hybrid identities of
|
||
[`../identity`](../identity/) and, for the AIP-23 envelope, [`../proof-kinds`](../proof-kinds/). The two commands that touch a
|
||
chain (`notarize`, `reading`) use [`../agents`](../agents/) and the `ethers` package.
|
||
|
||
**Read this first.** The device key is a **software key**, and the verifier judges the chain it is **shown**. Nothing here binds
|
||
the key to hardware, and nothing says that the transfers shown are all the transfers there are. See
|
||
[What it is not](#what-it-is-not) before deciding what a VALID verdict is worth to you.
|
||
|
||
## The chain
|
||
|
||
| link | who signs | what it says |
|
||
|---|---|---|
|
||
| 1. manufacture | the manufacturer, a hybrid identity (Ed25519 + ML-DSA-65, both required) | a credential of type `DeviceManufacture`: this device key `K` (ML-DSA-65), this model, this serial. The device id is derived from `K` (`aere-device:` + the first 20 bytes of the SHA-256 of its SPKI). The credential can name a recall list of the manufacturer (an identity status list) |
|
||
| 2. firmware | the manufacturer | a release: model, version, a sequence number that only grows, the SHA-256 of the image, optionally the hash of a Proof of Software attestation of that image. And a short-lived **firmware policy**: the lowest sequence still allowed and the digests retracted |
|
||
| 3. ownership | each owner in turn | the manufacturer is the first owner. A **transfer** is signed by the owner before it and names the hash of the link before it (the manufacture credential, then the previous transfer). The current owner signs an **authorization**: the actions the device may ask for, a time window, the ownership head it was given under |
|
||
| 4. status | the manufacturer or the current owner | a registry of signed records: `active`, `suspended`, `retired`. The manufacturer's retirement is final. The owner's holds while the chain shown says it owns the device: see [Status](#status-whose-record-counts-and-for-how-long) |
|
||
| 5. attestation | the device, with `K` | a fresh statement: the verifier's nonce and audience, the device's clock, the digest and the sequence of the firmware it runs, the ownership head it knows, the action it asks for |
|
||
|
||
The attestation has an AIP-23 envelope (kind `device`) that commits to it by hash. That envelope can be notarized on Aere
|
||
Network; a verifier that reads it back through the AIP-23 reference verifier, under a post-quantum certified anchor, learns a time
|
||
at which the attestation already existed, written by the chain and chosen by nobody in this list. On the mainnet of today that
|
||
reading says the validators certified the block with post-quantum seals; the finality is the one of the chain it was notarized on.
|
||
|
||
Purposes are separated: a signature made for one kind of link (`firmware`, `firmware-policy`, `transfer`, `authorization`,
|
||
`status`, `attestation`) does not verify as another.
|
||
|
||
## The verdict
|
||
|
||
`verifyDevice(bundle, options)` makes **every check it can reach**: it does not stop at the first refusal. Each row of its answer
|
||
is `{ link, name, pass, detail, rule }`; a check that could not be made is `{ pass: null, unjudged: <cause> }`.
|
||
|
||
- **INVALID**: at least one rule refused. `rules` lists every rule that did, by name.
|
||
- **PARTIAL**: nothing refused, and something was not brought or not read. `unjudged` names each cause. A link missing from the
|
||
bundle, the verifier's own nonce or audience, the manufacturers it trusts, the recall list, a current firmware policy (or one
|
||
that is signed and cannot be read), a current status record (or one of the manufacturer or of the owner that cannot be read), a
|
||
status record of another manufacturer the verifier trusts, a Proof of Software attestation the release names, a notarization
|
||
the envelope claims and nobody read, a hardware root this verifier cannot judge, something handed to the verifier in another
|
||
shape than the one it reads or beyond the number of things it judges: each keeps the verdict from VALID.
|
||
- **VALID**: every link was brought and judged, and what could revoke it was read.
|
||
|
||
Four causes are **named and do not change the verdict** (the export `NOTATE`):
|
||
|
||
- `manufacture-status-none`: the manufacture credential names no recall list.
|
||
- `status-ignored`: a status record that is not applied because it is not a record of who may speak about this device now. That
|
||
is a record of a stranger; a record that is not signed, whose signature does not verify, or that stands under an id its keys
|
||
do not derive; a record of a previous owner whose device id is not a device id; the current owner's `active` under another
|
||
ownership head than the current one; an `active` whose time cannot be read.
|
||
- `status-prior-ownership`: the status records of a **previous** owner.
|
||
- `status-future`: a status record dated in the verifier's future.
|
||
|
||
Each has a row that says what was seen; `verify` prints them on a line of their own (`noted, the verdict stands: ...`). A VALID
|
||
verdict with `status-prior-ownership` beside it is not the same news as a plain VALID: read
|
||
[Status](#status-whose-record-counts-and-for-how-long).
|
||
|
||
The verifier judges on **its own clock** (`now`), with a tolerance of 60 seconds (`clockSkewS`, 0 to 600) given only to
|
||
beginnings (a validity that starts, a record that takes effect) and to a date written by a clock that runs fast, never to endings.
|
||
An ending includes its last instant; the edge of the tolerance is inside it. The attestation must be dated **no more than that
|
||
tolerance ahead** of the verifier's clock and **no more than `maxAgeS` (300 s) before it**: a date further ahead than the
|
||
tolerance is refused, also when it is well inside the allowed age.
|
||
|
||
A time is an RFC 3339 UTC text (`2026-10-05T12:00:00Z`, with up to three decimals of a second). A time without a zone, with a
|
||
zone offset, or one that is not a date is not a time. In a link of the bundle, the bundle cannot be read (`unreadable`). In a
|
||
firmware policy or a recall list handed to the verifier, that policy or list cannot be read (PARTIAL). In a status record, see
|
||
[Status](#status-whose-record-counts-and-for-how-long): a retirement or a suspension is applied all the same, an `active` is
|
||
not believed.
|
||
|
||
What the verifier brings, and what happens without it:
|
||
|
||
| option | without it |
|
||
|---|---|
|
||
| `nonce`, `audience` | PARTIAL: an old attestation, or one made for another verifier, would be accepted |
|
||
| `trustedManufacturers` (ids or public keys) | PARTIAL: anyone can issue a manufacture credential with their own keys |
|
||
| `statusLists` (the manufacturer's recall lists) | PARTIAL when the credential names a list: a recall that was not handed cannot be seen |
|
||
| `firmwarePolicies` | PARTIAL: a retracted or outdated firmware cannot be seen |
|
||
| `statusRecords` | PARTIAL: a suspension or a retirement cannot be seen |
|
||
| `softwareAttestation` | PARTIAL when the release names one |
|
||
| `anchors` (the verifier's readings of the notarized envelope) | PARTIAL when the envelope claims a notarization |
|
||
|
||
A configuration of the verifier that cannot be read (a clock that is not a time, a tolerance outside 0 to 600 seconds, a trusted
|
||
manufacturer that is neither an id nor a set of public keys, a list that is not a list) is not an invalid bundle: `verifyDevice`
|
||
throws an error that begins with `verifyDevice:`.
|
||
|
||
### What the verifier is handed: its shape, and how much of it is judged
|
||
|
||
`statusRecords`, `firmwarePolicies`, `statusLists` and `anchors` are flat lists of objects. An element that is not one (a list
|
||
inside the list, a registry object `{ records: [...] }`, a file of another kind, `null`) holds things that were **not read**. It is
|
||
not passed over: it is named with the cause of its kind (`status-unread`, `firmware-policy-unread`, `manufacture-status-unread`,
|
||
`witness-unread`) and the verdict is PARTIAL. The command line reads a file that holds a list, or `{ "records": [...] }`, element
|
||
by element, so a registry kept in one file is judged whole.
|
||
|
||
At most 512 status records, 64 firmware policies, 64 recall lists and 64 readings are judged (the exports
|
||
`MAX_STATUS_RECORDS`, `MAX_FIRMWARE_POLICIES`, `MAX_STATUS_LISTS`, `MAX_READINGS`). What lies beyond is not read, and the verdict
|
||
says so (PARTIAL, with the same causes): a padded registry cannot make the verifier work without end, nor push a retirement out
|
||
of sight in silence. Hand the verifier the records of the device it judges, not a whole registry.
|
||
|
||
### Rules that decide the hard cases
|
||
|
||
- **Firmware.** With several current policies of the manufacturer the strictest holds: the highest floor, and a digest retracted
|
||
by any of them stays retracted. A release below the floor is refused (`firmware-rollback`), a retracted one too
|
||
(`firmware-retracted`). The device must attest the digest and the sequence of the release shown (`attestation-firmware`).
|
||
A policy signed by the manufacturer for this model, not out of its validity, that **cannot be read** (a retracted entry that
|
||
is not `0x` and 64 hex digits, a floor that is not a whole number from 0 up, a validity that is not a time, a version this
|
||
verifier does not read) is not read as a policy that retracts nothing: the verdict is PARTIAL (`firmware-policy-unread`), also
|
||
when a clean policy stands beside it. What the readable policies refuse is still refused. An expired policy says nothing about
|
||
now. The same holds for a recall list of the manufacturer whose validity is not a time (`manufacture-status-unread`). A policy
|
||
or a list counts as the manufacturer's only when it names the manufacturer as its issuer **and** its signature verifies with
|
||
the manufacturer's keys.
|
||
- **Ownership.** A transfer counts only when signed by the owner at that point of the chain (`transfer-from`), and each transfer
|
||
is dated after the one before it. An authorization counts only when granted by the current owner of the chain shown, under its
|
||
ownership head (`authorization-owner`, `authorization-ownership`), and when it was in force both on the verifier's clock and
|
||
at the time the device attested (`authorization-window`). In the chain that is shown, a previous owner that still signs is
|
||
refused. The verifier cannot refuse an owner the chain does not show: see
|
||
[What it is not](#what-it-is-not), "It judges the chain it is shown".
|
||
- **Replay.** The attestation carries the verifier's nonce and audience and must be recent on the verifier's clock, and not
|
||
dated ahead of it (`nonce`, `audience`, `freshness`). With the verifier's reading of the notarized envelope, an attestation
|
||
dated after the moment its envelope was already on the chain is refused (`witness-time`); with several readings the earliest
|
||
is the bound. A reading is a time in whole seconds: one in milliseconds, or written as text, is not used, and the verdict is
|
||
PARTIAL (`witness-unread`).
|
||
- **Keys and signatures.** The device key must be a canonical ML-DSA-65 public key and the device id must be derived from it, in
|
||
the manufacture credential and in the attestation, and the two must be the same key (`device-key`, `device-id`,
|
||
`attestation-key`, `attestation-device`). An Ed25519 key in a field named ML-DSA-65 is refused. The hybrid signatures need
|
||
both halves, and each signature must declare its scheme. Every signature, like the device key, is accepted in **one text
|
||
only**, its canonical base64: the same bytes in another base64 text are refused.
|
||
- **The form of a link.** A link of the bundle is exactly `{ statement, signature }`, and a signature object exactly its members
|
||
(`alg`, `ed25519`, `mldsa65`; for the device `alg`, `value`). One member more, beside the statement or inside the signature,
|
||
is refused by the signature rule of that link (`manufacture-signature`, `firmware-signature`, `transfer-signature`,
|
||
`authorization-signature`, `attestation-signature`). The hash of a link covers the whole object and only the statement is
|
||
under the signature: without this rule anybody could give one signed statement another text, and so another hash. With it a
|
||
link has one hash. A status record and a firmware policy are named by no hash; their signature object is held to the same
|
||
form, and a member more beside their statement and their signature is not looked at.
|
||
|
||
### Status: whose record counts, and for how long
|
||
|
||
- **The manufacturer.** Its records always count, whatever ownership head they name. **The manufacturer's retirement is
|
||
final**: no later record lifts it, its own included, and no sale does. When both the manufacturer and the owner retired the
|
||
device, the row names the manufacturer's.
|
||
- **The current owner.** Its `retired` and its `suspended` count under any ownership head, and under none: the owner of now can
|
||
only harm itself by signing one, so the head written in the record is not a condition. Its `active` counts only under the
|
||
current ownership head. **The owner's retirement holds while the chain shown says it owns the device**: its own later
|
||
`active` does not lift it, and it stops binding in a chain that shows a transfer to another identity.
|
||
- **Bought back.** An owner that sold the device and owns it again is the current owner again. Every `retired` and `suspended`
|
||
record it ever signed, under any ownership head, counts again: its old retirement comes back with the device. Nothing it signs
|
||
lifts that retirement; only a transfer to another identity does.
|
||
- **A previous owner.** A transfer starts a new ownership, and the records of the owner before **do not bind** the owner of
|
||
now. The reason is the seller and the date: a seller can sign a retirement **after** the sale and date it before the sale,
|
||
and nothing in a signed record says when it was really signed. If such a record were binding, anyone who once owned a device
|
||
could disable it for ever. So it is not applied. It is also **not silent**: each previous owner whose records are in the
|
||
registry gets one row with the cause `status-prior-ownership` and the number of its records, `subject.priorOwnership` lists
|
||
what the records of each previous owner say (`retired` if any says so, else the state of its highest record), and `verify`
|
||
prints it. The verdict stands; a relying party that wants to refuse a device a previous owner retired reads that field and
|
||
decides.
|
||
- **What this means, plainly.** An owner **cannot retire a device for good**. It can retire it for as long as the chain shown
|
||
says it owns it; whoever it transfers the device to, another identity of its own included, starts a new ownership in which
|
||
the earlier retirement is named and not applied. And a chain can be shown shorter than it is, which makes the retirement of
|
||
the real owner of now a stranger's record (see [What it is not](#what-it-is-not)). A definitive retirement by the owner (a
|
||
"kill switch" that survives a sale) needs a **witness**: of time, for the retirement and the transfer, and of the ownership
|
||
head. **That is not built here.** Until it is, the only definitive retirement is the manufacturer's.
|
||
- **Which device a record is about.** The device id in a record is compared like a digest: its hex in upper case is the same
|
||
id. A record that names another device is not about this one. A record whose device id is **not a device id at all** (a space
|
||
after it, a number, a list) may have been meant for this device: when the manufacturer or the current owner signed it, the
|
||
registry is not read as clean and the verdict is PARTIAL (`status-unread`); from anybody else it is ignored, and named.
|
||
- **Another manufacturer the verifier trusts.** One device key can be certified by two manufacturers. A status record validly
|
||
signed by a manufacturer the verifier trusts, other than the one of the credential shown, is **not applied** (a manufacturer
|
||
does not retire the devices of another) and **not passed over** either: this verifier cannot judge by what right that
|
||
manufacturer speaks about this key, so the verdict is PARTIAL (`status-other-manufacturer`). The same record from a
|
||
manufacturer the verifier does not trust, or under a trusted manufacturer's id with keys that do not derive it, is a stranger's
|
||
record.
|
||
- **Anybody else.** See `status-ignored` above: ignored, and named.
|
||
- **Suspension, active, time.** A suspension is lifted only by a later record of the signer that suspended, and it does not
|
||
expire with its record. Of the records of one signer the one with the highest number holds, wherever it stands in the list;
|
||
of two with one number, the stricter. `active` is believed only while its record is current. A record dated more than the
|
||
tolerance ahead of the verifier's clock is not in effect yet: it is not applied, and it is named (`status-future`). A
|
||
retirement or a suspension by who may give it is applied even when its date cannot be read; an `active` with such a date is
|
||
not believed.
|
||
- **A record this verifier cannot read.** A record signed by the manufacturer or by the current owner in a version, with a
|
||
state or with a number this verifier does not read may be a retirement: the registry is not read as clean, and the verdict
|
||
is PARTIAL (`status-unread`), whatever the other records say.
|
||
|
||
The producer `statusRecord` has no default for whose record it writes: the manufacturer signs with `manufacture` (its own
|
||
manufacture credential of the device) and names no ownership head; anybody else must name the ownership head it signs under.
|
||
|
||
The 47 rules are the export `REGULI` of `device.mjs`; each check carries a marker with its rule id. The conformance suite
|
||
([`../conformance`](../conformance/)) maps each to a public id (`device.<rule>`), a level and a sentence.
|
||
|
||
## Use
|
||
|
||
```sh
|
||
node device-cli.mjs new-identity --out maker.keys.json # the manufacturer (key files are written 0600)
|
||
node device-cli.mjs new-identity --out owner.keys.json
|
||
node device-cli.mjs new-device --out device.key.json # the device key K
|
||
|
||
node device-cli.mjs manufacture --manufacturer maker.keys.json --device device.key.json \
|
||
--model AX-200 --serial SN-7 --days 3650 --out manufacture.json
|
||
node device-cli.mjs release --signer maker.keys.json --model AX-200 --version 2.0.0 --sequence 2 \
|
||
--image firmware.bin --out firmware.json
|
||
node device-cli.mjs policy --manufacturer maker.keys.json --model AX-200 --min-sequence 2 --hours 24 --out policy.json
|
||
node device-cli.mjs transfer --from maker.keys.json --to owner.keys.json --manufacture manufacture.json --out t1.json
|
||
node device-cli.mjs authorize --owner owner.keys.json --manufacture manufacture.json --transfer t1.json \
|
||
--action telemetry.publish --hours 24 --out authorization.json
|
||
node device-cli.mjs status --by owner.keys.json --manufacture manufacture.json --transfer t1.json \
|
||
--state active --seq 1 --hours 24 --out status.json
|
||
|
||
# the verifier sends a nonce; the device answers
|
||
node device-cli.mjs attest --device device.key.json --nonce n-123 --audience https://gateway.example \
|
||
--firmware firmware.json --manufacture manufacture.json --transfer t1.json --action telemetry.publish --out attestation.json
|
||
node device-cli.mjs bundle --manufacture manufacture.json --firmware firmware.json --transfer t1.json \
|
||
--authorization authorization.json --attestation attestation.json --out bundle.json
|
||
|
||
# the verifier
|
||
node device-cli.mjs verify --bundle bundle.json --nonce n-123 --audience https://gateway.example \
|
||
--trust <manufacturer id> --policy policy.json --status status.json
|
||
```
|
||
|
||
`verify` prints every row and the verdict (`--json` for the whole answer). What is named without changing the verdict is printed
|
||
on a line of its own (`noted, the verdict stands: ...`), and so is what the status records of a previous owner say. `--to`
|
||
takes a keys file, or a file with only the public keys of the new owner.
|
||
|
||
**Exit codes.** For `verify`, 0 is VALID, 1 is INVALID and 2 is PARTIAL, and these three numbers mean nothing else. 3: no
|
||
verdict was reached, because the usage is wrong or an input cannot be read (a file that is missing or is not JSON, a clock that
|
||
is not a time, a trusted manufacturer that is neither an id nor keys). 4: an unexpected failure of `verify`. The other commands
|
||
exit 0 when done, 1 when they failed, 2 when not measured (`notarize`, `reading`), and 3 for wrong usage or an input that cannot
|
||
be read.
|
||
|
||
**Files that hold several things.** A file given to `--status`, `--policy`, `--status-list` or `--reading` holds one object, a
|
||
JSON list of them, or `{ "records": [...] }`; every element is handed to the verifier. An object of another form is handed as it
|
||
is, and the verifier names it (PARTIAL).
|
||
|
||
**What is printed.** Everything `verify` prints that came from a file (a model, an id, a date) passes through one function,
|
||
`visible()`, exported by `device.mjs`: the C0 and C1 control characters, DEL, the Unicode line and paragraph separators, the
|
||
bidirectional controls and the byte order mark are printed in a visible form (`\x1b`, `
`), and a backslash is doubled so
|
||
that the form cannot be forged. A terminal executes nothing a bundle wrote, and a bundle cannot draw a second verdict line.
|
||
`--json` prints JSON, whose strings escape control characters; its rows carry the text exactly as it came, so a program that
|
||
shows them to a person passes them through `visible()` itself.
|
||
|
||
`status` writes the record of whoever signs it: with the manufacturer's keys, a record of the manufacturer (no ownership head);
|
||
with any other keys, a record under the ownership head of the chain given (`--manufacture` and every `--transfer`, in order).
|
||
Give the whole chain: a record signed under an older head is still the owner's when it says `retired` or `suspended`, and is
|
||
not believed when it says `active`.
|
||
|
||
With the chain as witness:
|
||
|
||
```sh
|
||
node device-cli.mjs envelope --attestation attestation.json --out envelope.json
|
||
node device-cli.mjs notarize --envelope envelope.json --rpc <endpoint> --key-file <funded key> --out notarized.json
|
||
node device-cli.mjs reading --envelope notarized.json --rpc <endpoint> --chain 28001 \
|
||
--verify-proof <verify-proof.mjs> --out reading.json # made by the VERIFIER
|
||
node device-cli.mjs bundle ... --anchor notarized.json --out bundle.json
|
||
node device-cli.mjs verify --bundle bundle.json ... --reading reading.json
|
||
```
|
||
|
||
`notarize` refuses chain 2800 unless `AERE_CONFIRM_MAINNET=yes`: there it is a real transaction paid by the key's account.
|
||
`reading` needs the AIP-23 reference verifier published at aere.network/tools: `verify-proof.mjs` with the five files beside it
|
||
(`verify-anchor.mjs`, `mpt.mjs`, `falcon512.mjs`, `registry-v3.mjs`, `package.json`) and `npm install` done there. A reading
|
||
handed over by the party being verified proves nothing: it would be that party's own statement.
|
||
|
||
As a module:
|
||
|
||
```js
|
||
import * as D from './device.mjs';
|
||
const r = D.verifyDevice(bundle, { now, nonce, audience, trustedManufacturers: [id], statusLists, firmwarePolicies, statusRecords, anchors });
|
||
// r.verdict, r.rules, r.unjudged, r.links, r.rows, r.subject
|
||
```
|
||
|
||
`r.subject` (device id, model, serial, manufacturer, owner, firmware, action, state, `priorOwnership`: what the status records
|
||
of each previous owner say and how many they are, and the witness reading used, with the chain the verifier says it read) is
|
||
returned only when no rule refused. The rows carry text as the bundle wrote it: show them to a person through `D.visible()`.
|
||
|
||
## What it is not
|
||
|
||
- **It is not a hardware root of trust.** `K` is generated and held in software. Whoever can read the device's storage can copy
|
||
`K`; the copy is indistinguishable from the device. A compromised device signs whatever it is told, including the digest of a
|
||
firmware it does not run: the attestation says what the holder of `K` **claims** to run, not what was measured at boot. No TPM,
|
||
no secure element, no TEE is used or checked anywhere in this module.
|
||
- **What a hardware root would add, and where it would bind.** (1) An endorsement that `K` was generated inside a specific chip
|
||
and cannot leave it: it would sit in the field `hardwareRoot` of the manufacture claims, beside `deviceKey`. (2) A quote, signed
|
||
by that chip, over the measurements of the boot chain and the verifier's nonce: it would sit in the field `hardwareRoot` of
|
||
the attestation, beside `firmware`. Both fields exist, are `null` in everything this module produces, and are **not used**:
|
||
a value in either is reported as not judged (`hardware-root`) and the verdict is PARTIAL. Nothing here verifies an endorsement
|
||
certificate or a quote.
|
||
- **It judges the chain it is shown, and a chain can be shown shorter than it is.** Nothing in a bundle says that the transfers
|
||
shown are all the transfers there are. Whoever holds `K` (a software key, which can be copied) and the documents of an earlier
|
||
time (the manufacture credential, the earlier transfers, an authorization and an `active` record that are still current) can
|
||
show a chain that **stops before the last sale**. In that chain the earlier owner is the current owner: its authorization
|
||
counts, its records count, and a retirement signed by the real owner of now is a stranger's record, named `status-ignored` and
|
||
not applied. The verdict is VALID. Rows K05 and K06 of the probe measure this, for a chain shown one transfer short and for
|
||
one shown with no transfer at all. What holds against a chain shown shorter: the manufacturer's retirement, the manufacturer's
|
||
recall list, the firmware policy, and the endings of the documents used (an authorization and an `active` record expire, which
|
||
is why they should be short-lived). **The only retirement that holds against a shortened chain is the manufacturer's.**
|
||
Closing this needs a witness of the **ownership head**: the head notarized at each transfer, and a verifier that reads the
|
||
latest. It is not built here.
|
||
- **No detection of a double sale by itself**, for the same reason: an owner that signs two different transfers at the same
|
||
position makes two valid chains, and a verifier shown one of them cannot know the other exists.
|
||
- **No definitive retirement by an owner.** The owner's retirement holds while the chain shown says it owns the device; a
|
||
transfer starts a new ownership, in which the earlier retirement is named and not applied (see
|
||
[Status](#status-whose-record-counts-and-for-how-long)). An owner that retires a device and then transfers it to another
|
||
identity of its own has a device that verifies again, with `status-prior-ownership` beside the verdict. Closing that needs a
|
||
witness of **when** the retirement and the transfer were signed (their notarization, read by the verifier). It is not built
|
||
here. The manufacturer's retirement is final.
|
||
- **Not a Proof of Software verifier.** When a release names a Proof of Software attestation, this verifier checks that the
|
||
attestation handed is the one named (by hash), that it is a Proof of Software attestation, and that it lists the image digest.
|
||
It does not verify the attestation's own signature, its builder credential or its SBOM: that is the job of the Proof of
|
||
Software verifier.
|
||
- **Not a statement about the real world.** It does not say who a manufacturer is; the verifier chooses whom it trusts
|
||
(`trustedManufacturers`). It does not say the serial number is printed on the device.
|
||
- **Not a registry service.** Recall lists, firmware policies and status records are files somebody publishes and the verifier
|
||
fetches. A record the verifier was not handed cannot be seen; the verifier is told when it read none (PARTIAL), not when one
|
||
was withheld among others it did read: a retirement left out of the records shown, beside a current `active` record, is not
|
||
noticed. A record or a policy damaged on the way (its signature no longer verifies, or is not in its canonical text) is no
|
||
longer a signed record: it is ignored like one that was withheld. Read the registry from who publishes it, not from the
|
||
device.
|
||
- **No time for the links but the one their signers wrote.** A transfer, an authorization and a status record carry the date
|
||
their signer chose. Only the attestation can be bounded by the chain today (its envelope, notarized and read back).
|
||
- **No key rotation or recovery** for `K` or for the identities. A device whose key is lost or copied is recalled by the
|
||
manufacturer (the recall list) or retired (a status record), and made again.
|
||
- **One signer for firmware.** A release must be signed by the manufacturer's own identity. Delegating release signing to a
|
||
separate key is not built.
|
||
- **Not a certification and not an audit.** No third party has reviewed this code.
|
||
|
||
## Not measured
|
||
|
||
- Any real device, any embedded implementation of the attestation, and the cost of an ML-DSA-65 signature on a constrained
|
||
processor.
|
||
- The chain as witness on Aere Network mainnet (2800): measured only on testnet 28001, where the finality is the testnet's.
|
||
- The chain as witness with the verifier as it is now, end to end: the run on testnet 28001 was made on 2026-10-05 before the
|
||
repairs of that day and of the next (see below). What was recorded then (the bundles, what the verifier brought, its two
|
||
readings) is judged again offline by the verifier of now in the probe (row D08) and gives the six verdicts recorded; nothing
|
||
was notarized or read on the chain again.
|
||
- A witness of time for transfers, authorizations and status records, and a witness of the ownership head: none is built.
|
||
- A second implementation of the verifier: the conformance suite's Python implementation covers none of the 47 rules.
|
||
- The key-file mode on Linux and macOS (the tests ran on Windows, where the mode is not enforced).
|
||
- A terminal: the row of the probe that measures what `verify` prints reads the BYTES of its output (no control byte but the
|
||
line feeds the command writes); no terminal emulator was driven.
|
||
- The conditions of the **producers** and of the key files (the functions that write links), one at a time. The search described
|
||
below covers the verifier and everything it calls. What a producer refuses to write is a convenience to its caller, not a
|
||
guarantee to a verifier, which must assume links written by other tools; rows D01 and D02 of the probe measure the refusals
|
||
this page names. @@INAFARA@@ conditions lie there.
|
||
- The conditions of `device-cli.mjs`, one at a time: the command line is covered by the plantings written by hand (the exit
|
||
codes, the list files, what is printed), not by the search.
|
||
- The kinds of change the search does not derive: a constant changed, an arithmetic operator changed, a statement removed, two
|
||
conditions changed together.
|
||
|
||
## How it is checked
|
||
|
||
| what | command | measured |
|
||
|---|---|---|
|
||
| the probe | `AERE_VERIFY_PROOF=<verify-proof.mjs> node proba-device.mjs` | @@PROBA@@ |
|
||
| the negative control | `node control-negativ-device.mjs` | @@CONTROL@@ |
|
||
| the search for conditions without a row | `AERE_ACORN=<directory of the acorn parser> node mutanti-device.mjs` | @@MUTANTI@@ |
|
||
| the chain as witness | `AERE_TESTNET_KEY_FILE=<funded testnet key> AERE_VERIFY_PROOF=<verify-proof.mjs> node proba-device-ancora-testnet.mjs` | 10/10 on testnet 28001 on 2026-10-05, with the verifier as it was before the repairs of that day: two envelopes notarized (two transactions), both read back by the published reference verifier under a post-quantum certified anchor (after 17 s and 16 s); the honest bundle VALID with the reading and PARTIAL without it; an attestation the device dated twenty minutes ahead, judged on a clock set to the time it claims, passes without the chain and is refused with the reading (`witness-time`); the envelope of another attestation and the reading of another envelope do not witness. Evidence in `dovezi-ancora-28001/`. Not run again after the repairs: the recorded bundles and readings give the same six verdicts under the verifier of now (row D08 of the probe, offline) |
|
||
| the conformance suite | `node ../conformance/proba-conformance.mjs` | @@SUITA@@ |
|
||
|
||
An attack row of the probe requires the verdict INVALID **and the exact set of rules that refused**: refused for another reason is
|
||
a red row. A row that must be PARTIAL requires the exact set of causes. Three things check that the rows can go red.
|
||
|
||
1. **Each rule taken out whole.** The negative control takes each of the 47 rules out of a copy, one at a time, and requires
|
||
that the rows which expect that rule, and only they, go red.
|
||
2. **Plantings written by hand** (`plantari-device.mjs`), each with its rows named beside it, and exactly those rows must go
|
||
red. They are the defects of behaviour (no purpose separation, one half of a hybrid signature accepted, a retirement lifted,
|
||
a previous owner's record applied or passed in silence, the last record in the list holding instead of the highest, the
|
||
loosest policy holding, something handed in another shape dropped in silence, text printed as it came, an input that cannot
|
||
be read exiting like a verdict) and the conditions that a search by mutation does not derive: a tolerance **given** to an
|
||
ending, an order turned round, and two checks that guard one thing taken out together (where either alone holds, a single
|
||
planting shows nothing, and the planting says so). A planting whose pattern is not found exactly once, or after which the
|
||
probe does not reach its summary, counts as a failure of the control.
|
||
3. **A search derived from the code** (`mutanti-device.mjs`). A list written by hand stays behind the code, so the conditions
|
||
of the verifier, one at a time, are not listed: a parser derives them. Each side of every `&&` and `||`, every `===` and
|
||
`!==` made always true and always false, every `<`, `<=`, `>`, `>=` moved by its edge and made always true, every clock
|
||
tolerance removed, and every yes-or-no call made to answer yes and to answer no. The probe runs on each; a mutant that leaves
|
||
every row green is a condition without a row. The form checks are searched like the rest: each field a link must have is a
|
||
row (section R of the probe: the field replaced by values of the wrong form and the link signed again by its signer), each
|
||
edge of an interval is a row (section T). Survivors are allowed only when declared in the tool with the reason no row can
|
||
see them; the run fails on an undeclared survivor and on a declaration that names none.
|
||
|
||
What the search does not cover is listed under [Not measured](#not-measured). It needs the `acorn` parser, which is not a
|
||
dependency of the verifier and is not shipped here; without it the search reports NEMASURAT and measures nothing.
|
||
|
||
`fixturi/firmware-2.0.0.bin` is a made-up image. `fixturi/atestare-firmware.json` is a probe fixture: a Proof of Software
|
||
attestation of that image, written by the Proof of Software tool outside any source repository (its `source` is null), with a
|
||
key made for it and discarded. Every other key is made at the start of a run and discarded at its end.
|
||
`dovezi-ancora-28001/` holds the evidence of the testnet run: no private key is in it.
|
||
|
||
Code comments are in English; a few internal names are Romanian (`REGULI` rules, `NEJUDECATE` not judged, `PARTIALE`,
|
||
`OPRIRI` stops, `PAZA` guard, `ECHIVALENTI` equivalents, `PRODUCATORI` producers).
|