| 1 | package engines |
| 2 | |
| 3 | import ( |
| 4 | "fmt" |
| 5 | "sort" |
| 6 | "strings" |
| 7 | ) |
| 8 | |
| 9 | // fail records a violation of invariant inv, once per invariant id: the |
| 10 | // first message is the one the sweep reports and the later ones are the same |
| 11 | // fault again. The stored text begins "<inv>: ", which invariantOf reads back. |
| 12 | func (w *world) fail(inv, format string, args ...any) { |
| 13 | for _, v := range w.violations { |
| 14 | if invariantOf(v) == inv { |
| 15 | return |
| 16 | } |
| 17 | } |
| 18 | w.violations = append(w.violations, inv+": "+fmt.Sprintf(format, args...)) |
| 19 | } |
| 20 | |
| 21 | // invariantOf is the invariant id a violation string was recorded under. |
| 22 | func invariantOf(violation string) string { |
| 23 | if i := strings.Index(violation, ": "); i >= 0 { |
| 24 | return violation[:i] |
| 25 | } |
| 26 | return violation |
| 27 | } |
| 28 | |
| 29 | // The invariants of Task 2 (spec §5.1, §6.3): |
| 30 | // |
| 31 | // - INV-P (event, recorded in deliver): a public request is never delivered |
| 32 | // to a process whose build declares doc_engine. |
| 33 | // - INV-I1: no process of a declaring build runs unless its group is fenced |
| 34 | // as internal. Checked when each process starts, on every launch path |
| 35 | // (systemd and socket starts included), and again at every step boundary |
| 36 | // for every running process, since a later change can unfence a group |
| 37 | // under a process already running. It is two conditions: |
| 38 | // 1. the fence itself, as the spec states I1: the edge's fenced counter |
| 39 | // has reached the registry change that set the group's mark to 1, and |
| 40 | // nothing later cleared it (fencedTruth). A group open, NULL but never |
| 41 | // loaded (a new row), unloaded or written but not yet fenced fails here. |
| 42 | // 2. the fact the fence stands for: no row of the group is served 0 by |
| 43 | // the edge's map. This catches a counter advanced without a swap, which |
| 44 | // condition 1 cannot see because it reads that counter. |
| 45 | |
| 46 | // i1Broken reports why process p breaks I1, or "" when it does not. |
| 47 | func (w *world) i1Broken(b *box, p *proc) string { |
| 48 | if !w.builds[p.Ver].Declares { |
| 49 | return "" |
| 50 | } |
| 51 | if !w.fencedTruth(b, p.Group) { |
| 52 | at := "never" |
| 53 | if w.recorded(b, p.Group) { |
| 54 | at = fmt.Sprint(b.SetAt[p.Group]) |
| 55 | } |
| 56 | return fmt.Sprintf("the group is not fenced (registry %v, fenced %d, set at %s)", w.groupMark(b, p.Group), b.Fenced, at) |
| 57 | } |
| 58 | hosts := make([]string, 0, len(b.EdgeRows)) |
| 59 | for h := range b.EdgeRows { |
| 60 | hosts = append(hosts, h) |
| 61 | } |
| 62 | sort.Strings(hosts) |
| 63 | for _, h := range hosts { |
| 64 | if edgeGroup(b, h) == p.Group && b.Serving[h] == markPublic { |
| 65 | return fmt.Sprintf("the edge serves %s public", h) |
| 66 | } |
| 67 | } |
| 68 | return "" |
| 69 | } |
| 70 | |
| 71 | // checkStart is I1 at the moment process p starts. |
| 72 | func (w *world) checkStart(b *box, p *proc) { |
| 73 | if why := w.i1Broken(b, p); why != "" { |
| 74 | w.failProc(b, p, "INV-I1", true, "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why) |
| 75 | } |
| 76 | } |
| 77 | |
| 78 | // check runs the state invariants over every running process. doStep calls |
| 79 | // it after every action; a witness calls it at each of its step boundaries. |
| 80 | // Task 5 adds INV-ARM (checkArm); its event invariants INV-ID and INV-G are |
| 81 | // recorded when an engine call reaches a process (checkCall). |
| 82 | func (w *world) check() { |
| 83 | w.endResidualWindows() |
| 84 | for _, b := range w.boxes { |
| 85 | for _, p := range b.Procs { |
| 86 | if why := w.i1Broken(b, p); why != "" { |
| 87 | w.failProc(b, p, "INV-I1", true, "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why) |
| 88 | } |
| 89 | } |
| 90 | } |
| 91 | w.checkArm() |
| 92 | } |
| 93 | |
| 94 | // edgeGroup is group over the edge's loaded rows. |
| 95 | func edgeGroup(b *box, host string) string { |
| 96 | if r, ok := b.EdgeRows[host]; ok && r.Kind == "instance" && r.Owner != "" { |
| 97 | return r.Owner |
| 98 | } |
| 99 | return host |
| 100 | } |
| 101 | |
| 102 | // INV-AV (liveness, Task 3): at the end of the calm phase, every row of a |
| 103 | // group whose mark is 0 answers a public request. It is what catches the |
| 104 | // rules that only protect availability (static-minted-public, |
| 105 | // owner-nonempty-unique), which no safety invariant can see. Checked in |
| 106 | // final() only, after every edge has polled with its faults cleared. |
| 107 | // |
| 108 | // The truth, not the model's resolution, decides which rows must answer: |
| 109 | // - a static or service row is 0 by construction (spec §5.1, "The column"), |
| 110 | // minted or not; |
| 111 | // - an instance row answers when its group's mark is 0: the registry mark |
| 112 | // of its own row, or for a minted row, of the row it was minted from |
| 113 | // (Source); |
| 114 | // - alias rows are skipped: they answer as their target does. |
| 115 | // |
| 116 | // Not counted, as the spec's fail-closed choices or another rule's stated |
| 117 | // refusal: a minted row whose owner the correct fallback cannot find |
| 118 | // uniquely (refused and logged until the reconciler records its owner), and |
| 119 | // any row an avExemption names. |
| 120 | func (w *world) checkAV() { |
| 121 | for _, b := range w.boxes { |
| 122 | hosts := make([]string, 0, len(b.Rows)) |
| 123 | for h := range b.Rows { |
| 124 | hosts = append(hosts, h) |
| 125 | } |
| 126 | sort.Strings(hosts) |
| 127 | for _, h := range hosts { |
| 128 | r := b.Rows[h] |
| 129 | switch r.Kind { |
| 130 | case "alias": |
| 131 | continue |
| 132 | case "instance": |
| 133 | owner := h |
| 134 | if r.Platform { |
| 135 | if _, ok := b.resolveOwnerWith(r, true); !ok { |
| 136 | w.logf("box%d: final: minted row %s has no unique owner; refused by design, not counted", b.ID, h) |
| 137 | continue |
| 138 | } |
| 139 | owner = r.Source |
| 140 | } |
| 141 | if b.Mark[owner] != markPublic { |
| 142 | continue |
| 143 | } |
| 144 | } |
| 145 | if why := w.avExempt(b, h); why != "" { |
| 146 | w.logf("box%d: final: %s exempt from INV-AV: %s", b.ID, h, why) |
| 147 | continue |
| 148 | } |
| 149 | req, outcome := w.admit(b, h, "/") |
| 150 | switch outcome { |
| 151 | case admitted: |
| 152 | w.deliver(req) |
| 153 | case answered: |
| 154 | default: |
| 155 | w.fail("INV-AV", "box%d: row %s (%s) of a public group is %s a public request at the end of the calm phase (registry %v, edge %v)", b.ID, h, r.Kind, outcome, b.Mark[h], b.Serving[h]) |
| 156 | } |
| 157 | } |
| 158 | } |
| 159 | } |
| 160 | |
| 161 | // avExemptions are later tasks' stated refusals of a public row (each |
| 162 | // returns why, or ""), which INV-AV must not count. |
| 163 | var avExemptions []func(w *world, b *box, host string) string |
| 164 | |
| 165 | func (w *world) avExempt(b *box, host string) string { |
| 166 | for _, f := range avExemptions { |
| 167 | if why := f(w, b, host); why != "" { |
| 168 | return why |
| 169 | } |
| 170 | } |
| 171 | return "" |
| 172 | } |
| 173 | |
| 174 | // ---------- Task 5: INV-ID, INV-G, INV-ARM (calls_test.go) ---------- |
| 175 | |
| 176 | // checkCall is INV-ID and INV-G for an engine call that reached process q on |
| 177 | // home, sent by process p (nil: a public client) on box from through the |
| 178 | // engine socket or door key of instance via. |
| 179 | // |
| 180 | // - INV-ID: the caller the engine box records is the app whose code made |
| 181 | // the call. The flat-era residual covers only a call whose recorded |
| 182 | // caller is the compromised instance itself (compromisedItself). |
| 183 | // - INV-G: the call reaches the engine's exact route, and grantBreach finds |
| 184 | // no breach of the grant's freshness. |
| 185 | func (w *world) checkCall(home, from *box, mark caller, via, real string, p, q *proc) { |
| 186 | if mark.app() != real { |
| 187 | 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)) |
| 188 | if w.flatEraTamper && w.compromisedItself(from, mark, via, p) { |
| 189 | w.residual("flatEraTamper", "%s: code planted before the box was armed", msg) |
| 190 | } else { |
| 191 | w.fail("INV-ID", "%s", msg) |
| 192 | } |
| 193 | } |
| 194 | exact, _ := w.exactRoute(home, engineHosts[mark.Engine]) |
| 195 | if want := truthGroup(home, exact.Host); q.Group != want { |
| 196 | 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) |
| 197 | } |
| 198 | if why := w.grantBreach(home, from, mark.key()); why != "" { |
| 199 | w.fail("INV-G", "box%d: an engine call for %s reached process %d of %s; %s", home.ID, mark.key(), q.ID, q.Group, why) |
| 200 | } |
| 201 | } |
| 202 | |
| 203 | // compromisedItself: the flat-era residual's own case, from facts no rule |
| 204 | // changes. Process p is the instance via's own process, in via's own slice, |
| 205 | // running the code planted in via's directory, and the caller recorded is |
| 206 | // via's own app. Planted code that borrows another instance's socket or |
| 207 | // forges a hop caller is a violation like any other. |
| 208 | func (w *world) compromisedItself(from *box, mark caller, via string, p *proc) bool { |
| 209 | if p == nil || p.Code == "" || p.Unisolated || via == "" { |
| 210 | return false |
| 211 | } |
| 212 | r := from.Rows[via] |
| 213 | return r != nil && p.Group == via && p.Slice == "inst:"+via && from.Tampered[via] == p.Code && mark.app() == r.App |
| 214 | } |
| 215 | |
| 216 | // grantBreach is INV-G's grant clauses for key on a call admitted by the |
| 217 | // tables of from and home, each from facts no rule changes (spec §5.3, §6.4, |
| 218 | // ruling R5). It returns the first breach, or "". |
| 219 | // |
| 220 | // 1. Expiry: a key the newest record grants is granted by no table once that |
| 221 | // record has expired (every older record expired first), at once. |
| 222 | // 2. Revoke age: a key the newest record does not grant is granted by no |
| 223 | // table more than ten minutes plus one poll after the revoke, whatever |
| 224 | // was replayed (every record that grants it was signed before the |
| 225 | // revoke, and is stale ten minutes after its signing). A key no record |
| 226 | // ever granted is never granted. |
| 227 | // 3. The admitting tables: neither box admits on a table that was never |
| 228 | // read, holds an expired record, has had no good read for ten minutes, or |
| 229 | // holds a record signed ten minutes ago or more, whatever the key's |
| 230 | // revoke (from always checks its table; home is the engine box, whose |
| 231 | // table must be empty too). |
| 232 | // 4. A revoke a box has read stays in force there (§6.4: the floor refuses |
| 233 | // every older record). |
| 234 | func (w *world) grantBreach(home, from *box, key string) string { |
| 235 | c := &w.console |
| 236 | now := w.now() |
| 237 | newest := c.Records[c.Rev] |
| 238 | if newest.Grants[key] && now >= newest.Expires { |
| 239 | return fmt.Sprintf("the newest record (revision %d), which grants it, expired at %d, now %d", newest.Rev, newest.Expires, now) |
| 240 | } |
| 241 | if !newest.Grants[key] { |
| 242 | since, ok := c.RevokedAt[key] |
| 243 | if !ok { |
| 244 | return fmt.Sprintf("no record has granted it (newest revision %d)", newest.Rev) |
| 245 | } |
| 246 | if now-since > staleTicks+pollTicks { |
| 247 | return fmt.Sprintf("the newest record (revision %d) has not granted it since tick %d, now %d", newest.Rev, since, now) |
| 248 | } |
| 249 | } |
| 250 | boxes := []*box{from} |
| 251 | if home != from { |
| 252 | boxes = append(boxes, home) |
| 253 | } |
| 254 | for _, b := range boxes { |
| 255 | if why := w.tableStale(b); why != "" { |
| 256 | return fmt.Sprintf("box%d admitted it on a table that %s", b.ID, why) |
| 257 | } |
| 258 | } |
| 259 | if rr, ok := c.RevokedRev[key]; ok && !newest.Grants[key] { |
| 260 | for _, b := range boxes { |
| 261 | if b.ReadRev >= rr { |
| 262 | return fmt.Sprintf("box%d had read revision %d, which revoked it (read %d)", b.ID, rr, b.ReadRev) |
| 263 | } |
| 264 | } |
| 265 | } |
| 266 | return "" |
| 267 | } |
| 268 | |
| 269 | // tableStale says why b's table must be empty, or "". |
| 270 | func (w *world) tableStale(b *box) string { |
| 271 | m, now := b.Mirror, w.now() |
| 272 | switch { |
| 273 | case m.Rec == nil: |
| 274 | return "was never read" |
| 275 | case now >= m.Rec.Expires: |
| 276 | return fmt.Sprintf("holds revision %d, expired at %d, now %d", m.Rec.Rev, m.Rec.Expires, now) |
| 277 | case now-m.ReadAt >= staleTicks: |
| 278 | return fmt.Sprintf("has had no good read for %d ticks", now-m.ReadAt) |
| 279 | case now-m.Rec.SignedAt >= staleTicks: |
| 280 | return fmt.Sprintf("holds revision %d, signed at %d, %d ticks ago", m.Rec.Rev, m.Rec.SignedAt, now-m.Rec.SignedAt) |
| 281 | } |
| 282 | return "" |
| 283 | } |
| 284 | |
| 285 | func procID(p *proc) any { |
| 286 | if p == nil { |
| 287 | return "none" |
| 288 | } |
| 289 | return p.ID |
| 290 | } |
| 291 | |
| 292 | // INV-ARM (state): no unisolated tenant process exists on a box while an |
| 293 | // engine socket is open there. check() runs it. |
| 294 | func (w *world) checkArm() { |
| 295 | for _, b := range w.boxes { |
| 296 | if !b.Sockets { |
| 297 | continue |
| 298 | } |
| 299 | for _, p := range b.Procs { |
| 300 | if p.Unisolated { |
| 301 | w.fail("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) |
| 302 | } |
| 303 | } |
| 304 | } |
| 305 | } |
| 306 | |
| 307 | // residual records the stated residual name once: "residual:<name>: ...". |
| 308 | func (w *world) residual(name, format string, args ...any) { |
| 309 | for _, r := range w.residuals { |
| 310 | if strings.HasPrefix(r, "residual:"+name+":") { |
| 311 | return |
| 312 | } |
| 313 | } |
| 314 | w.residuals = append(w.residuals, "residual:"+name+": "+fmt.Sprintf(format, args...)) |
| 315 | w.logf("residual:%s recorded", name) |
| 316 | } |
| 317 | |
| 318 | // failProc is fail for a breach process p on b causes. It records the stated |
| 319 | // residual p belongs to instead only when the breach is the residual's own: |
| 320 | // viaClassification says the breach came by a path the upgrade's 0 opened |
| 321 | // (I1 itself, the edge serving the group, a ports listener rendered for a |
| 322 | // public group), and the residual's window still holds (residualHolds). Any |
| 323 | // other breach of a tagged process is a violation. |
| 324 | func (w *world) failProc(b *box, p *proc, inv string, viaClassification bool, format string, args ...any) { |
| 325 | if viaClassification && w.residualHolds(b, p) { |
| 326 | w.residual(p.Residual, inv+": "+format, args...) |
| 327 | return |
| 328 | } |
| 329 | w.fail(inv, format, args...) |
| 330 | } |
| 331 | |
| 332 | // residualHolds: p is tagged with the unwritten-manifest residual and its |
| 333 | // group is still open, as the upgrade classified it. The window ends for good |
| 334 | // the first time the group is closed again (a grant, a gate's 1): the tag is |
| 335 | // cleared, so a later 0 (another rule's failure) is never misfiled as the |
| 336 | // upgrade's. |
| 337 | func (w *world) residualHolds(b *box, p *proc) bool { |
| 338 | if p == nil || p.Residual == "" { |
| 339 | return false |
| 340 | } |
| 341 | if w.closed(b, p.Group) { |
| 342 | w.logf("box%d: %s is closed again: process %d's residual window (%s) ends", b.ID, p.Group, p.ID, p.Residual) |
| 343 | p.Residual = "" |
| 344 | return false |
| 345 | } |
| 346 | return true |
| 347 | } |
| 348 | |
| 349 | // endResidualWindows runs residualHolds on every tagged process, so a window |
| 350 | // ends when its group closes even if nothing breaches meanwhile. |
| 351 | func (w *world) endResidualWindows() { |
| 352 | for _, b := range w.boxes { |
| 353 | for _, p := range b.Procs { |
| 354 | if p.Residual != "" { |
| 355 | w.residualHolds(b, p) |
| 356 | } |
| 357 | } |
| 358 | } |
| 359 | } |
| 360 | |
amadan