diff --git a/doc/verification/prepareSCMP.md b/doc/verification/prepareSCMP.md new file mode 100644 index 000000000..05287a0c7 --- /dev/null +++ b/doc/verification/prepareSCMP.md @@ -0,0 +1,777 @@ +# 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 +(`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) +``` + +(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.) + +--- + +## 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)`). (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 + 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)` — 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 + 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 + +> **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`): + +```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. + +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 is low-ripple. Its `len % 2 == 0` conjuncts follow + from `AddrType.Length() ∈ {4, 8, 12, 16}` (small lemma). + 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) + +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: 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 The trusted `SerializeLayers` spec + +Since the call must stay, `writer.gobra:105-112` gets a real (trusted) +quantified specification. Sketch: + +```gobra +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 */ +``` + +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))`. + +--- + +## 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 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)`); + 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 + `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`. + **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 — 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. + The §4.3 items are also resolved on this branch: + * ~~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` + 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 + `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.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. + **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. + +## 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. +* **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 + 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`. 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/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/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index 1ebbce5a3..a7892cba5 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -200,4 +200,41 @@ 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. +// 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). 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) + unfold acc(d.Base.Mem(), R50) + fold acc(d.Base.Mem(), R50) + fold acc(d.Mem(ub), R50) +} + +// 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 b74c6d61d..17bcfa512 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) @@ -650,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() @@ -683,10 +686,18 @@ 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 +// @ 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 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) @@ -700,7 +711,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 @@ -720,6 +735,11 @@ 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 +// @ 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 @@ -738,6 +758,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 @@ -775,7 +797,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) @@ -798,13 +828,18 @@ 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 +// @ 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 { @@ -977,16 +1012,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 @@ -1006,15 +1044,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() @@ -1044,43 +1082,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 3bcf6a96f..ad8d62a50 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -233,19 +233,172 @@ 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 +} + +// 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) +// 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 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() +} + +// 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:])) +} + +// 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 @@ -519,6 +672,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/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)), _) diff --git a/pkg/slayers/scmp.go b/pkg/slayers/scmp.go index 6892c007d..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) { @@ -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..a63b15a61 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 @@ -111,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) { @@ -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 @@ -256,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) { @@ -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 @@ -421,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) { @@ -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 @@ -551,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) { @@ -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 @@ -731,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) { @@ -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 @@ -862,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) { @@ -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 @@ -982,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/pkg/slayers/scmp_msg_spec.gobra b/pkg/slayers/scmp_msg_spec.gobra index f4cd61b64..8b3a461ef 100644 --- a/pkg/slayers/scmp_msg_spec.gobra +++ b/pkg/slayers/scmp_msg_spec.gobra @@ -40,21 +40,48 @@ 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 } +// 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 +// 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,20 +99,47 @@ 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 } +// 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 +// 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,20 +157,47 @@ 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 } +// 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 +// 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,20 +215,47 @@ 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 } +// 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 +// 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,20 +278,47 @@ 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 } +// 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 +// 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,20 +337,47 @@ 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 } +// 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 +// 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,16 +395,91 @@ 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 } +// 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 + +// 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) +} + +// 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/pkg/slayers/scmp_spec.gobra b/pkg/slayers/scmp_spec.gobra index edc47876d..8f1c3e0f4 100644 --- a/pkg/slayers/scmp_spec.gobra +++ b/pkg/slayers/scmp_spec.gobra @@ -58,17 +58,44 @@ 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) +} + +// 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/router/dataplane.go b/router/dataplane.go index 7803ba3c7..5de34c9a7 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 @@ -2556,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) @@ -2656,6 +2694,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 +2746,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 +2913,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 +3218,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 +3322,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 +3745,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, @@ -3790,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)) @@ -3920,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)) @@ -4055,6 +4109,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) { @@ -4097,6 +4153,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 +4167,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() @@ -4169,6 +4232,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) @@ -4905,10 +4970,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 ==> @@ -5061,25 +5134,53 @@ 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 + // 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) + // @ 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 @@ -5089,6 +5190,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{ @@ -5096,9 +5200,15 @@ func (p *scionPacketProcessor) prepareSCMP( FixLengths: true, } scmpLayers := []gopacket.SerializableLayer{&scionL, &scmpH, scmpP} + // (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. - 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 @@ -5108,17 +5218,70 @@ 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 + // @ 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 { quote = quote[:maxQuoteLen] } - scmpLayers = append( /*@ noPerm, @*/ scmpLayers, gopacket.Payload(quote)) + // @ assert quote === ub[0:len(quote)] + // @ sl.SplitRange_Bytes(ub, 0, len(quote), R55) + // @ ghost pld := gopacket.Payload(quote) + // @ fold pld.Mem(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) } // 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/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra index 1e9927cbe..383f2e759 100644 --- a/verification/dependencies/github.com/google/gopacket/base.gobra +++ b/verification/dependencies/github.com/google/gopacket/base.gobra @@ -67,12 +67,24 @@ 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) +// (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 @@ -119,3 +131,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 +} diff --git a/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra b/verification/dependencies/github.com/google/gopacket/layers/bfd.gobra index 14214df43..3e364e8c6 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) @@ -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 9c8f84252..9ca3ad88b 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -15,17 +15,39 @@ 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())) 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) + // (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 @@ -102,11 +124,52 @@ 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 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]) +// 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) ==> + acc(sl.Bytes(layerBufs[i], 0, len(layerBufs[i])), R55) +ensures w.Mem() && sl.Bytes(w.UBuf(), 0, len(w.UBuf())) +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) ==> + 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) error +func SerializeLayers(w SerializeBuffer, opts SerializeOptions, ghost layerBufs seq[[]byte], layers ...SerializableLayer) (err error)