aere-network/aere-quantum
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
main
aere-quantum/device-identity/README.md

432 lines
40 KiB
Markdown
Raw Permalink Blame History

# 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.
**PARTIAL is not a weaker VALID.** Whoever hands the bundle chooses which links it brings. A link left out turns every refusal
that link would have drawn into its `-missing` cause: a device the manufacturer retired, an authorization a stranger signed, an
attestation to an old nonce are each INVALID, and each is PARTIAL with the refused link left out (row W08 of the probe). It is
never VALID that way, and what can still be judged without the link is judged: with the release left out, the firmware the device
attests is judged against the policies all the same (rows W01 to W07). Admit on `verdict === 'VALID'`, or on a PARTIAL whose causes
are exactly the ones you chose not to bring. The field `valid` is `true` when no rule refused, PARTIAL included: it is not a
verdict.
Every cause, by the name `unjudged` gives it:
| cause | what was not brought or not read | verdict |
|---|---|---|
| `manufacture-missing`, `firmware-missing`, `authorization-missing`, `attestation-missing` | that link of the bundle | PARTIAL |
| `ownership-unrooted` | transfers shown without the manufacture credential they start from | PARTIAL |
| `manufacturer-trust` | the manufacturers the verifier trusts | PARTIAL |
| `manufacture-status-unread` | the recall list the credential names (none current, one that cannot be read, or something handed in its place) | PARTIAL |
| `firmware-policy-unread` | a current firmware policy that can be read | PARTIAL |
| `software-unread` | the Proof of Software attestation the release names | PARTIAL |
| `status-unread` | a status record that can be applied, or a record of the manufacturer or of the current owner that cannot be read | PARTIAL |
| `status-other-manufacturer` | a record of another manufacturer the verifier trusts (not applied, and not judged) | PARTIAL |
| `nonce`, `audience` | the verifier's own nonce, its own audience | PARTIAL |
| `hardware-root` | a hardware root carried by the credential or the attestation (never judged here) | PARTIAL |
| `witness-unread` | a reading of the notarization the envelope claims, or a reading that cannot be read | PARTIAL |
| `manufacture-status-none`, `status-ignored`, `status-prior-ownership`, `status-future` | see below | named, VALID stands |
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, and a day that does not exist is not a date: a date parser moves
`2026-02-30` to March 2 and `T24:00:00` to the next day, and this verifier refuses both. In a time a link of the bundle carries and
the verifier reads (the validity of the manufacture credential and when it was issued, the date of a transfer, the window of an
authorization, the date of the attestation), the bundle cannot be read (`unreadable`). The `issuedAt` of a release and of an
authorization are carried and not read: nothing is decided on them. 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:`. The clock `now` is a `Date`, a number of milliseconds since 1970, or an RFC 3339
UTC text, and nothing else: a text without a zone (which a date parser reads as local time), `"1"` (which it reads as the year
2001), a date alone, `null` or a list are not a clock.
### 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. **With the release left out** (`firmware-missing`), the firmware the device attests, its digest and its
sequence, is judged against the same policies of the manufacturer of the credential for its model: a retracted digest or a
sequence below the floor is refused all the same (`firmware-retracted`, `firmware-rollback`), and no current policy is said
(`firmware-policy-unread`). Leaving the release out keeps the verdict from VALID; it does not hide what the device itself says
it runs.
- **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`). The witness is offered by whoever hands the bundle: a bundle without an envelope is judged without
one (on the verifier's clock and nonce), and a reading handed for an envelope the bundle does not carry is not used.
- **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 of a link, of a status record and of a firmware
policy, like the device key, is accepted in **one text only**, its canonical base64: the same bytes in another base64 text are
refused. A recall list is an identity status list, judged by the identity verifier's signature check, which does not hold its
signature to one text; a list is named by no hash, so nothing depends on that text.
- **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 (a key file is created 0600, never written over)
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 (U+061C, U+200E, U+200F, U+202A to U+202E, U+2066 to U+2069: the characters Unicode gives the property
Bidi_Control) and the byte order mark are printed in a visible form (`\x1b`, `\u2028`), 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 through `visibleJson()`, also exported: JSON escapes C0, and every other character `visible()` replaces is written
as a `\u` escape, so the bytes printed hold no control character but the line feeds of the layout, and the text parses to
exactly the same value. 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, of the next and of 2026-10-14 (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. The search counts 164 mutants there and runs none of them.
- 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` | 372/372 on 2026-10-14 (Node 24.14.1, Windows): 54 bundles that must be VALID; 77 PARTIAL, each for exactly its named causes; 204 attack rows, each refused for exactly its named rules; 37 other rows (the command line through files and processes, the envelope under the reference verifier, the evidence recorded on testnet 28001 judged again offline, the rows of the third adversarial review); 804 damaged bundles each given a verdict |
| the negative control | `node control-negativ-device.mjs` | 220/220 on 2026-10-14: the untouched copy green; each of the 47 rules taken out, the rows that expect it and only they go red; 172 more plantings, each with exactly its rows |
| the search for conditions without a row | `AERE_ACORN=<directory of the acorn parser> node mutanti-device.mjs` | 892 mutants of the verifier on 2026-10-14 (acorn 8.16.0): 890 killed (36 of them because the probe could no longer build its world), 2 survive, both declared in the tool with the reason no row can see them (two assertions of the verifier about itself); 164 more lie in the producers and the key files and are not run. The run before row W14 found one condition without a row (the release judged only when it is left out), and W14 was written for it |
| 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` | 12/12 on 2026-10-14 with the AIP-23 verifier, Python 3 and testnet 28001 read (`--online`; nothing is sent): 181 rules of 11 verifiers, the published verifiers pass 467 of 467 vectors, 194 of them device bundles |
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).
Reference in New Issue View Git Blame Copy Permalink