carlos / platform Public

enginesim: calls, identity, grants and arming (#335 plan 1)

The signed engines record and the grant mirror (durable floor, stale,
expired and never-read tables empty), the call path (peer cgroup on the
engine socket, the door's uid rule, the hop caller signed into the MAC,
the engine box's own grant check on the exact route only), and armed
boxes (arm checks the box; unisolated launches refused while armed).

Invariants INV-G, INV-ID and INV-ARM; rules cgroup-identity, door-uid,
hop-caller-signed, engine-box-recheck, exact-route-engine,
floor-persisted, stale-clears-grants, armed-refuses-unisolated and
arm-checks-box, each with a witness and caught by the 200-seed sweep.
The three stated residuals (freshBoxReplay,
unwrittenManifestAcrossUpgrade, flatEraTamper) are flags, off by
default; with one on, its sequence is recorded as residual:<name>.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude agent, operated by paul@keymail.dev 3a2169f43ae1f64cb0a727a3b2a96c6bec25fd92 parent b2f3a42
10 files changed, +1344 −11
  • internal/sim/engines/calls_test.go +768 −0
  • internal/sim/engines/classify_test.go +26 −4
  • internal/sim/engines/dedicated_test.go +2 −2
  • internal/sim/engines/edge_test.go +2 −2
  • internal/sim/engines/invariants_test.go +89 −2
  • internal/sim/engines/launch_test.go +1 −0
  • internal/sim/engines/rules_test.go +12 −0
  • internal/sim/engines/sim_test.go +5 −0
  • internal/sim/engines/witness_test.go +395 −0
  • internal/sim/engines/world_test.go +44 −1
diff --git a/internal/sim/engines/calls_test.go b/internal/sim/engines/calls_test.go
new file mode 100644
index 000000000..8042d03af
--- /dev/null
+++ b/internal/sim/engines/calls_test.go
@@ -0,0 +1,768 @@
+package engines
+
+import (
+ "fmt"
+ "strings"
+)
+
+// Calls, identity, grants and arming (spec §5.2 the signed record; §5.3 the
+// grant mirror; §5.4 the call path; §6.1 identity; §6.2 armed boxes; §6.4
+// freshness).
+//
+// The console publishes the grant set as one signed record with a strictly
+// increasing revision and a 72-hour expiry; every edge mirrors it, keeps a
+// durable revision floor, and treats a stale, expired or never-read table as
+// empty. A nested instance calls an engine through its engine socket, which
+// is open only on an armed box; a host-app process calls through the door.
+// The calling box proves the caller (the peer's cgroup, or a door key from a
+// uid other than carlos), checks its own table and hops to the engine's home
+// box with the caller signed into the hop's MAC. The engine box checks its
+// own table again and dispatches to the engine hostname's own route only.
+//
+// The model leaves out the per-app cap, the transport limits and the deploy
+// watch ticket (Plan 2 tests those directly).
+
+// Time: one tick is 10 s.
+const (
+ pollTicks = 3 // the mirror polls every 30 s
+ staleTicks = 60 // no good read for ten minutes: stale
+ lifetimeTicks = 25920 // a record expires 72 hours after it is signed
+)
+
+// now is the model's clock: one tick per step, plus any fast-forward.
+func (w *world) now() int { return w.step + w.skew }
+
+// advance is time passing with no step: n ticks in which nothing polls (an
+// outage, a console down for days).
+func (w *world) advance(n int) {
+ w.skew += n
+ w.logf("%d ticks pass (now %d)", n, w.now())
+}
+
+// ---------- the console's record (spec §5.2) ----------
+
+// record is one signed control/engines.json: its revision, its expiry (in
+// ticks), and its grants by account/app/engine.
+type record struct {
+ Rev, Expires int
+ Grants map[string]bool
+}
+
+// mirror is an edge's grant mirror (§5.3): the record it holds, its revision
+// floor and the tick of its last good read, and what it has persisted to its
+// data directory (the record and the floor, written before either is used).
+type mirror struct {
+ Rec *record
+ Floor, ReadAt int
+ Persisted *record
+ PersistedFloor int
+}
+
+// engConsole is the console's side: its database (Grants, the authority),
+// every record it has signed, the newest revision, and the object in the
+// bucket. RevokedAt is the oracle's: the tick of the publish that stopped
+// granting a key. BucketDown: the edges cannot read the bucket.
+type engConsole struct {
+ Rev int
+ Records map[int]*record
+ Grants map[string]bool
+ RevokedAt map[string]int
+ Bucket *record
+ BucketDown bool
+}
+
+// The engines the operator has named (carlos engines add): name to its
+// hostname. eng's hostname is the engine group's minted row; site's is box
+// 0's static row, whose path map sends /convert to eng's route (R4-2: the
+// console cannot check a hostname, and path targets may cross apps).
+const site = "site"
+
+var engineHosts = map[string]string{eng: engHost, site: engSite}
+
+// callerOf is the caller account/app calling engine.
+func callerOf(app, engine string) caller {
+ acct, a, _ := strings.Cut(app, "/")
+ return caller{Account: acct, App: a, Engine: engine}
+}
+
+func (c caller) app() string { return c.Account + "/" + c.App }
+func (c caller) key() string { return c.app() + "/" + c.Engine }
+
+// initEngines is the starting world: the console's first record grants shop
+// the engine eng, and every edge has read it.
+func (w *world) initEngines() {
+ w.console = engConsole{Records: map[int]*record{}, Grants: map[string]bool{"acct/shop/eng": true}, RevokedAt: map[string]int{}}
+ w.publish(1)
+ for _, b := range w.boxes {
+ w.mirrorTick(b)
+ }
+}
+
+// publish is the console signing its grant set as revision rev, expiring 72
+// hours out, and writing it to the bucket. A revision is strictly increasing;
+// a re-sign with the same grants is a new revision.
+func (w *world) publish(rev int) {
+ c := &w.console
+ if rev <= c.Rev {
+ panic(fmt.Sprintf("publish: revision %d after %d", rev, c.Rev))
+ }
+ rec := &record{Rev: rev, Expires: w.now() + lifetimeTicks, Grants: map[string]bool{}}
+ for k, v := range c.Grants {
+ if v {
+ rec.Grants[k] = true
+ }
+ }
+ if prev := c.Records[c.Rev]; prev != nil {
+ for _, k := range sortedKeys(prev.Grants) {
+ if !rec.Grants[k] {
+ c.RevokedAt[k] = w.now()
+ }
+ }
+ }
+ for k := range rec.Grants {
+ delete(c.RevokedAt, k)
+ }
+ c.Records[rev], c.Rev, c.Bucket = rec, rev, rec
+ w.logf("console: publishes revision %d, expiring at %d, grants %v", rev, rec.Expires, sortedKeys(rec.Grants))
+}
+
+// consoleGrant and consoleRevoke are carlos engines grant/revoke: the
+// database changes and the console publishes the next revision.
+func (w *world) consoleGrant(key string) {
+ w.console.Grants[key] = true
+ w.publish(w.console.Rev + 1)
+}
+
+func (w *world) consoleRevoke(key string) {
+ delete(w.console.Grants, key)
+ w.publish(w.console.Rev + 1)
+}
+
+// replay is a bucket writer restoring an older signed record: validly signed,
+// and unexpired unless 72 hours have passed.
+func (w *world) replay(rev int) {
+ rec := w.console.Records[rev]
+ if rec == nil {
+ panic(fmt.Sprintf("replay: no revision %d", rev))
+ }
+ w.console.Bucket = rec
+ w.logf("bucket writer: replays revision %d (newest %d) into the bucket", rev, w.console.Rev)
+}
+
+func (w *world) setBucketDown(down bool) {
+ w.console.BucketDown = down
+ w.logf("the bucket is unreachable = %v", down)
+}
+
+// newestGrants is the oracle's truth for key: whether the newest record the
+// console published grants it, and if not, since when. An expired newest
+// record grants nothing from its expiry (a console down for 72 hours drops
+// every grant, §6.4). A key no record ever granted has never been granted.
+func (w *world) newestGrants(key string) (bool, int) {
+ rec := w.console.Records[w.console.Rev]
+ if w.now() >= rec.Expires {
+ return false, rec.Expires
+ }
+ if rec.Grants[key] {
+ return true, 0
+ }
+ if t, ok := w.console.RevokedAt[key]; ok {
+ return false, t
+ }
+ return false, -1 << 30
+}
+
+// ---------- the grant mirror (spec §5.3) ----------
+
+// mirrorTick is one poll of b's mirror. It verifies the record's expiry and
+// refuses a revision below its floor (an equal revision is the same signed
+// bytes: the model's records are immutable per revision). A good read
+// replaces the record, raises the floor, and persists both before either is
+// used (floor-persisted).
+func (w *world) mirrorTick(b *box) {
+ m := &b.Mirror
+ c := &w.console
+ if c.BucketDown || c.Bucket == nil {
+ return
+ }
+ rec, now := c.Bucket, w.now()
+ if now >= rec.Expires {
+ if m.Rec != rec {
+ w.logf("box%d: mirror refuses revision %d: expired at %d", b.ID, rec.Rev, rec.Expires)
+ }
+ return
+ }
+ if rec.Rev < m.Floor {
+ w.logf("box%d: mirror refuses revision %d: below the floor %d", b.ID, rec.Rev, m.Floor)
+ return
+ }
+ if rec.Rev > m.Floor || m.Rec == nil {
+ b.FreshRead = m.Floor == 0 && b.Rebuilt
+ w.logf("box%d: mirror reads revision %d (floor %d -> %d)", b.ID, rec.Rev, m.Floor, rec.Rev)
+ }
+ m.Rec, m.ReadAt = rec, now
+ if rec.Rev > m.Floor {
+ m.Floor = rec.Rev
+ }
+ if on("floor-persisted") {
+ m.Persisted, m.PersistedFloor = m.Rec, m.Floor
+ }
+}
+
+// restartEdge is b's edge restarting: it loads the persisted record and
+// floor before any engine socket opens. The time of the last good read is
+// persisted with the record, so a restart is not a good read.
+func (w *world) restartEdge(b *box) {
+ m := &b.Mirror
+ m.Rec, m.Floor = m.Persisted, m.PersistedFloor
+ rev := 0
+ if m.Rec != nil {
+ rev = m.Rec.Rev
+ }
+ w.logf("box%d: edge restarts: mirror loads revision %d, floor %d", b.ID, rev, m.Floor)
+}
+
+// rebuild is a new or rebuilt box: its edge's data directory is gone, so it
+// has no floor and no record until its first read (the fresh-box residual,
+// §5.3).
+func (w *world) rebuild(b *box) {
+ b.Mirror = mirror{}
+ b.Rebuilt, b.FreshRead = true, false
+ w.logf("box%d: rebuilt: the edge has no persisted floor", b.ID)
+}
+
+// tableGrants is b's grant table on key. Stale (no good read for ten
+// minutes), expired, or never read: empty (stale-clears-grants).
+func (w *world) tableGrants(b *box, key string) bool {
+ m := b.Mirror
+ if m.Rec == nil {
+ return false
+ }
+ if on("stale-clears-grants") && (w.now()-m.ReadAt >= staleTicks || w.now() >= m.Rec.Expires) {
+ return false
+ }
+ return m.Rec.Grants[key]
+}
+
+// ---------- the call path (spec §5.4) ----------
+
+// call is one engine call as its sender makes it. host is the instance
+// whose engine socket the process connects to, or whose door key it
+// presents; engine is the Host: header; forged an X-Carlos-Hop-Caller header
+// the sender wrote, or nil.
+type call struct {
+ from *box
+ p *proc
+ viaDoor bool
+ uid string
+ host string
+ engine string
+ path string
+ forged *caller
+}
+
+// engineCall is process p on box from calling engine (its Host:) at path,
+// through the engine socket of instance host, or through the door with
+// host's door key under uid. It reports whether the call reached an engine
+// process.
+func (w *world) engineCall(from *box, p *proc, viaDoor bool, uid string, host, engine, path string) bool {
+ return w.placeCall(call{from: from, p: p, viaDoor: viaDoor, uid: uid, host: host, engine: engine, path: path})
+}
+
+// unitBacked: the route runs as a unit-backed DynamicUser service. The
+// model's engine route is (§8: arm succeeds with nested callers and a
+// unit-backed engine); every other instance route is nested. Unit-backed
+// routes are not callers (ruling R2): they have no engine socket.
+func unitBacked(g string) bool { return g == eng }
+
+// socketOpen: instance g on b has an engine socket: the box is armed and
+// its listener manager has the sockets open, and g is a nested instance.
+func (w *world) socketOpen(b *box, g string) bool {
+ if !b.Armed || !b.Sockets || unitBacked(g) {
+ return false
+ }
+ for _, x := range w.groups(b) {
+ if x == g {
+ return true
+ }
+ }
+ return false
+}
+
+// realApp is the account/app whose code process p runs: planted code's app,
+// else its group's route's, else (a tenant with no row in the model: a flat,
+// foreign or worker tenant) acct/<group). nil is a public client: no app.
+func (w *world) realApp(b *box, p *proc) string {
+ switch {
+ case p == nil:
+ return ""
+ case p.Code != "":
+ return p.Code
+ }
+ if r := b.Rows[p.Group]; r != nil && r.App != "" {
+ return r.App
+ }
+ return "acct/" + p.Group
+}
+
+func (w *world) placeCall(c call) bool {
+ b := c.from
+ how := "socket of " + c.host
+ if c.viaDoor {
+ how = "door (uid " + c.uid + ", key of " + c.host + ")"
+ }
+ who := "a public client"
+ if c.p != nil {
+ who = fmt.Sprintf("process %d (%s)", c.p.ID, c.p.Slice)
+ }
+ w.logf("box%d: %s calls Host: %s%s through the %s", b.ID, who, c.engine, c.path, how)
+ if strings.Contains(c.engine, ".") {
+ w.logf("box%d: Host: %s is no engine name (it has a dot): not an engine call", b.ID, c.engine)
+ return false
+ }
+ r := b.Rows[c.host]
+ if r == nil || r.Kind != "instance" || r.Platform {
+ w.logf("box%d: no instance route %s", b.ID, c.host)
+ return false
+ }
+ // who is calling
+ if !c.viaDoor {
+ if !w.socketOpen(b, c.host) {
+ w.logf("box%d: %s has no engine socket (armed %v)", b.ID, c.host, b.Armed)
+ return false
+ }
+ if on("cgroup-identity") && c.p.Slice != "inst:"+c.host {
+ w.logf("box%d: engine socket of %s: peer cgroup %s is not the instance's slice; closed unread", b.ID, c.host, c.p.Slice)
+ return false
+ }
+ } else if on("door-uid") && c.uid == "carlos" {
+ w.logf("box%d: door: an engine call from uid carlos: 404 engine not granted", b.ID)
+ return false
+ }
+ mark := callerOf(r.App, c.engine)
+ // the listener strips every X-Carlos-* header the sender wrote
+ if c.forged != nil && on("hop-caller-signed") {
+ w.logf("box%d: X-Carlos-Hop-Caller %s from the sender deleted", b.ID, c.forged.key())
+ c.forged = nil
+ }
+ if !w.tableGrants(b, mark.key()) {
+ w.logf("box%d: %s not in the grant table: 404 engine not granted", b.ID, mark.key())
+ return false
+ }
+ hostname := engineHosts[c.engine]
+ home := w.homeOf(hostname)
+ if home == nil {
+ w.logf("box%d: %s homed nowhere: 502 engine unreachable", b.ID, hostname)
+ return false
+ }
+ seen := mark
+ if home != b {
+ w.logf("box%d: hop to box%d, caller %s signed into the MAC", b.ID, home.ID, mark.key())
+ if c.forged != nil {
+ w.logf("box%d: the hop also carries the sender's X-Carlos-Hop-Caller %s; the engine box takes it", home.ID, c.forged.key())
+ seen = *c.forged
+ }
+ }
+ return w.engineAdmit(home, b, seen, hostname, c.path, w.realApp(b, c.p), c.p)
+}
+
+// clientHop is a public client sending b's edge a request for hostname that
+// carries X-Carlos-Hop-Caller with no hop MAC. Only a verified hop's caller
+// is a caller (hop-caller-signed): the header is deleted and the request is
+// a public request like any other.
+func (w *world) clientHop(b *box, hostname, path string, forged caller) bool {
+ w.logf("box%d: a public client sends %s%s with X-Carlos-Hop-Caller %s", b.ID, hostname, path, forged.key())
+ if on("hop-caller-signed") {
+ w.logf("box%d: unverified X-Carlos-Hop-Caller deleted; a public request", b.ID)
+ if r := w.admitPublic(b, hostname, path); r != nil {
+ w.deliver(r)
+ }
+ return false
+ }
+ return w.engineAdmit(b, b, forged, hostname, path, "", nil)
+}
+
+// homeOf is the box whose registry has hostname (the edge's home map).
+func (w *world) homeOf(hostname string) *box {
+ for _, b := range w.boxes {
+ if b.Rows[hostname] != nil {
+ return b
+ }
+ }
+ return nil
+}
+
+// exactRoute is the row an engine call to hostname resolves to on b: the
+// hostname's own row, through an alias (the same route), never a path map
+// (exact-route-engine). ok is false for an unknown host.
+func (w *world) exactRoute(b *box, hostname string) (row, bool) {
+ final, ok := b.EdgeRows[hostname]
+ if ok && final.Alias != "" {
+ final, ok = b.EdgeRows[final.Alias]
+ }
+ return final, ok
+}
+
+// engineAdmit is the engine box (home) deciding an engine-marked request for
+// hostname: the route must be internal, the engine box's own table must name
+// the hostname for the mark's engine and grant it to the mark's app
+// (engine-box-recheck), and the route must be the hostname's own
+// (exact-route-engine). Then the activator's dispatch, which may wake the
+// engine. real is the calling process's real app; p the process.
+func (w *world) engineAdmit(home, from *box, mark caller, hostname, path, real string, p *proc) bool {
+ final, ok := w.exactRoute(home, hostname)
+ if !ok {
+ w.logf("box%d: engine call to %s: unknown host", home.ID, hostname)
+ return false
+ }
+ if !on("exact-route-engine") {
+ if to, ok := final.PathTo[path]; ok {
+ if t, ok := home.EdgeRows[to]; ok {
+ w.logf("box%d: engine call to %s%s follows the path map to %s", home.ID, hostname, path, to)
+ final = t
+ }
+ }
+ }
+ if home.Serving[final.Host] != markInternal {
+ w.logf("box%d: engine call to %s: %s is not internal (%v): the internal refusal", home.ID, hostname, final.Host, home.Serving[final.Host])
+ return false
+ }
+ if on("engine-box-recheck") {
+ if engineHosts[mark.Engine] != hostname || !w.tableGrants(home, mark.key()) {
+ w.logf("box%d: engine box: %s not granted for %s: the internal refusal", home.ID, mark.key(), hostname)
+ return false
+ }
+ }
+ g := truthGroup(home, final.Host)
+ q := w.newest(home, g)
+ if q == nil {
+ w.wake(home, g, "recovery", nil)
+ q = w.newest(home, g)
+ }
+ if q == nil {
+ w.logf("box%d: engine call: %s has no process; the wake failed", home.ID, g)
+ return false
+ }
+ w.logf("box%d: engine call reaches process %d (%s v%d); the access log records caller %s", home.ID, q.ID, q.Group, q.Ver, mark.app())
+ w.checkCall(home, from, mark, real, p, q)
+ return true
+}
+
+// ---------- armed boxes (spec §6.2) ----------
+
+// unisolatedKinds are the launch paths that run tenant code outside an
+// instance slice: a flat instance, a foreign one, and an app's worker.
+var unisolatedKinds = []string{"flat", "foreign", "worker"}
+
+// arm is `carlos engines arm`: refused unless every exec-backed instance
+// route is nested (unit-backed routes are judged by backing and admitted),
+// no route spawns workers, and every carlos-exec@ cgroup is empty
+// (arm-checks-box). Then the box records the armed state and the edge opens
+// the engine sockets.
+func (w *world) arm(b *box) bool {
+ if b.Armed {
+ return true
+ }
+ if on("arm-checks-box") {
+ var why []string
+ for _, k := range sortedKeys(b.Unisolated) {
+ why = append(why, "a "+k+" route")
+ }
+ for _, p := range b.Procs {
+ if p.Unisolated {
+ why = append(why, fmt.Sprintf("process %d in %s", p.ID, p.Slice))
+ }
+ }
+ if len(why) > 0 {
+ w.logf("box%d: carlos engines arm: refused: %s", b.ID, strings.Join(why, ", "))
+ return false
+ }
+ }
+ b.Armed = true
+ b.Sockets = true
+ w.logf("box%d: armed; engine sockets open (arming vouches for the present, not the past)", b.ID)
+ return true
+}
+
+// disarm is `carlos engines disarm`: it closes every engine socket first,
+// then clears the state; launches follow.
+func (w *world) disarm(b *box) {
+ if !b.Armed {
+ return
+ }
+ b.Sockets = false
+ b.Armed = false
+ w.logf("box%d: disarmed: engine sockets closed, then the state cleared", b.ID)
+}
+
+// launchUnisolated starts tenant code outside an instance slice: kind flat
+// or foreign (an instance of that layout, through the exec-child path) or
+// worker (an app's worker in carlos-exec@). While armed it is refused before
+// any process starts (armed-refuses-unisolated). The model's unisolated
+// tenants are one route per kind, acct/<kind>.
+func (w *world) launchUnisolated(b *box, kind string) bool {
+ if b.Armed && on("armed-refuses-unisolated") {
+ w.logf("box%d: %s launch refused: the box is armed (carlos engines disarm to run it)", b.ID, kind)
+ return false
+ }
+ b.Unisolated[kind] = true
+ w.nextID++
+ p := &proc{ID: w.nextID, Group: kind, Slice: "exec:" + kind, Unisolated: true}
+ b.Procs = append(b.Procs, p)
+ w.logf("box%d: %s tenant started as process %d in %s", b.ID, kind, p.ID, p.Slice)
+ return true
+}
+
+// moveToNested is the operator moving the kind route off the box's
+// unisolated layouts (or its workers into instance slices): its processes
+// stop and the route no longer blocks arming.
+func (w *world) moveToNested(b *box, kind string) {
+ w.stopGroup(b, kind)
+ delete(b.Unisolated, kind)
+ w.logf("box%d: the %s route moved to nested; its processes stopped", b.ID, kind)
+}
+
+// tamper is unisolated process by writing nested group g's instance
+// directory (an environment file and an LD_PRELOAD): g's next start runs by's
+// code inside g's slice. Only an unisolated process can, which an armed box
+// never runs; the walk generates it only under flatEraTamper.
+func (w *world) tamper(b *box, by *proc, g string) {
+ b.Tampered[g] = w.realApp(b, by)
+ w.logf("box%d: process %d (%s) plants code in %s's instance directory", b.ID, by.ID, by.Slice, g)
+}
+
+// applyTamper is a nested start picking up planted code (launch calls it).
+func (w *world) applyTamper(b *box, p *proc) {
+ if app := b.Tampered[p.Group]; app != "" {
+ p.Code = app
+ w.logf("box%d: process %d of %s runs code %s planted", b.ID, p.ID, p.Group, app)
+ }
+}
+
+// ---------- the random walk ----------
+
+// walkApps are the apps the console may grant: the model's routes' apps and
+// the unisolated tenants'.
+var walkApps = []string{"acct/eng", "acct/flat", "acct/shop", "acct/tcp"}
+
+func (w *world) pickEngine() string { return []string{eng, site}[w.rng.Intn(2)] }
+func (w *world) pickPath() string { return []string{"/", engSitePath}[w.rng.Intn(2)] }
+func (w *world) pickKey() string {
+ return walkApps[w.rng.Intn(len(walkApps))] + "/" + w.pickEngine()
+}
+
+// maybeForged is, one call in four, an X-Carlos-Hop-Caller the sender wrote.
+func (w *world) maybeForged() *caller {
+ if w.rng.Intn(4) != 0 {
+ return nil
+ }
+ c := callerOf(walkApps[w.rng.Intn(len(walkApps))], w.pickEngine())
+ return &c
+}
+
+// replayable: a bucket writer's replay in the default world lands only once
+// every edge that has a floor has read the newest revision, so a floor
+// refuses it everywhere but on a box with no floor. A replay before an edge
+// has read the newest revision withholds that revision from it, which no
+// floor can refuse; see the Task 5 report (an unstated residual).
+func (w *world) replayable() bool {
+ if w.console.Rev < 2 {
+ return false
+ }
+ for _, b := range w.boxes {
+ if b.Mirror.Floor > 0 && b.Mirror.Floor < w.console.Rev {
+ return false
+ }
+ }
+ return true
+}
+
+// pickReplay is the revision a bucket writer replays: one that grants a key
+// the console has since revoked, if any (the damaging choice), else any
+// older one.
+func (w *world) pickReplay() int {
+ var damaging []int
+ for r := 1; r < w.console.Rev; r++ {
+ for k := range w.console.Records[r].Grants {
+ if g, _ := w.newestGrants(k); !g {
+ damaging = append(damaging, r)
+ break
+ }
+ }
+ }
+ if len(damaging) > 0 {
+ return damaging[w.rng.Intn(len(damaging))]
+ }
+ return 1 + w.rng.Intn(w.console.Rev-1)
+}
+
+// callers are the nested instance groups on b with an engine socket open.
+func (w *world) callers(b *box) []string {
+ var out []string
+ for _, g := range w.groups(b) {
+ if w.socketOpen(b, g) {
+ out = append(out, g)
+ }
+ }
+ return out
+}
+
+func init() {
+ // the mirror polls every 30 s, whatever the walk does
+ stepHooks = append(stepHooks, func(w *world) {
+ if w.now()%pollTicks == 0 {
+ for _, b := range w.boxes {
+ w.mirrorTick(b)
+ }
+ }
+ })
+ actions = append(actions,
+ action{name: "engine-call", weight: 4, run: func(w *world) {
+ b := w.pickBox()
+ gs := w.callers(b)
+ if len(gs) == 0 || len(b.Procs) == 0 {
+ return
+ }
+ host := gs[w.rng.Intn(len(gs))]
+ // usually the instance's own process; one call in three, any
+ // process on the box connects to the socket (mode 0666)
+ p := w.newest(b, host)
+ if p == nil || w.rng.Intn(3) == 0 {
+ p = b.Procs[w.rng.Intn(len(b.Procs))]
+ }
+ c := call{from: b, p: p, uid: "carlos", host: host, engine: w.pickEngine(), path: w.pickPath()}
+ c.forged = w.maybeForged()
+ w.placeCall(c)
+ }},
+ action{name: "door-call", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ gs := w.groups(b)
+ if len(gs) == 0 {
+ return
+ }
+ host := gs[w.rng.Intn(len(gs))]
+ c := call{from: b, viaDoor: true, host: host, engine: w.pickEngine(), path: w.pickPath()}
+ if len(b.Procs) > 0 && w.rng.Intn(2) == 0 {
+ // any process running as carlos presents host's door key
+ // (every flat tenant can read every other's config)
+ c.p, c.uid = b.Procs[w.rng.Intn(len(b.Procs))], "carlos"
+ } else {
+ // an enrolled host-app user: its own app's key, its own uid
+ c.p, c.uid = &proc{Group: host, Slice: "user:u-" + host}, "u-"+host
+ }
+ c.forged = w.maybeForged()
+ w.placeCall(c)
+ }},
+ action{name: "client-hop", weight: 1, run: func(w *world) {
+ hosts := []string{engHost, engSite}
+ c := callerOf(walkApps[w.rng.Intn(len(walkApps))], w.pickEngine())
+ w.clientHop(w.pickBox(), hosts[w.rng.Intn(2)], w.pickPath(), c)
+ }},
+ action{name: "console-grant", weight: 1, run: func(w *world) { w.consoleGrant(w.pickKey()) }},
+ action{name: "console-revoke", weight: 1, run: func(w *world) {
+ keys := sortedKeys(w.console.Grants)
+ if len(keys) > 0 {
+ w.consoleRevoke(keys[w.rng.Intn(len(keys))])
+ }
+ }},
+ action{name: "console-resign", weight: 1, run: func(w *world) { w.publish(w.console.Rev + 1) }},
+ action{name: "bucket-down", weight: 1, run: func(w *world) {
+ w.setBucketDown(!w.console.BucketDown && !w.calm())
+ }},
+ action{name: "fast-forward", weight: 1, run: func(w *world) {
+ if w.calm() {
+ return
+ }
+ if w.rng.Intn(8) == 0 {
+ w.advance(lifetimeTicks + staleTicks) // the console is down for three days
+ return
+ }
+ w.advance(staleTicks) // ten minutes with no poll
+ }},
+ action{name: "replay", weight: 1, run: func(w *world) {
+ if w.replayable() {
+ w.replay(w.pickReplay())
+ }
+ }},
+ action{name: "restart-edge", weight: 2, run: func(w *world) {
+ switch w.rng.Intn(3) {
+ case 0: // a release roll restarts every edge
+ for _, b := range w.boxes {
+ w.restartEdge(b)
+ }
+ case 1:
+ w.restartEdge(w.pickBox())
+ default:
+ // a rebuilt box: the calling box, or under freshBoxReplay any
+ // box (the engine's home too); a bucket writer may replay at once
+ b := w.boxes[1]
+ if w.freshBoxReplay {
+ b = w.pickBox()
+ }
+ w.rebuild(b)
+ if w.rng.Intn(2) == 0 && w.replayable() {
+ w.replay(w.pickReplay())
+ }
+ }
+ }},
+ action{name: "arm", weight: 2, run: func(w *world) { w.arm(w.pickBox()) }},
+ action{name: "disarm", weight: 1, run: func(w *world) { w.disarm(w.pickBox()) }},
+ action{name: "launch-unisolated", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ kind := unisolatedKinds[w.rng.Intn(len(unisolatedKinds))]
+ if !w.launchUnisolated(b, kind) || !w.flatEraTamper || b.Armed {
+ return
+ }
+ var gs []string
+ for _, g := range w.groups(b) {
+ if !unitBacked(g) {
+ gs = append(gs, g)
+ }
+ }
+ if len(gs) > 0 {
+ w.tamper(b, w.newest(b, kind), gs[w.rng.Intn(len(gs))])
+ }
+ }},
+ action{name: "unisolated-exit", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ var ps []*proc
+ for _, p := range b.Procs {
+ if p.Unisolated {
+ ps = append(ps, p)
+ }
+ }
+ if len(ps) == 0 {
+ return
+ }
+ p := ps[w.rng.Intn(len(ps))]
+ for i, x := range b.Procs {
+ if x == p {
+ b.Procs = append(b.Procs[:i], b.Procs[i+1:]...)
+ break
+ }
+ }
+ w.logf("box%d: process %d (%s) exited", b.ID, p.ID, p.Slice)
+ }},
+ action{name: "move-to-nested", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ if ks := sortedKeys(b.Unisolated); len(ks) > 0 {
+ w.moveToNested(b, ks[w.rng.Intn(len(ks))])
+ }
+ }},
+ )
+}
+
+// mirrorsState is a one-line summary of the console and every mirror, for a
+// failing witness.
+func (w *world) mirrorsState() string {
+ out := []string{fmt.Sprintf("console{rev %d bucket %d down %v now %d}", w.console.Rev, w.console.Bucket.Rev, w.console.BucketDown, w.now())}
+ for _, b := range w.boxes {
+ m := b.Mirror
+ rev := 0
+ if m.Rec != nil {
+ rev = m.Rec.Rev
+ }
+ out = append(out, fmt.Sprintf("box%d{rec %d floor %d readAt %d persisted %d armed %v sockets %v rebuilt %v}", b.ID, rev, m.Floor, m.ReadAt, m.PersistedFloor, b.Armed, b.Sockets, b.Rebuilt))
+ }
+ return strings.Join(out, " ")
+}
diff --git a/internal/sim/engines/classify_test.go b/internal/sim/engines/classify_test.go
index e0032cb56..78d6d4454 100644
--- a/internal/sim/engines/classify_test.go
+++ b/internal/sim/engines/classify_test.go
@@ -305,6 +305,14 @@ func (w *world) classifiedGroups(b *box) []string {
// classified map: in-flight requests did not survive the restart, and the
// fence covers everything written. Running processes are untouched.
func (w *world) upgrade(b *box) {
+ if w.unwrittenManifestAcrossUpgrade {
+ if why, procs := w.upgradeResidual(b); why != "" {
+ for _, p := range procs {
+ p.Residual = "unwrittenManifestAcrossUpgrade"
+ }
+ w.logf("box%d: upgrade: the stated residual (%s); its processes' breaches are counted as residual", b.ID, why)
+ }
+ }
gs := w.classifiedGroups(b)
w.logf("box%d: upgrade: routes.internal arrives NULL on %v", b.ID, gs)
for _, g := range gs {
@@ -331,13 +339,24 @@ func (w *world) upgrade(b *box) {
// would produce it: a running declaring build whose manifest cannot be read,
// in a group the (correct) classification would mark 0 because the live
// manifest reads and does not declare. The default world does not generate
-// it; Task 5's flag does.
+// it; Task 5's flag (unwrittenManifestAcrossUpgrade) does.
func (w *world) residualAtUpgrade(b *box) string {
+ why, _ := w.upgradeResidual(b)
+ return why
+}
+
+// upgradeResidual is residualAtUpgrade with the processes it names: every
+// running unreadable declaring process of each group it applies to.
+func (w *world) upgradeResidual(b *box) (string, []*proc) {
+ first := ""
+ var procs []*proc
for _, g := range w.groups(b) {
var unreadable *proc
+ var group []*proc
for _, p := range b.Procs {
if bd := w.builds[p.Ver]; p.Group == g && bd.Declares && !bd.ManifestOK {
unreadable = p
+ group = append(group, p)
}
}
if unreadable == nil {
@@ -358,10 +377,13 @@ func (w *world) residualAtUpgrade(b *box) string {
}
}
if !staged {
- return fmt.Sprintf("%s runs v%d (declares, manifest unreadable) while live v%d reads as plain", g, unreadable.Ver, b.Live[g])
+ if first == "" {
+ first = fmt.Sprintf("%s runs v%d (declares, manifest unreadable) while live v%d reads as plain", g, unreadable.Ver, b.Live[g])
+ }
+ procs = append(procs, group...)
}
}
- return ""
+ return first, procs
}
// ---------- the operator clear ----------
@@ -459,7 +481,7 @@ func init() {
actions = append(actions,
action{name: "upgrade", weight: 1, run: func(w *world) {
b := w.pickBox()
- if why := w.residualAtUpgrade(b); why != "" {
+ if why := w.residualAtUpgrade(b); why != "" && !w.unwrittenManifestAcrossUpgrade {
w.logf("box%d: upgrade not generated: the stated residual (%s)", b.ID, why)
return
}
diff --git a/internal/sim/engines/dedicated_test.go b/internal/sim/engines/dedicated_test.go
index d666bb39f..e4c890aca 100644
--- a/internal/sim/engines/dedicated_test.go
+++ b/internal/sim/engines/dedicated_test.go
@@ -341,9 +341,9 @@ func (w *world) reach(b *box, p *proc, public bool, how string) *proc {
}
w.logf("box%d: %s reached process %d (%s v%d) past the edge", b.ID, how, p.ID, p.Group, p.Ver)
if public && w.builds[p.Ver].Declares {
- w.fail("INV-P", "box%d: a public connection through %s reached process %d of %s running v%d, which declares doc_engine, past the edge", b.ID, how, p.ID, p.Group, p.Ver)
+ w.failProc(p, "INV-P", "box%d: a public connection through %s reached process %d of %s running v%d, which declares doc_engine, past the edge", b.ID, how, p.ID, p.Group, p.Ver)
} else if g := w.grantLoaded(b, p.Group); public && g != "" {
- w.fail("INV-P", "box%d: a public connection through %s reached process %d of %s running v%d, whose group holds the doc-engine grant (on %s), past the edge", b.ID, how, p.ID, p.Group, p.Ver, g)
+ w.failProc(p, "INV-P", "box%d: a public connection through %s reached process %d of %s running v%d, whose group holds the doc-engine grant (on %s), past the edge", b.ID, how, p.ID, p.Group, p.Ver, g)
}
return p
}
diff --git a/internal/sim/engines/edge_test.go b/internal/sim/engines/edge_test.go
index 9145be3c5..36b26f297 100644
--- a/internal/sim/engines/edge_test.go
+++ b/internal/sim/engines/edge_test.go
@@ -284,9 +284,9 @@ func (w *world) deliver(r *req) {
r.Reached = p.ID
w.logf("box%d: request %d delivered to process %d (%s v%d)", b.ID, r.ID, p.ID, p.Group, p.Ver)
if r.Public && w.builds[p.Ver].Declares {
- w.fail("INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, which declares doc_engine", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver)
+ w.failProc(p, "INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, which declares doc_engine", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver)
} else if r.Public && w.grantLoaded(b, g) != "" {
- w.fail("INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, whose group holds the doc-engine grant (on %s)", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver, w.grantLoaded(b, g))
+ w.failProc(p, "INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, whose group holds the doc-engine grant (on %s)", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver, w.grantLoaded(b, g))
}
if p.Ver == b.Live[g] {
b.Good[g] = p.Ver // the live build answered: it is the good version now
diff --git a/internal/sim/engines/invariants_test.go b/internal/sim/engines/invariants_test.go
index 40d2357d8..5067236ab 100644
--- a/internal/sim/engines/invariants_test.go
+++ b/internal/sim/engines/invariants_test.go
@@ -67,20 +67,23 @@ func (w *world) i1Broken(b *box, p *proc) string {
// checkStart is I1 at the moment process p starts.
func (w *world) checkStart(b *box, p *proc) {
if why := w.i1Broken(b, p); why != "" {
- w.fail("INV-I1", "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
+ w.failProc(p, "INV-I1", "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
}
}
// check runs the state invariants over every running process. doStep calls
// it after every action; a witness calls it at each of its step boundaries.
+// Task 5 adds INV-ARM (checkArm); its event invariants INV-ID and INV-G are
+// recorded when an engine call reaches a process (checkCall).
func (w *world) check() {
for _, b := range w.boxes {
for _, p := range b.Procs {
if why := w.i1Broken(b, p); why != "" {
- w.fail("INV-I1", "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
+ w.failProc(p, "INV-I1", "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
}
}
}
+ w.checkArm()
}
// edgeGroup is group over the edge's loaded rows.
@@ -162,3 +165,87 @@ func (w *world) avExempt(b *box, host string) string {
}
return ""
}
+
+// ---------- Task 5: INV-ID, INV-G, INV-ARM (calls_test.go) ----------
+
+// checkCall is INV-ID and INV-G for an engine call that reached process q on
+// home, sent by process p (nil: a public client) on box from.
+//
+// - INV-ID: the caller the engine box records is the app whose code made
+// the call.
+// - INV-G: the call reaches the engine's exact route, and the newest record
+// the console published grants it, unless the revoke is younger than the
+// freshness bound (§6.4: within ten minutes of the last good read a box
+// may still grant; both boxes' bounds run from the same revoke, so a call
+// past it got through two tables that should both have dropped it).
+func (w *world) checkCall(home, from *box, mark caller, real string, p, q *proc) {
+ if mark.app() != real {
+ msg := fmt.Sprintf("box%d: the engine box records caller %s for a call made by %q (process %v)", home.ID, mark.app(), real, procID(p))
+ if w.flatEraTamper && p != nil && p.Code != "" && !p.Unisolated {
+ w.residual("flatEraTamper", "%s: code planted before the box was armed", msg)
+ } else {
+ w.fail("INV-ID", "%s", msg)
+ }
+ }
+ exact, _ := w.exactRoute(home, engineHosts[mark.Engine])
+ if want := truthGroup(home, exact.Host); q.Group != want {
+ w.fail("INV-G", "box%d: an engine call for %s reached process %d of %s, not the engine's exact route %s", home.ID, mark.key(), q.ID, q.Group, want)
+ }
+ if granted, since := w.newestGrants(mark.key()); !granted && w.now()-since >= staleTicks {
+ msg := fmt.Sprintf("box%d: an engine call for %s reached process %d of %s; the newest record (revision %d) has not granted it since tick %d, now %d", home.ID, mark.key(), q.ID, q.Group, w.console.Rev, since, w.now())
+ if w.freshBoxReplay && w.freshGrant(from, mark.key()) && w.freshGrant(home, mark.key()) {
+ w.residual("freshBoxReplay", "%s: both boxes hold a replayed record with no floor", msg)
+ } else {
+ w.fail("INV-G", "%s", msg)
+ }
+ }
+}
+
+// freshGrant: b's table grants key from a record b accepted with no floor
+// after it was rebuilt (the fresh-box residual).
+func (w *world) freshGrant(b *box, key string) bool {
+ return b.FreshRead && w.tableGrants(b, key)
+}
+
+func procID(p *proc) any {
+ if p == nil {
+ return "none"
+ }
+ return p.ID
+}
+
+// INV-ARM (state): no unisolated tenant process exists on a box while an
+// engine socket is open there. check() runs it.
+func (w *world) checkArm() {
+ for _, b := range w.boxes {
+ if !b.Sockets {
+ continue
+ }
+ for _, p := range b.Procs {
+ if p.Unisolated {
+ w.failProc(p, "INV-ARM", "box%d: engine sockets are open (armed %v) while process %d runs unisolated in %s", b.ID, b.Armed, p.ID, p.Slice)
+ }
+ }
+ }
+}
+
+// residual records the stated residual name once: "residual:<name>: ...".
+func (w *world) residual(name, format string, args ...any) {
+ for _, r := range w.residuals {
+ if strings.HasPrefix(r, "residual:"+name+":") {
+ return
+ }
+ }
+ w.residuals = append(w.residuals, "residual:"+name+": "+fmt.Sprintf(format, args...))
+ w.logf("residual:%s recorded", name)
+}
+
+// failProc is fail for a breach process p causes: a process a stated
+// residual covers records the residual instead.
+func (w *world) failProc(p *proc, inv, format string, args ...any) {
+ if p != nil && p.Residual != "" {
+ w.residual(p.Residual, inv+": "+format, args...)
+ return
+ }
+ w.fail(inv, format, args...)
+}
diff --git a/internal/sim/engines/launch_test.go b/internal/sim/engines/launch_test.go
index e8c5943f5..8c9cf0a37 100644
--- a/internal/sim/engines/launch_test.go
+++ b/internal/sim/engines/launch_test.go
@@ -102,6 +102,7 @@ func (w *world) launch(b *box, g string, ver int, path string) bool {
p := &proc{ID: w.nextID, Group: g, Ver: ver, Slice: "inst:" + g}
b.Procs = append(b.Procs, p)
w.logf("box%d: %s started %s v%d as process %d", b.ID, path, g, ver, p.ID)
+ w.applyTamper(b, p)
w.checkStart(b, p)
return true
}
diff --git a/internal/sim/engines/rules_test.go b/internal/sim/engines/rules_test.go
index 8cf130086..b7a6fc16c 100644
--- a/internal/sim/engines/rules_test.go
+++ b/internal/sim/engines/rules_test.go
@@ -74,4 +74,16 @@ var allRules = []string{
"dedicated-launch-check", // a declaring launch is refused on a box with a proxying row outside its group (R12-2)
"dedicated-edge-refusal", // the edge refuses every proxying row outside the internal group homed on its box (R12-2)
"ingress-precondition", // the operator's firewall admits only the edge's ports, from every source (R12-1, R13-1)
+
+ // Task 5: calls, identity, grants and arming (spec §5.2 the signed
+ // record; §5.3 the grant mirror; §5.4 the call path; §6.1, §6.2, §6.4)
+ "cgroup-identity", // the engine socket admits only a process in its own instance's slice (R1-1)
+ "door-uid", // the door makes an engine call only for a uid other than carlos (R2-3)
+ "hop-caller-signed", // the engine box takes the caller only from a MAC-verified hop; the header is stripped elsewhere
+ "engine-box-recheck", // the engine box checks its own grant table, whatever the calling box admitted (G4)
+ "exact-route-engine", // an engine call reaches only the engine hostname's own route, never through a path map (R4-2)
+ "floor-persisted", // the mirror's revision floor and record survive a restart (R1-4)
+ "stale-clears-grants", // a stale, expired or never-read table grants nothing (§5.3, §6.4)
+ "armed-refuses-unisolated", // an armed box refuses flat, foreign and worker launches before they start (R3-2, R4-1)
+ "arm-checks-box", // arming refuses a box with an unisolated route or a non-empty carlos-exec@ cgroup (R5-2)
}
diff --git a/internal/sim/engines/sim_test.go b/internal/sim/engines/sim_test.go
index 08c06537e..3d17dd14d 100644
--- a/internal/sim/engines/sim_test.go
+++ b/internal/sim/engines/sim_test.go
@@ -76,6 +76,11 @@ func TestEngines(t *testing.T) {
if failed > 0 {
t.Fatalf("%d of %d seeds violated an invariant", failed, n)
}
+ // the default world sets no residual flag, so it never generates one of
+ // the spec's stated residuals (TestResidualsAreCountedNotFailed)
+ if residuals > 0 {
+ t.Fatalf("the default world recorded %d residuals; only a test's flag may generate one", residuals)
+ }
}
// TestSeedDeterministic: one seed gives one trace, or no reported seed can
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go
index 562ce1142..019e7bd09 100644
--- a/internal/sim/engines/witness_test.go
+++ b/internal/sim/engines/witness_test.go
@@ -99,6 +99,30 @@ var witnesses = []witness{
"R13-1: a service row on the calling box aimed at the engine box's address; a firewall that admits it lets a public request through the calling box's edge reach the engine directly", wIngressPrivate},
{"ingress-precondition", "ingress-precondition", "INV-P",
"R12-1: the engine binds a port of its own on every interface; a firewall that admits it lets a public connection reach the engine", wOwnPort},
+
+ // Task 5: calls, identity, grants and arming
+ {"cgroup-identity", "cgroup-identity", "INV-ID",
+ "R1-1: on an armed box a sibling instance's process connects to the granted instance's engine socket (mode 0666); a socket whose path is the identity records the granted app as the caller", wCgroupIdentity},
+ {"door-uid", "door-uid", "INV-ID",
+ "R2-3: a flat tenant running as carlos reads a granted app's door key and calls an engine through the door; a door that takes the key from uid carlos records the granted app as the caller", wDoorUID},
+ {"hop-caller-signed", "hop-caller-signed", "INV-ID",
+ "a public client sends the engine box a request carrying X-Carlos-Hop-Caller naming a granted app; an engine box that takes the caller from the header rather than a verified hop records that app as the caller", wHopCallerSigned},
+ {"engine-box-recheck", "engine-box-recheck", "INV-G",
+ "G4: the calling box is rebuilt (no floor) and a bucket writer replays the record revoked ten minutes ago; the calling box admits on its superseded table; an engine box that trusts the calling box's admission serves the revoked app", wEngineBoxRecheck},
+ {"exact-route-engine", "exact-route-engine", "INV-G",
+ "R4-2: an app holds engine A's grant only; A's hostname is a static row whose path map points at engine B's route; an engine call resolved through the path map reaches B", wExactRouteEngine},
+ {"floor-persisted", "floor-persisted", "INV-G",
+ "R1-4: a grant is revoked and read everywhere; a bucket writer replays the older record, which the floor refuses; both edges restart; a floor not persisted admits the replay and the revoked grant serves past the freshness bound", wFloorPersisted},
+ {"stale-clears-grants", "stale-clears-grants", "INV-G",
+ "§6.4: the bucket is unreachable when a revoke is published; ten minutes pass with no good read; a stale table that still grants serves the revoked app past the bound", wStaleClearsGrants},
+ {"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
+ "R3-2/R4-1: on an armed box with engine sockets open, a foreign instance starts and a worker spawns; a box that does not refuse them runs unisolated tenant code beside open sockets", wArmedRefusesUnisolated},
+ {"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
+ "R4-1: on an armed box, an app's worker spawns into carlos-exec@ (worker alone)", wArmedRefusesWorker},
+ {"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
+ "R3-2: on an armed box, a flat instance starts (flat alone)", wArmedRefusesFlat},
+ {"arm-checks-box", "arm-checks-box", "INV-ARM",
+ "R5-2: an app's worker runs in carlos-exec@ on an unarmed box; arming that does not check the box opens engine sockets beside it", wArmChecksBox},
}
// TestWitnesses is the deterministic half of the mutation evidence.
@@ -1238,3 +1262,374 @@ func TestEngineBoxKeepsStaticRows(t *testing.T) {
dump(t, w)
}
}
+
+// ---------- Task 5: calls, identity, grants and arming ----------
+
+// shopEng is the grant every Task 5 world starts with: shop may call eng.
+const shopEng = "acct/shop/eng"
+
+// armedShop starts shop on box 1 on the plain build and arms box 1, so
+// shop's engine socket is open. It returns shop's process.
+func (w *world) armedShop(t *testing.T) *proc {
+ b := w.boxes[1]
+ b.Live["shop"], b.Good["shop"] = vPlain, vPlain
+ if !w.launch(b, "shop", vPlain, "seed") {
+ t.Fatalf("witness: shop did not start: %s", w.boxesState())
+ }
+ if !w.arm(b) {
+ t.Fatalf("witness: arming box 1 with only nested shop refused: %s", w.boxesState())
+ }
+ w.check()
+ if len(w.violations) > 0 {
+ t.Fatalf("witness: the fixture violates: %v", w.violations)
+ }
+ return w.newest(b, "shop")
+}
+
+// pollAll is one mirror poll on every box.
+func (w *world) pollAll() {
+ for _, b := range w.boxes {
+ w.mirrorTick(b)
+ }
+}
+
+// wCgroupIdentity (R1-1): box 1 runs shop and a sibling instance, other,
+// and is armed; other's process connects to shop's engine socket.
+func wCgroupIdentity(t *testing.T, w *world) {
+ w.runningEngine(t)
+ b := w.boxes[1]
+ if !w.provision(b, "other", "acct/other", "127.0.0.1:9002", vPlain) {
+ t.Fatalf("witness: provisioning other refused: %s", w.boxesState())
+ }
+ w.armedShop(t)
+ op := w.newest(b, "other")
+ if op == nil {
+ t.Fatalf("witness: other is not running: %s", w.boxesState())
+ }
+ w.engineCall(b, op, false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// wDoorUID (R2-3): a flat tenant on unarmed box 1, running as carlos,
+// presents shop's door key with Host: eng.
+func wDoorUID(t *testing.T, w *world) {
+ w.runningEngine(t)
+ b := w.boxes[1]
+ if !w.launchUnisolated(b, "flat") {
+ t.Fatalf("witness: a flat start on an unarmed box refused: %s", w.boxesState())
+ }
+ w.check()
+ w.engineCall(b, w.newest(b, "flat"), true, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// wHopCallerSigned: a public client sends box 0 a request for the engine's
+// hostname carrying X-Carlos-Hop-Caller: acct/shop/eng and no hop MAC.
+func wHopCallerSigned(t *testing.T, w *world) {
+ b, _ := w.runningEngine(t)
+ w.clientHop(b, engHost, "/", callerOf("acct/shop", eng))
+ w.check()
+}
+
+// wEngineBoxRecheck (G4): shop's grant is revoked and read everywhere; box
+// 1's data directory is lost (a rebuilt box: no floor), and a bucket writer
+// replays revision 1; box 1 accepts it, box 0's floor refuses it; ten
+// minutes pass; shop calls eng.
+func wEngineBoxRecheck(t *testing.T, w *world) {
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ b1 := w.boxes[1]
+ w.consoleRevoke(shopEng)
+ w.pollAll()
+ w.rebuild(b1)
+ w.replay(1)
+ w.pollAll()
+ w.advance(staleTicks)
+ w.pollAll()
+ w.check()
+ if !w.tableGrants(b1, shopEng) {
+ t.Fatalf("witness: the rebuilt calling box does not hold the replayed grant: %s", w.mirrorsState())
+ }
+ w.engineCall(b1, shop, false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// wExactRouteEngine (R4-2): shop holds engine site's grant and not eng's;
+// site's hostname is box 0's static row, whose path map sends /convert to
+// eng's route; shop calls site at /convert.
+func wExactRouteEngine(t *testing.T, w *world) {
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.consoleGrant("acct/shop/" + site)
+ w.consoleRevoke(shopEng)
+ w.pollAll()
+ w.check()
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", site, engSitePath)
+ w.check()
+}
+
+// wFloorPersisted (R1-4): shop's grant is revoked and read everywhere; ten
+// minutes pass; a bucket writer replays revision 1, which both floors
+// refuse; both edges restart; each polls; shop calls eng.
+func wFloorPersisted(t *testing.T, w *world) {
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.consoleRevoke(shopEng)
+ w.pollAll()
+ w.advance(staleTicks)
+ w.replay(1)
+ w.pollAll()
+ for _, b := range w.boxes {
+ w.restartEdge(b)
+ }
+ w.pollAll()
+ w.check()
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// wStaleClearsGrants (§6.4): the bucket is unreachable; shop's grant is
+// revoked; ten minutes pass with no good read; shop calls eng.
+func wStaleClearsGrants(t *testing.T, w *world) {
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.setBucketDown(true)
+ w.consoleRevoke(shopEng)
+ w.advance(staleTicks)
+ w.pollAll()
+ w.check()
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// armedRefuses: box 1 is armed with shop's socket open; each kind of
+// unisolated launch is tried in turn.
+func armedRefuses(kinds ...string) func(*testing.T, *world) {
+ return func(t *testing.T, w *world) {
+ w.armedShop(t)
+ b := w.boxes[1]
+ for _, k := range kinds {
+ ok := w.launchUnisolated(b, k)
+ if ok && on("armed-refuses-unisolated") {
+ t.Fatalf("witness: an armed box admitted a %s launch: %s", k, w.boxesState())
+ }
+ w.check()
+ }
+ }
+}
+
+func wArmedRefusesUnisolated(t *testing.T, w *world) { armedRefuses("foreign", "worker")(t, w) }
+func wArmedRefusesWorker(t *testing.T, w *world) { armedRefuses("worker")(t, w) }
+func wArmedRefusesFlat(t *testing.T, w *world) { armedRefuses("flat")(t, w) }
+
+// wArmChecksBox (R5-2): an app's worker runs in carlos-exec@ on unarmed box
+// 1 beside nested shop; the operator arms box 1.
+func wArmChecksBox(t *testing.T, w *world) {
+ b := w.boxes[1]
+ b.Live["shop"], b.Good["shop"] = vPlain, vPlain
+ w.launch(b, "shop", vPlain, "seed")
+ if !w.launchUnisolated(b, "worker") {
+ t.Fatalf("witness: a worker spawn on an unarmed box refused: %s", w.boxesState())
+ }
+ w.check()
+ ok := w.arm(b)
+ if ok && on("arm-checks-box") {
+ t.Fatalf("witness: arming a box with a running worker succeeded: %s", w.boxesState())
+ }
+ w.check()
+}
+
+// TestResidualsAreCountedNotFailed: each of the spec's three stated
+// residuals, as a fixed scenario. With its flag off the scenario is a
+// violation (the sequence really breaks the invariant the residual
+// concedes); with the flag on the world records residual:<name> and no
+// violation. The default world never sets a flag (TestEngines asserts the
+// sweep records no residual).
+func TestResidualsAreCountedNotFailed(t *testing.T) {
+ cases := []struct {
+ name string
+ set func(w *world)
+ run func(t *testing.T, w *world)
+ }{
+ {"freshBoxReplay", func(w *world) { w.freshBoxReplay = true }, residualFreshBoxReplay},
+ {"unwrittenManifestAcrossUpgrade", func(w *world) { w.unwrittenManifestAcrossUpgrade = true }, residualUnwrittenManifest},
+ {"flatEraTamper", func(w *world) { w.flatEraTamper = true }, residualFlatEraTamper},
+ }
+ for _, c := range cases {
+ t.Run(c.name, func(t *testing.T) {
+ off := newWitness()
+ c.run(t, off)
+ if len(off.violations) == 0 || len(off.residuals) > 0 {
+ t.Errorf("flag off: want a violation and no residual, got violations %v residuals %v", off.violations, off.residuals)
+ dump(t, off)
+ }
+ on := newWitness()
+ c.set(on)
+ c.run(t, on)
+ if len(on.violations) > 0 || len(on.residuals) == 0 {
+ t.Errorf("flag on: want residuals and no violation, got violations %v residuals %v", on.violations, on.residuals)
+ dump(t, on)
+ }
+ for _, r := range on.residuals {
+ if !strings.HasPrefix(r, "residual:"+c.name) {
+ t.Errorf("flag on: residual %q is not residual:%s", r, c.name)
+ }
+ }
+ })
+ }
+}
+
+// residualFreshBoxReplay (§5.3): shop's grant is revoked and read
+// everywhere; both boxes are rebuilt (no floor anywhere); a bucket writer
+// replays revision 1; both accept it; ten minutes pass; shop calls eng.
+func residualFreshBoxReplay(t *testing.T, w *world) {
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.consoleRevoke(shopEng)
+ w.pollAll()
+ for _, b := range w.boxes {
+ w.rebuild(b)
+ }
+ w.replay(1)
+ w.pollAll()
+ w.advance(staleTicks)
+ w.pollAll()
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// residualUnwrittenManifest (§5.1 "Classification before serving"): the
+// engine runs a declaring build whose staged manifest was never written;
+// an awake repoint moves its live link to a plain build without a restart;
+// the box takes the upgrade, which classifies the group 0 under the
+// running engine; a public request arrives.
+func residualUnwrittenManifest(t *testing.T, w *world) {
+ b := w.boxes[0]
+ b.Live[eng], b.Good[eng] = vUnreadable, vUnreadable
+ if !w.launch(b, eng, vUnreadable, "seed") {
+ t.Fatalf("scenario: the engine did not start: %s", w.boxesState())
+ }
+ if !w.repointAwake(b, eng, vPlain) {
+ t.Fatalf("scenario: the awake repoint refused: %s", w.boxesState())
+ }
+ w.check()
+ if w.residualAtUpgrade(b) == "" {
+ t.Fatalf("scenario: the upgrade residual is not set up: %s", w.boxesState())
+ }
+ w.upgrade(b)
+ w.check()
+ w.requestBy(b, engHost)
+ w.check()
+}
+
+// residualFlatEraTamper (§6.2): a flat tenant on unarmed box 1 plants code
+// in shop's instance directory; the operator moves the flat route off and
+// arms the box (arming vouches for the present, not the past); shop's next
+// start runs the planted code in shop's slice, which calls eng.
+func residualFlatEraTamper(t *testing.T, w *world) {
+ w.runningEngine(t)
+ b := w.boxes[1]
+ b.Live["shop"], b.Good["shop"] = vPlain, vPlain
+ if !w.launchUnisolated(b, "flat") {
+ t.Fatalf("scenario: a flat start on an unarmed box refused: %s", w.boxesState())
+ }
+ w.tamper(b, w.newest(b, "flat"), "shop")
+ w.moveToNested(b, "flat")
+ if !w.arm(b) {
+ t.Fatalf("scenario: arming refused after the flat route moved: %s", w.boxesState())
+ }
+ if !w.launch(b, "shop", vPlain, "seed") {
+ t.Fatalf("scenario: shop did not start: %s", w.boxesState())
+ }
+ w.check()
+ w.engineCall(b, w.newest(b, "shop"), false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// TestGrantedCallsReach is the positive control for the Task 5 witnesses,
+// which hold by refusing: with every rule on, a granted caller reaches the
+// engine through the socket (across a hop) and through the door from an
+// enrolled host-app uid (spec §8), and a revoke is in force once read.
+func TestGrantedCallsReach(t *testing.T) {
+ w := newWitness()
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ b1 := w.boxes[1]
+ if !w.engineCall(b1, shop, false, "carlos", "shop", eng, "/") {
+ t.Errorf("shop's own process through shop's socket did not reach eng")
+ }
+ user := &proc{Group: "shop", Slice: "user:u-shop"}
+ if !w.engineCall(b1, user, true, "u-shop", "shop", eng, "/") {
+ t.Errorf("the door from shop's enrolled uid with shop's key did not reach eng")
+ }
+ if w.engineCall(b1, user, true, "carlos", "shop", eng, "/") {
+ t.Errorf("the same key from uid carlos reached eng")
+ }
+ w.consoleRevoke(shopEng)
+ w.pollAll()
+ if w.engineCall(b1, shop, false, "carlos", "shop", eng, "/") {
+ t.Errorf("a revoke read by both boxes did not stop the call")
+ }
+ w.check()
+ if len(w.violations) > 0 {
+ t.Errorf("violations: %v", w.violations)
+ }
+ if t.Failed() {
+ dump(t, w)
+ }
+}
+
+// TestArmRefusesAndAdmits (spec §8): arming refuses a box with a flat
+// route, a foreign route, a route with workers, or a non-empty carlos-exec@
+// cgroup; it succeeds on the engine's box (a unit-backed engine) and on a box
+// of nested callers; on an armed box every unisolated launch is refused
+// before a process starts; disarm closes the engine sockets, and then
+// launches resume.
+func TestArmRefusesAndAdmits(t *testing.T) {
+ for _, kind := range unisolatedKinds {
+ w := newWitness()
+ b := w.boxes[1]
+ w.launchUnisolated(b, kind)
+ if w.arm(b) {
+ t.Errorf("%s: arming succeeded with the %s tenant running", kind, kind)
+ }
+ w.stopGroup(b, kind) // the cgroup is empty; the route remains
+ if w.arm(b) {
+ t.Errorf("%s: arming succeeded with a %s route on the box", kind, kind)
+ }
+ w.moveToNested(b, kind)
+ if !w.arm(b) {
+ t.Errorf("%s: arming refused once the route moved to nested", kind)
+ }
+ }
+ w := newWitness()
+ w.runningEngine(t)
+ if !w.arm(w.boxes[0]) {
+ t.Errorf("arming the engine's box (unit-backed engine) refused")
+ }
+ w.armedShop(t)
+ b := w.boxes[1]
+ n := len(b.Procs)
+ for _, kind := range unisolatedKinds {
+ if w.launchUnisolated(b, kind) {
+ t.Errorf("an armed box admitted a %s launch", kind)
+ }
+ }
+ if len(b.Procs) != n {
+ t.Errorf("a refused launch started a process: %d -> %d", n, len(b.Procs))
+ }
+ w.disarm(b)
+ if b.Sockets || b.Armed {
+ t.Errorf("disarm left sockets %v armed %v", b.Sockets, b.Armed)
+ }
+ if !w.launchUnisolated(b, "worker") {
+ t.Errorf("a worker spawn after disarm refused")
+ }
+ w.check()
+ if len(w.violations) > 0 {
+ t.Errorf("violations: %v", w.violations)
+ }
+ if t.Failed() {
+ dump(t, w)
+ }
+}
diff --git a/internal/sim/engines/world_test.go b/internal/sim/engines/world_test.go
index 608bba4e0..67ee029e9 100644
--- a/internal/sim/engines/world_test.go
+++ b/internal/sim/engines/world_test.go
@@ -39,12 +39,18 @@ type build struct {
// proc is a running process. Slice is the cgroup the peer check reads:
// inst:<group>, exec:<host> or unit:<host>.
+//
+// Code is the account/app whose code the process runs when that is not its
+// group's: code a flat-era tamper planted in the group's instance directory
+// (Task 5). Residual names the stated residual the process belongs to, if
+// any; a breach it causes is recorded as that residual, not a violation.
type proc struct {
ID int
Group string
Ver int
Slice string
Unisolated, OwnPort bool
+ Code, Residual string
}
// row is a host row of a box's table. Kind is instance, service, static or
@@ -128,6 +134,22 @@ type box struct {
// ListenStream sockets the capability pass has rendered, port to group
// (spec §5.1, "The edge is the only ingress").
PortGrant, Listen map[string]string
+
+ // Task 5 (calls_test.go). Mirror is the edge's grant mirror (spec §5.3).
+ // Armed is `carlos engines arm`; Sockets is whether the edge's listener
+ // manager has the engine sockets open (§5.4, §6.2). Unisolated is every
+ // route on the box whose tenant code runs outside an instance slice, by
+ // kind (flat, foreign, worker). Tampered is a nested group's instance
+ // directory written by an unisolated tenant: the planter's app.
+ //
+ // Rebuilt and FreshRead are the oracle's, not the protocol's: the box was
+ // rebuilt (its data directory lost), and its table holds a record it
+ // accepted with no floor since then (the fresh-box residual, §5.3).
+ Mirror mirror
+ Sockets bool
+ Unisolated map[string]bool
+ Tampered map[string]string
+ Rebuilt, FreshRead bool
}
type world struct {
@@ -151,6 +173,18 @@ type world struct {
// activator or control service failed to complete).
clearStopMisses bool
+ // Task 5 (calls_test.go): the console's engines record and the bucket
+ // that carries it; skew is time that passed without a step (a
+ // fast-forward), so now() is step+skew.
+ console engConsole
+ skew int
+
+ // The spec's three stated residuals. Off by default and set only by
+ // tests: with one on, the walk may generate its sequence, and the breach
+ // it causes is recorded in residuals as residual:<name>, never in
+ // violations.
+ freshBoxReplay, unwrittenManifestAcrossUpgrade, flatEraTamper bool
+
verbose bool
}
@@ -164,6 +198,10 @@ type action struct {
var actions []action
+// stepHooks run at the start of every step, before its action: what happens
+// on a timer whatever the walk chooses (Task 5: the mirror's poll).
+var stepHooks []func(*world)
+
func newWorld(seed int64, verbose bool) *world {
w := &world{
seed: seed,
@@ -175,7 +213,8 @@ func newWorld(seed int64, verbose bool) *world {
newBox := func(id int) *box {
return &box{ID: id, Rows: map[string]*row{}, Mark: map[string]mark{}, Live: map[string]int{}, Good: map[string]int{}, Staged: map[string][]int{},
EdgeRows: map[string]row{}, Serving: map[string]mark{}, SetAt: map[string]int{},
- PortGrant: map[string]string{}, Listen: map[string]string{}}
+ PortGrant: map[string]string{}, Listen: map[string]string{},
+ Unisolated: map[string]bool{}, Tampered: map[string]string{}}
}
home, calling := newBox(0), newBox(1)
w.boxes = []*box{home, calling}
@@ -202,6 +241,7 @@ func newWorld(seed int64, verbose bool) *world {
for _, b := range w.boxes {
b.loadEdge()
}
+ w.initEngines() // the console's first record, read by every edge
for v := 1; v <= nBuilds; v++ {
w.builds[v] = build{Ver: v, Declares: w.rng.Intn(2) == 0, ManifestOK: w.rng.Intn(2) == 0}
@@ -270,6 +310,9 @@ func (w *world) pick() *action {
// counts it under its name.
func (w *world) doStep() {
w.step++
+ for _, h := range stepHooks {
+ h(w)
+ }
a := w.pick()
if a == nil {
if w.verbose {