From 84d03bce7244fa27aaffa43ebb4dc55e8fdaf3c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 22:43:49 +0000 Subject: [PATCH 01/19] Add verification plan for prepareSCMP (dropping the TODO()) Analyzes whether Mem(ubuf) can be established for the layers passed to gopacket.SerializeLayers in prepareSCMP (it cannot, for any buffer, with the current predicate definitions) and lays out a nil-buffer 'serialize-mode' predicate design, the required SerializeTo/interface spec changes (FixLengths, error-case preservation, checksum permission accounting), a route to derive !IsSupportedPkt(result), and milestones. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 501 ++++++++++++++++++++++++++++++++ 1 file changed, 501 insertions(+) create mode 100644 doc/verification/prepareSCMP.md diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md new file mode 100644 index 000000000..076ea1616 --- /dev/null +++ b/doc/verification/prepareSCMP.md @@ -0,0 +1,501 @@ +# Plan: verifying `prepareSCMP` completely (dropping the `TODO()`) + +This document analyzes what it takes to remove the `TODO()` at +`router/dataplane.go:5064` and verify the remainder of +`scionPacketProcessor.prepareSCMP`, i.e., the construction of the SCMP reply +(`scionL`, `scmpH`, `scmpP`, quote) and the call + +```go +err = gopacket.SerializeLayers(p.buffer, sopts /*@ , nil @*/, scmpLayers...) +``` + +whose current specification in +`verification/dependencies/github.com/google/gopacket/writer.gobra` is +`requires false`. + +The immediate question that motivated this document: **`SerializeLayers` +requires `layers[i].Mem(layerBufs[i])` for every layer — can we establish +`Mem` for all elements of `scmpLayers`, possibly with a `nil` underlying +buffer?** + +--- + +## 1. Answer to the `Mem` question + +**Short answer: no — not with the current predicate definitions, and not for +any choice of buffer, `nil` or otherwise.** For three of the four layers the +*state* of a freshly constructed layer contradicts the predicate body, so no +choice of the `ubuf` argument can make the fold succeed. The predicates were +designed for *decoded* layers (established by `DecodeFromBytes`, which ties +`Contents`/`Payload` to sub-slices of the input buffer); a fresh, about-to-be- +serialized layer has no underlying buffer yet. + +However, the predicates can be *generalized* with a `nil`-buffer +("serialize-only") mode, and the codebase already contains all the precedents +needed to do this (see §3). The `(VerifiedSCION) TODO: adapt *SCION.Mem(...)` +comment at `router/dataplane.go:5068` anticipates exactly this. + +### 1.1 Per-layer analysis + +`scmpLayers = []gopacket.SerializableLayer{&scionL, &scmpH, scmpP}` plus, +when `cause != nil`, `gopacket.Payload(quote)`. + +| Layer | `Mem(nil)` foldable? | `Mem(ub)` foldable for some `ub != nil`? | Blocking conjuncts | +|---|---|---|---| +| `gopacket.Payload(quote)` | n/a | **yes**, with `ub := quote` | none — body is `ub === p` (`base.gobra:36`) | +| `scmpP` (e.g. `*SCMPParameterProblem`) | **no** | **no** | `BaseLayer.Mem(ub, 4)` (`scmp_msg_spec.gobra:125`) | +| `&scmpH` (`*SCMP`) | **no** | **no** | `BaseLayer.Mem(ub, 4)` (`scmp_spec.gobra:37`) | +| `&scionL` (`*SCION`) | **no** | **no** | several, see below (`scion_spec.gobra:149`) | + +**Why `BaseLayer.Mem` kills `scmpH`/`scmpP` for every buffer.** The body of +`BaseLayer.Mem(ub, breakPoint)` (`pkg/slayers/scion_spec.gobra:244`) is + +```gobra +0 <= breakPoint && breakPoint <= len(ub) && +acc(b) && +b.Contents === ub[:breakPoint] && +b.Payload === ub[breakPoint:] +``` + +with `breakPoint = 4` (or larger constants for the other SCMP messages): + +* `ub == nil`: `4 <= len(nil) = 0` is false. Fold fails on arithmetic alone. +* `ub != nil`: a fresh `slayers.SCMP{TypeCode: typeCode}` has + `Contents == nil` (length 0). `ub[:4]` has length 4, and `===` on slices + implies equal lengths, so `Contents === ub[:4]` is unsatisfiable. No ghost + code can fix this: `Contents` is a real field and only real code (i.e., + `DecodeFromBytes`, or the serialization itself) assigns it. + +**Why `*SCION.Mem` fails additionally.** For the freshly constructed +`scionL` in `prepareSCMP` (fields assigned at `router/dataplane.go:5067-5085`): + +* `s.HdrLen == 0` — it is only ever assigned inside `SerializeTo`'s + `opts.FixLengths` branch (`pkg/slayers/scion.go:246-250`), which is + currently dead (`Unreachable()`). Hence + `CmnHdrLen + s.AddrHdrLenSpecInternal() <= int(s.HdrLen)*LineLen` + (`scion_spec.gobra:163`) reads `12 + (≥24) <= 0` — false. This is circular: + `Mem` (as-is) can only hold *after* the serialization that requires it. +* `CmnHdrLen <= len(ubuf)` fails for `ubuf == nil`. +* `s.HeaderMem(ubuf[CmnHdrLen:])` requires `RawDstAddr`/`RawSrcAddr` to be + sub-slices of `ubuf`; after `SetDstAddr`/`SetSrcAddr` + (`router/dataplane.go:5079-5084`) they alias the *request packet's* buffer + (`srcA` comes from `p.scionLayer`) and `p.d.internalIP` respectively — not + any single fresh buffer. +* `s.Path.Mem(ubuf[CmnHdrLen+...:HdrLen*LineLen])` ties the path's resources + to a sub-slice of the same `ubuf`, but we hold `revPath.Mem(rawPath)` where + `rawPath` is a region of the original packet `ub`. + +### 1.2 The experiment (what "try it" boils down to) + +The negative results above are decidable by inspection (linear arithmetic +over slice lengths plus `===`-injectivity); a Gobra run is not needed to +refute them, but the following snippets make the attempts concrete. The first +three folds fail, the last two succeed: + +```gobra +// context: fresh layers as in prepareSCMP +var scionL slayers.SCION // + field assignments as in prepareSCMP +scmpH := slayers.SCMP{TypeCode: typeCode} + +fold scmpH.BaseLayer.Mem(nil, 4) // FAILS: 4 <= len(nil) +fold scmpH.BaseLayer.Mem(big, 4) // FAILS: scmpH.Contents === big[:4] + // (nil vs. length-4 slice) +fold scionL.Mem(nil) // FAILS: CmnHdrLen <= len(nil), and + // 12 + AddrHdrLen <= HdrLen*LineLen = 0 + +fold gopacket.Payload(quote).Mem(quote) // OK: body is `quote === quote` + +unfold revPath.Mem(rawPath) // OK: *scion.Decoded's Mem body +fold revPath.Mem(nil) // never mentions ubuf (see §3) +``` + +(These snippets cannot live in a `*_test.gobra` file in-tree, because the +failing folds would fail CI; run them ad hoc when validating this plan. +Note that `pkg/slayers` CI verification takes ~25 min per run, +`.github/workflows/gobra.yml:214-234`.) + +--- + +## 2. Full inventory of blockers between `TODO()` and `return` + +Removing `TODO()` requires all of the following, not just the `Mem` folds: + +1. **`SerializeLayers` has no usable spec** (`writer.gobra:105-112`, + `requires false`, with the note "requires changes to provide access to the + underlying layers"). The ghost `layerBufs` parameter already exists; the + call site passes `nil` as a placeholder. +2. **The `SerializableLayer` interface forbids `FixLengths`** + (`writer.gobra:18`: `requires !opts.FixLengths`), but `prepareSCMP` uses + `SerializeOptions{ComputeChecksums: true, FixLengths: true}`. + Correspondingly, `(*SCION).SerializeTo`'s `FixLengths` branch is marked + `Unreachable()` (`scion.go:246-250`) and must now be verified: it *writes* + `s.HdrLen` and `s.PayloadLen`, so it needs write permission to those + fields (the current spec takes only `acc(s.Mem(ubuf), R0)`), and the + `uint8`/`uint16` casts need justified bounds. +3. **`SerializeTo` loses `Mem` on error** (interface post: + `err == nil ==> Mem(ubuf) && b.Mem()`). `prepareSCMP`'s error path must + still restore `sl.Bytes(ub, ...)` and `p.buffer.Mem()` to satisfy its own + postconditions, and the fractions of `ub` carved into the fresh layers' + predicates would be lost. The implementations (`SCMP.SerializeTo`, + the SCMP messages) already re-fold `Mem` on every error path, so the + interface can be strengthened to `preserves`-style without new proof work + in the bodies. +4. **Double demand on `scionL`'s address bytes.** + `scmpH.Mem(...)` contains `s.scn != nil ==> s.scn.ChecksumMem()` + (`scmp_spec.gobra:34-40`), and after + `scmpH.SetNetworkLayerForChecksum(&scionL)` (`dataplane.go:5089`), + `s.scn == &scionL`. `ChecksumMem` (`scion_spec.gobra:236-242`) holds + *full* `acc(&s.RawSrcAddr)`, `acc(&s.RawDstAddr)` and *full* + `sl.Bytes(...)` of both — while a serialize-mode `scionL.Mem(nil)` also + needs (at least read) access to the same locations for + `SerializeAddrHdr`. Both predicates must coexist inside the + `SerializeLayers` call, so the permission amounts must be split + (fractions), or the bytes moved into exactly one of the two. +5. **`p.d.internalIP` is only available at wildcard permission.** + The processor holds `acc(p.d.Mem(), _)`, so the bytes of + `p.d.internalIP` (used by `SetSrcAddr(&net.IPAddr{IP: p.d.internalIP})`, + `dataplane.go:5082`) can only ever be obtained at wildcard amount. A + predicate that stores a *concrete* fraction of `RawSrcAddr`'s bytes is + therefore unfoldable here, and a wildcard-typed requires clause is lossy + for the *other* address (whose bytes come from `ub` and must be returned + at full permission). See §4.3 for the options. +6. **Missing frame in `prepareSCMP`'s own spec**: no permissions for + `p.rawPkt` (read at `dataplane.go:5110` for the quote), no resources for + `scmpP` (the spec at `dataplane.go:4900-4919` does not mention it at + all), and the same for `packSCMP` (`dataplane.go:2181`) and its ~9 call + sites, which construct `scmpP` as fresh literals + (e.g. `&slayers.SCMPParameterProblem{...}`, `dataplane.go:2422`). +7. **The IO-level postcondition** `result != nil ==> + !slayers.IsSupportedPkt(result)` (`dataplane.go:4917-4918`) is currently + assumed via the `TODO()`. It must be *derived* from serialization. The + existing mechanism (`scion.go:225-226`: + `IsSupportedRawPkt(b.View()) == old(IsSupportedPkt(ubuf))`) is unusable + here because there is no meaningful old buffer; a new route is needed + (§4.6). Note `IsSupportedPkt` (`scion_spec.gobra:503-509`) is simply + "path type is `scion.PathType` **and** `NextHdr != L4SCMP`" over the raw + bytes — and `prepareSCMP` sets `scionL.NextHdr = slayers.L4SCMP`, so the + packet is unsupported by construction; we only need the specs to carry + the fact that byte 4 of the output equals `uint8(s.NextHdr)`. +8. **Misc**: `fold`ing `scmpError`'s `ErrorMem` for the success-with-error + return (`dataplane.go:5122`), bounds for the `hdrLen` computation + (`dataplane.go:5101-5109`, calling `AddrHdrLen(nil, false)` and + `Path.Len(nil)` on the *fresh* layer — consistent with the `nil`-mode + design below), and re-establishing `sl.Bytes(ub, 0, len(ub))` by + recombining all split ranges on every path. + +--- + +## 3. Enabling observations (why a `nil`-mode design works) + +1. **`(*scion.Decoded).Mem(ubuf)` never mentions `ubuf`** + (`pkg/slayers/path/scion/decoded_spec.gobra:39-48`): it holds + `Base.Mem()`, `InfoFields`, `HopFields` — all struct-internal. Hence + `revPath.Mem(rawPath)` can be re-folded as `revPath.Mem(nil)` by a + trivial (un)fold pair, and `(*Decoded).SerializeTo(b, ubuf)` + (`decoded.go:128-133`) as well as `Len(ubuf)` already work fine with + `ubuf = nil` (`sl.Bytes(nil, 0, 0)` is trivially foldable — precedent in + `packSCMP`, `dataplane.go:2206`). **The reversed path is already fully + buffer-independent.** +2. **`Mem(nil)` is an established idiom**: `empty.Path` + (`pkg/slayers/path/empty/empty_spec_test.gobra:26`), and `decodeLayers`' + postconditions explicitly produce `opts[i].Mem(nil)` for nil payloads + (`dataplane.go:5159-5160`). Using `ubuf == nil` as the discriminator for + "fresh / serialize-only" is consistent with existing usage. +3. **The set of `SerializableLayer` implementations is small and closed**: + `*SCION`, `*SCMP`, the seven `SCMP*` message types, `gopacket.Payload`, + and the trusted stub `*layers.BFD`. The extension layers do *not* + implement it (`extn_spec.gobra:163` is commented out; their `SerializeTo` + is `requires false` and lacks the ghost parameter). Interface-spec + changes therefore have a bounded, known ripple. +4. **The SCMP message `SerializeTo` bodies never touch `BaseLayer`** — they + read the semantic fields (`Pointer`, `Identifier`, ...) and write into + prepended buffer space. Their proofs survive a weakened `BaseLayer` + conjunct essentially unchanged. The same holds for `SCMP.SerializeTo`. + +--- + +## 4. Proposed design + +### 4.1 `nil`-mode `BaseLayer.Mem` (one change, many beneficiaries) + +Redefine (`scion_spec.gobra:244`): + +```gobra +pred (b *BaseLayer) Mem(ghost ub []byte, ghost breakPoint int) { + acc(b) && + (ub != nil ==> (0 <= breakPoint && breakPoint <= len(ub) && + b.Contents === ub[:breakPoint] && + b.Payload === ub[breakPoint:])) +} +``` + +Consequences: + +* `Mem(nil)` becomes foldable for **fresh** `SCMP` and all seven SCMP + message types with zero changes to their own predicate bodies. +* All *decoded* contexts keep working: wherever the aliasing facts are used, + `len(data) >= 4` (or similar) is in scope, which implies `data != nil`. +* `LayerPayload(ghost ub)`-style specs that unconditionally state + `res === ub[start:end]` need either a `ub != nil` precondition or a + weakened (conditional) postcondition, matching the `gopacket.Layer` + interface, which is already conditional (`base.gobra:28-29`). + Fresh layers never have `LayerPayload` called on them in verified code. + +### 4.2 Serialize-mode `*SCION.Mem` + +Split the body of `(*SCION).Mem(ubuf)` (`scion_spec.gobra:149-187`) into + +* unconditional field permissions (as today, incl. the path-pool clauses, + `acc(&s.Path)`, `s.Path != nil`), and +* `ubuf != nil ==> (` all current buffer-dependent conjuncts: length bounds, + `Path.Mem(ubuf[...])`, `BaseLayer` ties, `HeaderMem(ubuf[CmnHdrLen:])`, + one-hop clause `)`, and +* `ubuf == nil ==> (` serialize-mode: + `s.Path.Mem(nil)` + + `acc(&s.RawDstAddr)/acc(&s.RawSrcAddr)` + + length agreement `len(s.RawDstAddr) == s.DstAddrType.Length()` (and src + analogously) + byte permissions for the two raw addresses (amounts: §4.3) + `)`. + +Notes: + +* In serialize mode `HdrLen`/`PayloadLen` are deliberately unconstrained — + the `FixLengths` branch assigns them. +* The `HalfPerm` split of `DstAddrType`/`SrcAddrType` between `Mem` and + `HeaderMem` must be revisited: in serialize mode `HeaderMem` is absent, so + the other halves belong directly to the `ubuf == nil` branch. +* `ValidPathMetaData`, `EqAbsHeader`, etc. are decoded-mode notions; guard + their `unfolding`s with `ub != nil` where needed. + +### 4.3 `ChecksumMem` and the address-byte permission accounting + +Constraints discovered in §2 (items 4, 5): + +* `scionL.Mem(nil)` (for `SerializeAddrHdr`) and + `ChecksumMem(scionL)` inside `scmpH.Mem(nil)` (for `computeChecksum`) + must **coexist**; both only read the raw address bytes. +* `RawDstAddr` bytes come (via `SrcAddr()`) from `ub` — held at **full, + concrete** permission by `prepareSCMP`, which must return them at full + permission. So every predicate touching them must use *concrete* + fractions (wildcards are lossy: once a wildcard is exhaled from a + concrete amount, full recovery is unprovable). +* `RawSrcAddr` bytes come from `p.d.internalIP` — available **only at + wildcard** (`acc(p.d.Mem(), _)`), so no concrete fraction of them can + ever be folded. + +Two workable resolutions: + +* **(a) Copy the internal IP (recommended).** Change + `dataplane.go:5082` to pass a fresh copy of `p.d.internalIP` (a marked + `(VerifiedSCION)` deviation; one small allocation on the SCMP error + path — cf. the precedent of changed signatures at `dataplane.go:4774-4777`). + Then both raw addresses are backed by permissions `prepareSCMP` fully + controls, and the design is symmetric: give `ChecksumMem` and the + serialize-mode branch of `SCION.Mem` complementary concrete fractions + (e.g. `R50` each) of `sl.Bytes(RawSrcAddr)/sl.Bytes(RawDstAddr)`. + `ChecksumMem`'s only verified users are `prepareSCMP`, + `SCMP.SerializeTo`/`computeChecksum`, and the `SCMP` predicates + (`SetNetworkLayerForChecksum` is called nowhere else in verified code), + so re-fractioning it is low-ripple. Its `len % 2 == 0` conjuncts follow + from `AddrType.Length() ∈ {4, 8, 12, 16}` (small lemma). +* **(b) Asymmetric predicates.** Keep the code unchanged and bake the + asymmetry in: serialize-mode holds + `acc(sl.Bytes(s.RawDstAddr, ...), R50)` but + `acc(sl.Bytes(s.RawSrcAddr, ...), _)`. Works, but hard-codes + `prepareSCMP`'s aliasing situation into `pkg/slayers` and will not fit + the BFD sender (§8) whose source address has yet another origin. Not + recommended. + +### 4.4 `SerializeTo` spec changes (interface + implementations) + +In `writer.gobra`'s `SerializableLayer`: + +```gobra +requires opts.FixLengths ==> ubuf == nil // was: !opts.FixLengths +requires b != nil && b.Mem() +requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) +requires Mem(ubuf) +preserves sl.Bytes(ubuf, 0, len(ubuf)) +ensures Mem(ubuf) && b.Mem() // was: only on err == nil +ensures sl.Bytes(b.UBuf(), 0, len(b.UBuf())) +ensures err != nil ==> err.ErrorMem() +``` + +* Conditioning `FixLengths` on `ubuf == nil` protects all decoded-mode + callers/proofs (nothing changes for them) while permitting exactly the + fresh-layer case. Implementations must now verify their `FixLengths` + behavior only under serialize mode. +* The unconditional `Mem`/`b.Mem()` in the post is provable for `SCMP` and + the message types as-is (their bodies already re-fold on all error paths); + `Payload` and `layers.BFD` are trusted stubs to adjust textually. +* `(*SCION).SerializeTo` (`scion.go:212-228`) gets a mode-split spec: + `ubuf != nil ==> acc(s.Mem(ubuf), R0)` (as today) and + `ubuf == nil ==> s.Mem(nil)` (full — the `FixLengths` branch writes + `HdrLen`/`PayloadLen`). The body needs: + * `pathSlice := ubuf == nil ? nil : ubuf[startP:endP]` ghost branching + for the `Path.Len`/`Path.SerializeTo` calls (both already fine with + `nil`, §3.1); + * a serialize-mode variant of `SerializeAddrHdr`'s spec (address bytes + from the predicate instead of `ubuf`); + * verification of the `FixLengths` branch: `uint8(scnLen/LineLen)` is + bounded by the existing `scnLen <= MaxHdrLen` check; + `uint16(len(b.Bytes()) - scnLen)` needs a precondition bounding the + buffer contents (e.g. `ubuf == nil ==> len(b.UBuf()) + scnLen <= 0xffff`), + dischargeable at the call site because the buffer was `Clear()`ed and + the prepends are bounded by `MaxSCMPPacketLen` (1232) via the quote + truncation (`dataplane.go:5111-5114`); + * the new IO postcondition (§4.6). + +### 4.5 `SerializeLayers`: trusted quantified spec vs. direct calls + +**Option A — keep the call, write a trusted quantified spec** (fill in the +existing skeleton in `writer.gobra:105-112` with per-layer `layerBufs`, +pairwise-distinctness like `decodeLayers`, `Mem(layerBufs[i])` + +`sl.Bytes(layerBufs[i], ...)` preserved for all `i`). This is sound and +straightforward, **but it cannot deliver item 7 (§2)**: `gopacket` cannot +import `slayers` (dependency direction), so no `SerializeLayers` post can +mention `NextHdr`/`IsSupportedPkt`, and the `SerializableLayer` interface +has no abstraction through which the output bytes' provenance can be +stated generically. The IO fact would need a localized `assume` — i.e., the +`TODO()` merely shrinks instead of disappearing. + +**Option B — inline the serialization in `prepareSCMP` (recommended).** +Replace the single call with the equivalent reverse-order sequence (a +marked `(VerifiedSCION)` change; `p.buffer.Clear()` already happens at +`dataplane.go:5091`, and the skipped `PushLayer` bookkeeping is +unobservable — `Layers()` is never called in the router and is +`requires false` in the spec): + +```go +// gopacket.SerializeLayers(p.buffer, sopts, scmpLayers...) is equivalent to: +for i := len(scmpLayers) - 1; i >= 0; i-- { // or fully unrolled + if err := scmpLayers[i].SerializeTo(p.buffer, sopts /*@, layerBuf(i) @*/); err != nil { ... } +} +``` + +Unrolling fully is preferable for the proof: the `&scionL` and `&scmpH` +calls become *concrete* method calls (using `(*SCION).SerializeTo`'s +own, richer spec — including the IO postcondition and the mode-split +permission amounts, neither of which fits through the interface), +while `scmpP` and the payload still go through the interface with +`Mem(nil)` / `Mem(quote)`. As a bonus, `*SCION` no longer *needs* to +satisfy the (relaxed) `SerializableLayer` interface, though with the +mode-split spec of §4.4 it still can. + +`bfdSend.Send` (`dataplane.go:4891`) can later adopt the same pattern (§8). + +### 4.6 Deriving `!IsSupportedPkt(result)` + +Add to `(*SCION).SerializeTo` a serialize-mode postcondition, e.g.: + +```gobra +ensures e == nil && ubuf == nil ==> + IsSupportedRawPkt(b.View()) == + (s.PathType == scion.PathType && s.NextHdr != L4SCMP) +``` + +This is provable in the body: the common-header write +(`buf[4] = uint8(s.NextHdr)`, `buf[8] = uint8(s.PathType)`, +`scion.go:258-262`) determines exactly the two bytes `IsSupportedRawPkt` +inspects, and the subsequent `SerializeAddrHdr`/`Path.SerializeTo` calls only +touch offsets ≥ `CmnHdrLen` (the existing `IsSupportedPktSubslice` lemma +machinery, `scion_spec.gobra:522-534`, already frames this). + +In `prepareSCMP`: since SCION is serialized **last** (prepended at the +front), the buffer state at its return *is* the final state; +`scionL.NextHdr == L4SCMP` gives `!IsSupportedRawPkt(b.View())`; a small +lemma `IsSupportedRawPkt(b.View()) == IsSupportedPkt(b.UBuf())` +(`View() == seqs.ToSeqByte(UBuf())` by the `SerializeBuffer` spec, +`writer.gobra:48-54`; both functions read bytes 4 and 8) transports it to +`!IsSupportedPkt(p.buffer.UBuf())`, and `Bytes()` (`writer.gobra:56-59`) +gives `result === p.buffer.UBuf()`. This mirrors the existing pattern in +`updateSCIONLayer` (`dataplane.go:4784-4789`), just sourced from field +values instead of `old(IsSupportedPkt(rawPkt))`. + +--- + +## 5. Changes to `prepareSCMP` / `packSCMP` and call sites + +* **Preconditions to add** (`prepareSCMP`, and threaded through + `packSCMP` + its ~9 call sites): + * `scmpP != nil && scmpP.Mem(nil)` — foldable at each construction site, + where the literal's field permissions are freshly available (e.g. + `dataplane.go:2422`); with §4.1 this is a one-line `fold` per site. + * `acc(&p.rawPkt, R55)` and the relation between `p.rawPkt` and `ub` + (they are the same slice in all callers) so the quote's + `Payload.Mem(quote)`/`sl.Bytes(quote, ...)` can be carved out of + `sl.Bytes(ub, ...)` and recombined afterwards. +* **Proof work in the body (post-`TODO()` region)**: + 1. re-fold `revPath.Mem(rawPath)` → `revPath.Mem(nil)`; + 2. fold serialize-mode `scionL.Mem(nil)` after the field assignments and + `Set{Dst,Src}Addr` calls (the `SetSrcAddr` ghost argument and/or code + adapted per §4.3); fold `ChecksumMem(scionL)` and then + `scmpH.Mem(nil)` after `SetNetworkLayerForChecksum`; + 3. discharge the `hdrLen` computation (`AddrHdrLen(nil, ...)`, + `Path.Len(nil)` through pure helper functions over `Mem(nil)`), and + the `MaxSCMPPacketLen` bound for §4.4's buffer-size precondition; + 4. serialization calls per §4.5 Option B, restoring all predicates on + both success and error paths (possible thanks to the strengthened + error postconditions, §4.4); + 5. at the end: unfold the fresh layers' predicates (they die with the + function), apply the `SrcAddr()` magic wand, recombine all `ub` + ranges to return `sl.Bytes(ub, 0, len(ub))` and + `acc(p.scionLayer.Mem(ub), R4)`; + 6. fold `ErrorMem` for `scmpError{...}` and conclude the + `!IsSupportedPkt(result)` post per §4.6. + +--- + +## 6. Milestones + +Ordered so that each step keeps CI green (`pkg/slayers` ≈ 25 min, +`pkg/slayers/path/scion` ≈ 30 min, `router` ≈ up to 6 h per CI run — +budget accordingly; perf regressions in `dataplane.go` are a real risk). + +1. **M1 — `BaseLayer.Mem` nil-mode** (§4.1) + adapt `SCMP`/message-type + proofs and `LayerPayload` specs. Small/medium; contained in + `pkg/slayers`. +2. **M2 — serialize-mode `*SCION.Mem`** (§4.2) + `ChecksumMem` + re-fractioning and the address-permission decision (§4.3). Medium; + touches many `SCION` lemmas' guards (`ub != nil`). +3. **M3 — `(*SCION).SerializeTo`**: mode-split spec, `SerializeAddrHdr` + serialize-mode, verify the `FixLengths` branch (bounds!), add the §4.6 + postcondition. This is the hardest single item. Large. +4. **M4 — interface updates** in `writer.gobra` (§4.4) + re-verify the + closed set of implementers; adjust the `Payload`/`BFD` trusted stubs. + Small/medium. +5. **M5 — `prepareSCMP` itself** (§5): spec extensions, call-site folds, + inlined serialization (§4.5 B), drop the `TODO()`. Large, but mostly + mechanical once M1–M4 are in; expect iteration on router CI time. +6. **M6 — cleanup**: remove `Unreachable()` from the `FixLengths` branch, + revisit `bfdSend` (§8), document the serialize-mode idiom. + +## 7. Risks / open points + +* **Verification time** of `dataplane.go` (already the 6 h/`chop 10` + package). Mitigate with `outline(...)` blocks and `opaque` helper + functions for the new fold-heavy regions. +* **`FixLengths` overflow bounds** require threading a buffer-size bound + through a *trusted-interface* boundary (`SerializeBuffer` is a trusted + spec); double-check `PrependBytes`' postconditions suffice to track + `len(UBuf())` across the four prepends. +* **Gobra interface-implementation proofs** with mode-split permission + amounts (`ubuf == nil ? full : R0`) are unusual; if the implementation + proof for `*SCION` becomes brittle, fall back to dropping + `*SCION implements gopacket.SerializableLayer` (safe under §4.5 B since + the only interface-dispatched uses are `scmpP` and the payload). +* **`SrcAddr()`/`SetDstAddr` aliasing**: the `RawDstAddr` fraction + originates from `acc(p.scionLayer.Mem(ub), R4)`-governed memory via a + magic wand; getting the fraction arithmetic right (so that the wand can + be applied at exit) needs care, but has precedent (`addEndhostPort`, + `dataplane.go:4734-4755`). + +## 8. Side benefit + +The same serialize-mode machinery is exactly what +`newBFDSend`/`bfdSend.Send` (`dataplane.go:4817-4898`, currently +`trusted` / `requires false`) need: fresh `SCION` layer, `FixLengths: true`, +`SerializeLayers` with a fresh `layers.BFD`. M1–M4 unlock that verification +almost for free (the BFD layer's spec is a trusted stub in +`verification/dependencies`), with `empty.Path`/`onehop.Path` (both already +`Mem(nil)`-friendly or buffer-light) instead of `scion.Decoded`. From 2aac6cb2c8a343d9f8179152efc0cb14f8286be9 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Jul 2026 00:20:35 +0000 Subject: [PATCH 02/19] Rework prepareSCMP plan for the annotations-only constraint Executable Go code cannot change, so: keep the gopacket.SerializeLayers call and give it a trusted quantified spec; derive !IsSupportedPkt via a ghost pure hook on the SerializableLayer interface plus a gopacket-level IsSupportedRawPkt twin and bridging lemma; handle the internalIP wildcard problem with asymmetric permission amounts in the serialize-mode predicates (SetSrcAddr switched to wildcard mode via its ghost argument) and strengthened SetDstAddr/SetSrcAddr postconditions. Drop the overflow-bound concern (CI runs with overflow checking disabled). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 360 ++++++++++++++++++++++---------- 1 file changed, 248 insertions(+), 112 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index 076ea1616..db64396bd 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -1,5 +1,13 @@ # Plan: verifying `prepareSCMP` completely (dropping the `TODO()`) +**Ground rule for this plan: the executable Go code cannot be changed.** +Everything below is confined to specifications, predicates, ghost +annotations/arguments (including those embedded in `.go` files as `// @` +comments), `.gobra` files, and the trusted stubs under +`verification/dependencies`. In particular, the +`gopacket.SerializeLayers` call stays, and `p.d.internalIP` is passed to +`SetSrcAddr` as-is. + This document analyzes what it takes to remove the `TODO()` at `router/dataplane.go:5064` and verify the remainder of `scionPacketProcessor.prepareSCMP`, i.e., the construction of the SCMP reply @@ -130,8 +138,11 @@ Removing `TODO()` requires all of the following, not just the `Mem` folds: Correspondingly, `(*SCION).SerializeTo`'s `FixLengths` branch is marked `Unreachable()` (`scion.go:246-250`) and must now be verified: it *writes* `s.HdrLen` and `s.PayloadLen`, so it needs write permission to those - fields (the current spec takes only `acc(s.Mem(ubuf), R0)`), and the - `uint8`/`uint16` casts need justified bounds. + fields (the current spec takes only `acc(s.Mem(ubuf), R0)`). (The + `uint8`/`uint16` casts in that branch generate no proof obligations — + CI runs with `overflow: '0'`, `.github/workflows/gobra.yml:32` — so no + buffer-size bound needs to be threaded through the trusted + `SerializeBuffer` interface.) 3. **`SerializeTo` loses `Mem` on error** (interface post: `err == nil ==> Mem(ubuf) && b.Mem()`). `prepareSCMP`'s error path must still restore `sl.Bytes(ub, ...)` and `p.buffer.Mem()` to satisfy its own @@ -283,28 +294,66 @@ Constraints discovered in §2 (items 4, 5): wildcard** (`acc(p.d.Mem(), _)`), so no concrete fraction of them can ever be folded. -Two workable resolutions: - -* **(a) Copy the internal IP (recommended).** Change - `dataplane.go:5082` to pass a fresh copy of `p.d.internalIP` (a marked - `(VerifiedSCION)` deviation; one small allocation on the SCMP error - path — cf. the precedent of changed signatures at `dataplane.go:4774-4777`). - Then both raw addresses are backed by permissions `prepareSCMP` fully - controls, and the design is symmetric: give `ChecksumMem` and the - serialize-mode branch of `SCION.Mem` complementary concrete fractions - (e.g. `R50` each) of `sl.Bytes(RawSrcAddr)/sl.Bytes(RawDstAddr)`. - `ChecksumMem`'s only verified users are `prepareSCMP`, +Since the code cannot change (no copying of `p.d.internalIP`), the +**asymmetric-fractions design is the only option**: the serialize-mode +predicates must hold the two address-byte resources at *different* amounts, +matching where they come from: + +* `RawDstAddr` (aliases the request packet / `srcA`): **concrete + fraction** (e.g. `R50`), because `prepareSCMP` must hand back + `sl.Bytes(ub, 0, len(ub))` at full permission and wildcards are + unrecoverable. +* `RawSrcAddr` (aliases `p.d.internalIP`): **wildcard** (`acc(..., _)`), + because wildcard is all the processor ever has of `d`'s state. + +Concretely: + +* Serialize-mode branch of `SCION.Mem(nil)` (§4.2) holds + `acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R50)` and + `acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)`; + `ChecksumMem` is re-declared with complementary amounts (e.g. the + other `R50` half for dst, another wildcard for src, and *fractional* + `acc(&s.RawSrcAddr, ...)`/`acc(&s.RawDstAddr, ...)` field permissions + instead of today's full ones). Both users only read, so fractions + suffice. `ChecksumMem`'s only verified users are `prepareSCMP`, `SCMP.SerializeTo`/`computeChecksum`, and the `SCMP` predicates (`SetNetworkLayerForChecksum` is called nowhere else in verified code), - so re-fractioning it is low-ripple. Its `len % 2 == 0` conjuncts follow + so re-fractioning is low-ripple. Its `len % 2 == 0` conjuncts follow from `AddrType.Length() ∈ {4, 8, 12, 16}` (small lemma). -* **(b) Asymmetric predicates.** Keep the code unchanged and bake the - asymmetry in: serialize-mode holds - `acc(sl.Bytes(s.RawDstAddr, ...), R50)` but - `acc(sl.Bytes(s.RawSrcAddr, ...), _)`. Works, but hard-codes - `prepareSCMP`'s aliasing situation into `pkg/slayers` and will not fit - the BFD sender (§8) whose source address has yet another origin. Not - recommended. + Wildcard amounts inside predicate bodies should be confirmed early with + a smoke test (see risk §7). +* **`SetSrcAddr` must be called in wildcard mode**: the ghost argument at + `dataplane.go:5082` changes from `false` to `true` (a ghost-only edit). + Its wildcard-mode postcondition + (`scion.go:710`: `acc(sl.Bytes(s.RawSrcAddr, ...), _)`) is exactly what + the predicate above needs. Two sub-issues to resolve on the way: + * the wildcard-mode *pre*condition currently demands `acc(src.Mem(), _)` + — folding `(&net.IPAddr{IP: p.d.internalIP}).Mem()` requires byte + permissions for `internalIP`, which are only available at wildcard; + check whether the fold at a wildcard amount goes through, and if not, + weaken `SetSrcAddr`'s wildcard-mode precondition to take the raw + components (`acc(&src.IP, R18)` + `acc(sl.Bytes(src.IP, ...), _)`) + instead of a folded `Mem()`; + * access to `p.d.internalIP` itself should follow the existing + dup-invariant getter idiom (`getExternalMem()` at + `dataplane.go:5029`), i.e., add a `getInternalIPMem()`-style ghost + getter to `DataPlane` if none exists. +* **`SetDstAddr`'s postconditions are too weak today**: for the + `!wildcard`, IP-typed case it returns `acc(dst.Mem(), R18)` and says + nothing about `s.RawDstAddr`'s bytes — the aliasing postconditions are + commented out (`scion.go:677-680`). To fold the serialize-mode + predicate we need the `R50` fraction of `sl.Bytes(s.RawDstAddr, ...)`. + Strengthen the spec (spec-only) to return that fraction directly, + plus a magic wand restoring `acc(dst.Mem(), R18)` from it, or + re-enable (a weakened form of) the commented-out aliasing + postconditions so the caller can carve the fraction out of + `sl.Bytes(ub, ...)` itself. + +The asymmetry does bake `prepareSCMP`'s aliasing situation into +`pkg/slayers`' serialize-mode predicates. That is acceptable: serialize +mode is new (no existing clients), and the BFD sender (§8) — whose source +address has a different origin — can be accommodated later by +generalizing the amounts, not the shape. ### 4.4 `SerializeTo` spec changes (interface + implementations) @@ -337,80 +386,148 @@ ensures err != nil ==> err.ErrorMem() `nil`, §3.1); * a serialize-mode variant of `SerializeAddrHdr`'s spec (address bytes from the predicate instead of `ubuf`); - * verification of the `FixLengths` branch: `uint8(scnLen/LineLen)` is - bounded by the existing `scnLen <= MaxHdrLen` check; - `uint16(len(b.Bytes()) - scnLen)` needs a precondition bounding the - buffer contents (e.g. `ubuf == nil ==> len(b.UBuf()) + scnLen <= 0xffff`), - dischargeable at the call site because the buffer was `Clear()`ed and - the prepends are bounded by `MaxSCMPPacketLen` (1232) via the quote - truncation (`dataplane.go:5111-5114`); + * verification of the `FixLengths` branch: the field writes need the + full-permission serialize-mode `Mem` (above); the `uint8`/`uint16` + casts produce no obligations since CI disables overflow checking + (`overflow: '0'`), and serialize mode leaves `HdrLen`/`PayloadLen` + unconstrained, so no buffer-size bound is required; * the new IO postcondition (§4.6). -### 4.5 `SerializeLayers`: trusted quantified spec vs. direct calls - -**Option A — keep the call, write a trusted quantified spec** (fill in the -existing skeleton in `writer.gobra:105-112` with per-layer `layerBufs`, -pairwise-distinctness like `decodeLayers`, `Mem(layerBufs[i])` + -`sl.Bytes(layerBufs[i], ...)` preserved for all `i`). This is sound and -straightforward, **but it cannot deliver item 7 (§2)**: `gopacket` cannot -import `slayers` (dependency direction), so no `SerializeLayers` post can -mention `NextHdr`/`IsSupportedPkt`, and the `SerializableLayer` interface -has no abstraction through which the output bytes' provenance can be -stated generically. The IO fact would need a localized `assume` — i.e., the -`TODO()` merely shrinks instead of disappearing. - -**Option B — inline the serialization in `prepareSCMP` (recommended).** -Replace the single call with the equivalent reverse-order sequence (a -marked `(VerifiedSCION)` change; `p.buffer.Clear()` already happens at -`dataplane.go:5091`, and the skipped `PushLayer` bookkeeping is -unobservable — `Layers()` is never called in the router and is -`requires false` in the spec): - -```go -// gopacket.SerializeLayers(p.buffer, sopts, scmpLayers...) is equivalent to: -for i := len(scmpLayers) - 1; i >= 0; i-- { // or fully unrolled - if err := scmpLayers[i].SerializeTo(p.buffer, sopts /*@, layerBuf(i) @*/); err != nil { ... } -} -``` - -Unrolling fully is preferable for the proof: the `&scionL` and `&scmpH` -calls become *concrete* method calls (using `(*SCION).SerializeTo`'s -own, richer spec — including the IO postcondition and the mode-split -permission amounts, neither of which fits through the interface), -while `scmpP` and the payload still go through the interface with -`Mem(nil)` / `Mem(quote)`. As a bonus, `*SCION` no longer *needs* to -satisfy the (relaxed) `SerializableLayer` interface, though with the -mode-split spec of §4.4 it still can. +### 4.5 The trusted `SerializeLayers` spec -`bfdSend.Send` (`dataplane.go:4891`) can later adopt the same pattern (§8). - -### 4.6 Deriving `!IsSupportedPkt(result)` - -Add to `(*SCION).SerializeTo` a serialize-mode postcondition, e.g.: +Since the call must stay, `writer.gobra:105-112` gets a real (trusted) +quantified specification. Sketch: ```gobra -ensures e == nil && ubuf == nil ==> - IsSupportedRawPkt(b.View()) == - (s.PathType == scion.PathType && s.NextHdr != L4SCMP) +requires len(layerBufs) == len(layers) +requires w != nil && w.Mem() +requires sl.Bytes(w.UBuf(), 0, len(w.UBuf())) +requires opts.FixLengths ==> forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> + layerBufs[i] == nil // cf. §4.4 +requires forall i, j int :: { &layers[i], &layers[j] } 0 <= i && i < j && j < len(layers) ==> + layers[i] !== layers[j] // injectivity, cf. decodeLayers +requires acc(layerBufs, R20) +requires forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> + (acc(&layers[i], R20) && layers[i] != nil && layers[i].Mem(layerBufs[i])) +requires forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> + sl.Bytes(layerBufs[i], 0, len(layerBufs[i])) +ensures w.Mem() && sl.Bytes(w.UBuf(), 0, len(w.UBuf())) +ensures acc(layerBufs, R20) +ensures forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> + (acc(&layers[i], R20) && layers[i].Mem(layerBufs[i]) && + sl.Bytes(layerBufs[i], 0, len(layerBufs[i]))) // also on error, cf. §4.4 +ensures err != nil ==> err.ErrorMem() +ensures err == nil && 0 < len(layers) ==> /* IO clause, §4.6 */ ``` -This is provable in the body: the common-header write -(`buf[4] = uint8(s.NextHdr)`, `buf[8] = uint8(s.PathType)`, -`scion.go:258-262`) determines exactly the two bytes `IsSupportedRawPkt` -inspects, and the subsequent `SerializeAddrHdr`/`Path.SerializeTo` calls only -touch offsets ≥ `CmnHdrLen` (the existing `IsSupportedPktSubslice` lemma -machinery, `scion_spec.gobra:522-534`, already frames this). - -In `prepareSCMP`: since SCION is serialized **last** (prepended at the -front), the buffer state at its return *is* the final state; -`scionL.NextHdr == L4SCMP` gives `!IsSupportedRawPkt(b.View())`; a small -lemma `IsSupportedRawPkt(b.View()) == IsSupportedPkt(b.UBuf())` -(`View() == seqs.ToSeqByte(UBuf())` by the `SerializeBuffer` spec, -`writer.gobra:48-54`; both functions read bytes 4 and 8) transports it to -`!IsSupportedPkt(p.buffer.UBuf())`, and `Bytes()` (`writer.gobra:56-59`) -gives `result === p.buffer.UBuf()`. This mirrors the existing pattern in -`updateSCIONLayer` (`dataplane.go:4784-4789`), just sourced from field -values instead of `old(IsSupportedPkt(rawPkt))`. +Notes: + +* In `prepareSCMP`, `layerBufs` becomes a real ghost sequence built + alongside `scmpLayers` — `[nil, nil, nil]`, extended with `quote` in the + `cause != nil` branch — replacing today's `nil` placeholder at + `dataplane.go:5118`. +* Three layers share the buffer `nil`, so the quantified + `sl.Bytes(layerBufs[i], 0, 0)` demands three instances of + `sl.Bytes(nil, 0, 0)`. That is fine: the predicate body quantifies over + zero locations, so arbitrarily many full instances can be folded + (precedent: `fold sl.Bytes(nil, 0, 0)` in `packSCMP`, + `dataplane.go:2206`). +* The spec is justified against the (unverified) gopacket implementation: + it calls `w.Clear()` and then `layers[i].SerializeTo(w, opts)` from last + to first, returning on the first error; with the strengthened interface + postconditions of §4.4 (unconditional `Mem`), every quantified resource + is restored on both success and failure. The `PushLayer` bookkeeping it + also performs is unobservable to the router (`Layers()` is + `requires false` and never called). +* Since *all four* layers — including `&scionL` — are now dispatched + through the `SerializableLayer` interface, everything + `(*SCION).SerializeTo` needs must fit through the interface footprint: + full `Mem(ubuf)` (which the interface provides) plus + `sl.Bytes(ubuf, ...)`. This is precisely why the serialize-mode + `SCION.Mem(nil)` (§4.2/§4.3) must be *self-contained* (path resources, + address bytes, field permissions all inside), and `*SCION` must keep + satisfying the (relaxed) interface via its mode-split implementation + spec. + +### 4.6 Deriving `!IsSupportedPkt(result)` through the interface + +This is the delicate part under the no-code-change constraint: the fact +"byte 4 of the output is `L4SCMP`" must flow from `(*SCION).SerializeTo` +through two abstraction boundaries that cannot name SCION concepts — +the `SerializableLayer` interface and the generic `SerializeLayers` spec +(`gopacket` cannot import `slayers`). The route: + +1. **A gopacket-level twin of `IsSupportedRawPkt`.** Define in the + `gopacket` stubs a ghost, opaque + `pure func IsSupportedRawPkt(raw seq[byte]) bool` with the same body as + `slayers.IsSupportedRawPkt` (`scion_spec.gobra:514-520`) — it only + reads `raw[4]`/`raw[8]` against numeric constants, so no `slayers` + import is needed — plus a one-line bridging lemma in `slayers` + (`reveal` both) equating the two. +2. **An abstraction hook on the interface.** Extend `SerializableLayer` + with a ghost pure method, e.g. + + ```gobra + ghost + requires acc(Mem(ubuf), _) + decreases + pure SerializesToSupportedPkt(ghost ubuf []byte) bool + ``` + + with the documented meaning "if this layer serializes *outermost*, the + resulting packet is supported". Implementations: + `*SCION` returns, in serialize mode (`ubuf == nil`), + `s.PathType == scion.PathType && s.NextHdr != L4SCMP` over its fields, + and in decoded mode `IsSupportedPkt(ubuf)`; the SCMP message types, + `Payload`, and the BFD stub return `false` (they never serialize + outermost in verified code — see the caveat below). +3. **Interface postconditions on `SerializeTo`**: + * *stability*: `err == nil ==> SerializesToSupportedPkt(ubuf) == + old(SerializesToSupportedPkt(ubuf))` — provable for `*SCION` because + serialization never writes `NextHdr`/`PathType` (the `FixLengths` + branch only writes `HdrLen`/`PayloadLen`); trivial for layers with a + constant hook. Without this clause the hook's value would be unknown + after the call (the caller only gets `Mem(ubuf)` back, not field + equalities). + * *on `*SCION` only* (implementation spec, used for the implementation + proof): `err == nil ==> gopacket.IsSupportedRawPkt(b.View()) == + SerializesToSupportedPkt(ubuf)`. This is provable in the body: the + common-header write (`buf[4] = uint8(s.NextHdr)`, + `buf[8] = uint8(s.PathType)`, `scion.go:258-262`) determines exactly + the two inspected bytes, and the later + `SerializeAddrHdr`/`Path.SerializeTo` calls only touch offsets + ≥ `CmnHdrLen` (the existing `IsSupportedPktSubslice` machinery, + `scion_spec.gobra:522-534`, and the serialize-mode analog of + `IsSupportedPktLemma`, `scion.go:267-270`, frame this). +4. **Forwarding through `SerializeLayers`** (trusted): + + ```gobra + ensures err == nil && 0 < len(layers) ==> + IsSupportedRawPkt(w.View()) == layers[0].SerializesToSupportedPkt(layerBufs[0]) + ``` + + Justification: the implementation serializes `layers[0]` *last*, so the + buffer state at that call's return is the final state, and for the + network-header layer the clause is exactly its per-implementation + postcondition from step 3. **Caveat**: as stated, the trusted clause + asserts this for *any* first layer, including ones (e.g. `Payload`) + whose hook cannot truthfully describe the final bytes. Since the spec + is trusted either way, this is a documented soundness assumption + ("only meaningful when `layers[0]` is the outermost network-header + layer"); it can be made self-guarding by adding a second hook + (`ghost pure IsNetworkHeaderLayer() bool`, `true` only for `*SCION`) + and conditioning the clause on it. +5. **Back in `prepareSCMP`**: `scionL.NextHdr == L4SCMP` (set at + `dataplane.go:5085`, stable by step 3) makes the hook `false`, so + `!gopacket.IsSupportedRawPkt(p.buffer.View())`; the bridging lemma and + a small `View`/`UBuf` lemma + (`View() == seqs.ToSeqByte(UBuf())`, `writer.gobra:48-54`; both + functions read bytes 4 and 8) yield + `!slayers.IsSupportedPkt(p.buffer.UBuf())`, and `Bytes()` + (`writer.gobra:56-59`) gives `result === p.buffer.UBuf()` — closing + postcondition `dataplane.go:4917-4918`. This mirrors the pattern in + `updateSCIONLayer` (`dataplane.go:4784-4789`), sourced from field + values instead of `old(IsSupportedPkt(rawPkt))`. --- @@ -428,15 +545,17 @@ values instead of `old(IsSupportedPkt(rawPkt))`. * **Proof work in the body (post-`TODO()` region)**: 1. re-fold `revPath.Mem(rawPath)` → `revPath.Mem(nil)`; 2. fold serialize-mode `scionL.Mem(nil)` after the field assignments and - `Set{Dst,Src}Addr` calls (the `SetSrcAddr` ghost argument and/or code - adapted per §4.3); fold `ChecksumMem(scionL)` and then + `Set{Dst,Src}Addr` calls (the `SetSrcAddr` ghost argument flipped to + wildcard mode and the `SetDstAddr`/`SetSrcAddr` postconditions + strengthened per §4.3); fold `ChecksumMem(scionL)` and then `scmpH.Mem(nil)` after `SetNetworkLayerForChecksum`; 3. discharge the `hdrLen` computation (`AddrHdrLen(nil, ...)`, - `Path.Len(nil)` through pure helper functions over `Mem(nil)`), and - the `MaxSCMPPacketLen` bound for §4.4's buffer-size precondition; - 4. serialization calls per §4.5 Option B, restoring all predicates on - both success and error paths (possible thanks to the strengthened - error postconditions, §4.4); + `Path.Len(nil)` through pure helper functions over `Mem(nil)`); + 4. build the ghost `layerBufs` sequence alongside `scmpLayers` + (`[nil, nil, nil]`, plus `quote` in the `cause != nil` branch) and + invoke `SerializeLayers` against the new trusted spec (§4.5); all + predicates come back on both success and error paths thanks to the + strengthened error postconditions (§4.4); 5. at the end: unfold the fresh layers' predicates (they die with the function), apply the `SrcAddr()` magic wand, recombine all `ub` ranges to return `sl.Bytes(ub, 0, len(ub))` and @@ -456,17 +575,24 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). proofs and `LayerPayload` specs. Small/medium; contained in `pkg/slayers`. 2. **M2 — serialize-mode `*SCION.Mem`** (§4.2) + `ChecksumMem` - re-fractioning and the address-permission decision (§4.3). Medium; - touches many `SCION` lemmas' guards (`ub != nil`). + re-fractioning, the asymmetric address-byte amounts, and the + `SetDstAddr`/`SetSrcAddr` postcondition strengthening (§4.3). Medium; + touches many `SCION` lemmas' guards (`ub != nil`). Start with a smoke + test that a wildcard conjunct inside a predicate body folds/unfolds as + expected. 3. **M3 — `(*SCION).SerializeTo`**: mode-split spec, `SerializeAddrHdr` - serialize-mode, verify the `FixLengths` branch (bounds!), add the §4.6 - postcondition. This is the hardest single item. Large. -4. **M4 — interface updates** in `writer.gobra` (§4.4) + re-verify the - closed set of implementers; adjust the `Payload`/`BFD` trusted stubs. - Small/medium. + serialize-mode, verify the `FixLengths` branch, prove the + hook postcondition of §4.6 (step 3). This is the hardest single item. + Large. +4. **M4 — interface + `SerializeLayers` spec updates** in `writer.gobra` + (§4.4, §4.5, §4.6 steps 1–2, 4): relax `FixLengths`, strengthen error + postconditions, add the ghost hook, the gopacket-level + `IsSupportedRawPkt` twin + bridging lemma, and the quantified trusted + `SerializeLayers` spec; re-verify the closed set of implementers; + adjust the `Payload`/`BFD` trusted stubs. Medium. 5. **M5 — `prepareSCMP` itself** (§5): spec extensions, call-site folds, - inlined serialization (§4.5 B), drop the `TODO()`. Large, but mostly - mechanical once M1–M4 are in; expect iteration on router CI time. + ghost `layerBufs`, drop the `TODO()`. Large, but mostly mechanical once + M1–M4 are in; expect iteration on router CI time. 6. **M6 — cleanup**: remove `Unreachable()` from the `FixLengths` branch, revisit `bfdSend` (§8), document the serialize-mode idiom. @@ -475,15 +601,25 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). * **Verification time** of `dataplane.go` (already the 6 h/`chop 10` package). Mitigate with `outline(...)` blocks and `opaque` helper functions for the new fold-heavy regions. -* **`FixLengths` overflow bounds** require threading a buffer-size bound - through a *trusted-interface* boundary (`SerializeBuffer` is a trusted - spec); double-check `PrependBytes`' postconditions suffice to track - `len(UBuf())` across the four prepends. +* **Wildcard permission amounts inside predicate bodies** (§4.3) and + wildcard-mode folds of `net.IPAddr.Mem()` are less-trodden Gobra + territory; validate with a small experiment before building M2 on them. + Fallback: keep the `RawSrcAddr` bytes *outside* the predicates entirely + and weaken `SerializeAddrHdr`/`computeChecksum`'s specs to take them as + separate wildcard clauses — workable because those specs are on concrete + methods, but it makes the serialize-mode `SCION.Mem` non-self-contained, + which conflicts with interface dispatch (§4.5); in that case the src + bytes would have to ride in a second, `slayers`-internal predicate + referenced from `Mem`'s serialize branch. * **Gobra interface-implementation proofs** with mode-split permission - amounts (`ubuf == nil ? full : R0`) are unusual; if the implementation - proof for `*SCION` becomes brittle, fall back to dropping - `*SCION implements gopacket.SerializableLayer` (safe under §4.5 B since - the only interface-dispatched uses are `scmpP` and the payload). + amounts (`ubuf == nil ? full : R0`) and ghost pure interface methods are + unusual; unlike in a design where the SCION call is concrete, `*SCION` + **must** remain a `SerializableLayer` implementer here, so brittleness + in the implementation proof has no cheap fallback — prototype early + (M4 before M3 completion is fine, the two are independent). +* **The trusted `SerializeLayers` IO clause** (§4.6 step 4) is a genuine + (if small) soundness assumption about which layer is outermost; gate it + with the `IsNetworkHeaderLayer()` hook to keep it honest. * **`SrcAddr()`/`SetDstAddr` aliasing**: the `RawDstAddr` fraction originates from `acc(p.scionLayer.Mem(ub), R4)`-governed memory via a magic wand; getting the fraction arithmetic right (so that the wand can From b4772959a3714c8ffd328657c104806b17713453 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Jul 2026 07:50:36 +0000 Subject: [PATCH 03/19] Implement M1 of the prepareSCMP plan: fresh mode for BaseLayer.Mem Generalize BaseLayer.Mem with a fresh mode (ub == nil): a freshly constructed, not-yet-decoded layer holds only the field permissions, with zero-valued Contents/Payload, instead of the buffer-aliasing facts. This makes Mem(nil) foldable for freshly constructed SCMP and SCMP message layers, a prerequisite for serializing them in prepareSCMP. - extnBase.Mem pins ActualLen == 0 in fresh mode so all facts previously derivable for a nil buffer are preserved. - LayerPayload specs over BaseLayer are conditionalized on ub != nil (their conclusions still imply the gopacket.Layer/DecodingLayer interface contracts). - DecodeFromBytes of SCMP and the seven SCMP message types now ensure their minimum length on success, so decoded-mode proof sites can derive data != nil and keep the aliasing facts (asserts added at the traceroute handler's unfolds). - FoldFreshMem witness lemmas for SCMP and all seven message types machine-check that fresh layers satisfy Mem(nil). - Add gopacket.IsSupportedRawPkt (twin of the slayers definition, which gopacket cannot import) plus a bridging lemma, needed later to thread the router's !IsSupportedPkt postcondition through SerializeLayers. Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 28 +++- pkg/slayers/extn.go | 6 +- pkg/slayers/extn_spec.gobra | 10 +- pkg/slayers/scion.go | 7 +- pkg/slayers/scion_spec.gobra | 32 ++++- pkg/slayers/scmp.go | 1 + pkg/slayers/scmp_msg.go | 7 + pkg/slayers/scmp_msg_spec.gobra | 133 ++++++++++++++++-- pkg/slayers/scmp_spec.gobra | 19 ++- router/dataplane.go | 7 + .../github.com/google/gopacket/base.gobra | 16 +++ 11 files changed, 236 insertions(+), 30 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index db64396bd..a9951942a 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -117,10 +117,13 @@ unfold revPath.Mem(rawPath) // OK: *scion.Decoded's Mem body fold revPath.Mem(nil) // never mentions ubuf (see §3) ``` -(These snippets cannot live in a `*_test.gobra` file in-tree, because the -failing folds would fail CI; run them ad hoc when validating this plan. -Note that `pkg/slayers` CI verification takes ~25 min per run, -`.github/workflows/gobra.yml:214-234`.) +(The failing snippets cannot live in a `*_test.gobra` file in-tree, because +they would fail CI; run them ad hoc when validating this plan. Note that +`pkg/slayers` CI verification takes ~25 min per run, +`.github/workflows/gobra.yml:214-234`. The *positive* counterparts are +committed in-tree as `FoldFreshMem` witness lemmas — see the M1 status note +in §6 — so CI machine-checks that fresh layers satisfy `Mem(nil)` under the +reworked predicates.) --- @@ -574,6 +577,23 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). 1. **M1 — `BaseLayer.Mem` nil-mode** (§4.1) + adapt `SCMP`/message-type proofs and `LayerPayload` specs. Small/medium; contained in `pkg/slayers`. + **Status: implemented on this branch** (pending a CI/Gobra run): + * `BaseLayer.Mem` fresh mode, with `Contents == nil && Payload == nil` + in the `ub == nil` branch so the `gopacket.Layer` interface's + `LayerPayload` contract stays satisfiable; + * `extnBase.Mem` additionally pins `ActualLen == 0` in fresh mode, + preserving every fact the old definition yielded for a nil buffer; + * all `LayerPayload` specs over `BaseLayer` (SCMP, the 7 SCMP messages, + both extensions and both skippers, and `BaseLayer.LayerPayload` + itself) conditionalized on `ub != nil`; + * `FoldFreshMem` witness lemmas for `SCMP` and all 7 message types — + the machine-checked form of §1.2's positive experiments; + * `DecodeFromBytes` of `SCMP` + the 7 message types now ensure their + minimum length on success, so decoded-mode call sites (e.g. the + traceroute handler's unfolds, `router/dataplane.go:4100-4120`) can + derive `data != nil` and keep using the aliasing facts; + * §4.6 step 1 done early (it is additive): `gopacket.IsSupportedRawPkt` + twin + `slayers.IsSupportedRawPktEqGopacket` bridging lemma. 2. **M2 — serialize-mode `*SCION.Mem`** (§4.2) + `ChecksumMem` re-fractioning, the asymmetric address-byte amounts, and the `SetDstAddr`/`SetSrcAddr` postcondition strengthening (§4.3). Medium; diff --git a/pkg/slayers/extn.go b/pkg/slayers/extn.go index 2bbffd883..3f99b0878 100644 --- a/pkg/slayers/extn.go +++ b/pkg/slayers/extn.go @@ -309,7 +309,8 @@ func (h *HopByHopExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer // @ preserves acc(h.Mem(ub), R20) // @ ensures 0 <= start && start <= end && end <= len(ub) // @ ensures len(res) == end - start -// @ ensures res === ub[start:end] +// @ ensures ub != nil ==> res === ub[start:end] +// @ ensures ub == nil ==> (res == nil && start == 0 && end == 0) // @ decreases func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) { // @ unfold acc(h.Mem(ub), R20) @@ -458,7 +459,8 @@ func (e *EndToEndExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer // @ preserves acc(e.Mem(ub), R20) // @ ensures 0 <= start && start <= end && end <= len(ub) // @ ensures len(res) == end - start -// @ ensures res === ub[start:end] +// @ ensures ub != nil ==> res === ub[start:end] +// @ ensures ub == nil ==> (res == nil && start == 0 && end == 0) // @ decreases func (e *EndToEndExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) { // @ unfold acc(e.Mem(ub), R20) diff --git a/pkg/slayers/extn_spec.gobra b/pkg/slayers/extn_spec.gobra index 844859f8d..09cef8c3e 100644 --- a/pkg/slayers/extn_spec.gobra +++ b/pkg/slayers/extn_spec.gobra @@ -33,6 +33,10 @@ pred (e *extnBase) Mem(ubuf []byte) { acc(&e.NextHdr) && acc(&e.ExtLen) && acc(&e.ActualLen) && + // In fresh mode (ubuf == nil, cf. BaseLayer.Mem), ActualLen must be 0. + // This preserves the facts that were derivable from BaseLayer.Mem's + // old definition (breakPoint <= len(ubuf)) for a nil buffer. + (ubuf == nil ==> e.ActualLen == 0) && e.BaseLayer.Mem(ubuf, e.ActualLen) } @@ -96,7 +100,8 @@ func (h *HopByHopExtnSkipper) LayerContents() (res []byte) { preserves acc(h.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (h *HopByHopExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(h.Mem(ub), R20) @@ -186,7 +191,8 @@ func (e *EndToEndExtnSkipper) LayerContents() (res []byte) { preserves acc(e.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (e *EndToEndExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(e.Mem(ub), R20) diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index b74c6d61d..e9e4717f7 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -104,9 +104,10 @@ func (b *BaseLayer) LayerContents() (res []byte) { // LayerPayload returns the bytes contained within the packet layer. // @ preserves acc(b.Mem(ub, bp), R20) -// @ ensures len(res) == len(ub) - bp -// @ ensures 0 <= bp && bp <= len(ub) -// @ ensures res === ub[bp:] +// @ ensures ub != nil ==> len(res) == len(ub) - bp +// @ ensures ub != nil ==> (0 <= bp && bp <= len(ub)) +// @ ensures ub != nil ==> res === ub[bp:] +// @ ensures ub == nil ==> res == nil // @ decreases func (b *BaseLayer) LayerPayload( /*@ ghost ub []byte, ghost bp int @*/ ) (res []byte) { // @ unfold acc(b.Mem(ub, bp), R20) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 3bcf6a96f..d10e22a5f 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -241,11 +241,21 @@ pred (s *SCION) ChecksumMem() { sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)) } +// A BaseLayer predicate instance is in one of two modes: +// - decoded mode (ub != nil): the layer was obtained via DecodeFromBytes +// and Contents and Payload alias the underlying buffer ub around +// breakPoint (this is the original meaning of this predicate); +// - fresh mode (ub == nil): the layer was freshly constructed (e.g. to be +// serialized, cf. prepareSCMP in the router) and has no underlying +// buffer; Contents and Payload are still zero-valued. +// The fresh mode is what makes Mem(nil) foldable for freshly constructed +// layers, which is impossible in decoded mode whenever breakPoint > 0. pred (b *BaseLayer) Mem(ghost ub []byte, ghost breakPoint int) { - 0 <= breakPoint && breakPoint <= len(ub) && acc(b) && - b.Contents === ub[:breakPoint] && - b.Payload === ub[breakPoint:] + (ub == nil ==> (b.Contents == nil && b.Payload == nil)) && + (ub != nil ==> (0 <= breakPoint && breakPoint <= len(ub) && + b.Contents === ub[:breakPoint] && + b.Payload === ub[breakPoint:])) } ghost @@ -519,6 +529,22 @@ pure func IsSupportedRawPkt(raw seq[byte]) bool { nextHdr != L4SCMP } +// gopacket.IsSupportedRawPkt is a twin of IsSupportedRawPkt, defined in the +// gopacket stubs because gopacket cannot import slayers. This lemma keeps +// the two definitions in sync; it is the bridge through which +// supportedness facts established by (trusted) gopacket-level specs (e.g. +// SerializeLayers) become available in terms of the slayers definitions. +ghost +ensures gopacket.IsSupportedRawPkt(raw) == IsSupportedRawPkt(raw) +decreases +func IsSupportedRawPktEqGopacket(raw seq[byte]) { + reveal gopacket.IsSupportedRawPkt(raw) + reveal IsSupportedRawPkt(raw) + assert scion.PathType == path.Type(1) + assert L4SCMP == L4ProtocolType(202) + assert CmnHdrLen == 12 +} + ghost requires CmnHdrLen <= idx && idx <= len(raw) preserves acc(sl.Bytes(raw, 0, len(raw)), R55) diff --git a/pkg/slayers/scmp.go b/pkg/slayers/scmp.go index 6892c007d..e40c149fb 100644 --- a/pkg/slayers/scmp.go +++ b/pkg/slayers/scmp.go @@ -171,6 +171,7 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp // @ requires s.NonInitMem() // @ preserves df.Mem() // @ ensures res == nil ==> s.Mem(data) +// @ ensures res == nil ==> 4 <= len(data) // @ ensures res != nil ==> (s.NonInitMem() && res.ErrorMem()) // @ decreases func (s *SCMP) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res error) { diff --git a/pkg/slayers/scmp_msg.go b/pkg/slayers/scmp_msg.go index 86e9fd9f7..b49639f87 100644 --- a/pkg/slayers/scmp_msg.go +++ b/pkg/slayers/scmp_msg.go @@ -67,6 +67,7 @@ func (i *SCMPExternalInterfaceDown) NextLayerType() gopacket.LayerType { // @ requires sl.Bytes(data, 0, len(data)) // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> addr.IABytes+scmpRawInterfaceLen <= len(data) // @ ensures res != nil ==> (i.NonInitMem() && sl.Bytes(data, 0, len(data))) // @ ensures res != nil ==> res.ErrorMem() // @ decreases @@ -205,6 +206,7 @@ func (*SCMPInternalConnectivityDown) NextLayerType() gopacket.LayerType { // @ requires i.NonInitMem() // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> addr.IABytes+2*scmpRawInterfaceLen <= len(data) // @ ensures res != nil ==> (i.NonInitMem() && sl.Bytes(data, 0, len(data))) // @ ensures res != nil ==> res.ErrorMem() // @ decreases @@ -345,6 +347,7 @@ func (*SCMPEcho) NextLayerType() gopacket.LayerType { // @ requires sl.Bytes(data, 0, len(data)) // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> 4 <= len(data) // @ ensures res != nil ==> (i.NonInitMem() && sl.Bytes(data, 0, len(data))) // @ ensures res != nil ==> res.ErrorMem() // @ decreases @@ -498,6 +501,7 @@ func (*SCMPParameterProblem) NextLayerType() gopacket.LayerType { // @ requires sl.Bytes(data, 0, len(data)) // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> 2+2 <= len(data) // @ ensures res != nil ==> (i.NonInitMem() && sl.Bytes(data, 0, len(data))) // @ ensures res != nil ==> res.ErrorMem() // @ decreases @@ -641,6 +645,7 @@ func (*SCMPTraceroute) NextLayerType() gopacket.LayerType { // @ preserves acc(sl.Bytes(data, 0, len(data)), R40) // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> 2+2+addr.IABytes+scmpRawInterfaceLen <= len(data) // @ ensures res != nil ==> i.NonInitMem() // @ ensures res != nil ==> res.ErrorMem() // @ decreases @@ -829,6 +834,7 @@ func (*SCMPDestinationUnreachable) NextLayerType() gopacket.LayerType { // @ requires sl.Bytes(data, 0, len(data)) // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> 4 <= len(data) // @ ensures res != nil ==> (i.NonInitMem() && sl.Bytes(data, 0, len(data))) // @ ensures res != nil ==> res.ErrorMem() // @ decreases @@ -929,6 +935,7 @@ func (*SCMPPacketTooBig) NextLayerType() gopacket.LayerType { // @ requires i.NonInitMem() // @ preserves df.Mem() // @ ensures res == nil ==> i.Mem(data) +// @ ensures res == nil ==> 2+2 <= len(data) // @ ensures res != nil ==> (i.NonInitMem() && sl.Bytes(data, 0, len(data))) // @ ensures res != nil ==> res.ErrorMem() // @ decreases diff --git a/pkg/slayers/scmp_msg_spec.gobra b/pkg/slayers/scmp_msg_spec.gobra index f4cd61b64..4209bc0a4 100644 --- a/pkg/slayers/scmp_msg_spec.gobra +++ b/pkg/slayers/scmp_msg_spec.gobra @@ -40,12 +40,13 @@ func (b *SCMPExternalInterfaceDown) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPExternalInterfaceDown) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, addr.IABytes+scmpRawInterfaceLen) - start = addr.IABytes+scmpRawInterfaceLen + start = ub == nil ? 0 : addr.IABytes+scmpRawInterfaceLen end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -55,6 +56,20 @@ func (b *SCMPExternalInterfaceDown) LayerPayload(ghost ub []byte) (res []byte, g (*SCMPExternalInterfaceDown) implements gopacket.Layer (*SCMPExternalInterfaceDown) implements gopacket.SerializableLayer +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPExternalInterfaceDown layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.IA) && acc(&s.IfID) && acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPExternalInterfaceDown) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, addr.IABytes+scmpRawInterfaceLen) + fold s.Mem(nil) +} + pred (s *SCMPInternalConnectivityDown) NonInitMem() { acc(&s.IA) && acc(&s.Ingress) && acc(&s.Egress) && acc(&s.BaseLayer) } @@ -72,12 +87,13 @@ func (b *SCMPInternalConnectivityDown) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPInternalConnectivityDown) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, addr.IABytes+2*scmpRawInterfaceLen) - start = addr.IABytes+2*scmpRawInterfaceLen + start = ub == nil ? 0 : addr.IABytes+2*scmpRawInterfaceLen end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -86,6 +102,20 @@ func (b *SCMPInternalConnectivityDown) LayerPayload(ghost ub []byte) (res []byte (*SCMPInternalConnectivityDown) implements gopacket.Layer (*SCMPInternalConnectivityDown) implements gopacket.SerializableLayer +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPInternalConnectivityDown layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.IA) && acc(&s.Ingress) && acc(&s.Egress) && acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPInternalConnectivityDown) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, addr.IABytes+2*scmpRawInterfaceLen) + fold s.Mem(nil) +} + pred (s *SCMPEcho) NonInitMem() { acc(&s.Identifier) && acc(&s.SeqNumber) && acc(&s.BaseLayer) } @@ -103,12 +133,13 @@ func (b *SCMPEcho) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPEcho) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, 4) - start = 4 + start = ub == nil ? 0 : 4 end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -117,6 +148,20 @@ func (b *SCMPEcho) LayerPayload(ghost ub []byte) (res []byte, ghost start int, g (*SCMPEcho) implements gopacket.Layer (*SCMPEcho) implements gopacket.SerializableLayer +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPEcho layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.Identifier) && acc(&s.SeqNumber) && acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPEcho) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, 4) + fold s.Mem(nil) +} + pred (s *SCMPParameterProblem) NonInitMem() { acc(&s.Pointer) && acc(&s.BaseLayer) } @@ -134,12 +179,13 @@ func (b *SCMPParameterProblem) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPParameterProblem) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, 4) - start = 4 + start = ub == nil ? 0 : 4 end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -148,6 +194,20 @@ func (b *SCMPParameterProblem) LayerPayload(ghost ub []byte) (res []byte, ghost (*SCMPParameterProblem) implements gopacket.Layer (*SCMPParameterProblem) implements gopacket.SerializableLayer +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPParameterProblem layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.Pointer) && acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPParameterProblem) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, 4) + fold s.Mem(nil) +} + pred (s *SCMPTraceroute) NonInitMem() { acc(&s.Identifier) && acc(&s.Sequence) && acc(&s.IA) && acc(&s.Interface) && acc(&s.BaseLayer) } @@ -170,12 +230,13 @@ func (b *SCMPTraceroute) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPTraceroute) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, 4+addr.IABytes+scmpRawInterfaceLen) - start = 4+addr.IABytes+scmpRawInterfaceLen + start = ub == nil ? 0 : 4+addr.IABytes+scmpRawInterfaceLen end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -184,6 +245,20 @@ func (b *SCMPTraceroute) LayerPayload(ghost ub []byte) (res []byte, ghost start (*SCMPTraceroute) implements gopacket.Layer (*SCMPTraceroute) implements gopacket.SerializableLayer +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPTraceroute layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.Identifier) && acc(&s.Sequence) && acc(&s.IA) && acc(&s.Interface) && acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPTraceroute) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, 4+addr.IABytes+scmpRawInterfaceLen) + fold s.Mem(nil) +} + pred (s *SCMPDestinationUnreachable) NonInitMem() { acc(&s.BaseLayer) @@ -202,12 +277,13 @@ func (b *SCMPDestinationUnreachable) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPDestinationUnreachable) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, 4) - start = 4 + start = ub == nil ? 0 : 4 end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -216,6 +292,20 @@ func (b *SCMPDestinationUnreachable) LayerPayload(ghost ub []byte) (res []byte, (*SCMPDestinationUnreachable) implements gopacket.Layer (*SCMPDestinationUnreachable) implements gopacket.SerializableLayer +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPDestinationUnreachable layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPDestinationUnreachable) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, 4) + fold s.Mem(nil) +} + pred (s *SCMPPacketTooBig) NonInitMem() { acc(&s.MTU) && acc(&s.BaseLayer) } @@ -233,12 +323,13 @@ func (b *SCMPPacketTooBig) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMPPacketTooBig) LayerPayload(ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, 4) - start = 4 + start = ub == nil ? 0 : 4 end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end @@ -246,3 +337,17 @@ func (b *SCMPPacketTooBig) LayerPayload(ub []byte) (res []byte, ghost start int, (*SCMPPacketTooBig) implements gopacket.Layer (*SCMPPacketTooBig) implements gopacket.SerializableLayer + +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMPPacketTooBig layer with a nil underlying buffer. This is the +// witness that fresh layers, as constructed by the callers of the router's +// packSCMP, satisfy Mem(nil). +ghost +requires acc(&s.MTU) && acc(&s.BaseLayer) +requires s.Contents == nil && s.Payload == nil +ensures s.Mem(nil) +decreases +func (s *SCMPPacketTooBig) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, 4) + fold s.Mem(nil) +} diff --git a/pkg/slayers/scmp_spec.gobra b/pkg/slayers/scmp_spec.gobra index edc47876d..c7cdf7233 100644 --- a/pkg/slayers/scmp_spec.gobra +++ b/pkg/slayers/scmp_spec.gobra @@ -58,17 +58,32 @@ func (b *SCMP) LayerContents() (res []byte) { preserves acc(b.Mem(ub), R20) ensures 0 <= start && start <= end && end <= len(ub) ensures len(res) == end - start -ensures res === ub[start:end] +ensures ub != nil ==> res === ub[start:end] +ensures ub == nil ==> (res == nil && start == 0 && end == 0) decreases func (b *SCMP) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) { unfold acc(b.Mem(ub), R20) res = b.BaseLayer.LayerPayload(ub, 4) - start = 4 + start = ub == nil ? 0 : 4 end = len(ub) fold acc(b.Mem(ub), R20) return res, start, end } +// Folds the Mem predicate of a freshly constructed (i.e., not decoded) +// SCMP layer with a nil underlying buffer. This is the witness that fresh +// layers, as constructed by the router's prepareSCMP, satisfy Mem(nil). +ghost +requires acc(&s.TypeCode) && acc(&s.Checksum) && acc(&s.BaseLayer) && acc(&s.scn) +requires s.Contents == nil && s.Payload == nil +requires s.scn != nil ==> s.scn.ChecksumMem() +ensures s.Mem(nil) +decreases +func (s *SCMP) FoldFreshMem() { + fold s.BaseLayer.Mem(nil, 4) + fold s.Mem(nil) +} + (*SCMP) implements gopacket.Layer (*SCMP) implements gopacket.SerializableLayer (*SCMP) implements gopacket.DecodingLayer diff --git a/router/dataplane.go b/router/dataplane.go index 7803ba3c7..90b8cbc62 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -4097,6 +4097,9 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( } var scmpP /*@@@*/ slayers.SCMPTraceroute // @ fold scmpP.NonInitMem() + // scionPld is non-nil (and thus scmpH is in decoded mode) because + // DecodeFromBytes succeeded, which requires at least 4 bytes. + // @ assert scionPld != nil // @ unfold scmpH.Mem(scionPld) // @ unfold scmpH.BaseLayer.Mem(scionPld, 4) // @ sl.SplitRange_Bytes(scionPld, 4, len(scionPld), R1) @@ -4108,6 +4111,10 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } + // scmpH.Payload is non-nil (and thus scmpP is in decoded mode) because + // DecodeFromBytes succeeded, which requires at least the traceroute's + // minimum length. + // @ assert scmpH.Payload != nil // @ unfold scmpP.Mem(scmpH.Payload) // @ unfold scmpP.BaseLayer.Mem(scmpH.Payload, 4+addr.IABytes+slayers.scmpRawInterfaceLen) // @ p.d.getLocalIA() diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra index 1e9927cbe..6fc27f00d 100644 --- a/verification/dependencies/github.com/google/gopacket/base.gobra +++ b/verification/dependencies/github.com/google/gopacket/base.gobra @@ -119,3 +119,19 @@ type ErrorLayer interface { decreases Error(ghost ub []byte) error } + +// (VerifiedSCION) Twin of slayers.IsSupportedRawPkt. It must be defined +// here (rather than reusing the slayers definition) because gopacket is a +// dependency of slayers and cannot import it. The numeric literals pin +// down the relevant slayers constants: 12 is slayers.CmnHdrLen, 1 is +// scion.PathType, and 202 is slayers.L4SCMP. The lemma +// slayers.IsSupportedRawPktEqGopacket proves that the two definitions +// agree, keeping them in sync. +ghost +opaque +decreases +pure func IsSupportedRawPkt(raw seq[byte]) bool { + return 12 <= len(raw) && + raw[8] == 1 && // the path type is scion.PathType + raw[4] != 202 // the next header is not slayers.L4SCMP +} From e006e0dd55221e9ea0c7d75538d0587537dd85da Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Jul 2026 07:53:30 +0000 Subject: [PATCH 04/19] Strengthen SerializeTo error-case postconditions (M4, partial) The SerializableLayer interface previously only guaranteed Mem(ubuf) and the buffer resources when serialization succeeded. All implementations in fact keep them intact on error (SCMP and the SCMP message types fail only before unfolding Mem or re-fold it before every error return; Payload and BFD are trusted stubs; SCION's postconditions were already unconditional), so the guarantee can be made unconditional. prepareSCMP will rely on this to restore its resources on the error path of SerializeLayers. Also record in the plan that (*Decoded).Widen already provides the buffer-transfer lemma needed to re-fold the reversed path as Mem(nil). Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 14 ++++++++++++-- pkg/slayers/scmp.go | 2 +- pkg/slayers/scmp_msg.go | 14 +++++++------- .../github.com/google/gopacket/base.gobra | 4 ++-- .../github.com/google/gopacket/layers/bfd.gobra | 4 ++-- .../github.com/google/gopacket/writer.gobra | 8 ++++++-- 6 files changed, 30 insertions(+), 16 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index a9951942a..36162f2d7 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -204,8 +204,9 @@ Removing `TODO()` requires all of the following, not just the `Mem` folds: 1. **`(*scion.Decoded).Mem(ubuf)` never mentions `ubuf`** (`pkg/slayers/path/scion/decoded_spec.gobra:39-48`): it holds `Base.Mem()`, `InfoFields`, `HopFields` — all struct-internal. Hence - `revPath.Mem(rawPath)` can be re-folded as `revPath.Mem(nil)` by a - trivial (un)fold pair, and `(*Decoded).SerializeTo(b, ubuf)` + `revPath.Mem(rawPath)` can be re-folded as `revPath.Mem(nil)` — the + lemma for this already exists (`(*Decoded).Widen`, at the end of + `decoded_spec.gobra`) — and `(*Decoded).SerializeTo(b, ubuf)` (`decoded.go:128-133`) as well as `Len(ubuf)` already work fine with `ubuf = nil` (`sl.Bytes(nil, 0, 0)` is trivially foldable — precedent in `packSCMP`, `dataplane.go:2206`). **The reversed path is already fully @@ -610,6 +611,15 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). `IsSupportedRawPkt` twin + bridging lemma, and the quantified trusted `SerializeLayers` spec; re-verify the closed set of implementers; adjust the `Payload`/`BFD` trusted stubs. Medium. + **Status: partially implemented on this branch** (pending a CI/Gobra + run): the error-case postconditions of `SerializableLayer.SerializeTo` + and all implementations (`SCMP` + the 7 message types re-fold `Mem` + before every error return, so their strengthened specs remain provable; + `Payload`/`BFD` stubs adjusted textually; `SCION` was already + unconditional), plus the `IsSupportedRawPkt` twin + bridging lemma. + Deliberately *not* yet done: the `FixLengths` relaxation (it would + break `*SCION`'s implementation proof until M3 verifies the + `FixLengths` branch), the ghost hook, and the `SerializeLayers` spec. 5. **M5 — `prepareSCMP` itself** (§5): spec extensions, call-site folds, ghost `layerBufs`, drop the `TODO()`. Large, but mostly mechanical once M1–M4 are in; expect iteration on router CI time. diff --git a/pkg/slayers/scmp.go b/pkg/slayers/scmp.go index e40c149fb..ab808cfcb 100644 --- a/pkg/slayers/scmp.go +++ b/pkg/slayers/scmp.go @@ -112,7 +112,7 @@ func (s *SCMP) NextLayerType( /*@ ghost ub []byte @*/ ) gopacket.LayerType { // @ requires s.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> s.Mem(ubufMem) +// @ ensures s.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { diff --git a/pkg/slayers/scmp_msg.go b/pkg/slayers/scmp_msg.go index b49639f87..a63b15a61 100644 --- a/pkg/slayers/scmp_msg.go +++ b/pkg/slayers/scmp_msg.go @@ -112,7 +112,7 @@ func (i *SCMPExternalInterfaceDown) DecodeFromBytes(data []byte, // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPExternalInterfaceDown) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { @@ -258,7 +258,7 @@ func (i *SCMPInternalConnectivityDown) DecodeFromBytes(data []byte, // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPInternalConnectivityDown) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { @@ -424,7 +424,7 @@ func (i *SCMPEcho) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPEcho) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { @@ -555,7 +555,7 @@ func (i *SCMPParameterProblem) DecodeFromBytes(data []byte, df gopacket.DecodeFe // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPParameterProblem) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { @@ -736,7 +736,7 @@ func (i *SCMPTraceroute) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPTraceroute) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { @@ -868,7 +868,7 @@ func (i *SCMPDestinationUnreachable) DecodeFromBytes(data []byte, // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPDestinationUnreachable) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { @@ -989,7 +989,7 @@ func (i *SCMPPacketTooBig) DecodeFromBytes(data []byte, df gopacket.DecodeFeedba // @ requires i.Mem(ubufMem) // @ preserves b.Mem() // @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -// @ ensures err == nil ==> i.Mem(ubufMem) +// @ ensures i.Mem(ubufMem) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (i *SCMPPacketTooBig) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /*@, ghost ubufMem []byte @*/) (err error) { diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra index 6fc27f00d..a7a935fb3 100644 --- a/verification/dependencies/github.com/google/gopacket/base.gobra +++ b/verification/dependencies/github.com/google/gopacket/base.gobra @@ -67,8 +67,8 @@ func (p Payload) Payload(ghost ub []byte) (res []byte, ghost start int, ghost en requires b != nil && b.Mem() requires p.Mem(ubuf) requires slices.Bytes(b.UBuf(), 0, len(b.UBuf())) -ensures err == nil ==> (p.Mem(ubuf) && b.Mem()) -ensures err == nil ==> slices.Bytes(b.UBuf(), 0, len(b.UBuf())) +ensures p.Mem(ubuf) && b.Mem() +ensures slices.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err != nil ==> err.ErrorMem() decreases func (p Payload) SerializeTo(b SerializeBuffer, opts SerializeOptions, ghost ubuf []byte) (err error) diff --git a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra index 14214df43..e4c104698 100644 --- a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra +++ b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra @@ -194,8 +194,8 @@ func (d *BFD) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (err erro requires d.Mem(ub) requires b != nil && b.Mem() requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) -ensures err == nil ==> d.Mem(ub) && b.Mem() -ensures err == nil ==> sl.Bytes(b.UBuf(), 0, len(b.UBuf())) +ensures d.Mem(ub) && b.Mem() +ensures sl.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err != nil ==> err.ErrorMem() decreases func (d *BFD) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions, ghost ub []byte) (err error) diff --git a/verification/dependencies/github.com/google/gopacket/writer.gobra b/verification/dependencies/github.com/google/gopacket/writer.gobra index 9c8f84252..81df43eab 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -20,8 +20,12 @@ type SerializableLayer interface { requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) requires Mem(ubuf) preserves sl.Bytes(ubuf, 0, len(ubuf)) - ensures err == nil ==> (Mem(ubuf) && b.Mem()) - ensures err == nil ==> sl.Bytes(b.UBuf(), 0, len(b.UBuf())) + // The layer and the buffer survive also on error: all implementations + // fail without giving up Mem(ubuf) or the buffer resources. This is + // relied upon by callers that must restore their resources on the + // error path (e.g. the router's prepareSCMP). + ensures Mem(ubuf) && b.Mem() + ensures sl.Bytes(b.UBuf(), 0, len(b.UBuf())) ensures err != nil ==> err.ErrorMem() decreases SerializeTo(b SerializeBuffer, opts SerializeOptions, ghost ubuf []byte) (err error) From 2a0ca0de893ba08ff909c01537223c6a6ca4b716 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Jul 2026 12:30:20 +0000 Subject: [PATCH 05/19] Implement M2 (design v2): MemSerialize for fresh SCION headers Instead of adding a nil-buffer mode to SCION.Mem (which would make Mem(nil) satisfiable and thereby force nil-handling into every pure function and lemma that unfolds the predicate - they currently verify vacuously for nil), give freshly constructed SCION headers a separate predicate: - SCION.MemSerialize: field permissions, Path.Mem(nil) (satisfied for reversed paths via (*Decoded).Widen), fractional raw-address permissions that coexist with ChecksumMem, and the path pool. No facts about HdrLen/PayloadLen, which FixLengths computes during serialization. - SCION.IsSupportedSerialization: whether serializing this header yields a supported packet, expressed over PathType/NextHdr. - ChecksumMem re-fractioned (R25; wildcard for RawSrcAddr's bytes, which prepareSCMP can only obtain at wildcard amount from the data-plane's internal IP); computeChecksum/pseudoHeaderChecksum weakened to match (their only verified caller is SCMP.SerializeTo). - SerializableLayer gains MemSerialize and IsSupportedSerialization; trivial implementations for SCMP, the SCMP messages, Payload and BFD. - SerializeLayers gets a real trusted contract (replacing requires false): MemSerialize for the header layer, Mem(layerBufs[i]) for the rest, resources preserved also on error, and the trusted bridge IsSupportedRawPkt(w.View()) == old(layers[0].IsSupportedSerialization()). With this design the FixLengths relaxation of the SerializableLayer interface is unnecessary and verifying SCION.SerializeTo's FixLengths branch becomes optional hardening rather than a prerequisite: the fresh-flow serialization is axiomatized by the trusted SerializeLayers contract, documented as the load-bearing trusted assumption. Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 145 ++++++++++++------ pkg/slayers/scion.go | 55 +++---- pkg/slayers/scion_spec.gobra | 52 ++++++- pkg/slayers/scmp_msg_spec.gobra | 84 ++++++++++ pkg/slayers/scmp_spec.gobra | 12 ++ .../github.com/google/gopacket/base.gobra | 12 ++ .../google/gopacket/layers/bfd.gobra | 12 ++ .../github.com/google/gopacket/writer.gobra | 70 ++++++++- 8 files changed, 363 insertions(+), 79 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index 36162f2d7..96605e754 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -231,6 +231,47 @@ Removing `TODO()` requires all of the following, not just the `Mem` folds: ## 4. Proposed design +> **Design revision (v2), applied on this branch.** While implementing M2, +> a blocking property of the original §4.2 design surfaced: making +> `SCION.Mem(nil)` *satisfiable* forces nil-cases into every pure function +> and lemma that `unfolding`s the predicate (~21 sites in `pkg/slayers` +> alone, plus the router). Today those bodies verify for `ub == nil` +> vacuously — the precondition `Mem(nil)` is contradictory — but under the +> §4.2 rewrite each `ub[a:b]` slice inside them would need its own +> `ub != nil` guard or conditional, a large, error-prone ripple. +> +> The revised design instead leaves `SCION.Mem` **untouched** and gives the +> fresh SCION header a *separate* predicate: +> +> * `pred (s *SCION) MemSerialize()` (`scion_spec.gobra`) — field +> permissions, `Path.Mem(nil)` (satisfied by `(*Decoded).Widen`), the +> asymmetric fractional address-byte permissions of §4.3, and the path +> pool; deliberately nothing about `HdrLen`/`PayloadLen`. +> * `SerializableLayer` gains `pred MemSerialize()` and the ghost pure hook +> `IsSupportedSerialization()` (§4.6); all non-header layers implement +> them trivially (`true`/`false`). +> * The trusted `SerializeLayers` contract consumes +> `layers[0].MemSerialize()` for the header layer and +> `layers[i].Mem(layerBufs[i])` for `i ≥ 1` (the M1 `nil`-mode covers the +> fresh `scmpH`/`scmpP`; `Payload` uses the quote). +> +> Knock-on simplifications: the `FixLengths` relaxation of §4.4 is **no +> longer needed at all** — the interface `SerializeTo` spec is never +> invoked for the fresh flow (the only verified direct `SerializeTo` call, +> `updateSCIONLayer`, uses `FixLengths: false`), and `*SCION` keeps +> implementing the interface because its `Mem(nil)` stays unsatisfiable, +> making the nil-case of the implementation proof vacuous. Verifying +> `SCION.SerializeTo`'s `FixLengths` branch (old M3) is thereby demoted +> from a prerequisite to *optional hardening*: until it is done, the +> behavior of the fresh-flow serialization (including the `FixLengths` +> branch and the checksum computation) is axiomatized by the trusted +> `SerializeLayers` contract — a larger trusted surface, in exchange for a +> dramatically smaller and safer proof effort. +> +> §§4.1, 4.3, 4.5, 4.6 below remain accurate (4.5/4.6 modulo +> `MemSerialize` replacing "serialize-mode `Mem(nil)`" for the header +> layer); §4.2 and the `FixLengths` part of §4.4 are superseded. + ### 4.1 `nil`-mode `BaseLayer.Mem` (one change, many beneficiaries) Redefine (`scion_spec.gobra:244`): @@ -595,31 +636,45 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). derive `data != nil` and keep using the aliasing facts; * §4.6 step 1 done early (it is additive): `gopacket.IsSupportedRawPkt` twin + `slayers.IsSupportedRawPktEqGopacket` bridging lemma. -2. **M2 — serialize-mode `*SCION.Mem`** (§4.2) + `ChecksumMem` - re-fractioning, the asymmetric address-byte amounts, and the - `SetDstAddr`/`SetSrcAddr` postcondition strengthening (§4.3). Medium; - touches many `SCION` lemmas' guards (`ub != nil`). Start with a smoke - test that a wildcard conjunct inside a predicate body folds/unfolds as - expected. -3. **M3 — `(*SCION).SerializeTo`**: mode-split spec, `SerializeAddrHdr` - serialize-mode, verify the `FixLengths` branch, prove the - hook postcondition of §4.6 (step 3). This is the hardest single item. - Large. +2. **M2 — fresh-header predicate + checksum permission accounting** + (design revision v2, §4 preamble; supersedes the old serialize-mode + `*SCION.Mem` item). + **Status: implemented on this branch** (pending a CI/Gobra run): + * `SCION.MemSerialize` + the `IsSupportedSerialization` hook + (`scion_spec.gobra`); `SCION.Mem` untouched — zero ripple; + * `ChecksumMem` re-fractioned (R25, wildcard for `RawSrcAddr`'s bytes) + with `computeChecksum`/`pseudoHeaderChecksum` weakened accordingly + (R30 / wildcard; their only verified caller is `SCMP.SerializeTo`, + whose unfold/refold of `ChecksumMem` still balances); + * `SerializableLayer` extended with `MemSerialize` + + `IsSupportedSerialization`; trivial implementations for `SCMP`, the + 7 message types, `Payload`, and `BFD`; + * the trusted quantified `SerializeLayers` contract (§4.5, §4.6 step 4) + replacing `requires false` — including the + `IsSupportedRawPkt(w.View()) == old(layers[0].IsSupportedSerialization())` + bridge. No verified caller of `SerializeLayers` exists yet + (`bfdSend.Send` is trusted, `prepareSCMP`'s call is behind the + `TODO()`), so this lands without new obligations. + Still open from §4.3 (now M5 prerequisites): `SetDstAddr`'s + postcondition must expose a fraction of `sl.Bytes(s.RawDstAddr, ...)` + (with a wand to restore `dst.Mem()`), and `SetSrcAddr`'s wildcard mode + needs (a) a component-wise precondition (folding `net.IPAddr.Mem()` at + wildcard amount is not possible) and (b) length postconditions + (`len(s.RawSrcAddr)` even) also in wildcard mode. +3. **M3 (optional hardening) — `(*SCION).SerializeTo` fresh mode**: verify + the `FixLengths` branch and the byte-level hook postcondition of §4.6 + (step 3) against `MemSerialize`, then shrink the trusted + `SerializeLayers` contract to something justified per-layer. No longer + a prerequisite for removing the `TODO()` (see the §4 preamble). Large. 4. **M4 — interface + `SerializeLayers` spec updates** in `writer.gobra` - (§4.4, §4.5, §4.6 steps 1–2, 4): relax `FixLengths`, strengthen error - postconditions, add the ghost hook, the gopacket-level - `IsSupportedRawPkt` twin + bridging lemma, and the quantified trusted - `SerializeLayers` spec; re-verify the closed set of implementers; - adjust the `Payload`/`BFD` trusted stubs. Medium. - **Status: partially implemented on this branch** (pending a CI/Gobra - run): the error-case postconditions of `SerializableLayer.SerializeTo` - and all implementations (`SCMP` + the 7 message types re-fold `Mem` - before every error return, so their strengthened specs remain provable; - `Payload`/`BFD` stubs adjusted textually; `SCION` was already - unconditional), plus the `IsSupportedRawPkt` twin + bridging lemma. - Deliberately *not* yet done: the `FixLengths` relaxation (it would - break `*SCION`'s implementation proof until M3 verifies the - `FixLengths` branch), the ghost hook, and the `SerializeLayers` spec. + (§4.5, §4.6 steps 1–2, 4). + **Status: implemented on this branch** (pending a CI/Gobra run), + split across M2/M4 commits: error-case postconditions of + `SerializableLayer.SerializeTo` and all implementations strengthened + to unconditional; `IsSupportedRawPkt` twin + bridging lemma; the + `MemSerialize`/`IsSupportedSerialization` interface members; the + trusted `SerializeLayers` contract. The `FixLengths` relaxation + originally planned here is not needed under design v2. 5. **M5 — `prepareSCMP` itself** (§5): spec extensions, call-site folds, ghost `layerBufs`, drop the `TODO()`. Large, but mostly mechanical once M1–M4 are in; expect iteration on router CI time. @@ -631,25 +686,29 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). * **Verification time** of `dataplane.go` (already the 6 h/`chop 10` package). Mitigate with `outline(...)` blocks and `opaque` helper functions for the new fold-heavy regions. -* **Wildcard permission amounts inside predicate bodies** (§4.3) and - wildcard-mode folds of `net.IPAddr.Mem()` are less-trodden Gobra - territory; validate with a small experiment before building M2 on them. - Fallback: keep the `RawSrcAddr` bytes *outside* the predicates entirely - and weaken `SerializeAddrHdr`/`computeChecksum`'s specs to take them as - separate wildcard clauses — workable because those specs are on concrete - methods, but it makes the serialize-mode `SCION.Mem` non-self-contained, - which conflicts with interface dispatch (§4.5); in that case the src - bytes would have to ride in a second, `slayers`-internal predicate - referenced from `Mem`'s serialize branch. -* **Gobra interface-implementation proofs** with mode-split permission - amounts (`ubuf == nil ? full : R0`) and ghost pure interface methods are - unusual; unlike in a design where the SCION call is concrete, `*SCION` - **must** remain a `SerializableLayer` implementer here, so brittleness - in the implementation proof has no cheap fallback — prototype early - (M4 before M3 completion is fine, the two are independent). -* **The trusted `SerializeLayers` IO clause** (§4.6 step 4) is a genuine - (if small) soundness assumption about which layer is outermost; gate it - with the `IsNetworkHeaderLayer()` hook to keep it honest. +* **Wildcard permission amounts inside predicate bodies** + (`ChecksumMem`/`MemSerialize`, §4.3) have precedent in the codebase + (`fold acc(sl.Bytes(ip, ...), _)` in `scion.go`'s address helpers, + wildcard folds in `pkg/experimental/epic`), but the combination with + loop invariants in `pseudoHeaderChecksum` should be watched in the + first CI run. Fallback: keep the `RawSrcAddr` bytes outside the + predicates and thread them as separate wildcard clauses through + `computeChecksum` (concrete-method spec, no interface constraint). +* **Ghost pure interface methods with predicate-based preconditions** + (`IsSupportedSerialization` requiring `acc(MemSerialize(), _)`) follow + the `SerializeBuffer.UBuf()` pattern but are less common on + implementation-proved interfaces; if the implementation proofs are + brittle, the hook can move out of the interface into a + `*SCION`-specific pure function, at the cost of expressing the trusted + `SerializeLayers` IO clause via a type assertion on `layers[0]`. +* **The trusted `SerializeLayers` contract is now the load-bearing trusted + assumption**: it axiomatizes the fresh-flow serialization behavior + (including `SCION.SerializeTo`'s unverified `FixLengths` branch and the + checksum computation) and asserts the IO clause for whatever layer is + passed first. It is documented as such in `writer.gobra`; M3 exists to + shrink it. The IO clause could additionally be gated by an + `IsNetworkHeaderLayer()`-style hook to keep it honest against misuse + with a non-header first layer. * **`SrcAddr()`/`SetDstAddr` aliasing**: the `RawDstAddr` fraction originates from `acc(p.scionLayer.Mem(ub), R4)`-governed memory via a magic wand; getting the fraction arithmetic right (so that the wand can diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index e9e4717f7..23aae4991 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -978,16 +978,19 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) { } // computeChecksum computes the checksum with the SCION pseudo header. -// @ requires acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20) +// (VerifiedSCION) The permission amounts for the raw addresses are chosen +// so that they can be supplied from an unfolded ChecksumMem instance (which +// holds them at R25, resp. at wildcard amount for RawSrcAddr's bytes). +// @ requires acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30) // @ requires len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0 -// @ requires acc(&s.SrcIA, R20) && acc(&s.DstIA, R20) -// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) -// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) +// @ requires acc(&s.SrcIA, R30) && acc(&s.DstIA, R30) +// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) +// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ preserves acc(sl.Bytes(upperLayer, 0, len(upperLayer)), R20) -// @ ensures acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20) -// @ ensures acc(&s.SrcIA, R20) && acc(&s.DstIA, R20) -// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) -// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) +// @ ensures acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30) +// @ ensures acc(&s.SrcIA, R30) && acc(&s.DstIA, R30) +// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) +// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ ensures s == nil ==> err != nil // @ ensures len(s.RawDstAddr) == 0 ==> err != nil // @ ensures len(s.RawSrcAddr) == 0 ==> err != nil @@ -1007,15 +1010,15 @@ func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (res uint16, return folded, nil } -// @ requires acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20) +// @ requires acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30) // @ requires len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0 -// @ requires acc(&s.SrcIA, R20) && acc(&s.DstIA, R20) -// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) -// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) -// @ ensures acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20) -// @ ensures acc(&s.SrcIA, R20) && acc(&s.DstIA, R20) -// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) -// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) +// @ requires acc(&s.SrcIA, R30) && acc(&s.DstIA, R30) +// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) +// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) +// @ ensures acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30) +// @ ensures acc(&s.SrcIA, R30) && acc(&s.DstIA, R30) +// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) +// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ ensures len(s.RawDstAddr) == 0 ==> err != nil // @ ensures len(s.RawSrcAddr) == 0 ==> err != nil // @ ensures err != nil ==> err.ErrorMem() @@ -1045,43 +1048,43 @@ func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (res uint32, er } // Address length is guaranteed to be a multiple of 2 by the protocol. // @ ghost var rawSrcAddrLen int = len(s.RawSrcAddr) - // @ invariant acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) + // @ invariant acc(&s.RawSrcAddr, R30) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) // @ invariant len(s.RawSrcAddr) == rawSrcAddrLen // @ invariant len(s.RawSrcAddr) % 2 == 0 // @ invariant i % 2 == 0 // @ invariant 0 <= i && i <= len(s.RawSrcAddr) // @ decreases len(s.RawSrcAddr) - i for i := 0; i < len(s.RawSrcAddr); i += 2 { - // @ requires acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) + // @ requires acc(&s.RawSrcAddr, R30) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) // @ requires 0 <= i && i < len(s.RawSrcAddr) && i % 2 == 0 && len(s.RawSrcAddr) % 2 == 0 - // @ ensures acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) + // @ ensures acc(&s.RawSrcAddr, R30) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) // @ ensures s.RawSrcAddr === before(s.RawSrcAddr) // @ decreases // @ outline( - // @ unfold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) + // @ unfold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) csum += uint32(s.RawSrcAddr[i]) << 8 csum += uint32(s.RawSrcAddr[i+1]) - // @ fold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) + // @ fold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) // @ ) } // @ ghost var rawDstAddrLen int = len(s.RawDstAddr) - // @ invariant acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) + // @ invariant acc(&s.RawDstAddr, R30) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ invariant len(s.RawDstAddr) == rawDstAddrLen // @ invariant len(s.RawDstAddr) % 2 == 0 // @ invariant i % 2 == 0 // @ invariant 0 <= i && i <= len(s.RawDstAddr) // @ decreases len(s.RawDstAddr) - i for i := 0; i < len(s.RawDstAddr); i += 2 { - // @ requires acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) + // @ requires acc(&s.RawDstAddr, R30) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ requires 0 <= i && i < len(s.RawDstAddr) && i % 2 == 0 && len(s.RawDstAddr) % 2 == 0 - // @ ensures acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) + // @ ensures acc(&s.RawDstAddr, R30) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ ensures s.RawDstAddr === before(s.RawDstAddr) // @ decreases // @ outline( - // @ unfold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) + // @ unfold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) csum += uint32(s.RawDstAddr[i]) << 8 csum += uint32(s.RawDstAddr[i+1]) - // @ fold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) + // @ fold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30) // @ ) } l := uint32(length) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index d10e22a5f..970c2c021 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -233,12 +233,56 @@ func (s *SCION) DowngradePerm(ghost ub []byte) { fold s.NonInitMem() } +// ChecksumMem holds the resources of a SCION header that are needed to +// compute an upper layer's checksum (cf. computeChecksum). An instance is +// handed to the upper layer via SetNetworkLayerForChecksum and must be able +// to coexist with the same header's own memory predicate (cf. MemSerialize +// and the router's prepareSCMP), so all permission amounts are fractional. +// The bytes of RawSrcAddr are held at wildcard amount because prepareSCMP +// can obtain the buffer underlying the source address (the data-plane's +// internal IP) only at wildcard amount itself. pred (s *SCION) ChecksumMem() { - acc(&s.RawSrcAddr) && acc(&s.RawDstAddr) && + acc(&s.RawSrcAddr, R25) && acc(&s.RawDstAddr, R25) && len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0 && - acc(&s.SrcIA) && acc(&s.DstIA) && - sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)) && - sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)) + acc(&s.SrcIA, R25) && acc(&s.DstIA, R25) && + acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) && + acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R25) +} + +// MemSerialize is the memory predicate of a freshly constructed (i.e., not +// decoded) SCION layer that is about to be serialized, e.g. the SCMP reply +// header built by the router's prepareSCMP. Unlike Mem, it does not tie the +// layer to an underlying buffer: the path is held with a nil buffer (which +// *scion.Decoded supports, cf. (*Decoded).Widen), and the raw addresses are +// held fractionally so that a ChecksumMem instance for the same header can +// coexist with it during serialization. The bytes of RawSrcAddr are held at +// wildcard amount for the same reason as in ChecksumMem. Deliberately, no +// facts are stated about HdrLen and PayloadLen: they are computed during +// serialization (SerializeOptions.FixLengths). +pred (s *SCION) MemSerialize() { + acc(&s.Version) && acc(&s.TrafficClass) && acc(&s.FlowID) && + acc(&s.NextHdr) && acc(&s.HdrLen) && acc(&s.PayloadLen) && + acc(&s.PathType) && 0 <= s.PathType && s.PathType < path.MaxPathType && + acc(&s.DstAddrType) && acc(&s.SrcAddrType) && + acc(&s.Path) && s.Path != nil && s.Path.Mem(nil) && + acc(&s.BaseLayer) && + acc(&s.DstIA, R25) && acc(&s.SrcIA, R25) && + acc(&s.RawDstAddr, R25) && acc(&s.RawSrcAddr, R25) && + acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R25) && + acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) && + acc(&s.pathPool) && acc(&s.pathPoolRaw) && + PathPoolMem(s.pathPool, s.pathPoolRaw) +} + +// Returns whether serializing this (freshly constructed) SCION header as +// the outermost header yields a supported packet in the sense of +// IsSupportedPkt/IsSupportedRawPkt, expressed over the header's fields. +ghost +requires acc(s.MemSerialize(), _) +decreases +pure func (s *SCION) IsSupportedSerialization() bool { + return unfolding acc(s.MemSerialize(), _) in + s.PathType == scion.PathType && s.NextHdr != L4SCMP } // A BaseLayer predicate instance is in one of two modes: diff --git a/pkg/slayers/scmp_msg_spec.gobra b/pkg/slayers/scmp_msg_spec.gobra index 4209bc0a4..97f03332c 100644 --- a/pkg/slayers/scmp_msg_spec.gobra +++ b/pkg/slayers/scmp_msg_spec.gobra @@ -53,6 +53,18 @@ func (b *SCMPExternalInterfaceDown) LayerPayload(ghost ub []byte) (res []byte, g } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPExternalInterfaceDown they are trivial. +pred (s *SCMPExternalInterfaceDown) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPExternalInterfaceDown) IsSupportedSerialization() bool { + return false +} + (*SCMPExternalInterfaceDown) implements gopacket.Layer (*SCMPExternalInterfaceDown) implements gopacket.SerializableLayer @@ -99,6 +111,18 @@ func (b *SCMPInternalConnectivityDown) LayerPayload(ghost ub []byte) (res []byte return res, start, end } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPInternalConnectivityDown they are trivial. +pred (s *SCMPInternalConnectivityDown) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPInternalConnectivityDown) IsSupportedSerialization() bool { + return false +} + (*SCMPInternalConnectivityDown) implements gopacket.Layer (*SCMPInternalConnectivityDown) implements gopacket.SerializableLayer @@ -145,6 +169,18 @@ func (b *SCMPEcho) LayerPayload(ghost ub []byte) (res []byte, ghost start int, g return res, start, end } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPEcho they are trivial. +pred (s *SCMPEcho) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPEcho) IsSupportedSerialization() bool { + return false +} + (*SCMPEcho) implements gopacket.Layer (*SCMPEcho) implements gopacket.SerializableLayer @@ -191,6 +227,18 @@ func (b *SCMPParameterProblem) LayerPayload(ghost ub []byte) (res []byte, ghost return res, start, end } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPParameterProblem they are trivial. +pred (s *SCMPParameterProblem) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPParameterProblem) IsSupportedSerialization() bool { + return false +} + (*SCMPParameterProblem) implements gopacket.Layer (*SCMPParameterProblem) implements gopacket.SerializableLayer @@ -242,6 +290,18 @@ func (b *SCMPTraceroute) LayerPayload(ghost ub []byte) (res []byte, ghost start return res, start, end } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPTraceroute they are trivial. +pred (s *SCMPTraceroute) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPTraceroute) IsSupportedSerialization() bool { + return false +} + (*SCMPTraceroute) implements gopacket.Layer (*SCMPTraceroute) implements gopacket.SerializableLayer @@ -289,6 +349,18 @@ func (b *SCMPDestinationUnreachable) LayerPayload(ghost ub []byte) (res []byte, return res, start, end } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPDestinationUnreachable they are trivial. +pred (s *SCMPDestinationUnreachable) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPDestinationUnreachable) IsSupportedSerialization() bool { + return false +} + (*SCMPDestinationUnreachable) implements gopacket.Layer (*SCMPDestinationUnreachable) implements gopacket.SerializableLayer @@ -335,6 +407,18 @@ func (b *SCMPPacketTooBig) LayerPayload(ub []byte) (res []byte, ghost start int, return res, start, end } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMPPacketTooBig they are trivial. +pred (s *SCMPPacketTooBig) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMPPacketTooBig) IsSupportedSerialization() bool { + return false +} + (*SCMPPacketTooBig) implements gopacket.Layer (*SCMPPacketTooBig) implements gopacket.SerializableLayer diff --git a/pkg/slayers/scmp_spec.gobra b/pkg/slayers/scmp_spec.gobra index c7cdf7233..8f1c3e0f4 100644 --- a/pkg/slayers/scmp_spec.gobra +++ b/pkg/slayers/scmp_spec.gobra @@ -84,6 +84,18 @@ func (s *SCMP) FoldFreshMem() { fold s.Mem(nil) } +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for SCMP they are trivial. +pred (s *SCMP) MemSerialize() { true } + +ghost +pure +decreases +func (s *SCMP) IsSupportedSerialization() bool { + return false +} + (*SCMP) implements gopacket.Layer (*SCMP) implements gopacket.SerializableLayer (*SCMP) implements gopacket.DecodingLayer diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra index a7a935fb3..383f2e759 100644 --- a/verification/dependencies/github.com/google/gopacket/base.gobra +++ b/verification/dependencies/github.com/google/gopacket/base.gobra @@ -73,6 +73,18 @@ ensures err != nil ==> err.ErrorMem() decreases func (p Payload) SerializeTo(b SerializeBuffer, opts SerializeOptions, ghost ubuf []byte) (err error) +// (VerifiedSCION) MemSerialize and IsSupportedSerialization are only +// meaningful for network-header layers serialized as the outermost layer +// of a packet (cf. SerializableLayer); for Payload they are trivial. +pred (p Payload) MemSerialize() { true } + +ghost +pure +decreases +func (p Payload) IsSupportedSerialization() bool { + return false +} + Payload implements Layer Payload implements ApplicationLayer Payload implements SerializableLayer diff --git a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra index e4c104698..3e364e8c6 100644 --- a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra +++ b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra @@ -218,4 +218,16 @@ ensures d.NonInitMem() decreases func (d *BFD) DowngradePerm(ghost ub []byte) +// MemSerialize and IsSupportedSerialization are only meaningful for +// network-header layers serialized as the outermost layer of a packet +// (cf. gopacket.SerializableLayer); for BFD they are trivial. +pred (d *BFD) MemSerialize() { true } + +ghost +pure +decreases +func (d *BFD) IsSupportedSerialization() bool { + return false +} + (*BFD) implements gopacket.SerializableLayer \ No newline at end of file diff --git a/verification/dependencies/github.com/google/gopacket/writer.gobra b/verification/dependencies/github.com/google/gopacket/writer.gobra index 81df43eab..de0c944d0 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -15,6 +15,13 @@ import "verification/utils/seqs" type SerializableLayer interface { pred Mem(ubuf []byte) + // (VerifiedSCION) Resources of a freshly constructed (i.e., not + // decoded) instance that is about to be serialized without an + // underlying buffer. Only meaningful for layers that SerializeLayers + // serializes as the outermost header of a packet (cf. slayers.SCION); + // all other layers may define it as true. + pred MemSerialize() + requires !opts.FixLengths requires b != nil && b.Mem() requires sl.Bytes(b.UBuf(), 0, len(b.UBuf())) @@ -30,6 +37,17 @@ type SerializableLayer interface { decreases SerializeTo(b SerializeBuffer, opts SerializeOptions, ghost ubuf []byte) (err error) + // (VerifiedSCION) Whether serializing this (freshly constructed) + // instance as the outermost header of a packet yields a supported + // packet in the sense of IsSupportedRawPkt. Only meaningful for + // network-header layers (cf. slayers.SCION); all other layers may + // define it as false. + ghost + pure + requires acc(MemSerialize(), _) + decreases + IsSupportedSerialization() bool + pure decreases LayerType() LayerType @@ -106,11 +124,51 @@ ensures sl.Bytes(res.UBuf(), 0, len(res.UBuf())) decreases func NewSerializeBuffer() (res SerializeBuffer) -// TODO: requires changes to provide access to the underlying layers -requires false +// SerializeLayers clears the given write buffer, then writes all layers +// into it so they correctly wrap each other. +// +// (VerifiedSCION) This specification is trusted. It is justified against +// the (unverified) implementation, which calls w.Clear() and then +// layers[i].SerializeTo(w, opts) from the last layer to the first, +// returning on the first error (plus PushLayer bookkeeping that is +// unobservable through this package's specifications). It is specialized +// to the call shape of the verified router: layers[0] is the freshly +// constructed network-header layer of the packet (a *slayers.SCION), whose +// resources are given by MemSerialize; all later layers are either freshly +// constructed layers with a nil underlying buffer or a raw payload +// aliasing layerBufs[i], with resources given by Mem(layerBufs[i]). +// +// The last postcondition is the trusted bridge for the router's +// IO-level property that SCMP replies are unsupported packets: the header +// layer is serialized last and prepended at the front of the buffer, so +// the bytes inspected by IsSupportedRawPkt are exactly the ones it wrote, +// and they are determined by the fields captured in the old state of its +// MemSerialize (serialization does not change them; FixLengths only +// assigns the header/payload lengths). +requires w != nil && w.Mem() +requires sl.Bytes(w.UBuf(), 0, len(w.UBuf())) requires len(layerBufs) == len(layers) -preserves w.Mem() -preserves acc(layerBufs, R20) -preserves forall i int :: {&layers[i]} 0 <= i && i < len(layers) ==> acc(&layers[i]) && layers[i].Mem(layerBufs[i]) +requires 0 < len(layers) +requires acc(layerBufs, R50) +requires forall i, j int :: { &layers[i], &layers[j] } 0 <= i && i < j && j < len(layers) ==> + layers[i] !== layers[j] +requires forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> + (acc(&layers[i], R50) && layers[i] != nil) +requires layers[0].MemSerialize() +requires forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> + layers[i].Mem(layerBufs[i]) +requires forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> + sl.Bytes(layerBufs[i], 0, len(layerBufs[i])) +ensures w.Mem() && sl.Bytes(w.UBuf(), 0, len(w.UBuf())) +ensures acc(layerBufs, R50) +ensures forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> acc(&layers[i], R50) +ensures layers[0].MemSerialize() +ensures forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> + layers[i].Mem(layerBufs[i]) +ensures forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> + sl.Bytes(layerBufs[i], 0, len(layerBufs[i])) +ensures err == nil ==> + IsSupportedRawPkt(w.View()) == old(layers[0].IsSupportedSerialization()) +ensures err != nil ==> err.ErrorMem() decreases -func SerializeLayers(w SerializeBuffer, opts SerializeOptions, ghost layerBufs []([]byte), layers ...SerializableLayer) error +func SerializeLayers(w SerializeBuffer, opts SerializeOptions, ghost layerBufs []([]byte), layers ...SerializableLayer) (err error) From 202d480aa0670bfd4bc865222e2020d0449af60d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Jul 2026 12:34:38 +0000 Subject: [PATCH 06/19] Strengthen address-setter contracts for the fresh-header flow - SetDstAddr (IP case) no longer applies packAddr's magic wand internally; it exposes the R20 fraction of the bytes underlying RawDstAddr together with the wand to give it back, so that prepareSCMP can store byte fractions in the fresh header's MemSerialize/ChecksumMem predicates during serialization and still restore dst.Mem() afterwards. Its only verified caller is prepareSCMP's currently-unverified tail, so the post shape is free to change. - packAddr/SetDstAddr/SetSrcAddr gain 'T4Ip implies length 4' postconditions, provable from To4's contract. - Add FoldFreshMemSerializeWithChecksumMem: the machine-checked witness that MemSerialize and ChecksumMem fold together from the resources prepareSCMP holds (fraction accounting 2xR25 within R20, wildcard source bytes, path with nil buffer). Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 29 +++++++++++++++++++++++------ pkg/slayers/scion.go | 21 +++++++++++++++++---- pkg/slayers/scion_spec.gobra | 30 ++++++++++++++++++++++++++++++ 3 files changed, 70 insertions(+), 10 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index 96605e754..51a05bddb 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -655,12 +655,29 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). bridge. No verified caller of `SerializeLayers` exists yet (`bfdSend.Send` is trusted, `prepareSCMP`'s call is behind the `TODO()`), so this lands without new obligations. - Still open from §4.3 (now M5 prerequisites): `SetDstAddr`'s - postcondition must expose a fraction of `sl.Bytes(s.RawDstAddr, ...)` - (with a wand to restore `dst.Mem()`), and `SetSrcAddr`'s wildcard mode - needs (a) a component-wise precondition (folding `net.IPAddr.Mem()` at - wildcard amount is not possible) and (b) length postconditions - (`len(s.RawSrcAddr)` even) also in wildcard mode. + The §4.3 items are also resolved on this branch: + * `SetDstAddr` (IP case) no longer applies packAddr's magic wand + internally; it exposes `acc(sl.Bytes(s.RawDstAddr, ...), R20)` plus + the wand `... --* acc(dst.Mem(), R20)` to the caller (its only + verified caller is prepareSCMP's currently-dead code, so the + post-shape change is safe), alongside `acc(dst.Mem(), R19+R20)`; + * `SetSrcAddr`'s wildcard mode needs **no** component-wise + precondition after all: folding `net.IPAddr.Mem()` at wildcard + amount is legal (precedent: the wildcard branches inside `packAddr` + itself, e.g. `fold acc(sl.Bytes(ip, ...), _)`), and its wildcard + postcondition already returns the wildcard bytes of `RawSrcAddr`; + * `packAddr`/`SetDstAddr`/`SetSrcAddr` gained `T4Ip ==> len == 4` + postconditions (from `To4`'s contract); + * `FoldFreshMemSerializeWithChecksumMem` is the machine-checked + witness that `MemSerialize` and `ChecksumMem` fold together from + prepareSCMP's resources (fraction accounting: 2 × R25 ⊆ R20). + Remaining genuine gap for M5: the evenness of `len(s.RawSrcAddr)` when + the source is the data-plane's `internalIP` and the `T16Ip` fallback is + taken — `internalIPInv` (`router/dataplane_spec.gobra:111`) does not + constrain the IP's length, so it must be strengthened to + `len ∈ {4, 16}` (dischargeable at the config boundary + `dataplane.go:408`, possibly with a justified assumption like the + existing `assume 0 <= e.ExtLen` precedent). 3. **M3 (optional hardening) — `(*SCION).SerializeTo` fresh mode**: verify the `FixLengths` branch and the byte-level hook postcondition of §4.6 (step 3) against `MemSerialize`, then shrink the trusted diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index 23aae4991..4882dcbcd 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -674,7 +674,16 @@ func (s *SCION) SrcAddr() (res net.Addr, err error) { // @ ensures res == nil && wildcard && isIP(dst) ==> acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), _) // @ ensures res == nil && wildcard && isHostSVC(dst) ==> sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)) // @ ensures res == nil && !wildcard && isHostSVC(dst) ==> sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)) -// @ ensures res == nil && !wildcard ==> acc(dst.Mem(), R18) +// @ ensures res == nil && !wildcard && isHostSVC(dst) ==> acc(dst.Mem(), R18) +// (VerifiedSCION) In the IP case, a fraction of the bytes underlying +// RawDstAddr is exposed to the caller (together with a magic wand to give +// it back), instead of returning acc(dst.Mem(), R18) in one piece. This is +// needed by the router's prepareSCMP, which must store that fraction in +// the fresh header's MemSerialize/ChecksumMem predicates while serializing. +// @ ensures res == nil && !wildcard && isIP(dst) ==> acc(dst.Mem(), R19) && acc(dst.Mem(), R20) +// @ ensures res == nil && !wildcard && isIP(dst) ==> +// @ acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) && +// @ (acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) --* acc(dst.Mem(), R20)) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv4(dst) ==> forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> &s.RawDstAddr[i] == &dst.(*net.IPAddr).IP[i])) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv6(dst) && isConvertibleToIPv4(dst) ==> forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> &s.RawDstAddr[i] == &dst.(*net.IPAddr).IP[12+i])) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (!isIPv4(dst) && !isIPv6(dst) ==> forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> &s.RawDstAddr[i] == &dst.(*net.IPAddr).IP[i])) @@ -684,14 +693,16 @@ func (s *SCION) SrcAddr() (res net.Addr, err error) { // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (!isIPv4(dst) && !isIPv6(dst) ==> len(dst.(*net.IPAddr).IP) == len(s.RawDstAddr))) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv6(dst) && !isConvertibleToIPv4(dst) ==> len(dst.(*net.IPAddr).IP) == len(s.RawDstAddr))) // @ ensures (res == nil) == (typeOf(dst) == type[*net.IPAddr] || typeOf(dst) == type[addr.HostSVC]) +// @ ensures res == nil && isIP(dst) && s.DstAddrType == T4Ip ==> len(s.RawDstAddr) == 4 // @ decreases func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res error) { var err error var verScionTmp []byte s.DstAddrType, verScionTmp, err = packAddr(dst /*@ , wildcard @*/) - // @ ghost if !wildcard && err == nil && isIP(dst) { - // @ apply acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(dst.Mem(), R20) - // @ } + // (VerifiedSCION) The magic wand returned by packAddr is deliberately + // not applied here: it is passed on to the caller (cf. the + // postconditions), so that the byte fraction of the raw address + // remains directly available during serialization. s.RawDstAddr = verScionTmp return err } @@ -721,6 +732,7 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro // @ ensures res == nil && !wildcard && isIP(src) ==> (unfolding acc(src.Mem(), R20) in (!isIPv4(src) && !isIPv6(src) ==> len(src.(*net.IPAddr).IP) == len(s.RawSrcAddr))) // @ ensures res == nil && !wildcard && isIP(src) ==> (unfolding acc(src.Mem(), R20) in (isIPv6(src) && !isConvertibleToIPv4(src) ==> len(src.(*net.IPAddr).IP) == len(s.RawSrcAddr))) // @ ensures (res == nil) == (typeOf(src) == type[*net.IPAddr] || typeOf(src) == type[addr.HostSVC]) +// @ ensures res == nil && isIP(src) && s.SrcAddrType == T4Ip ==> len(s.RawSrcAddr) == 4 // @ decreases func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error) { var err error @@ -799,6 +811,7 @@ func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) { // @ ensures err == nil && !wildcard && isIP(hostAddr) ==> (unfolding acc(hostAddr.Mem(), R20) in (!isIPv4(hostAddr) && !isIPv6(hostAddr) ==> len(hostAddr.(*net.IPAddr).IP) == len(b))) // @ ensures err == nil && !wildcard && isIP(hostAddr) ==> (unfolding acc(hostAddr.Mem(), R20) in (isIPv6(hostAddr) && !isConvertibleToIPv4(hostAddr) ==> len(hostAddr.(*net.IPAddr).IP) == len(b))) // @ ensures (err == nil) == (typeOf(hostAddr) == type[*net.IPAddr] || typeOf(hostAddr) == type[addr.HostSVC]) +// @ ensures err == nil && isIP(hostAddr) && addrtyp == T4Ip ==> len(b) == 4 // @ decreases func packAddr(hostAddr net.Addr /*@ , ghost wildcard bool @*/) (addrtyp AddrType, b []byte, err error) { switch a := hostAddr.(type) { diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 970c2c021..1e712bb16 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -285,6 +285,36 @@ pure func (s *SCION) IsSupportedSerialization() bool { s.PathType == scion.PathType && s.NextHdr != L4SCMP } +// Folds MemSerialize together with a coexisting ChecksumMem instance for a +// freshly constructed (i.e., not decoded) SCION header, from the resources +// that the router's prepareSCMP holds after constructing the SCMP reply +// header: full permissions to the header's own fields, the reversed path +// re-associated with a nil buffer (cf. (*Decoded).Widen), an R20 fraction +// of the destination address bytes (cf. SetDstAddr), and a wildcard +// fraction of the source address bytes (cf. SetSrcAddr in wildcard mode). +// This lemma is the machine-checked witness that the fraction accounting +// of the two predicates works out. +ghost +requires acc(&s.Version) && acc(&s.TrafficClass) && acc(&s.FlowID) +requires acc(&s.NextHdr) && acc(&s.HdrLen) && acc(&s.PayloadLen) +requires acc(&s.PathType) && 0 <= s.PathType && s.PathType < path.MaxPathType +requires acc(&s.DstAddrType) && acc(&s.SrcAddrType) +requires acc(&s.Path) && s.Path != nil && s.Path.Mem(nil) +requires acc(&s.BaseLayer) +requires acc(&s.DstIA, R20) && acc(&s.SrcIA, R20) +requires acc(&s.RawDstAddr, R20) && acc(&s.RawSrcAddr, R20) +requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) +requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) +requires len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0 +requires acc(&s.pathPool) && acc(&s.pathPoolRaw) +requires PathPoolMem(s.pathPool, s.pathPoolRaw) +ensures s.MemSerialize() && s.ChecksumMem() +decreases +func (s *SCION) FoldFreshMemSerializeWithChecksumMem() { + fold s.MemSerialize() + fold s.ChecksumMem() +} + // A BaseLayer predicate instance is in one of two modes: // - decoded mode (ub != nil): the layer was obtained via DecodeFromBytes // and Contents and Payload alias the underlying buffer ub around From 2c2b53e888aac70a81817af1fc956ab957906b85 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 12 Jul 2026 10:57:12 +0000 Subject: [PATCH 07/19] Fix well-formedness of the SerializeLayers contract The pairwise-distinctness clause dereferenced layers[i]/layers[j] before the quantifier granting permission to the slice cells; contract well-formedness is checked left to right, so all three CI jobs failed with 'Permission to layers[i] might not suffice' (writer.gobra:153). Reorder the clauses, permissions first, matching decodeLayers. This was the only error in the entire run: router/ verified across all 10 chops otherwise, and every package that ran before the error was clean (pkg/slayers had not run yet - verify-deps aborts at the first package importing gopacket). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- .../dependencies/github.com/google/gopacket/writer.gobra | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/verification/dependencies/github.com/google/gopacket/writer.gobra b/verification/dependencies/github.com/google/gopacket/writer.gobra index de0c944d0..603d9ae77 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -150,10 +150,11 @@ requires sl.Bytes(w.UBuf(), 0, len(w.UBuf())) requires len(layerBufs) == len(layers) requires 0 < len(layers) requires acc(layerBufs, R50) -requires forall i, j int :: { &layers[i], &layers[j] } 0 <= i && i < j && j < len(layers) ==> - layers[i] !== layers[j] requires forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> (acc(&layers[i], R50) && layers[i] != nil) +// Due to Viper's very strict injectivity constraints (cf. decodeLayers): +requires forall i, j int :: { &layers[i], &layers[j] } 0 <= i && i < j && j < len(layers) ==> + layers[i] !== layers[j] requires layers[0].MemSerialize() requires forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> layers[i].Mem(layerBufs[i]) From ce5ea3be7c66ccd1fe5c5a1f5e76ccb36b496269 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 12 Jul 2026 11:06:49 +0000 Subject: [PATCH 08/19] Fix SetDstAddr wand shape and adapt testDstSetter pkg/slayers reported two errors on the previous run (everything else, including the router job, was green): - scion.go:684: the postcondition wand over s.RawDstAddr could not be matched against the wand instance created inside packAddr (which is shaped over packAddr's own variables; Silicon matches wand instances structurally). Re-package the wand in SetDstAddr's body with exactly the postcondition's shape, applying packAddr's wand inside the package block. - scion_test.gobra:75: testDstSetter expected the full dst.Mem() back immediately; under the new contract the caller first applies the returned wand to give back the loaned byte fraction. Adapting the test also documents the intended usage of the new postcondition. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- pkg/slayers/scion.go | 10 +++++++++- pkg/slayers/scion_test.gobra | 5 +++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index 4882dcbcd..dbb6c9d1f 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -702,8 +702,16 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro // (VerifiedSCION) The magic wand returned by packAddr is deliberately // not applied here: it is passed on to the caller (cf. the // postconditions), so that the byte fraction of the raw address - // remains directly available during serialization. + // remains directly available during serialization. It is re-packaged + // below so that the instance held matches the shape stated in the + // postcondition (a wand over s.RawDstAddr instead of over packAddr's + // return value). s.RawDstAddr = verScionTmp + // @ ghost if !wildcard && err == nil && isIP(dst) { + // @ package acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) --* acc(dst.Mem(), R20) { + // @ apply acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(dst.Mem(), R20) + // @ } + // @ } return err } diff --git a/pkg/slayers/scion_test.gobra b/pkg/slayers/scion_test.gobra index 3678ddaee..5849d80d3 100644 --- a/pkg/slayers/scion_test.gobra +++ b/pkg/slayers/scion_test.gobra @@ -18,6 +18,7 @@ package slayers import ( "net" + . "github.com/scionproto/scion/verification/utils/definitions" sl "github.com/scionproto/scion/verification/utils/slices" "github.com/scionproto/scion/pkg/addr" ) @@ -71,6 +72,10 @@ requires acc(&s.DstAddrType) requires acc(dst.Mem()) func testDstSetter(s *SCION, dst *net.IPAddr) { res := s.SetDstAddr(dst, false) + // SetDstAddr loans a fraction of the bytes underlying s.RawDstAddr to + // the caller; applying the returned magic wand gives it back, after + // which the full permission to dst.Mem() is restored. + apply acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) --* acc(dst.Mem(), R20) // unfolding dst.Mem() grants us permission to s.RawDstAddr since they are aliased unfold dst.Mem() assert forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> acc(&s.RawDstAddr[i]) From 8c27094df08a59155a44d633e7f57e8fa47f03a7 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 12 Jul 2026 11:16:04 +0000 Subject: [PATCH 09/19] Revert SetDstAddr contract change; carve dst bytes caller-side instead CI showed that exposing the RawDstAddr byte fraction through SetDstAddr's postcondition cannot work: a magic wand whose assertion dereferences a field is not self-framing, so it can neither be stated in the postcondition (Silicon cannot match it against packAddr's variable-shaped instance) nor re-packaged in the body ('Permission to s.RawDstAddr might not suffice'), and a ghost out-parameter would require restructuring the real call sites. Restore the original acc(dst.Mem(), R18) contract (keeping the new T4Ip length postconditions) and revert testDstSetter. The plan now designates the caller-side extraction for M5: unfold a fraction of dst.Mem(), transfer the element permissions to RawDstAddr via SetDstAddr's pointwise aliasing postconditions, and package the restoring wand over locals - the verified addEndhostPort pattern. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 23 ++++++++++++++++++----- pkg/slayers/scion.go | 24 +++--------------------- pkg/slayers/scion_test.gobra | 5 ----- 3 files changed, 21 insertions(+), 31 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index 51a05bddb..399e0997a 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -656,11 +656,24 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). (`bfdSend.Send` is trusted, `prepareSCMP`'s call is behind the `TODO()`), so this lands without new obligations. The §4.3 items are also resolved on this branch: - * `SetDstAddr` (IP case) no longer applies packAddr's magic wand - internally; it exposes `acc(sl.Bytes(s.RawDstAddr, ...), R20)` plus - the wand `... --* acc(dst.Mem(), R20)` to the caller (its only - verified caller is prepareSCMP's currently-dead code, so the - post-shape change is safe), alongside `acc(dst.Mem(), R19+R20)`; + * ~~expose the `RawDstAddr` byte fraction through `SetDstAddr`'s + postcondition~~ — **attempted and reverted**: a wand whose assertion + dereferences a field (`s.RawDstAddr`) is not self-framing, so it can + neither be stated in the postcondition (Silicon cannot match it + against packAddr's variable-shaped instance: *"Magic wand instance + not found"*) nor re-`package`d (*"Permission to s.RawDstAddr might + not suffice"*), and a ghost out-parameter would force restructuring + the real `if err := ...` call sites. `SetDstAddr` keeps its original + `acc(dst.Mem(), R18)` contract. Instead, **prepareSCMP (M5) carves + the byte fraction caller-side**: unfold `acc(dst.Mem(), R20)`, + convert the element permissions of `dst.IP` into permissions over + `s.RawDstAddr` via the (active) pointwise aliasing postconditions of + `SetDstAddr` (`scion.go:678-685`, three cases: IPv4 direct, + IPv6-mapped at offset 12, IPv6 direct), fold + `sl.Bytes(s.RawDstAddr, ...)`, and package the restoring wand over + local variables — exactly the verified `addEndhostPort` pattern + (`router/dataplane.go:4734-4755`). This should live in a dedicated + slayers lemma so the case split is proven once; * `SetSrcAddr`'s wildcard mode needs **no** component-wise precondition after all: folding `net.IPAddr.Mem()` at wildcard amount is legal (precedent: the wildcard branches inside `packAddr` diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index dbb6c9d1f..efe90c092 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -674,16 +674,7 @@ func (s *SCION) SrcAddr() (res net.Addr, err error) { // @ ensures res == nil && wildcard && isIP(dst) ==> acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), _) // @ ensures res == nil && wildcard && isHostSVC(dst) ==> sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)) // @ ensures res == nil && !wildcard && isHostSVC(dst) ==> sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)) -// @ ensures res == nil && !wildcard && isHostSVC(dst) ==> acc(dst.Mem(), R18) -// (VerifiedSCION) In the IP case, a fraction of the bytes underlying -// RawDstAddr is exposed to the caller (together with a magic wand to give -// it back), instead of returning acc(dst.Mem(), R18) in one piece. This is -// needed by the router's prepareSCMP, which must store that fraction in -// the fresh header's MemSerialize/ChecksumMem predicates while serializing. -// @ ensures res == nil && !wildcard && isIP(dst) ==> acc(dst.Mem(), R19) && acc(dst.Mem(), R20) -// @ ensures res == nil && !wildcard && isIP(dst) ==> -// @ acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) && -// @ (acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) --* acc(dst.Mem(), R20)) +// @ ensures res == nil && !wildcard ==> acc(dst.Mem(), R18) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv4(dst) ==> forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> &s.RawDstAddr[i] == &dst.(*net.IPAddr).IP[i])) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv6(dst) && isConvertibleToIPv4(dst) ==> forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> &s.RawDstAddr[i] == &dst.(*net.IPAddr).IP[12+i])) // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (!isIPv4(dst) && !isIPv6(dst) ==> forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> &s.RawDstAddr[i] == &dst.(*net.IPAddr).IP[i])) @@ -699,19 +690,10 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro var err error var verScionTmp []byte s.DstAddrType, verScionTmp, err = packAddr(dst /*@ , wildcard @*/) - // (VerifiedSCION) The magic wand returned by packAddr is deliberately - // not applied here: it is passed on to the caller (cf. the - // postconditions), so that the byte fraction of the raw address - // remains directly available during serialization. It is re-packaged - // below so that the instance held matches the shape stated in the - // postcondition (a wand over s.RawDstAddr instead of over packAddr's - // return value). - s.RawDstAddr = verScionTmp // @ ghost if !wildcard && err == nil && isIP(dst) { - // @ package acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) --* acc(dst.Mem(), R20) { - // @ apply acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(dst.Mem(), R20) - // @ } + // @ apply acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(dst.Mem(), R20) // @ } + s.RawDstAddr = verScionTmp return err } diff --git a/pkg/slayers/scion_test.gobra b/pkg/slayers/scion_test.gobra index 5849d80d3..3678ddaee 100644 --- a/pkg/slayers/scion_test.gobra +++ b/pkg/slayers/scion_test.gobra @@ -18,7 +18,6 @@ package slayers import ( "net" - . "github.com/scionproto/scion/verification/utils/definitions" sl "github.com/scionproto/scion/verification/utils/slices" "github.com/scionproto/scion/pkg/addr" ) @@ -72,10 +71,6 @@ requires acc(&s.DstAddrType) requires acc(dst.Mem()) func testDstSetter(s *SCION, dst *net.IPAddr) { res := s.SetDstAddr(dst, false) - // SetDstAddr loans a fraction of the bytes underlying s.RawDstAddr to - // the caller; applying the returned magic wand gives it back, after - // which the full permission to dst.Mem() is restored. - apply acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) --* acc(dst.Mem(), R20) // unfolding dst.Mem() grants us permission to s.RawDstAddr since they are aliased unfold dst.Mem() assert forall i int :: { &s.RawDstAddr[i] } 0 <= i && i < len(s.RawDstAddr) ==> acc(&s.RawDstAddr[i]) From 41261fa5fe3a48213fefed522eac5e49e5a32ba3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 11:00:55 +0000 Subject: [PATCH 10/19] Implement M5: drop the TODO() in prepareSCMP prepareSCMP is now fully annotated end to end; the trusted-assumption TODO() marker is gone. The proof: - closes the path section early (mirroring the error cases) and refolds the SCION layer, then re-associates the reversed path with a nil buffer via the new (*Decoded).ChangeUbuf (Mem is buffer-independent; Widen requires a superslice and does not apply); - carves the source-address bytes out of ub via the new ExtractAccSrc (mirroring resolveLocalDst's use of ExtractAcc) and, after SetDstAddr, extracts a fraction of the destination-address bytes from srcA via the new ExtractIPBytes (addEndhostPort-style wand); - calls SetSrcAddr in wildcard mode; packAddr/SetSrcAddr now take the resources of wildcard IP addresses component-wise, since Mem() cannot be folded at a concrete amount for the wildcard-held internal IP. net.IP.Mem()'s length constraint (4 or 16), exposed through the new getInternalIPMem getter, provides the checksum evenness facts together with new length postconditions on packAddr/SetSrcAddr/ SetDstAddr/parseAddr/SrcAddr/PackWithPad; - folds MemSerialize + ChecksumMem + the SCMP header's and payload's Mem(nil), builds the ghost layerBufs (now a seq[[]byte]; payload buffers at fraction R55 so the quote can be carved from the split ub), and invokes SerializeLayers against its trusted contract; - derives !IsSupportedPkt(result) from the contract's IO bridge, the IsSupportedRawPktEqGopacket lemma, and revealing both definitions; - restores all resources on every path (the SerializeLayers contract preserves them also on error). packSCMP receives the payload layer's resources field-wise (it is constructed inline at the call sites, where nothing can be folded) and folds Mem(nil) via the new slayers.FoldFreshSCMPPayloadMem; the rawPkt === ub relation is threaded through the ten functions between process/processPkt and packSCMP for the quote. Annotations/contracts only; no executable code changes (go build unchanged). Needs CI iteration. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- doc/verification/prepareSCMP.md | 21 +++ pkg/addr/host.go | 1 + pkg/slayers/path/scion/decoded_spec.gobra | 13 ++ pkg/slayers/scion.go | 36 ++++- pkg/slayers/scion_spec.gobra | 77 +++++++++- pkg/slayers/scmp_msg_spec.gobra | 48 ++++++ router/dataplane.go | 143 +++++++++++++++++- router/dataplane_spec.gobra | 15 ++ .../github.com/google/gopacket/writer.gobra | 10 +- 9 files changed, 345 insertions(+), 19 deletions(-) diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md index 399e0997a..05287a0c7 100644 --- a/doc/verification/prepareSCMP.md +++ b/doc/verification/prepareSCMP.md @@ -708,6 +708,27 @@ budget accordingly; perf regressions in `dataplane.go` are a real risk). 5. **M5 — `prepareSCMP` itself** (§5): spec extensions, call-site folds, ghost `layerBufs`, drop the `TODO()`. Large, but mostly mechanical once M1–M4 are in; expect iteration on router CI time. + **Status: implemented on this branch** (pending CI iteration): the + `TODO()` is gone. Key mechanisms beyond the plan text: + * `(*Decoded).ChangeUbuf` re-associates the reversed path with `nil` + (`Widen` requires a superslice and does not apply); + * `ExtractAccSrc` + `SrcAddr`'s wand carve the source-address bytes + out of `ub` (mirroring `resolveLocalDst`), and `ExtractIPBytes` + carves the destination-address byte fraction out of `srcA`; + * `SetSrcAddr` is called in wildcard mode with a component-wise + precondition (folding `net.IPAddr.Mem()` at a concrete amount is + impossible for the wildcard-held internal IP); `net.IP.Mem()`'s + length constraint (4 or 16) closes the checksum-evenness gap via + `getInternalIPMem`; + * `packSCMP` receives the payload's resources field-wise (the payload + is built inline at its ~13 call sites, where nothing can be folded) + and folds `Mem(nil)` via `slayers.FoldFreshSCMPPayloadMem`; + * `acc(&p.rawPkt, R51) && p.rawPkt === ub` is threaded through the ten + functions between `process`/`processPkt` (which already carry the + relation) and `packSCMP`, for the quote's byte fraction; + * `SerializeLayers`' ghost `layerBufs` became a `seq[[]byte]` (no + permissions needed) and the payload buffers are required only at + fraction R55, so the quote can be carved from the split `ub`. 6. **M6 — cleanup**: remove `Unreachable()` from the `FixLengths` branch, revisit `bfdSend` (§8), document the serialize-mode idiom. diff --git a/pkg/addr/host.go b/pkg/addr/host.go index ce971e76c..f96ffde50 100644 --- a/pkg/addr/host.go +++ b/pkg/addr/host.go @@ -360,6 +360,7 @@ func (h HostSVC) Pack() (res []byte) { // @ requires pad >= 0 // @ ensures acc(res) +// @ ensures len(res) == HostLenSVC + pad // @ decreases func (h HostSVC) PackWithPad(pad int) (res []byte) { out := make([]byte, HostLenSVC+pad) diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index 1ebbce5a3..787270173 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -200,4 +200,17 @@ func (d *Decoded) Widen(ubuf1, ubuf2 []byte) { fold d.Mem(ubuf2) } +// The resources captured by Mem are independent of the buffer parameter, +// so a Decoded path can be re-associated with an arbitrary other buffer, +// in particular with nil. This is used to serialize a decoded path +// without an underlying buffer (cf. prepareSCMP in the router). +ghost +requires d.Mem(ubuf1) +ensures d.Mem(ubuf2) +decreases +func (d *Decoded) ChangeUbuf(ubuf1, ubuf2 []byte) { + unfold d.Mem(ubuf1) + fold d.Mem(ubuf2) +} + /**** End of Lemmas ****/ diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index efe90c092..efc2db2e1 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -651,6 +651,8 @@ func (s *SCION) DstAddr() (res net.Addr, err error) { // @ ensures err == nil ==> // @ let rawSrcAddr := s.RawSrcAddr in // @ (acc(res.Mem(), R15) --* acc(sl.Bytes(rawSrcAddr, 0, len(rawSrcAddr)), R15)) +// @ ensures err == nil && typeOf(res) == type[*net.IPAddr] ==> +// @ unfolding acc(res.Mem(), R15) in len(res.(*net.IPAddr).IP) == len(s.RawSrcAddr) // @ ensures err != nil ==> // @ acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R15) // @ ensures err != nil ==> err.ErrorMem() @@ -685,6 +687,8 @@ func (s *SCION) SrcAddr() (res net.Addr, err error) { // @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv6(dst) && !isConvertibleToIPv4(dst) ==> len(dst.(*net.IPAddr).IP) == len(s.RawDstAddr))) // @ ensures (res == nil) == (typeOf(dst) == type[*net.IPAddr] || typeOf(dst) == type[addr.HostSVC]) // @ ensures res == nil && isIP(dst) && s.DstAddrType == T4Ip ==> len(s.RawDstAddr) == 4 +// @ ensures res == nil ==> s.DstAddrType.Has3Bits() +// @ ensures res == nil && isHostSVC(dst) ==> len(s.RawDstAddr) == 4 // @ decreases func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res error) { var err error @@ -702,7 +706,11 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro // Changes to src might leave the layer in an inconsistent state. // @ requires acc(&s.RawSrcAddr) // @ requires acc(&s.SrcAddrType) -// @ requires wildcard ==> acc(src.Mem(), _) +// (VerifiedSCION) See the corresponding remark on packAddr. +// @ requires wildcard && isIP(src) ==> acc(&src.(*net.IPAddr).IP, _) && +// @ (forall i int :: { &src.(*net.IPAddr).IP[i] } 0 <= i && i < len(src.(*net.IPAddr).IP) ==> +// @ acc(&src.(*net.IPAddr).IP[i], _)) +// @ requires wildcard && !isIP(src) ==> acc(src.Mem(), _) // @ requires !wildcard ==> acc(src.Mem(), R18) // @ ensures isIP(src) ==> res == nil // @ ensures isHostSVC(src) ==> res == nil @@ -723,6 +731,10 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro // @ ensures res == nil && !wildcard && isIP(src) ==> (unfolding acc(src.Mem(), R20) in (isIPv6(src) && !isConvertibleToIPv4(src) ==> len(src.(*net.IPAddr).IP) == len(s.RawSrcAddr))) // @ ensures (res == nil) == (typeOf(src) == type[*net.IPAddr] || typeOf(src) == type[addr.HostSVC]) // @ ensures res == nil && isIP(src) && s.SrcAddrType == T4Ip ==> len(s.RawSrcAddr) == 4 +// @ ensures res == nil ==> s.SrcAddrType.Has3Bits() +// @ ensures res == nil && isHostSVC(src) ==> len(s.RawSrcAddr) == 4 +// @ ensures res == nil && wildcard && isIP(src) && s.SrcAddrType == T16Ip ==> +// @ len(s.RawSrcAddr) == old(len(src.(*net.IPAddr).IP)) // @ decreases func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error) { var err error @@ -741,6 +753,8 @@ func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error // @ ensures err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC // @ ensures err == nil ==> // @ (acc(res.Mem(), R15) --* acc(sl.Bytes(raw, 0, len(raw)), R15)) +// @ ensures err == nil && typeOf(res) == type[*net.IPAddr] ==> +// @ unfolding acc(res.Mem(), R15) in len(res.(*net.IPAddr).IP) == len(raw) // @ ensures err != nil ==> acc(sl.Bytes(raw, 0, len(raw)), R15) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -778,7 +792,15 @@ func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) { "type", addrType, "len", addrType.Length()) } -// @ requires wildcard ==> acc(hostAddr.Mem(), _) +// (VerifiedSCION) In wildcard mode, the resources of an IP-typed address +// are taken component-wise instead of as a folded Mem() predicate: the +// caller may hold the bytes of the underlying IP only at wildcard amount +// (e.g. the router's internal IP), in which case Mem() cannot be folded +// at any concrete amount. +// @ requires wildcard && isIP(hostAddr) ==> acc(&hostAddr.(*net.IPAddr).IP, _) && +// @ (forall i int :: { &hostAddr.(*net.IPAddr).IP[i] } 0 <= i && i < len(hostAddr.(*net.IPAddr).IP) ==> +// @ acc(&hostAddr.(*net.IPAddr).IP[i], _)) +// @ requires wildcard && !isIP(hostAddr) ==> acc(hostAddr.Mem(), _) // @ requires !wildcard ==> acc(hostAddr.Mem(), R19) // @ ensures !wildcard ==> acc(hostAddr.Mem(), R20) // @ ensures hostAddr === old(hostAddr) @@ -802,13 +824,17 @@ func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) { // @ ensures err == nil && !wildcard && isIP(hostAddr) ==> (unfolding acc(hostAddr.Mem(), R20) in (isIPv6(hostAddr) && !isConvertibleToIPv4(hostAddr) ==> len(hostAddr.(*net.IPAddr).IP) == len(b))) // @ ensures (err == nil) == (typeOf(hostAddr) == type[*net.IPAddr] || typeOf(hostAddr) == type[addr.HostSVC]) // @ ensures err == nil && isIP(hostAddr) && addrtyp == T4Ip ==> len(b) == 4 +// @ ensures err == nil ==> addrtyp.Has3Bits() +// @ ensures err == nil && isHostSVC(hostAddr) ==> len(b) == 4 +// @ ensures err == nil && wildcard && isIP(hostAddr) && addrtyp == T16Ip ==> +// @ len(b) == old(len(hostAddr.(*net.IPAddr).IP)) // @ decreases func packAddr(hostAddr net.Addr /*@ , ghost wildcard bool @*/) (addrtyp AddrType, b []byte, err error) { switch a := hostAddr.(type) { case *net.IPAddr: - // @ ghost if wildcard { - // @ unfold acc(hostAddr.Mem(), _) - // @ } else { + // (VerifiedSCION) In wildcard mode the resources are already + // available component-wise (cf. the precondition). + // @ ghost if !wildcard { // @ unfold acc(hostAddr.Mem(), R20) // @ } if ip := a.IP.To4( /*@ wildcard @*/ ); ip != nil { diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 1e712bb16..ad8d62a50 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -301,16 +301,24 @@ requires acc(&s.PathType) && 0 <= s.PathType && s.PathType < path.MaxPathType requires acc(&s.DstAddrType) && acc(&s.SrcAddrType) requires acc(&s.Path) && s.Path != nil && s.Path.Mem(nil) requires acc(&s.BaseLayer) -requires acc(&s.DstIA, R20) && acc(&s.SrcIA, R20) -requires acc(&s.RawDstAddr, R20) && acc(&s.RawSrcAddr, R20) -requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) +// Exactly the amounts stored in MemSerialize and ChecksumMem are +// consumed (R25 each), so that the caller keeps any remainder and can +// recover the full fractions it started from by unfolding the two +// predicates again. +requires acc(&s.DstIA, R25) && acc(&s.SrcIA, R25) +requires acc(&s.DstIA, R25) && acc(&s.SrcIA, R25) +requires acc(&s.RawDstAddr, R25) && acc(&s.RawSrcAddr, R25) +requires acc(&s.RawDstAddr, R25) && acc(&s.RawSrcAddr, R25) +requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R25) +requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R25) requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) requires len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0 requires acc(&s.pathPool) && acc(&s.pathPoolRaw) -requires PathPoolMem(s.pathPool, s.pathPoolRaw) +requires s.pathPool == nil && s.pathPoolRaw == nil ensures s.MemSerialize() && s.ChecksumMem() decreases func (s *SCION) FoldFreshMemSerializeWithChecksumMem() { + fold PathPoolMem(s.pathPool, s.pathPoolRaw) fold s.MemSerialize() fold s.ChecksumMem() } @@ -332,6 +340,67 @@ pred (b *BaseLayer) Mem(ghost ub []byte, ghost breakPoint int) { b.Payload === ub[breakPoint:])) } +// ExtractIPBytes converts a fraction of an IP-typed address' resources +// into a byte predicate over `raw`, a slice that aliases the address' +// underlying IP buffer as described by SetDstAddr's postconditions (either +// the whole buffer or, for IPv4-in-IPv6 addresses, its 4-byte suffix). +// The returned magic wand gives the fraction back. This follows the +// pattern of the router's addEndhostPort. +ghost +requires typeOf(dst) == type[*net.IPAddr] +requires acc(dst.Mem(), R20) +requires unfolding acc(dst.Mem(), R20) in (isIPv4(dst) ==> + len(raw) == len(dst.(*net.IPAddr).IP) && + (forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> &raw[i] == &dst.(*net.IPAddr).IP[i])) +requires unfolding acc(dst.Mem(), R20) in ((isIPv6(dst) && isConvertibleToIPv4(dst)) ==> + len(dst.(*net.IPAddr).IP) == len(raw) + 12 && + (forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> &raw[i] == &dst.(*net.IPAddr).IP[12+i])) +requires unfolding acc(dst.Mem(), R20) in ((isIPv6(dst) && !isConvertibleToIPv4(dst)) ==> + len(dst.(*net.IPAddr).IP) == len(raw) && + (forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> &raw[i] == &dst.(*net.IPAddr).IP[i])) +requires unfolding acc(dst.Mem(), R20) in ((!isIPv4(dst) && !isIPv6(dst)) ==> + len(raw) == len(dst.(*net.IPAddr).IP) && + (forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> &raw[i] == &dst.(*net.IPAddr).IP[i])) +ensures acc(sl.Bytes(raw, 0, len(raw)), R20) +ensures acc(sl.Bytes(raw, 0, len(raw)), R20) --* acc(dst.Mem(), R20) +decreases +func ExtractIPBytes(dst net.Addr, raw []byte) { + unfold acc(dst.Mem(), R20) + assert forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> acc(&raw[i], R20) + fold acc(sl.Bytes(raw, 0, len(raw)), R20) + package acc(sl.Bytes(raw, 0, len(raw)), R20) --* acc(dst.Mem(), R20) { + unfold acc(sl.Bytes(raw, 0, len(raw)), R20) + fold acc(dst.Mem(), R20) + } +} + +// ExtractAccSrc is the analog of ExtractAcc for the source address. +ghost +requires acc(s.Mem(ub), R15) +ensures acc(s, R16) +ensures s.SrcAddrType == T4Svc ==> len(s.RawSrcAddr) >= addr.HostLenSVC +ensures 0 <= start && start <= end && end <= len(ub) +ensures s.RawSrcAddr === ub[start:end] +ensures end - start == s.SrcAddrType.Length() +ensures s.SrcAddrType.Length() == 4 || s.SrcAddrType.Length() == 8 || + s.SrcAddrType.Length() == 12 || s.SrcAddrType.Length() == 16 +ensures acc(s, R16) --* acc(s.Mem(ub), R15) +decreases +func (s *SCION) ExtractAccSrc(ghost ub []byte) (start, end int) { + unfold acc(s.Mem(ub), R16) + unfold acc(s.HeaderMem(ub[CmnHdrLen:]), R16) + start = CmnHdrLen+2*addr.IABytes+s.DstAddrType.Length() + end = CmnHdrLen+2*addr.IABytes+s.DstAddrType.Length()+s.SrcAddrType.Length() + assert s.RawSrcAddr === ub[start:end] + package acc(s, R16) --* acc(s.Mem(ub), R15) { + unfold acc(s.Mem(ub), R16) + unfold acc(s.HeaderMem(ub[CmnHdrLen:]), R16) + fold acc(s.HeaderMem(ub[CmnHdrLen:]), R15) + fold acc(s.Mem(ub), R15) + } + return start, end +} + ghost requires acc(s.Mem(ub), R15) ensures acc(s, R16) diff --git a/pkg/slayers/scmp_msg_spec.gobra b/pkg/slayers/scmp_msg_spec.gobra index 97f03332c..8b3a461ef 100644 --- a/pkg/slayers/scmp_msg_spec.gobra +++ b/pkg/slayers/scmp_msg_spec.gobra @@ -435,3 +435,51 @@ func (s *SCMPPacketTooBig) FoldFreshMem() { fold s.BaseLayer.Mem(nil, 4) fold s.Mem(nil) } + +// FoldFreshSCMPPayloadMem folds the Mem(nil) predicate of a freshly +// constructed SCMP payload layer held behind the SerializableLayer +// interface. It exists because the router's packSCMP receives the payload +// as an interface value constructed inline at its call sites, where no +// fold can be performed. The supported types are exactly the ones the +// router constructs. +ghost +requires scmpP != nil +requires typeOf(scmpP) == type[*SCMPParameterProblem] || + typeOf(scmpP) == type[*SCMPDestinationUnreachable] || + typeOf(scmpP) == type[*SCMPTraceroute] || + typeOf(scmpP) == type[*SCMPExternalInterfaceDown] || + typeOf(scmpP) == type[*SCMPInternalConnectivityDown] +requires typeOf(scmpP) == type[*SCMPParameterProblem] ==> + (acc(&scmpP.(*SCMPParameterProblem).Pointer) && acc(&scmpP.(*SCMPParameterProblem).BaseLayer) && + scmpP.(*SCMPParameterProblem).Contents == nil && scmpP.(*SCMPParameterProblem).Payload == nil) +requires typeOf(scmpP) == type[*SCMPDestinationUnreachable] ==> + (acc(&scmpP.(*SCMPDestinationUnreachable).BaseLayer) && + scmpP.(*SCMPDestinationUnreachable).Contents == nil && scmpP.(*SCMPDestinationUnreachable).Payload == nil) +requires typeOf(scmpP) == type[*SCMPTraceroute] ==> + (acc(&scmpP.(*SCMPTraceroute).Identifier) && acc(&scmpP.(*SCMPTraceroute).Sequence) && + acc(&scmpP.(*SCMPTraceroute).IA) && acc(&scmpP.(*SCMPTraceroute).Interface) && + acc(&scmpP.(*SCMPTraceroute).BaseLayer) && + scmpP.(*SCMPTraceroute).Contents == nil && scmpP.(*SCMPTraceroute).Payload == nil) +requires typeOf(scmpP) == type[*SCMPExternalInterfaceDown] ==> + (acc(&scmpP.(*SCMPExternalInterfaceDown).IA) && acc(&scmpP.(*SCMPExternalInterfaceDown).IfID) && + acc(&scmpP.(*SCMPExternalInterfaceDown).BaseLayer) && + scmpP.(*SCMPExternalInterfaceDown).Contents == nil && scmpP.(*SCMPExternalInterfaceDown).Payload == nil) +requires typeOf(scmpP) == type[*SCMPInternalConnectivityDown] ==> + (acc(&scmpP.(*SCMPInternalConnectivityDown).IA) && acc(&scmpP.(*SCMPInternalConnectivityDown).Ingress) && + acc(&scmpP.(*SCMPInternalConnectivityDown).Egress) && acc(&scmpP.(*SCMPInternalConnectivityDown).BaseLayer) && + scmpP.(*SCMPInternalConnectivityDown).Contents == nil && scmpP.(*SCMPInternalConnectivityDown).Payload == nil) +ensures scmpP.Mem(nil) +decreases +func FoldFreshSCMPPayloadMem(scmpP gopacket.SerializableLayer) { + if typeOf(scmpP) == type[*SCMPParameterProblem] { + scmpP.(*SCMPParameterProblem).FoldFreshMem() + } else if typeOf(scmpP) == type[*SCMPDestinationUnreachable] { + scmpP.(*SCMPDestinationUnreachable).FoldFreshMem() + } else if typeOf(scmpP) == type[*SCMPTraceroute] { + scmpP.(*SCMPTraceroute).FoldFreshMem() + } else if typeOf(scmpP) == type[*SCMPExternalInterfaceDown] { + scmpP.(*SCMPExternalInterfaceDown).FoldFreshMem() + } else { + scmpP.(*SCMPInternalConnectivityDown).FoldFreshMem() + } +} diff --git a/router/dataplane.go b/router/dataplane.go index 90b8cbc62..4020ea51a 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2159,6 +2159,36 @@ type macBuffersT struct { // @ requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// The SCMP payload layer is freshly constructed at the call sites, as an +// interface value built inline, where its Mem(nil) predicate cannot be +// folded. Its resources are therefore passed field-wise (matching +// slayers.FoldFreshSCMPPayloadMem, which folds them in the body): +// @ requires scmpP != nil +// @ requires typeOf(scmpP) == type[*slayers.SCMPParameterProblem] || +// @ typeOf(scmpP) == type[*slayers.SCMPDestinationUnreachable] || +// @ typeOf(scmpP) == type[*slayers.SCMPTraceroute] || +// @ typeOf(scmpP) == type[*slayers.SCMPExternalInterfaceDown] || +// @ typeOf(scmpP) == type[*slayers.SCMPInternalConnectivityDown] +// @ requires typeOf(scmpP) == type[*slayers.SCMPParameterProblem] ==> +// @ (acc(&scmpP.(*slayers.SCMPParameterProblem).Pointer) && acc(&scmpP.(*slayers.SCMPParameterProblem).BaseLayer) && +// @ scmpP.(*slayers.SCMPParameterProblem).Contents == nil && scmpP.(*slayers.SCMPParameterProblem).Payload == nil) +// @ requires typeOf(scmpP) == type[*slayers.SCMPDestinationUnreachable] ==> +// @ (acc(&scmpP.(*slayers.SCMPDestinationUnreachable).BaseLayer) && +// @ scmpP.(*slayers.SCMPDestinationUnreachable).Contents == nil && scmpP.(*slayers.SCMPDestinationUnreachable).Payload == nil) +// @ requires typeOf(scmpP) == type[*slayers.SCMPTraceroute] ==> +// @ (acc(&scmpP.(*slayers.SCMPTraceroute).Identifier) && acc(&scmpP.(*slayers.SCMPTraceroute).Sequence) && +// @ acc(&scmpP.(*slayers.SCMPTraceroute).IA) && acc(&scmpP.(*slayers.SCMPTraceroute).Interface) && +// @ acc(&scmpP.(*slayers.SCMPTraceroute).BaseLayer) && +// @ scmpP.(*slayers.SCMPTraceroute).Contents == nil && scmpP.(*slayers.SCMPTraceroute).Payload == nil) +// @ requires typeOf(scmpP) == type[*slayers.SCMPExternalInterfaceDown] ==> +// @ (acc(&scmpP.(*slayers.SCMPExternalInterfaceDown).IA) && acc(&scmpP.(*slayers.SCMPExternalInterfaceDown).IfID) && +// @ acc(&scmpP.(*slayers.SCMPExternalInterfaceDown).BaseLayer) && +// @ scmpP.(*slayers.SCMPExternalInterfaceDown).Contents == nil && scmpP.(*slayers.SCMPExternalInterfaceDown).Payload == nil) +// @ requires typeOf(scmpP) == type[*slayers.SCMPInternalConnectivityDown] ==> +// @ (acc(&scmpP.(*slayers.SCMPInternalConnectivityDown).IA) && acc(&scmpP.(*slayers.SCMPInternalConnectivityDown).Ingress) && +// @ acc(&scmpP.(*slayers.SCMPInternalConnectivityDown).Egress) && acc(&scmpP.(*slayers.SCMPInternalConnectivityDown).BaseLayer) && +// @ scmpP.(*slayers.SCMPInternalConnectivityDown).Contents == nil && scmpP.(*slayers.SCMPInternalConnectivityDown).Payload == nil) // @ preserves ubLL == nil || ubLL === ub[startLL:endLL] // @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil // @ preserves &p.scionLayer !== p.lastLayer ==> @@ -2169,6 +2199,7 @@ type macBuffersT struct { // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R45) +// @ ensures acc(&p.rawPkt, R51) // @ ensures p.d.validResult(respr, false) // @ ensures acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem() // @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) @@ -2229,6 +2260,7 @@ func (p *scionPacketProcessor) packSCMP( // @ } // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) // @ } + // @ slayers.FoldFreshSCMPPayloadMem(scmpP) rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , ub @*/) // @ ghost result := processResult{OutPkt: rawSCMP} // @ fold p.d.validResult(result, false) @@ -2389,6 +2421,8 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ubScionL)) == slayers.IsSupportedPkt(ubScionL) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { expiration := util.SecsToTime(p.infoField.Timestamp). @@ -2487,6 +2521,8 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho // @ AbsValidateIngressIDConstraint(absPkt(ubScionL), path.ifsToIO_ifs(p.ingressID)) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int@*/ ) (respr processResult, reserr error) { pktIngressID := p.hopField.ConsIngress @@ -2656,6 +2692,8 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) invalidSrcIA( // @ ghost ub []byte, @@ -2706,6 +2744,8 @@ func (p *scionPacketProcessor) invalidSrcIA( // @ ensures reserr != nil && reserr.ErrorMem() // @ ensures respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) invalidDstIA( // @ ghost ub []byte, @@ -2871,6 +2911,8 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ p.ingressID != 0 && AbsValidateEgressIDConstraintXover(absPkt(ubScionL), dp) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) validateEgressID( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) @@ -3174,6 +3216,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ ensures reserr == nil ==> p.LastHopLen(ubScionL) == old(p.LastHopLen(ubScionL)) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ ghost oldPkt := absPkt(ubScionL) @@ -3276,6 +3320,8 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ubScionL)) == slayers.IsSupportedPkt(ubScionL) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (resaddr *net.UDPAddr, respr processResult, reserr error /*@ , ghost addrAliasesUb bool @*/) { // (VerifiedSCION) the parameter used to be p.scionLayer, @@ -3697,6 +3743,8 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e // @ ensures reserr == nil ==> absPkt(ub) == old(absPkt(ub)) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// @ ensures acc(&p.rawPkt, R51) // @ decreases 0 if sync.IgnoreBlockingForTermination() func (p *scionPacketProcessor) validateEgressUp( // @ ghost ub []byte, @@ -4055,6 +4103,8 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ubScionL)) == slayers.IsSupportedPkt(ubScionL) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( interfaceID uint16 /*@, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/) (respr processResult, reserr error) { @@ -4176,6 +4226,8 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ubScionL)) == slayers.IsSupportedPkt(ubScionL) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ unfold acc(p.scionLayer.Mem(ubScionL), R20) @@ -4912,10 +4964,18 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { // @ requires acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() // @ requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ requires cause != nil ==> cause.ErrorMem() +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// @ requires scmpP != nil && scmpP.Mem(nil) +// @ requires typeOf(scmpP) == type[*slayers.SCMPParameterProblem] || +// @ typeOf(scmpP) == type[*slayers.SCMPDestinationUnreachable] || +// @ typeOf(scmpP) == type[*slayers.SCMPTraceroute] || +// @ typeOf(scmpP) == type[*slayers.SCMPExternalInterfaceDown] || +// @ typeOf(scmpP) == type[*slayers.SCMPInternalConnectivityDown] // @ ensures acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.ingressID, R50) +// @ ensures acc(&p.rawPkt, R51) // @ ensures acc(&p.buffer, R55) && p.buffer != nil && p.buffer.Mem() // @ ensures sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf())) // @ ensures result != nil ==> @@ -5068,25 +5128,50 @@ func (p *scionPacketProcessor) prepareSCMP( return nil, serrors.Wrap(cannotRoute, err, "details", "incrementing path for SCMP") } } - // @ TODO() + // (VerifiedSCION) The reversed path revPath is self-contained + // (cf. (*Decoded).ChangeUbuf below), so the original path's resources + // can be given back and the SCION layer refolded, mirroring the ghost + // code of the error cases above. + // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ ghost if pathFromEpic { + // @ epicPath := p.scionLayer.Path.(*epic.Path) + // @ assert acc(path.Mem(ubPath), R4) + // @ fold acc(epicPath.Mem(epicPathUb), R4) + // @ } else { + // @ rawP := p.scionLayer.Path.(*scion.Raw) + // @ assert acc(path.Mem(ubPath), R4) + // @ assert acc(rawP.Mem(ubPath), R4) + // @ } // create new SCION header for reply. var scionL /*@@@*/ slayers.SCION - // (VerifiedSCION) TODO: adapt *SCION.Mem(...) scionL.FlowID = p.scionLayer.FlowID scionL.TrafficClass = p.scionLayer.TrafficClass + // @ revPath.ChangeUbuf(rawPath, nil) scionL.PathType = revPath.Type( /*@ nil @*/ ) scionL.Path = revPath scionL.DstIA = p.scionLayer.SrcIA + // @ p.d.getLocalIA() scionL.SrcIA = p.d.localIA + // @ fold acc(p.scionLayer.Mem(ub), R4) + // @ ghost startSrc, endSrc := p.scionLayer.ExtractAccSrc(ub) + // @ assert p.scionLayer.RawSrcAddr === ub[startSrc:endSrc] + // @ sl.SplitRange_Bytes(ub, startSrc, endSrc, R15) srcA, err := p.scionLayer.SrcAddr() if err != nil { + // @ sl.CombineRange_Bytes(ub, startSrc, endSrc, R15) + // @ apply acc(&p.scionLayer, R16) --* acc(p.scionLayer.Mem(ub), R15) return nil, serrors.Wrap(cannotRoute, err, "details", "extracting src addr") } if err := scionL.SetDstAddr(srcA /*@ , false @*/); err != nil { + // The address returned by SrcAddr is always supported by SetDstAddr. + // @ Unreachable() return nil, serrors.Wrap(cannotRoute, err, "details", "setting dest addr") } - if err := scionL.SetSrcAddr(&net.IPAddr{IP: p.d.internalIP} /*@ , false @*/); err != nil { + // @ p.d.getInternalIPMem() + if err := scionL.SetSrcAddr(&net.IPAddr{IP: p.d.internalIP} /*@ , true @*/); err != nil { + // An IP address is always supported by SetSrcAddr. + // @ Unreachable() return nil, serrors.Wrap(cannotRoute, err, "details", "setting src addr") } scionL.NextHdr = slayers.L4SCMP @@ -5096,6 +5181,9 @@ func (p *scionPacketProcessor) prepareSCMP( scmpH.SetNetworkLayerForChecksum(&scionL) if err := p.buffer.Clear(); err != nil { + // @ apply acc(srcA.Mem(), R15) --* acc(sl.Bytes(ub[startSrc:endSrc], 0, len(ub[startSrc:endSrc])), R15) + // @ sl.CombineRange_Bytes(ub, startSrc, endSrc, R15) + // @ apply acc(&p.scionLayer, R16) --* acc(p.scionLayer.Mem(ub), R15) return nil, err } sopts := gopacket.SerializeOptions{ @@ -5103,9 +5191,11 @@ func (p *scionPacketProcessor) prepareSCMP( FixLengths: true, } scmpLayers := []gopacket.SerializableLayer{&scionL, &scmpH, scmpP} + // @ ghost layerBufs := seq[[]byte]{ nil, nil, nil } + // @ ghost quoteLen := 0 if cause != nil { // add quote for errors. - hdrLen := slayers.CmnHdrLen + scionL.AddrHdrLen( /*@ nil, false @*/ ) + scionL.Path.Len( /*@ nil @*/ ) + hdrLen := slayers.CmnHdrLen + scionL.AddrHdrLen( /*@ nil, true @*/ ) + scionL.Path.Len( /*@ nil @*/ ) switch scmpH.TypeCode.Type() { case slayers.SCMPTypeExternalInterfaceDown: hdrLen += 20 @@ -5115,17 +5205,60 @@ func (p *scionPacketProcessor) prepareSCMP( hdrLen += 8 } quote := p.rawPkt + // The header of the reply is short enough for a positive quote + // length to remain: the address header is at most 48 bytes long + // and the reversed path at most 796 bytes. + // @ assert scionL.AddrHdrLenSpecInternal() <= 48 + // @ assert revPath.LenSpec(nil) <= 4 + 3*8 + 64*12 maxQuoteLen := slayers.MaxSCMPPacketLen - hdrLen + // @ assert 0 <= maxQuoteLen if len(quote) > maxQuoteLen { quote = quote[:maxQuoteLen] } + // @ assert quote === ub[0:len(quote)] + // @ sl.SplitRange_Bytes(ub, 0, len(quote), R55) + // @ ghost pld := gopacket.Payload(quote) + // @ fold pld.Mem(quote) scmpLayers = append( /*@ noPerm, @*/ scmpLayers, gopacket.Payload(quote)) + // @ layerBufs = layerBufs ++ seq[[]byte]{ quote } + // @ quoteLen = len(quote) } // XXX(matzf) could we use iovec gather to avoid copying quote? - err = gopacket.SerializeLayers(p.buffer, sopts /*@ , nil @*/, scmpLayers...) + // (VerifiedSCION) Extract a fraction of the bytes underlying the + // destination address (which alias srcA's IP buffer) and fold the + // fresh header's predicates for serialization. + // @ ghost if typeOf(srcA) == type[*net.IPAddr] { + // @ slayers.ExtractIPBytes(srcA, scionL.RawDstAddr) + // @ } + // @ assert len(scionL.RawDstAddr) % 2 == 0 + // @ assert len(scionL.RawSrcAddr) % 2 == 0 + // @ scionL.FoldFreshMemSerializeWithChecksumMem() + // @ scmpH.FoldFreshMem() + // @ fold sl.Bytes(nil, 0, 0) + // @ fold sl.Bytes(nil, 0, 0) + // @ assert !scionL.IsSupportedSerialization() + err = gopacket.SerializeLayers(p.buffer, sopts /*@ , layerBufs @*/, scmpLayers...) + // @ unfold scmpH.Mem(nil) + // @ unfold scionL.ChecksumMem() + // @ unfold scionL.MemSerialize() + // @ ghost if typeOf(srcA) == type[*net.IPAddr] { + // @ apply acc(sl.Bytes(scionL.RawDstAddr, 0, len(scionL.RawDstAddr)), R20) --* acc(srcA.Mem(), R20) + // @ } + // @ apply acc(srcA.Mem(), R15) --* acc(sl.Bytes(ub[startSrc:endSrc], 0, len(ub[startSrc:endSrc])), R15) + // @ sl.CombineRange_Bytes(ub, startSrc, endSrc, R15) + // @ apply acc(&p.scionLayer, R16) --* acc(p.scionLayer.Mem(ub), R15) + // @ ghost if cause != nil { + // @ sl.CombineRange_Bytes(ub, 0, quoteLen, R55) + // @ } if err != nil { return nil, serrors.Wrap(cannotRoute, err, "details", "serializing SCMP message") } + // The serialized packet is an SCMP reply and thus not a supported + // packet in the sense of IsSupportedPkt: its NextHdr byte is L4SCMP. + // @ slayers.IsSupportedRawPktEqGopacket(p.buffer.View()) + // @ assert !(reveal slayers.IsSupportedRawPkt(p.buffer.View())) + // @ assert !(reveal slayers.IsSupportedPkt(p.buffer.UBuf())) + // @ fold scmpError{TypeCode: typeCode, Cause: cause}.ErrorMem() return p.buffer.Bytes(), scmpError{TypeCode: typeCode, Cause: cause} } diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index f6e3288f3..875fa55bf 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -490,6 +490,21 @@ func (d *DataPlane) getInternal() { unfold acc(internalInv(d.internal), _) } +ghost +requires acc(d.Mem(), _) +ensures acc(&d.internalIP, _) +ensures d.internalIP != nil ==> (len(d.internalIP) == 4 || len(d.internalIP) == 16) +ensures d.internalIP != nil ==> + forall i int :: { &d.internalIP[i] } 0 <= i && i < len(d.internalIP) ==> acc(&d.internalIP[i], _) +decreases +func (d *DataPlane) getInternalIPMem() { + unfold acc(d.Mem(), _) + unfold acc(internalIPInv(d.internalIP), _) + ghost if d.internalIP != nil { + unfold acc(d.internalIP.Mem(), _) + } +} + ghost requires acc(d.Mem(), _) && d.getMacFactory() != nil ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _) diff --git a/verification/dependencies/github.com/google/gopacket/writer.gobra b/verification/dependencies/github.com/google/gopacket/writer.gobra index 603d9ae77..9ca3ad88b 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -149,7 +149,6 @@ requires w != nil && w.Mem() requires sl.Bytes(w.UBuf(), 0, len(w.UBuf())) requires len(layerBufs) == len(layers) requires 0 < len(layers) -requires acc(layerBufs, R50) requires forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> (acc(&layers[i], R50) && layers[i] != nil) // Due to Viper's very strict injectivity constraints (cf. decodeLayers): @@ -158,18 +157,19 @@ requires forall i, j int :: { &layers[i], &layers[j] } 0 <= i && i < j && j < l requires layers[0].MemSerialize() requires forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> layers[i].Mem(layerBufs[i]) +// The buffers underlying the layers are only read during serialization, +// so a fraction suffices. requires forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> - sl.Bytes(layerBufs[i], 0, len(layerBufs[i])) + acc(sl.Bytes(layerBufs[i], 0, len(layerBufs[i])), R55) ensures w.Mem() && sl.Bytes(w.UBuf(), 0, len(w.UBuf())) -ensures acc(layerBufs, R50) ensures forall i int :: { &layers[i] } 0 <= i && i < len(layers) ==> acc(&layers[i], R50) ensures layers[0].MemSerialize() ensures forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> layers[i].Mem(layerBufs[i]) ensures forall i int :: { &layers[i] } 1 <= i && i < len(layers) ==> - sl.Bytes(layerBufs[i], 0, len(layerBufs[i])) + acc(sl.Bytes(layerBufs[i], 0, len(layerBufs[i])), R55) ensures err == nil ==> IsSupportedRawPkt(w.View()) == old(layers[0].IsSupportedSerialization()) ensures err != nil ==> err.ErrorMem() decreases -func SerializeLayers(w SerializeBuffer, opts SerializeOptions, ghost layerBufs []([]byte), layers ...SerializableLayer) (err error) +func SerializeLayers(w SerializeBuffer, opts SerializeOptions, ghost layerBufs seq[[]byte], layers ...SerializableLayer) (err error) From 0bba8cd8bb656db771afb33167f226f59515e187 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 11:03:08 +0000 Subject: [PATCH 11/19] Work around Gobra desugarer crash on nil in seq literal Gobra crashes with 'Logic error: found unexpected type: seq[[]byte]' when desugaring an untyped nil inside a seq composite literal (Desugar.litD -> nilType). Bind a typed nil []byte variable first and use it as the element. verify-deps and verify-third-party-libs were green on the M5 commit: all slayers/gopacket lemmas (ExtractAccSrc, ExtractIPBytes, FoldFreshSCMPPayloadMem, the seq-based SerializeLayers contract, and the address-setter postconditions) verify. Only the router package remains to be checked. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- router/dataplane.go | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index 4020ea51a..f07e5f0fa 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -5191,7 +5191,11 @@ func (p *scionPacketProcessor) prepareSCMP( FixLengths: true, } scmpLayers := []gopacket.SerializableLayer{&scionL, &scmpH, scmpP} - // @ ghost layerBufs := seq[[]byte]{ nil, nil, nil } + // (VerifiedSCION) Gobra's desugarer cannot type an untyped nil inside + // a seq composite literal, so the nil buffer is bound to a typed + // variable first. + // @ ghost var nilBuf []byte = nil + // @ ghost layerBufs := seq[[]byte]{ nilBuf, nilBuf, nilBuf } // @ ghost quoteLen := 0 if cause != nil { // add quote for errors. From c0688d410c6986b6ee9441b676f15b171d3cd559 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 11:08:50 +0000 Subject: [PATCH 12/19] Unfold wildcard IP address resources before component-wise calls The M5 run surfaced two follow-up errors from the component-wise wildcard preconditions of packAddr/SetSrcAddr: - SetDstAddr still held dst.Mem() folded when forwarding to packAddr in wildcard mode; unfold it (at wildcard amount) for IP addresses first. - testSrcSetterWildcard called SetSrcAddr(src, true) with the folded predicate; unfold it in the test body. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- pkg/slayers/scion.go | 5 +++++ pkg/slayers/scion_test.gobra | 3 +++ 2 files changed, 8 insertions(+) diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index efc2db2e1..17bcfa512 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -693,6 +693,11 @@ func (s *SCION) SrcAddr() (res net.Addr, err error) { func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res error) { var err error var verScionTmp []byte + // (VerifiedSCION) packAddr takes the resources of wildcard IP + // addresses component-wise (cf. its precondition). + // @ ghost if wildcard && isIP(dst) { + // @ unfold acc(dst.Mem(), _) + // @ } s.DstAddrType, verScionTmp, err = packAddr(dst /*@ , wildcard @*/) // @ ghost if !wildcard && err == nil && isIP(dst) { // @ apply acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(dst.Mem(), R20) diff --git a/pkg/slayers/scion_test.gobra b/pkg/slayers/scion_test.gobra index 3678ddaee..f14ac13a8 100644 --- a/pkg/slayers/scion_test.gobra +++ b/pkg/slayers/scion_test.gobra @@ -37,6 +37,9 @@ requires acc(&s.RawSrcAddr) requires acc(&s.SrcAddrType) requires acc(src.Mem(), _) func testSrcSetterWildcard(s *SCION, src *net.IPAddr) { + // SetSrcAddr takes the resources of wildcard IP addresses + // component-wise (cf. its precondition). + unfold acc(src.Mem(), _) res := s.SetSrcAddr(src, true) // in the wildcard case we have wildcard access to the address in the SCION struct assert acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) From 2609596a8c44c2d0dade113afcdac44c2e933a51 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 12:00:25 +0000 Subject: [PATCH 13/19] Fix the four remaining router errors in the prepareSCMP proof The first full run of the prepareSCMP body proof came back with only four errors: - the read of p.scionLayer.SrcIA needs the HeaderMem sub-predicate unfolded (unlike FlowID/TrafficClass, whose permissions sit at the top level of SCION.Mem); - validateSrcDstIA, handleIngressRouterAlert, and handleEgressRouterAlert are intermediate callers on the way to invalidSrcIA/handleSCMPTraceRouteRequest and were missed in the rawPkt threading. Everything else in the proof - the ExtractAccSrc/ExtractIPBytes wand chains, the MemSerialize/ChecksumMem folds, the SerializeLayers call against its trusted contract, and the !IsSupportedPkt derivation - verified on the first attempt. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- router/dataplane.go | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/router/dataplane.go b/router/dataplane.go index f07e5f0fa..0b13733f1 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2592,6 +2592,8 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ubScionL)) == slayers.IsSupportedPkt(ubScionL) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ubScionL +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ assert unfolding acc(p.scionLayer.Mem(ubScionL), R56) in slayers.CmnHdrLen <= len(ubScionL) @@ -3838,6 +3840,8 @@ func (p *scionPacketProcessor) validateEgressUp( // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ub)) == slayers.IsSupportedPkt(ub) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) handleIngressRouterAlert( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ reveal p.EqAbsHopField(absPkt(ub)) @@ -3968,6 +3972,8 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ ensures reserr == nil ==> old(slayers.IsSupportedPkt(ub)) == slayers.IsSupportedPkt(ub) // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported +// @ requires acc(&p.rawPkt, R51) && p.rawPkt === ub +// @ ensures acc(&p.rawPkt, R51) // @ decreases func (p *scionPacketProcessor) handleEgressRouterAlert( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { // @ reveal p.EqAbsHopField(absPkt(ub)) @@ -5150,7 +5156,10 @@ func (p *scionPacketProcessor) prepareSCMP( // @ revPath.ChangeUbuf(rawPath, nil) scionL.PathType = revPath.Type( /*@ nil @*/ ) scionL.Path = revPath + // SrcIA's permission sits inside the folded HeaderMem sub-predicate. + // @ unfold acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R4) scionL.DstIA = p.scionLayer.SrcIA + // @ fold acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R4) // @ p.d.getLocalIA() scionL.SrcIA = p.d.localIA // @ fold acc(p.scionLayer.Mem(ub), R4) From 85ec14e8ab05810c7f26c8b7ec866360a9c64e5a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 13:12:09 +0000 Subject: [PATCH 14/19] Prove the decoded path's length bound via an explicit lemma The last remaining router error was the quote-length bound assert in prepareSCMP: revPath.LenSpec(nil) <= 796 is not derivable at the call site because the NumINF/NumHops bounds are buried two predicate unfoldings deep (Decoded.Mem -> Base.Mem). Add (*Decoded).LenSpecBound, which surfaces the bound with explicit unfolds, and call it before the assert. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- pkg/slayers/path/scion/decoded_spec.gobra | 21 +++++++++++++++++++++ router/dataplane.go | 1 + 2 files changed, 22 insertions(+) diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index 787270173..f3fd20697 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -200,6 +200,27 @@ func (d *Decoded) Widen(ubuf1, ubuf2 []byte) { fold d.Mem(ubuf2) } +// LenSpecBound surfaces the upper bound on a decoded path's serialized +// length that follows from the bounds stored in Base.Mem (NumINF <= +// MaxINFs, NumHops <= MaxHops). It exists because the bound is buried two +// predicate unfoldings deep and is not derivable from LenSpec's +// definition alone at call sites. +ghost +requires d.Mem(ub) +ensures d.Mem(ub) +ensures d.LenSpec(ub) <= MetaLen + MaxINFs*path.InfoLen + MaxHops*path.HopLen +decreases +func (d *Decoded) LenSpecBound(ghost ub []byte) { + ghost l := d.LenSpec(ub) + unfold d.Mem(ub) + ghost numINF := unfolding d.Base.Mem() in d.Base.NumINF + ghost numHops := unfolding d.Base.Mem() in d.Base.NumHops + assert unfolding d.Base.Mem() in (numINF <= MaxINFs && numHops <= MaxHops) + assert d.Base.Len() == MetaLen + numINF*path.InfoLen + numHops*path.HopLen + assert l == d.Base.Len() + fold d.Mem(ub) +} + // The resources captured by Mem are independent of the buffer parameter, // so a Decoded path can be re-associated with an arbitrary other buffer, // in particular with nil. This is used to serialize a decoded path diff --git a/router/dataplane.go b/router/dataplane.go index 0b13733f1..9a4265fe5 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -5222,6 +5222,7 @@ func (p *scionPacketProcessor) prepareSCMP( // length to remain: the address header is at most 48 bytes long // and the reversed path at most 796 bytes. // @ assert scionL.AddrHdrLenSpecInternal() <= 48 + // @ revPath.LenSpecBound(nil) // @ assert revPath.LenSpec(nil) <= 4 + 3*8 + 64*12 maxQuoteLen := slayers.MaxSCMPPacketLen - hdrLen // @ assert 0 <= maxQuoteLen From 12762f5f6436a9a8c534e128172d386ed9d5423f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 13:20:04 +0000 Subject: [PATCH 15/19] Re-trigger CI after GitHub Actions infrastructure failure The verify-deps job on 85ec14e died before starting ('Failed to resolve action download info. Error: Service Unavailable') and the GitHub App integration is not permitted to re-run failed jobs. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 From 22588c8baf933e805d0846b76a8eb9fdcd69a09b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 20:54:06 +0000 Subject: [PATCH 16/19] Bridge interface and concrete path length in the quote bound proof The lemma-head run is down to a single error: 0 <= maxQuoteLen. The LenSpecBound lemma discharges the concrete bound revPath.LenSpec(nil) <= 796, but hdrLen's path summand comes from the interface-dispatched scionL.Path.Len(nil), whose postcondition speaks about the interface-level LenSpec. Assert the identity of the receiver and the equality of the two LenSpec applications so the bound transfers. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- router/dataplane.go | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/router/dataplane.go b/router/dataplane.go index 9a4265fe5..991c9da41 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -5224,6 +5224,10 @@ func (p *scionPacketProcessor) prepareSCMP( // @ assert scionL.AddrHdrLenSpecInternal() <= 48 // @ revPath.LenSpecBound(nil) // @ assert revPath.LenSpec(nil) <= 4 + 3*8 + 64*12 + // The path length in hdrLen was computed through the path.Path + // interface; bridge it to the concrete *scion.Decoded bound. + // @ assert scionL.Path === revPath + // @ assert scionL.Path.LenSpec(nil) == revPath.LenSpec(nil) maxQuoteLen := slayers.MaxSCMPPacketLen - hdrLen // @ assert 0 <= maxQuoteLen if len(quote) > maxQuoteLen { From fbd27d6b264998f8932b99189beb1fa6c47b0f29 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 22:07:13 +0000 Subject: [PATCH 17/19] Make LenSpecBound fractional to keep LenSpec stable across it The quote-bound assert still failed with the lemma in place: the lemma consumed the full Decoded.Mem, so its internal unfold/refold produced a fresh predicate snapshot, severing the link between LenSpec's value at the earlier Path.Len(nil) call and at the asserts. Taking (and giving back) only an R50 fraction leaves the caller with an anchoring fraction, so the heap-dependent LenSpec provably keeps its value across the lemma - the same mechanism by which Decoded.Len's own 'l == LenSpec(ubuf)' postcondition composes. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- pkg/slayers/path/scion/decoded_spec.gobra | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index f3fd20697..1a013cb5d 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -205,20 +205,21 @@ func (d *Decoded) Widen(ubuf1, ubuf2 []byte) { // MaxINFs, NumHops <= MaxHops). It exists because the bound is buried two // predicate unfoldings deep and is not derivable from LenSpec's // definition alone at call sites. +// The lemma takes only a fraction so that the caller's retained fraction +// anchors the predicate snapshot: the value of LenSpec then provably +// survives the unfold/refold inside this lemma (cf. Len, which relates +// its result to LenSpec under the same fraction). ghost -requires d.Mem(ub) -ensures d.Mem(ub) -ensures d.LenSpec(ub) <= MetaLen + MaxINFs*path.InfoLen + MaxHops*path.HopLen +preserves acc(d.Mem(ub), R50) +ensures d.LenSpec(ub) <= MetaLen + MaxINFs*path.InfoLen + MaxHops*path.HopLen decreases func (d *Decoded) LenSpecBound(ghost ub []byte) { - ghost l := d.LenSpec(ub) - unfold d.Mem(ub) - ghost numINF := unfolding d.Base.Mem() in d.Base.NumINF - ghost numHops := unfolding d.Base.Mem() in d.Base.NumHops - assert unfolding d.Base.Mem() in (numINF <= MaxINFs && numHops <= MaxHops) + unfold acc(d.Mem(ub), R50) + ghost numINF := unfolding acc(d.Base.Mem(), R50) in d.Base.NumINF + ghost numHops := unfolding acc(d.Base.Mem(), R50) in d.Base.NumHops + assert unfolding acc(d.Base.Mem(), R50) in (numINF <= MaxINFs && numHops <= MaxHops) assert d.Base.Len() == MetaLen + numINF*path.InfoLen + numHops*path.HopLen - assert l == d.Base.Len() - fold d.Mem(ub) + fold acc(d.Mem(ub), R50) } // The resources captured by Mem are independent of the buffer parameter, From 34d69433b367c623c407efbc37d9b2cd7402e627 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 13 Jul 2026 22:26:07 +0000 Subject: [PATCH 18/19] Minimize LenSpecBound to fit the scion package's time budget The scion path package hit its 30-minute wall-clock timeout: unrelated members (Widen*/Xover* IO lemmas, DecodeFromBytes) were reported as 'did not terminate' while LenSpecBound itself finished, i.e. the new member consumed budget the rest of the package needed. Strip the lemma to a bare unfold/refold of the two predicates: InfoLen and HopLen are compile-time constants, so the bounds already stored in Base.Mem (NumINF <= MaxINFs, NumHops <= MaxHops) discharge the postcondition without ghost variables, extra asserts, or nonlinear arithmetic. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- pkg/slayers/path/scion/decoded_spec.gobra | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index 1a013cb5d..a7892cba5 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -208,17 +208,19 @@ func (d *Decoded) Widen(ubuf1, ubuf2 []byte) { // The lemma takes only a fraction so that the caller's retained fraction // anchors the predicate snapshot: the value of LenSpec then provably // survives the unfold/refold inside this lemma (cf. Len, which relates -// its result to LenSpec under the same fraction). +// its result to LenSpec under the same fraction). The body is kept +// minimal because pkg/slayers/path/scion is close to its verification +// time budget: InfoLen and HopLen are compile-time constants, so the two +// exposed predicate bounds (NumINF <= MaxINFs, NumHops <= MaxHops) +// discharge the postcondition without nonlinear reasoning. ghost preserves acc(d.Mem(ub), R50) ensures d.LenSpec(ub) <= MetaLen + MaxINFs*path.InfoLen + MaxHops*path.HopLen decreases func (d *Decoded) LenSpecBound(ghost ub []byte) { unfold acc(d.Mem(ub), R50) - ghost numINF := unfolding acc(d.Base.Mem(), R50) in d.Base.NumINF - ghost numHops := unfolding acc(d.Base.Mem(), R50) in d.Base.NumHops - assert unfolding acc(d.Base.Mem(), R50) in (numINF <= MaxINFs && numHops <= MaxHops) - assert d.Base.Len() == MetaLen + numINF*path.InfoLen + numHops*path.HopLen + unfold acc(d.Base.Mem(), R50) + fold acc(d.Base.Mem(), R50) fold acc(d.Mem(ub), R50) } From 3450274d7b4d6d2dd1172d521a2904164d1bda20 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 15 Jul 2026 17:03:51 +0000 Subject: [PATCH 19/19] Use writePerm for the reallocating quote append The last router error was the append of the quote payload onto scmpLayers: the ghost permission was noPerm (perm 0), copied verbatim from upstream where it had never been verified. scmpLayers is a length-3 composite literal (len == cap), so this append always reallocates and Gobra must copy the three existing interface elements into the new backing array - which requires positive read permission. Full access is held from the literal, so pass writePerm. (The working zero-permission appends elsewhere all append within spare capacity and never reallocate.) With this, the maxQuoteLen bound now discharges (the minimized LenSpecBound worked) and this was the sole remaining router error. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48 --- router/dataplane.go | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index 991c9da41..5de34c9a7 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -5237,7 +5237,12 @@ func (p *scionPacketProcessor) prepareSCMP( // @ sl.SplitRange_Bytes(ub, 0, len(quote), R55) // @ ghost pld := gopacket.Payload(quote) // @ fold pld.Mem(quote) - scmpLayers = append( /*@ noPerm, @*/ scmpLayers, gopacket.Payload(quote)) + // (VerifiedSCION) scmpLayers is a length-3 literal (len == cap), so + // this append always reallocates and must copy the three existing + // elements; that copy needs positive read permission (noPerm, i.e. + // perm 0, does not suffice), and full access is held from the + // literal. + scmpLayers = append( /*@ writePerm, @*/ scmpLayers, gopacket.Payload(quote)) // @ layerBufs = layerBufs ++ seq[[]byte]{ quote } // @ quoteLen = len(quote) }