Dataplane

[jcp19]

TODO:

• bfdSend.Mem
• bfdSend.String
• bfdSend.Send (skipped)
• Strengthen spec of decodeLayers
• processPkt and dependencies
  • reset
  • cases:
    • interBFD
    • intraBFD
    • onehop (processOHP #191)
    • scion
      • resolveInbound
      • connect with the rest of the proof
• Run
  • realized that the spec for BatchConn is unnecessarily restrictive, we should make it weaker - use wildcard perms instead of full perms
  • converge in postconditions of processPkt
  • merge Verify core of Run method #240
  • verify calls to the closures in (*DataPlane).Run(...) (Verify loops in Run #244)
  • Packscmp (Packscmp #126, Clear-up all calls to packSCMP #192) (partially done in Verify packSCMP #243, but we might have run into a bug that keeps us from verifying it further)
    • come up with a spec for packSCMP (Verify packSCMP #243)
    • verify it according to the given spec (Verify packSCMP #243)
    • remove all @TODO() that precede calls to it (blocked on a bug from scion)

In summary, we verified mem. safety for when receiving and sending SCION packets (except when we send SCMP packets as reply - ongoing and depends on packSCMP), when handling empty and when handling onehop packets.
This means that the only things missing are the epic paths and the generation of SCMP packets.

Nice to have:

On a first step:

• processEpic (processEpic #196, processEpic #261) - kinda done, but we need to debug performance problems
  • libepic (libepic #199, Bring changes of libepic from PR #261 #266)
• newBFDSend (and the setter methods that call this)
  • requires making slayers.SCION.Mem() more general (to allow nil ubufs)
  • setters of bfd connections in the dataplane
    • AddExternalInterfaceBFD
    • AddNextHopBFD
  • send and new
• missing getters and setter

Later:

• finish prepareSCMP (Preparescmp #245, Finish prepareSCMP #360) past the @TODO()
  • this may require some refactor of (*SCION).Mem and the introduction of a ghost field to describe whether a SCION struct was created manually or parsed from a slice
• Split memory footprint predicates from functional properties, as started in Refactor Mem permissions for Paths #228
• finish and merge the refactor (refactor parts of the dataplane #122, router/dataplane.go: information hiding and refactoring #155)
  • adapt according to Private Specification, Partial Struct Encoding, and Constructor gobra#619
• merge the latest commits in the upstream SCION (Upstream #190)
• check op. for linearity to use our linear type system
• allow _ perm in iterated collections with range (gobra)
• bfdSend
• [x] issue Run Gobra and tests on the CI #2
• address all files that have been specified but not verified
• adapt to the new map encoding (Test better triggers for maps gobra#606)
• dataplane adapter
• ghost fields to simplify Dataplane

[jcp19]

I will close this issue. All major tasks that are still missing have open issues already, we will track progress through them.