Security & limits
Every limit, beside the capability it bounds.
One of byom's own safety invariants is about documentation: security claims name their actual profile, and same-UID developer mode is never described as confinement, credential separation or complete egress control. This page is that invariant applied to this site. Byom is v0.0.1, pre-release, not audited and not production-ready.
The assurance profile is developer
Channel authentication is same-UID SO_PEERCRED possession plus
process-bound channel proofs. There is
no UID separation between principals,
no attested process identity,
no mutual-TLS workload identity and
no asymmetric endpoint identity. A same-UID process can read the store
root key out of the SQLite file. No confinement is claimed.
This is not a gap that better hygiene closes; it is the profile the code implements, and every capability on this site should be read through it. In particular: the surfaces are separated by socket, and that separation is meaningful against confusion and against a misdirected client. It is not meaningful against a hostile process running as the same user, which can open any of the sockets and read the store directly.
The workload and candidate channel tokens are byomd-minted under the store root and
published 0600 in the daemon's own channels directory beside its
store. They are sender-constrained — each
binds the exact record whose authority it carries — which is what makes a stolen token
useless for anything other than the one thing it was for. It is not what makes it
unstealable.
What is closed
The developer profile still closes a real class of failure, and it is worth naming precisely so that the honest limits above are not read as "nothing works".
A copied credential file mints nothing
Channel proofs are process-bound. A credential file that is copied, backed up or transmitted does not become authority somewhere else — the exported-secret class is closed even though the same-UID class is not.
Unaddressable, not unauthorized
The registry is the whole surface. An operation with no row for the surface it arrived on is refused before any handler sees it, and the MCP profiles are closed enums that cannot name a governance, runtime or admin operation at all.
A restored database reopens sealed
Authority mutations run a three-step protocol against a non-rollbackable external witness. A snapshot-restore adversary cannot resurrect withdrawn authority: the startup comparison finds the mismatch and the endpoint opens sealed and diagnostic, minting nothing.
Possession grants nothing
A reference, receipt, mandate, event or projection row is never a bearer capability. Every use rechecks its current dependencies, so a held reference to a revoked mandate buys exactly nothing.
Byom does not sign its consumption receipt
The execution consumption receipt carries a portable_public binding
digest — an unkeyed SHA-256 anyone can recompute — and no signature. A
peer therefore cannot cryptographically verify consumption provenance.
It can check that the receipt's bytes are self-consistent and that they re-derive to the
published binding; it cannot check that byom issued them.
Byom's only signing primitive is a keyed MAC under the store root. That is enough for host-integration result envelopes, which this endpoint or a same-UID holder of its store verifies. It is not enough for a third party, and third-party-verifiable signing needs asymmetric endpoint identity, which the developer profile does not have.
The consequence is concrete and is carried on the counterparty's books, not hidden: the broker relying on that receipt holds an authority residual. This is deferred, not solved. Nothing on this site should be read as saying otherwise.
The models are not connected to the code
No test in crates/ reads a descriptor or a TLA+ model at
all. The Rust tests read the schemas, the vectors, the registry and the MCP
document; they never read spec/descriptors/ or proof/specs/.
The conformance oracle that would tie the daemon's transition functions to the committed
relations was expected to land with the daemon; the daemon landed and the oracle did
not. A daemon transition can therefore diverge from its committed descriptor row without
any gate in this repository noticing.
The decision record that requires the oracle carries an erratum saying so, and the proof
properties document records it as its largest open item. It also names a
cargo test invocation against a crate that has never existed in this
workspace — a second, smaller correction of fact from the same sweep.
The full statement, and which layers do and do not substitute for
it →
The governed-loop gate is partial
The end-to-end governed-loop gate runs two real daemons and drives a complete hosted turn. Of its 13 plan items, 5 are exercised with nothing standing in and 8 are explicitly simulated.
The verdict is not an annotation someone maintains. The gate derives it from probes over the daemons' own records and over the counterparty's source tree, so a stand-in cannot be quietly re-labelled as real — and an item stops being simulated on its own the day the missing subsystem ships.
Byom mints only attached_harness manifestation revisions. The "hosted
manifestation" in that gate is the reference kovee selects at placement and byom
commits on the episode and the placement admission — not a byom
host_kind row. The activation pipeline, the dual fences and the
cross-manifestation continuation resume are genuinely exercised; the distinct hosted
manifestation is not.
The other simulated items are of the same shape: an attention trigger whose deciding subsystem is a stub in the counterparty's pinned tree, the two attached execution paths, the completing model dispatch inside the counterparty's own worker socket, the ambiguous effect disposition, and the one-shot onboarding compute path. In each case the byom-side record is real and asserted from byom's own rows; what is standing in is the trigger or the far end.
Why ./run-checks.sh ends at exit 2
Running every check on this tree ends at exit 2, and that is the designed outcome rather than a failure to fix. Every suite before the last one is green. The last stage reports a skip for its two real-harness cells — they need external CLIs on the path — and it refuses to score a skip as a pass, so the script stops before printing its success line.
| Exit | Meaning |
|---|---|
0 | Everything ran, including the real harnesses. Needs the harness environment variable set and the external CLIs available. |
1 | A real failure. Something that ran did not pass. |
2 | Everything that ran passed, and something was skipped. On a default checkout this is what you get. |
A skip that scores as a pass is how a suite quietly stops testing anything. Byom's own gate has been narrowed once already for exactly that reason: an earlier default ran fewer cells than its own claim described, and the fix was to widen the default rather than to soften the claim.
Two open namespace gates
| Gate | State |
|---|---|
Schema $id namespace |
Every published schema uses the provisional reserved name
byom.example. Convention requires a project-controlled HTTPS namespace
before a stable release, and rewriting happens in one place when that gate is met.
No stable release may ship on byom.example. |
Problem type namespace |
The ratified profile pins problem types at
https://byom.dev/problems/<kind>, and the schemas, vectors and
runner enforce that prefix. Control of that namespace is
not yet established. It is recorded as an open fact, tracked to
closure — domain control demonstrated, or the profile amended — before any public
advertisement of the protocol. |
These are distinct: schema identifiers stay on the reserved example name, while problem types already carry the profile-pinned prefix on the wire.
Coverage boundaries worth knowing
- The descriptor-ownership rule ranges over the frozen sheet only. The mutating operations added by the later host-integration, runtime and acts bundles are registry-checked and schema-checked, and are not yet inside the one-descriptor-per-operation gate.
-
Ten registered operations are not implemented. They answer a typed
feature_unavailable, which includes the deny, cancel and expiry branches of the act-intent machine. The list → - No liveness is proved anywhere. Every checked property is safety, and no specification assumes fairness. "Eventually" is not a word this system's proofs support. Why →
- Model checking is bounded. Exhaustive at fixed constants is not proved for arbitrary run length; two invariants are flagged as inductive-proof candidates precisely because their bounds bite.
- Cryptographic soundness is assumed, not checked. Signatures, digests and witnesses are modeled as perfect; timing and side channels are not modeled at all.
- Two cross-boundary digest fields are recorded rather than fixed. Two optional counterparty-owned pairs would move under the cross-boundary class rule, fell outside the ratified decision, and are recorded for the contract owner rather than re-classed unilaterally. Detail →
The limits, in one table
| Limit | What it bounds | Status |
|---|---|---|
| Developer assurance profile | No UID separation, no attested process identity, no asymmetric endpoint identity, no confinement. | By design at this stage |
| Unsigned consumption receipt | A peer cannot cryptographically verify consumption provenance; the counterparty carries an authority residual. | Deferred, not solved |
| No model-to-code oracle | Nothing detects a daemon transition diverging from its committed descriptor row. | Largest open item |
| Governed-loop gate is partial | 5 of 13 items exercised, 8 simulated; only attached manifestations are minted. | Machine-derived each run |
| Bounded model checking | Exhaustive at fixed constants; no inductive proof, no liveness, no fairness. | Two induction candidates flagged |
| Descriptor gate scope | The one-to-one ownership rule covers the frozen sheet, not the later bundles' mutating rows. | Recorded in the spec |
| Namespace gates | Schema identifiers on a reserved example name; the problem-type namespace not yet controlled. | Blocks a stable release |
| Pre-release | v0.0.1, not audited, not production-ready, no compatibility claim. | Current |