From e71ba3a8e5d25dd9158cf9de4e90e583f9112085 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 19 Feb 2024 13:37:14 +0100 Subject: [PATCH] Changes to avoid unnecessary assumptions (#246) * try out a few changes * continue * continue * backup * fix preds * backup * continue * continue efforts * last setter * fix perm for runningPerm * only Run missing now * backup * cleanup unnecessary symbols * store progress * backup current status * backup * backup * backup * backup * backup * rm file commited by mistake * backup * backup * fix calls to initMetrics * backup * further cleanup * fix verification error --- router/assumptions.gobra | 6 + router/dataplane.go | 467 ++++++++++-------- router/dataplane_spec.gobra | 451 ++++++++++------- router/dataplane_spec_test.gobra | 34 ++ .../dependencies/context/context.gobra | 9 +- 5 files changed, 580 insertions(+), 387 deletions(-) diff --git a/router/assumptions.gobra b/router/assumptions.gobra index b09b0613b..f8811b007 100644 --- a/router/assumptions.gobra +++ b/router/assumptions.gobra @@ -39,6 +39,12 @@ ensures malformedPath.ErrorMem() decreases _ func establishMemMalformedPath() +ghost +ensures alreadySet != nil +ensures alreadySet.ErrorMem() +decreases _ +func establishAlreadySet() + ghost ensures unsupportedPathTypeNextHeader.ErrorMem() decreases _ diff --git a/router/dataplane.go b/router/dataplane.go index ec0b957e2..03da2c041 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -135,8 +135,10 @@ type BatchConn interface { // @ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, addr *net.UDPAddr) (n int, err error) // @ requires acc(Mem(), _) - // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> - // @ (acc(msgs[i].Mem(), R50) && msgs[i].HasActiveAddr()) + // (VerifiedSCION) opted for less reusable spec for WriteBatch for + // performance reasons. + // @ requires len(msgs) == 1 + // @ preserves acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr() // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() WriteBatch(msgs underlayconn.Messages, flags int) (n int, err error) @@ -210,19 +212,24 @@ func (e scmpError) Error() string { } // SetIA sets the local IA for the dataplane. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.localIA, 1/2) && d.localIA.IsZero() +// @ requires acc(d.Mem(), OutMutexPerm) +// @ requires !d.IsRunning() +// @ requires d.LocalIA().IsZero() // @ requires !ia.IsZero() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.localIA, 1/2) +// @ ensures acc(d.Mem(), OutMutexPerm) +// @ ensures !d.IsRunning() // @ ensures e == nil func (d *DataPlane) SetIA(ia addr.IA) (e error) { d.mtx.Lock() defer d.mtx.Unlock() // @ unfold MutexInvariant!() + // @ assert !d.IsRunning() + // @ d.isRunningEq() + // @ unfold d.Mem() // @ defer fold MutexInvariant!() + // @ defer fold d.Mem() if d.running { // @ Unreachable() return modifyExisting @@ -241,23 +248,28 @@ func (d *DataPlane) SetIA(ia addr.IA) (e error) { // SetKey sets the key used for MAC verification. The key provided here should // already be derived as in scrypto.HFMacFactory. -// @ requires acc(&d.key, 1/2) -// @ requires acc(d.key, 1/2) -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.macFactory, 1/2) && d.macFactory == nil +// @ requires acc(d.Mem(), OutMutexPerm) +// @ requires !d.IsRunning() +// @ requires !d.KeyIsSet() // @ requires len(key) > 0 // @ requires sl.AbsSlice_Bytes(key, 0, len(key)) // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.macFactory, 1/2) -// @ ensures res == nil ==> d.macFactory != nil +// @ ensures acc(d.Mem(), OutMutexPerm) +// @ ensures !d.IsRunning() +// @ ensures res == nil ==> d.KeyIsSet() func (d *DataPlane) SetKey(key []byte) (res error) { // @ share key d.mtx.Lock() defer d.mtx.Unlock() // @ unfold MutexInvariant!() + // @ assert !d.IsRunning() + // @ d.isRunningEq() + // @ unfold acc(d.Mem(), 1/2) + // @ d.keyIsSetEq() + // @ unfold acc(d.Mem(), 1/2) // @ defer fold MutexInvariant!() + // @ defer fold d.Mem() if d.running { // @ Unreachable() return modifyExisting @@ -299,20 +311,24 @@ func (d *DataPlane) SetKey(key []byte) (res error) { // send/receive traffic in the local AS. This can only be called once; future // calls will return an error. This can only be called on a not yet running // dataplane. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.internal, 1/2) && d.internal == nil -// @ requires acc(&d.internalIP, 1/2) +// @ requires acc(d.Mem(), OutMutexPerm) +// @ requires !d.IsRunning() +// @ requires !d.InternalConnIsSet() // @ requires conn != nil && conn.Mem() // @ requires ip.Mem() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.internal, 1/2) -// @ ensures acc(&d.internalIP, 1/2) +// @ ensures acc(d.Mem(), OutMutexPerm) +// @ ensures !d.IsRunning() func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { d.mtx.Lock() defer d.mtx.Unlock() // @ unfold MutexInvariant!() + // @ assert !d.IsRunning() + // @ d.isRunningEq() + // @ unfold acc(d.Mem(), 1/2) + // @ d.internalIsSetEq() + // @ unfold acc(d.Mem(), 1/2) if d.running { // @ Unreachable() return modifyExisting @@ -327,6 +343,7 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { } d.internal = conn d.internalIP = ip + // @ fold d.Mem() // @ fold MutexInvariant!() return nil } @@ -334,19 +351,18 @@ func (d *DataPlane) AddInternalInterface(conn BatchConn, ip net.IP) error { // AddExternalInterface adds the inter AS connection for the given interface ID. // If a connection for the given ID is already set this method will return an // error. This can only be called on a not yet running dataplane. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.external, 1/2) -// @ requires d.external != nil ==> acc(d.external, 1/2) -// @ requires !(ifID in domain(d.external)) // @ requires conn != nil && conn.Mem() +// @ preserves acc(d.Mem(), OutMutexPerm) +// @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.external, 1/2) && acc(d.external, 1/2) func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { d.mtx.Lock() defer d.mtx.Unlock() // @ unfold MutexInvariant!() + // @ assert !d.IsRunning() + // @ d.isRunningEq() + // @ unfold d.Mem() if d.running { // @ Unreachable() return modifyExisting @@ -355,10 +371,15 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { // @ Unreachable() return emptyValue } + // @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), 1/2) } if _, existsB := d.external[ifID]; existsB { - // @ Unreachable() + // @ establishAlreadySet() + // @ ghost if d.external != nil { fold acc(accBatchConn(d.external), 1/2) } + // @ fold d.Mem() + // @ fold MutexInvariant!() return serrors.WithCtx(alreadySet, "ifID", ifID) } + // @ ghost if d.external != nil { fold acc(accBatchConn(d.external), 1/2) } if d.external == nil { d.external = make(map[uint16]BatchConn) // @ fold accBatchConn(d.external) @@ -366,6 +387,7 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { // @ unfold accBatchConn(d.external) d.external[ifID] = conn // @ fold accBatchConn(d.external) + // @ fold d.Mem() // @ fold MutexInvariant!() return nil } @@ -373,20 +395,17 @@ func (d *DataPlane) AddExternalInterface(ifID uint16, conn BatchConn) error { // AddNeighborIA adds the neighboring IA for a given interface ID. If an IA for // the given ID is already set, this method will return an error. This can only // be called on a yet running dataplane. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.neighborIAs, 1/2) -// @ requires d.neighborIAs != nil ==> acc(d.neighborIAs, 1/2) // @ requires !remote.IsZero() -// @ requires !(ifID in domain(d.neighborIAs)) +// @ preserves acc(d.Mem(), OutMutexPerm) +// @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.neighborIAs,1/2) && acc(d.neighborIAs, 1/2) -// @ ensures domain(d.neighborIAs) == old(domain(d.neighborIAs)) union set[uint16]{ifID} func (d *DataPlane) AddNeighborIA(ifID uint16, remote addr.IA) error { d.mtx.Lock() defer d.mtx.Unlock() // @ unfold MutexInvariant!() + // @ d.isRunningEq() + // @ unfold d.Mem() if d.running { // @ Unreachable() return modifyExisting @@ -396,13 +415,16 @@ func (d *DataPlane) AddNeighborIA(ifID uint16, remote addr.IA) error { return emptyValue } if _, existsB := d.neighborIAs[ifID]; existsB { - // @ Unreachable() + // @ establishAlreadySet() + // @ fold d.Mem() + // @ fold MutexInvariant!() return serrors.WithCtx(alreadySet, "ifID", ifID) } if d.neighborIAs == nil { d.neighborIAs = make(map[uint16]addr.IA) } d.neighborIAs[ifID] = remote + // @ fold d.Mem() // @ fold MutexInvariant!() return nil } @@ -410,23 +432,24 @@ func (d *DataPlane) AddNeighborIA(ifID uint16, remote addr.IA) error { // AddLinkType adds the link type for a given interface ID. If a link type for // the given ID is already set, this method will return an error. This can only // be called on a not yet running dataplane. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.linkTypes, 1/2) -// @ requires d.linkTypes != nil ==> acc(d.linkTypes, 1/2) -// @ requires !(ifID in domain(d.linkTypes)) -// (VerifiedSCION) unlike all other setter methods, this does not lock -// d.mtx. Did the devs forget about it? +// @ preserves acc(d.Mem(), OutMutexPerm) +// @ preserves !d.IsRunning() +// (VerifiedSCION) unlike all other setter methods, this does not lock d.mtx. +// This was reported in https://github.com/scionproto/scion/issues/4282. // @ preserves MutexInvariant!() -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.linkTypes, 1/2) && acc(d.linkTypes, 1/2) -// @ ensures domain(d.linkTypes) == old(domain(d.linkTypes)) union set[uint16]{ifID} func (d *DataPlane) AddLinkType(ifID uint16, linkTo topology.LinkType) error { + // @ unfold acc(d.Mem(), OutMutexPerm) if _, existsB := d.linkTypes[ifID]; existsB { - // @ Unreachable() + // @ establishAlreadySet() + // @ fold acc(d.Mem(), OutMutexPerm) return serrors.WithCtx(alreadySet, "ifID", ifID) } + // @ fold acc(d.Mem(), OutMutexPerm) // @ unfold MutexInvariant!() + // @ d.isRunningEq() + // @ unfold d.Mem() // @ defer fold MutexInvariant!() + // @ defer fold d.Mem() if d.linkTypes == nil { d.linkTypes = make(map[uint16]topology.LinkType) } @@ -469,10 +492,10 @@ func (d *DataPlane) AddExternalInterfaceBFD(ifID uint16, conn BatchConn, // getInterfaceState checks if there is a bfd session for the input interfaceID and // returns InterfaceUp if the relevant bfdsession state is up, or if there is no BFD // session. Otherwise, it returns InterfaceDown. -// @ preserves acc(MutexInvariant!(), R5) +// @ preserves acc(d.Mem(), R5) func (d *DataPlane) getInterfaceState(interfaceID uint16) control.InterfaceState { - // @ unfold acc(MutexInvariant!(), R5) - // @ defer fold acc(MutexInvariant!(), R5) + // @ unfold acc(d.Mem(), R5) + // @ defer fold acc(d.Mem(), R5) bfdSessions := d.bfdSessions // @ ghost if bfdSessions != nil { // @ unfold acc(accBfdSession(d.bfdSessions), R20) @@ -493,11 +516,7 @@ func (d *DataPlane) getInterfaceState(interfaceID uint16) control.InterfaceState // (VerifiedSCION) marked as trusted because we currently do not support bfd.Session // @ trusted -// @ requires acc(metrics.PacketsSent.Mem(), _) && acc(metrics.PacketsReceived.Mem(), _) -// @ requires acc(metrics.Up.Mem(), _) && acc(metrics.StateChanges.Mem(), _) -// @ preserves MutexInvariant!() -// @ requires s.Mem() -// @ decreases +// @ requires false func (d *DataPlane) addBFDController(ifID uint16, s *bfdSend, cfg control.BFD, metrics bfd.Metrics) error { @@ -530,27 +549,29 @@ func (d *DataPlane) addBFDController(ifID uint16, s *bfdSend, cfg control.BFD, // times for the same service, with the address added to the list of addresses // that provide the service. // @ requires a != nil && acc(a.Mem(), R10) -// @ preserves acc(&d.svc, 1/2) +// @ preserves acc(d.Mem(), OutMutexPerm) +// @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error { d.mtx.Lock() + // @ unfold MutexInvariant!() + // @ d.isRunningEq() defer d.mtx.Unlock() if a == nil { return emptyValue } - // @ preserves MutexInvariant!() - // @ preserves acc(&d.svc, 1/2) - // @ ensures d.svc != nil + // @ preserves d.Mem() + // @ ensures unfolding d.Mem() in d.svc != nil // @ decreases // @ outline( - // @ unfold MutexInvariant!() + // @ unfold d.Mem() if d.svc == nil { d.svc = newServices() } - // @ fold MutexInvariant!() + // @ fold d.Mem() // @ ) - // @ unfold acc(MutexInvariant!(), R15) + // @ unfold acc(d.Mem(), R15) // @ assert acc(d.svc.Mem(), _) d.svc.AddSvc(svc, a) if d.Metrics != nil { @@ -569,22 +590,29 @@ func (d *DataPlane) AddSvc(svc addr.HostSVC, a *net.UDPAddr) error { d.Metrics.ServiceInstanceCount.With(labels).Add(float64(1)) // @ ) } - // @ fold acc(MutexInvariant!(), R15) + // @ fold acc(d.Mem(), R15) + // @ fold MutexInvariant!() return nil } // DelSvc deletes the address for the given service. +// (VerifiedSCION) the spec here is definitely weird. Even though +// the lock is acquired here, there is no check that the router is +// not yet running, thus acquiring the lock is not enough to guarantee +// absence of race conditions. To specify that the router is not running, +// we need to pass perms to d.Mem(), but if we do this, then we don't need +// the lock invariant to perform the operations in this function. // @ requires a != nil && acc(a.Mem(), R10) +// @ preserves acc(d.Mem(), OutMutexPerm/2) // @ preserves d.mtx.LockP() -// @ preserves d.mtx.LockInv() == MutexInvariant!; func (d *DataPlane) DelSvc(svc addr.HostSVC, a *net.UDPAddr) error { d.mtx.Lock() defer d.mtx.Unlock() if a == nil { return emptyValue } - // @ unfold acc(MutexInvariant!(), R15) - // @ ghost defer fold acc(MutexInvariant!(), R15) + // @ unfold acc(d.Mem(), R40) + // @ ghost defer fold acc(d.Mem(), R40) if d.svc == nil { return nil } @@ -602,34 +630,34 @@ func (d *DataPlane) DelSvc(svc addr.HostSVC, a *net.UDPAddr) error { // AddNextHop sets the next hop address for the given interface ID. If the // interface ID already has an address associated this operation fails. This can // only be called on a not yet running dataplane. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.internalNextHops, 1/2) -// @ requires d.internalNextHops != nil ==> acc(d.internalNextHops, 1/2) -// @ requires !(ifID in domain(d.internalNextHops)) // @ requires a != nil && a.Mem() +// @ preserves acc(d.Mem(), OutMutexPerm) +// @ preserves !d.IsRunning() // @ preserves d.mtx.LockP() // @ preserves d.mtx.LockInv() == MutexInvariant!; -// @ ensures acc(&d.running, 1/2) && !d.running -// @ ensures acc(&d.internalNextHops, 1/2) && acc(d.internalNextHops, 1/2) func (d *DataPlane) AddNextHop(ifID uint16, a *net.UDPAddr) error { d.mtx.Lock() defer d.mtx.Unlock() // @ unfold MutexInvariant!() + // @ d.isRunningEq() + // @ unfold d.Mem() // @ defer fold MutexInvariant!() + // @ defer fold d.Mem() if d.running { return modifyExisting } if a == nil { return emptyValue } + // @ ghost if d.internalNextHops != nil { unfold accAddr(d.internalNextHops) } if _, existsB := d.internalNextHops[ifID]; existsB { + // @ fold accAddr(d.internalNextHops) + // @ establishAlreadySet() return serrors.WithCtx(alreadySet, "ifID", ifID) } if d.internalNextHops == nil { d.internalNextHops = make(map[uint16]*net.UDPAddr) - // @ fold accAddr(d.internalNextHops) } - // @ unfold accAddr(d.internalNextHops) // @ defer fold accAddr(d.internalNextHops) d.internalNextHops[ifID] = a return nil @@ -678,37 +706,74 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro // Run starts running the dataplane. Note that configuration is not possible // after calling this method. -// @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.Metrics, 1/2) && d.Metrics != nil -// @ requires acc(&d.svc, 1/2) && d.svc != nil -// @ requires acc(&d.internal, 1/2) && d.internal != nil -// @ requires acc(&d.macFactory, 1/2) && d.macFactory != nil -// @ requires acc(&d.forwardingMetrics, 1/2) && acc(d.forwardingMetrics, 1/2) +// @ requires acc(d.Mem(), OutMutexPerm) +// @ requires !d.IsRunning() +// @ requires d.InternalConnIsSet() +// @ requires d.KeyIsSet() +// @ requires d.SvcsAreSet() +// @ requires d.MetricsAreSet() +// @ requires d.PreWellConfigured() +// (VerifiedSCION) here, the spec still uses a private field. // @ requires d.mtx.LockP() // @ requires d.mtx.LockInv() == MutexInvariant!; -// @ requires acc(ctx.Mem(), _) -// @ requires acc(&d.mtx, _) +// @ requires ctx != nil && ctx.Mem() func (d *DataPlane) Run(ctx context.Context) error { // @ share d, ctx d.mtx.Lock() // @ unfold MutexInvariant!() - // @ assert d.forwardingMetrics != nil - // @ assert acc(&d.forwardingMetrics, _) && acc(d.forwardingMetrics, _) + // @ assert !d.IsRunning() + // @ d.isRunningEq() + + // @ requires acc(&d, R50) + // @ requires acc(&d.running, runningPerm) + // @ requires d.Mem() && !d.IsRunning() + // @ requires d.InternalConnIsSet() + // @ requires d.KeyIsSet() + // @ requires d.SvcsAreSet() + // @ requires d.MetricsAreSet() + // @ requires d.PreWellConfigured() + // @ ensures acc(&d, R50) + // @ ensures MutexInvariant!() + // @ ensures d.Mem() && d.IsRunning() + // @ ensures d.InternalConnIsSet() + // @ ensures d.KeyIsSet() + // @ ensures d.SvcsAreSet() + // @ ensures d.MetricsAreSet() + // @ ensures d.PreWellConfigured() + // @ decreases + // @ outline ( + // @ reveal d.PreWellConfigured() + // @ unfold d.Mem() d.running = true - + // @ fold MutexInvariant!() + // @ fold d.Mem() + // @ reveal d.PreWellConfigured() + // @ ) d.initMetrics() read /*@@@*/ := - // @ requires acc(&d, _) - // @ requires acc(d, _) - // @ requires acc(MutexInvariant(d), _) && d.WellConfigured() - // @ requires d.getValSvc() != nil - // @ requires d.getValForwardingMetrics() != nil - // @ requires 0 in d.getDomForwardingMetrics() - // @ requires ingressID in d.getDomForwardingMetrics() - // @ requires d.macFactory != nil + // (VerifiedSCION) Due to issue https://github.com/viperproject/gobra/issues/723, + // there is currently an incompletness when calling closures that capture variables + // from (Viper) methods where they were not allocated. To address that, we introduce + // dPtr as an helper parameter. It always receives the value &d. + // @ requires acc(dPtr, _) + // @ requires let d := *dPtr in + // @ acc(&d.external, _) && acc(&d.linkTypes, _) && + // @ acc(&d.neighborIAs, _) && acc(&d.internal, _) && + // @ acc(&d.internalIP, _) && acc(&d.internalNextHops, _) && + // @ acc(&d.svc, _) && acc(&d.macFactory, _) && acc(&d.bfdSessions, _) && + // @ acc(&d.localIA, _) && acc(&d.running, _) && acc(&d.Metrics, _) && + // @ acc(&d.forwardingMetrics, _) && acc(&d.key, _) + // @ requires let d := *dPtr in + // @ acc(d.Mem(), _) && d.WellConfigured() + // @ requires let d := *dPtr in d.getValSvc() != nil + // @ requires let d := *dPtr in d.getValForwardingMetrics() != nil + // @ requires let d := *dPtr in (0 in d.getDomForwardingMetrics()) + // @ requires let d := *dPtr in (ingressID in d.getDomForwardingMetrics()) + // @ requires let d := *dPtr in d.macFactory != nil // @ requires rd != nil && acc(rd.Mem(), _) - func /*@ rc @*/ (ingressID uint16, rd BatchConn) { + func /*@ rc @*/ (ingressID uint16, rd BatchConn, dPtr **DataPlane) { + d := *dPtr msgs := conn.NewReadMessages(inputBatchCnt) // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ msgs[i].Mem() && msgs[i].GetAddr() == nil @@ -759,9 +824,14 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ msgs[i].Mem() // @ invariant writeMsgInv(writeMsgs) - // @ invariant acc(&d, _) - // @ invariant acc(d, _) - // @ invariant acc(MutexInvariant(d), _) && d.WellConfigured() + // @ invariant acc(dPtr, _) && *dPtr === d + // @ invariant acc(&d.external, _) && acc(&d.linkTypes, _) && + // @ acc(&d.neighborIAs, _) && acc(&d.internal, _) && + // @ acc(&d.internalIP, _) && acc(&d.internalNextHops, _) && + // @ acc(&d.svc, _) && acc(&d.macFactory, _) && acc(&d.bfdSessions, _) && + // @ acc(&d.localIA, _) && acc(&d.running, _) && acc(&d.Metrics, _) && + // @ acc(&d.forwardingMetrics, _) && acc(&d.key, _) + // @ invariant acc(d.Mem(), _) && d.WellConfigured() // @ invariant d.getValSvc() != nil // @ invariant d.getValForwardingMetrics() != nil // @ invariant 0 in d.getDomForwardingMetrics() @@ -792,9 +862,14 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ invariant acc(&scmpErr) // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ invariant writeMsgInv(writeMsgs) - // @ invariant acc(&d, _) - // @ invariant acc(d, _) - // @ invariant acc(MutexInvariant(d), _) && d.WellConfigured() + // @ invariant acc(dPtr, _) && *dPtr === d + // @ invariant acc(&d.external, _) && acc(&d.linkTypes, _) && + // @ acc(&d.neighborIAs, _) && acc(&d.internal, _) && + // @ acc(&d.internalIP, _) && acc(&d.internalNextHops, _) && + // @ acc(&d.svc, _) && acc(&d.macFactory, _) && acc(&d.bfdSessions, _) && + // @ acc(&d.localIA, _) && acc(&d.running, _) && acc(&d.Metrics, _) && + // @ acc(&d.forwardingMetrics, _) && acc(&d.key, _) + // @ invariant acc(d.Mem(), _) && d.WellConfigured() // @ invariant d.getValSvc() != nil // @ invariant d.getValForwardingMetrics() != nil // @ invariant 0 in d.getDomForwardingMetrics() @@ -907,8 +982,6 @@ func (d *DataPlane) Run(ctx context.Context) error { } // @ sl.NilAcc_Bytes() // @ fold acc(writeMsgs[0].Mem(), R50) - // @ assert forall i int :: { &writeMsgs[i] } 0 <= i && i < len(writeMsgs) ==> - // @ acc(writeMsgs[i].Mem(), R50) _, err = result.OutConn.WriteBatch(writeMsgs, syscall.MSG_DONTWAIT) // @ unfold acc(writeMsgs[0].Mem(), R50) // @ ghost if addrAliasesPkt && result.OutAddr != nil { @@ -938,8 +1011,8 @@ func (d *DataPlane) Run(ctx context.Context) error { inputCounters.DroppedPacketsTotal.Inc() continue } - // @ requires acc(&d, _) - // @ requires acc(MutexInvariant(d), _) + // @ requires acc(dPtr, _) && *dPtr === d + // @ requires acc(d.Mem(), _) // @ requires result.EgressID in d.getDomForwardingMetrics() // @ decreases // @ outline( @@ -959,12 +1032,9 @@ func (d *DataPlane) Run(ctx context.Context) error { } } - // @ fold acc(MutexInvariant(d), R55) + // @ unfold acc(d.Mem(), R1) + // @ assert d.WellConfigured() // @ assert 0 in d.getDomForwardingMetrics() - // (VerifiedSCION) the following cannot be expressed as a pre-condition: - // there is really no way of specifying that the dataplane protected by the lock - // satisfies this condition. - // @ assume d.WellConfigured() // @ ghost if d.bfdSessions != nil { unfold acc(accBfdSession(d.bfdSessions), R2) } @@ -1008,12 +1078,17 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ invariant acc(&read, _) && read implements rc // @ invariant acc(&d, _) // @ invariant acc(&d.external, _) && d.external === externals - // @ invariant acc(MutexInvariant(d), _) && d.WellConfigured() + // @ invariant acc(d.Mem(), _) && d.WellConfigured() // @ invariant externals != nil ==> acc(externals, R4) // @ invariant externals != nil ==> acc(accBatchConn(externals), R4) - // @ invariant acc(&d, _) - // @ invariant acc(d, _) - // @ invariant acc(MutexInvariant(d), _) && d.WellConfigured() + // (VerifiedSCION) can we drop a few of these perms? + // @ invariant acc(&d.external, _) && acc(&d.linkTypes, _) && + // @ acc(&d.neighborIAs, _) && acc(&d.internal, _) && + // @ acc(&d.internalIP, _) && acc(&d.internalNextHops, _) && + // @ acc(&d.svc, _) && acc(&d.macFactory, _) && acc(&d.bfdSessions, _) && + // @ acc(&d.localIA, _) && acc(&d.running, _) && acc(&d.Metrics, _) && + // @ acc(&d.forwardingMetrics, _) && acc(&d.key, _) + // @ invariant acc(d.Mem(), _) && d.WellConfigured() // @ invariant d.getValSvc() != nil // @ invariant d.getValForwardingMetrics() != nil // @ invariant 0 in d.getDomForwardingMetrics() @@ -1023,8 +1098,13 @@ func (d *DataPlane) Run(ctx context.Context) error { cl := // @ requires acc(&read, _) && read implements rc // @ requires acc(&d, _) - // @ requires acc(d, _) - // @ requires acc(MutexInvariant(d), _) && d.WellConfigured() + // @ requires acc(&d.external, _) && acc(&d.linkTypes, _) && + // @ acc(&d.neighborIAs, _) && acc(&d.internal, _) && + // @ acc(&d.internalIP, _) && acc(&d.internalNextHops, _) && + // @ acc(&d.svc, _) && acc(&d.macFactory, _) && acc(&d.bfdSessions, _) && + // @ acc(&d.localIA, _) && acc(&d.running, _) && acc(&d.Metrics, _) && + // @ acc(&d.forwardingMetrics, _) && acc(&d.key, _) + // @ requires acc(d.Mem(), _) && d.WellConfigured() // @ requires d.getValSvc() != nil // @ requires d.getValForwardingMetrics() != nil // @ requires 0 in d.getDomForwardingMetrics() @@ -1033,22 +1113,7 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ requires c != nil && acc(c.Mem(), _) func /*@ closure2 @*/ (i uint16, c BatchConn) { defer log.HandlePanic() - // @ assert read implements rc - // (VerifiedSCION) check preconditions of call to read(i, c) manually. - // @ assert acc(&d, _) - // @ assert acc(d, _) - // @ assert acc(MutexInvariant(d), _) && d.WellConfigured() - // @ assert d.getValSvc() != nil - // @ assert d.getValForwardingMetrics() != nil - // @ assert 0 in d.getDomForwardingMetrics() - // @ assert i in d.getDomForwardingMetrics() - // @ assert d.macFactory != nil - // @ assert c != nil && acc(c.Mem(), _) - - // (VerifiedSCION) Skip automated verification of the call due to a - // bug in Gobra. (https://github.com/viperproject/gobra/issues/723) - // @ TODO() - read(i, c) //@ as rc + read(i, c, &d) //@ as rc } // @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), R50) } // @ assert v in range(d.external) @@ -1060,8 +1125,13 @@ func (d *DataPlane) Run(ctx context.Context) error { cl := // @ requires acc(&read, _) && read implements rc // @ requires acc(&d, _) - // @ requires acc(d, _) - // @ requires acc(MutexInvariant(d), _) && d.WellConfigured() + // @ requires acc(&d.external, _) && acc(&d.linkTypes, _) && + // @ acc(&d.neighborIAs, _) && acc(&d.internal, _) && + // @ acc(&d.internalIP, _) && acc(&d.internalNextHops, _) && + // @ acc(&d.svc, _) && acc(&d.macFactory, _) && acc(&d.bfdSessions, _) && + // @ acc(&d.localIA, _) && acc(&d.running, _) && acc(&d.Metrics, _) && + // @ acc(&d.forwardingMetrics, _) && acc(&d.key, _) + // @ requires acc(d.Mem(), _) && d.WellConfigured() // @ requires d.getValSvc() != nil // @ requires d.getValForwardingMetrics() != nil // @ requires 0 in d.getDomForwardingMetrics() @@ -1069,57 +1139,37 @@ func (d *DataPlane) Run(ctx context.Context) error { // @ requires c != nil && acc(c.Mem(), _) func /*@ closure3 @*/ (c BatchConn) { defer log.HandlePanic() - // @ assert read implements rc - - // (VerifiedSCION) once again, check preconditions of call to read(0, c) - // manually, due to a completness issue with closures: - // https://github.com/viperproject/gobra/issues/723. - // @ assert acc(&d, _) - // @ assert acc(d, _) - // @ assert acc(MutexInvariant(d), _) && d.WellConfigured() - // @ assert d.getValSvc() != nil - // @ assert d.getValForwardingMetrics() != nil - // @ assert 0 in d.getDomForwardingMetrics() - // @ assert d.macFactory != nil - // @ assert c != nil && acc(c.Mem(), _) - - // (VerifiedSCION) Skip automated verification and rely on manual - // checks above. - // @ TODO() - read(0, c) //@ as rc + read(0, c, &d) //@ as rc } go cl(d.internal) //@ as closure3 - // (VerifiedSCION) we ignore verification from this point onward because of the - // call to Unlock. Supporting it is conceptually easy, but it requires changing - // the DataPlane invariant to distinguish between not running and not running. - // When not running, we get the same exact invariant as we have now. When running, - // we get a wildcard permission amount to the same exact invariant as we have now. - // This is easy, but cumbersome and slow to change everywhere. - // @ IgnoreFromHere() d.mtx.Unlock() - - r1 /*@ , r2 @*/ := ctx.Done() - <-r1 + // @ assert acc(ctx.Mem(), _) + c := ctx.Done() + // @ fold PredTrue!() + // @ assert c.RecvGivenPerm() == PredTrue! + <-c return nil } // initMetrics initializes the metrics related to packet forwarding. The // counters are already instantiated for all the relevant interfaces so this // will not have to be repeated during packet forwarding. -// @ preserves acc(&d.forwardingMetrics) -// @ preserves acc(&d.localIA, R15) -// @ preserves acc(&d.neighborIAs, R15) -// @ preserves d.neighborIAs != nil ==> acc(d.neighborIAs, R15) // required for call -// @ preserves acc(&d.Metrics, R15) && acc(d.Metrics.Mem(), _) -// @ preserves acc(&d.external, R15) -// @ preserves d.external != nil ==> acc(accBatchConn(d.external), R15) // required for call -// @ preserves acc(&d.internalNextHops, R15) -// @ preserves d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), R15) -// @ ensures accForwardingMetrics(d.forwardingMetrics) +// @ requires d.Mem() +// @ requires d.MetricsAreSet() +// @ requires d.PreWellConfigured() +// @ ensures d.Mem() +// @ ensures d.MetricsAreSet() +// @ ensures d.WellConfigured() // @ ensures 0 in d.DomainForwardingMetrics() +// @ ensures d.InternalConnIsSet() == old(d.InternalConnIsSet()) +// @ ensures d.KeyIsSet() == old(d.KeyIsSet()) +// @ ensures d.SvcsAreSet() == old(d.SvcsAreSet()) +// @ ensures d.getValForwardingMetrics() != nil // @ decreases func (d *DataPlane) initMetrics() { + // @ reveal d.PreWellConfigured() + // @ unfold d.Mem() // @ preserves acc(&d.forwardingMetrics) // @ preserves acc(&d.localIA, R20) // @ preserves acc(&d.neighborIAs, R20) @@ -1137,18 +1187,26 @@ func (d *DataPlane) initMetrics() { // @ liftForwardingMetricsNonInjectiveMem(d.forwardingMetrics[0], 0) // @ ) // @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), R15) } + // @ ghost if d.internalNextHops != nil { unfold acc(accAddr(d.internalNextHops), R15) } + // (VerifiedSCION) avoids incompletnes + // when folding acc(forwardingMetricsMem(d.forwardingMetrics[id], id), _) // @ fold acc(hideLocalIA(&d.localIA), R15) - // @ invariant acc(hideLocalIA(&d.localIA), R15) // avoids incompletnes when folding acc(forwardingMetricsMem(d.forwardingMetrics[id], id), _) + // @ ghost dExternal := d.external + // @ ghost dInternalNextHops := d.internalNextHops + + // @ invariant acc(hideLocalIA(&d.localIA), R15) // @ invariant acc(&d.external, R15) // @ invariant d.external != nil ==> acc(d.external, R20) - // @ invariant d.external === old(d.external) + // @ invariant d.external === dExternal // @ invariant acc(&d.forwardingMetrics) && acc(d.forwardingMetrics) + // @ invariant domain(d.forwardingMetrics) == set[uint16]{0} union visitedSet // @ invariant 0 in domain(d.forwardingMetrics) // @ invariant acc(&d.internalNextHops, R15) - // @ invariant d.internalNextHops === old(d.internalNextHops) - // @ invariant d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), R15) + // @ invariant d.internalNextHops === dInternalNextHops + // @ invariant d.internalNextHops != nil ==> acc(d.internalNextHops, R20) + // @ invariant domain(d.internalNextHops) intersection domain(d.external) == set[uint16]{} // @ invariant acc(&d.neighborIAs, R15) // @ invariant d.neighborIAs != nil ==> acc(d.neighborIAs, R15) // @ invariant forall i uint16 :: { d.forwardingMetrics[i] } i in domain(d.forwardingMetrics) ==> @@ -1157,26 +1215,21 @@ func (d *DataPlane) initMetrics() { // @ invariant acc(d.Metrics.Mem(), _) // @ decreases len(d.external) - len(visitedSet) for id := range d.external /*@ with visitedSet @*/ { - // @ ghost if d.internalNextHops != nil { - // @ unfold acc(accAddr(d.internalNextHops), R20) - // @ } if _, notOwned := d.internalNextHops[id]; notOwned { - // @ ghost if d.internalNextHops != nil { - // @ fold acc(accAddr(d.internalNextHops), R20) - // @ } + // @ Unreachable() continue } - // @ ghost if d.internalNextHops != nil { - // @ fold acc(accAddr(d.internalNextHops), R20) - // @ } labels = interfaceToMetricLabels(id, ( /*@ unfolding acc(hideLocalIA(&d.localIA), R20) in @*/ d.localIA), d.neighborIAs) d.forwardingMetrics[id] = initForwardingMetrics(d.Metrics, labels) // @ liftForwardingMetricsNonInjectiveMem(d.forwardingMetrics[id], id) // @ assert acc(forwardingMetricsMem(d.forwardingMetrics[id], id), _) } // @ ghost if d.external != nil { fold acc(accBatchConn(d.external), R15) } + // @ ghost if d.internalNextHops != nil { fold acc(accAddr(d.internalNextHops), R15) } // @ fold accForwardingMetrics(d.forwardingMetrics) // @ unfold acc(hideLocalIA(&d.localIA), R15) + // @ fold d.Mem() + // @ reveal d.WellConfigured() } type processResult struct { @@ -1187,7 +1240,7 @@ type processResult struct { } // @ requires acc(&d.macFactory, _) && d.macFactory != nil -// @ requires acc(MutexInvariant(d), _) +// @ requires acc(d.Mem(), _) // @ ensures res.sInit() && res.sInitD() == d // @ decreases func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcessor) { @@ -1245,12 +1298,12 @@ func (p *scionPacketProcessor) reset() (err error) { // @ requires sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)) // @ requires acc(srcAddr.Mem(), _) // @ requires let d := p.sInitD() in -// @ acc(MutexInvariant(d), _) && +// @ acc(d.Mem(), _) && // @ d.WellConfigured() && // @ d.getValSvc() != nil && // @ d.getValForwardingMetrics() != nil // @ ensures p.sInit() -// @ ensures acc(MutexInvariant(p.sInitD()), _) +// @ ensures acc(p.sInitD().Mem(), _) // @ ensures p.sInitD() == old(p.sInitD()) // @ ensures p.sInitD().validResult(respr, addrAliasesPkt) // @ ensures acc(sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)), 1 - R15) @@ -1369,7 +1422,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ } // @ } // @ assert sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)) - // @ unfold acc(MutexInvariant(p.d), _) + // @ unfold acc(p.d.Mem(), _) v1, v2 /*@, aliasesPkt @*/ := p.processOHP() // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) // @ fold p.sInit() @@ -1406,7 +1459,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ requires acc(&p.d, R20) // @ requires acc(&p.ingressID, R20) -// @ requires acc(MutexInvariant(p.d), _) +// @ requires acc(p.d.Mem(), _) // @ requires p.bfdLayer.NonInitMem() // @ preserves sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures acc(&p.d, R20) @@ -1414,7 +1467,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ ensures p.bfdLayer.NonInitMem() // @ ensures err != nil ==> err.ErrorMem() func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (err error) { - // @ unfold acc(MutexInvariant(p.d), _) + // @ unfold acc(p.d.Mem(), _) // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } if len(p.d.bfdSessions) == 0 { // @ establishMemNoBFDSessionConfigured() @@ -1441,7 +1494,7 @@ func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (er // @ requires acc(&p.d, R20) // @ requires acc(&p.srcAddr, R20) && acc(p.srcAddr.Mem(), _) // @ requires p.bfdLayer.NonInitMem() -// @ requires acc(MutexInvariant(p.d), _) +// @ requires acc(p.d.Mem(), _) // @ requires sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures acc(&p.d, R20) // @ ensures acc(&p.srcAddr, R20) @@ -1449,7 +1502,7 @@ func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (er // @ ensures sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures res != nil ==> res.ErrorMem() func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { - // @ unfold acc(MutexInvariant(p.d), _) + // @ unfold acc(p.d.Mem(), _) // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } if len(p.d.bfdSessions) == 0 { // @ establishMemNoBFDSessionConfigured() @@ -1506,7 +1559,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires acc(&p.d, R5) && acc(MutexInvariant(p.d), _) && p.d.WellConfigured() +// @ requires acc(&p.d, R5) && acc(p.d.Mem(), _) && p.d.WellConfigured() // @ requires p.d.getValSvc() != nil // The ghost param ub here allows us to introduce a bound variable to p.rawPkt, // which slightly simplifies the spec @@ -1686,7 +1739,7 @@ func (p *scionPacketProcessor) packSCMP( return processResult{OutPkt: rawSCMP}, err } -// @ requires acc(&p.d, R50) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R5) // @ requires acc(&p.path, R20) // @ requires p.path === p.scionLayer.GetPath(ub) @@ -1735,7 +1788,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) -// @ preserves acc(&p.d, R50) && acc(MutexInvariant(p.d), _) +// @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures p.d.validResult(respr, false) // @ ensures respr.OutPkt != nil ==> // @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) @@ -1772,7 +1825,7 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ preserves acc(&p.ingressID, R20) -// @ preserves acc(&p.d, R50) && acc(MutexInvariant(p.d), _) +// @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures p.d.validResult(respr, false) // @ ensures respr.OutPkt != nil ==> reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() @@ -1802,7 +1855,7 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr return processResult{}, nil } -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ubScionL), R19) // @ requires acc(&p.path, R20) // @ requires p.path === p.scionLayer.GetPath(ubScionL) @@ -1892,7 +1945,7 @@ func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { // @ requires let ubPath := p.scionLayer.UBPath(ub) in // @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrINF(ubPath) <= p.path.GetNumINF(ubPath) -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ requires acc(&p.srcAddr, R20) && acc(p.srcAddr.Mem(), _) // @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R4) // @ ensures acc(&p.path, R15) @@ -1940,7 +1993,7 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ return processResult{}, nil } -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ preserves acc(&p.ingressID, R20) // @ preserves acc(&p.segmentChange, R20) // @ preserves acc(&p.infoField, R20) @@ -2104,7 +2157,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/ // @ preserves acc(&p.macBuffers.scionInput, R20) // @ preserves sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) -// @ preserves acc(&p.d, R50) && acc(MutexInvariant(p.d), _) +// @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures p.d.validResult(respr, false) // @ ensures respr.OutPkt != nil ==> // @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) @@ -2141,7 +2194,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e } // @ requires acc(&p.d, R15) -// @ requires acc(MutexInvariant(p.d), _) +// @ requires acc(p.d.Mem(), _) // @ requires p.d.getValSvc() != nil // @ requires acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) // @ preserves acc(p.scionLayer.Mem(ubScionL), R10) @@ -2308,7 +2361,7 @@ func (p *scionPacketProcessor) egressInterface() uint16 { return p.hopField.ConsIngress } -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ preserves acc(&p.ingressID, R20) @@ -2351,7 +2404,7 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e // @ requires acc(&p.path, R20) // @ requires acc(p.scionLayer.Mem(ub), R10) // @ requires p.path === p.scionLayer.GetPath(ub) -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ preserves acc(&p.lastLayer, R19) // @ preserves p.lastLayer != nil @@ -2426,7 +2479,7 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ requires acc(&p.path, R20) // @ requires acc(p.scionLayer.Mem(ub), R14) // @ requires p.path === p.scionLayer.GetPath(ub) -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ preserves acc(&p.lastLayer, R19) // @ preserves p.lastLayer != nil @@ -2504,7 +2557,7 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) { // @ requires acc(&p.lastLayer, R20) // @ requires p.lastLayer != nil && acc(p.lastLayer.Mem(ubLastLayer), R15) -// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) // @ preserves sl.AbsSlice_Bytes(ubLastLayer, 0, len(ubLastLayer)) // @ ensures acc(&p.lastLayer, R20) // @ ensures acc(p.lastLayer.Mem(ubLastLayer), R15) @@ -2567,7 +2620,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( } // @ preserves acc(p.scionLayer.Mem(ubScionL), R20) -// @ preserves acc(&p.d, R50) && acc(MutexInvariant(p.d), _) +// @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) // @ ensures p.d.validResult(respr, false) // @ ensures respr.OutPkt != nil ==> reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr == nil ==> int(p.scionLayer.GetPayloadLen(ubScionL)) == len(p.scionLayer.GetPayload(ubScionL)) @@ -2591,7 +2644,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires acc(&p.d, R5) && acc(MutexInvariant(p.d), _) && p.d.WellConfigured() +// @ requires acc(&p.d, R5) && acc(p.d.Mem(), _) && p.d.WellConfigured() // @ requires p.d.getValSvc() != nil // The ghost param ub here allows us to introduce a bound variable to p.rawPkt, // which slightly simplifies the spec @@ -2759,7 +2812,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ requires acc(&p.rawPkt, R15) // @ requires p.scionLayer.Mem(p.rawPkt) // @ requires acc(&p.ingressID, R15) -// @ requires acc(&p.d, R15) && acc(MutexInvariant(p.d), _) && p.d.WellConfigured() +// @ requires acc(&p.d, R15) && acc(p.d.Mem(), _) && p.d.WellConfigured() // @ requires p.d.getValSvc() != nil // @ requires sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)) // @ preserves acc(&p.mac, R10) @@ -2964,7 +3017,7 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error / return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil /*@ , addrAliases @*/ } -// @ requires acc(MutexInvariant(d), _) +// @ requires acc(d.Mem(), _) // @ requires d.getValSvc() != nil // @ requires acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) // @ preserves acc(s.Mem(ub), R14) @@ -3180,7 +3233,7 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { return err } -// @ requires acc(&p.d, _) && acc(MutexInvariant(p.d), _) +// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index d1a7deeb3..656cef538 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -34,61 +34,71 @@ import ( sl "github.com/scionproto/scion/verification/utils/slices" ) +ghost const MutexPerm perm = 1/4 +ghost const OutMutexPerm perm = 3/4 +ghost const runningPerm perm = 1/2 + pred MutexInvariant(d *DataPlane) { + acc(&d.running, runningPerm) && + (!d.running ==> acc(d.Mem(), MutexPerm)) +} + +pred (d *DataPlane) Mem() { // access to the field 'mtx' ommited - acc(&d.external, 1/2) && - acc(&d.linkTypes, 1/2) && - acc(&d.neighborIAs, 1/2) && - acc(&d.internal, 1/2) && - acc(&d.internalIP, 1/2) && - acc(&d.internalNextHops, 1/2) && - acc(&d.svc, 1/2) && - acc(&d.macFactory, 1/2) && - acc(&d.bfdSessions, 1/2) && - acc(&d.localIA, 1/2) && - acc(&d.running, 1/2) && - acc(&d.Metrics, 1/2) && - acc(&d.forwardingMetrics, 1/2) && - acc(&d.key, 1/2) && - (d.external != nil ==> accBatchConn(d.external)) && - (d.linkTypes != nil ==> acc(d.linkTypes, 1/2)) && - (d.neighborIAs != nil ==> acc(d.neighborIAs, 1/2)) && - (d.internal != nil ==> d.internal.Mem()) && - (d.internalIP != nil ==> d.internalIP.Mem()) && - (d.internalNextHops != nil ==> accAddr(d.internalNextHops)) && - (d.svc != nil ==> d.svc.Mem()) && + acc(&d.external) && + acc(&d.linkTypes) && + acc(&d.neighborIAs) && + acc(&d.internal) && + acc(&d.internalIP) && + acc(&d.internalNextHops) && + acc(&d.svc) && + acc(&d.macFactory) && + acc(&d.bfdSessions) && + acc(&d.localIA) && + acc(&d.running, 1/2) && + acc(&d.Metrics) && + acc(&d.forwardingMetrics) && + acc(&d.key) && + (d.external != nil ==> accBatchConn(d.external)) && + (d.linkTypes != nil ==> acc(d.linkTypes)) && + (d.neighborIAs != nil ==> acc(d.neighborIAs)) && + (d.internal != nil ==> d.internal.Mem()) && + (d.internalIP != nil ==> d.internalIP.Mem()) && + (d.internalNextHops != nil ==> accAddr(d.internalNextHops)) && + (d.svc != nil ==> d.svc.Mem()) && (d.macFactory != nil ==> ( - acc(d.key, 1/2) && + acc(d.key) && acc(sl.AbsSlice_Bytes(*d.key, 0, len(*d.key)), _) && scrypto.ValidKeyForHash(*d.key) && - d.macFactory implements MacFactorySpec{d.key})) && - (d.bfdSessions != nil ==> accBfdSession(d.bfdSessions)) && - (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && + d.macFactory implements MacFactorySpec{d.key})) && + (d.bfdSessions != nil ==> accBfdSession(d.bfdSessions)) && + (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && // The following permissions are enough to call all methods needed in fields // of forwardingMetrics (d.forwardingMetrics != nil ==> accForwardingMetrics(d.forwardingMetrics)) } pred accAddr(addrs map[uint16]*net.UDPAddr) { - acc(addrs, 1/2) && + acc(addrs) && forall a *net.UDPAddr :: { a in range(addrs) } a in range(addrs) ==> acc(a.Mem(), _) } pred accBatchConn(batchConns map[uint16]BatchConn) { - acc(batchConns, 1/2) && + acc(batchConns) && forall b BatchConn :: { b in range(batchConns) }{ b.Mem() } b in range(batchConns) ==> b!= nil && acc(b.Mem(), _) } pred accBfdSession(bfdSessions map[uint16]bfdSession) { - acc(bfdSessions, 1/2) && + acc(bfdSessions) && (forall bfd bfdSession :: { bfd in range(bfdSessions) }{ bfd.Mem() } bfd in range(bfdSessions) ==> (bfd != nil && acc(bfd.Mem(), _))) } pred accForwardingMetrics(metrics map[uint16]forwardingMetrics) { - acc(metrics, 1/2) && - forall id uint16 :: { metrics[id] } id in domain(metrics) ==> acc(forwardingMetricsMem(metrics[id], id), _) + acc(metrics) && + forall id uint16 :: { metrics[id] } id in domain(metrics) ==> + acc(forwardingMetricsMem(metrics[id], id), _) } pred forwardingMetricsMem(v forwardingMetrics, ignoredForInjectivity uint16) { @@ -167,125 +177,48 @@ ensures forall i int :: {res[i]} 0 <= i && i < len(res) ==> res[i] == offsetPai decreases func newOffsetPair(n int) (res seq[offsetPair]) -ghost -requires acc(MutexInvariant!(), _) -ensures acc(MutexInvariant(d), _) -decreases -func (d *DataPlane) SimplifyPermInv() { - unfold acc(MutexInvariant!(), _) - // This big assertion seems to be necessary for the fold to succeed :( - assert acc(&d.external, _) && - acc(&d.linkTypes, _) && - acc(&d.neighborIAs, _) && - acc(&d.internal, _) && - acc(&d.internalIP, _) && - acc(&d.internalNextHops, _) && - acc(&d.svc, _) && - acc(&d.macFactory, _) && - acc(&d.bfdSessions, _) && - acc(&d.localIA, _) && - acc(&d.running, _) && - acc(&d.Metrics, _) && - acc(&d.forwardingMetrics, _) && - acc(&d.key, _) && - (d.external != nil ==> acc(accBatchConn(d.external), _)) && - (d.linkTypes != nil ==> acc(d.linkTypes, _)) && - (d.neighborIAs != nil ==> acc(d.neighborIAs, _)) && - (d.internal != nil ==> acc(d.internal.Mem(), _)) && - (d.internalIP != nil ==> acc(d.internalIP.Mem(), _)) && - (d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), _)) && - (d.svc != nil ==> acc(d.svc.Mem(), _)) && - (d.macFactory != nil ==> ( - acc(d.key, _) && - acc(sl.AbsSlice_Bytes(*d.key, 0, len(*d.key)), _) && - scrypto.ValidKeyForHash(*d.key) && - d.macFactory implements MacFactorySpec{d.key})) && - (d.bfdSessions != nil ==> acc(accBfdSession(d.bfdSessions), _)) && - (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && - (d.forwardingMetrics != nil ==> acc(accForwardingMetrics(d.forwardingMetrics), _)) - fold acc(MutexInvariant(d), _) -} - -ghost -requires acc(MutexInvariant(d), _) -ensures acc(MutexInvariant!(), _) -decreases -func (d *DataPlane) ElaboratePermInv() { - unfold acc(MutexInvariant(d), _) - // This big assertion seems to be necessary for the fold to succeed :( - assert acc(&d.external, _) && - acc(&d.linkTypes, _) && - acc(&d.neighborIAs, _) && - acc(&d.internal, _) && - acc(&d.internalIP, _) && - acc(&d.internalNextHops, _) && - acc(&d.svc, _) && - acc(&d.macFactory, _) && - acc(&d.bfdSessions, _) && - acc(&d.localIA, _) && - acc(&d.running, _) && - acc(&d.Metrics, _) && - acc(&d.forwardingMetrics, _) && - acc(&d.key, _) && - (d.external != nil ==> acc(accBatchConn(d.external), _)) && - (d.linkTypes != nil ==> acc(d.linkTypes, _)) && - (d.neighborIAs != nil ==> acc(d.neighborIAs, _)) && - (d.internal != nil ==> acc(d.internal.Mem(), _)) && - (d.internalIP != nil ==> acc(d.internalIP.Mem(), _)) && - (d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), _)) && - (d.svc != nil ==> acc(d.svc.Mem(), _)) && - (d.macFactory != nil ==> ( - acc(d.key, _) && - acc(sl.AbsSlice_Bytes(*d.key, 0, len(*d.key)), _) && - scrypto.ValidKeyForHash(*d.key) && - d.macFactory implements MacFactorySpec{d.key})) && - (d.bfdSessions != nil ==> acc(accBfdSession(d.bfdSessions), _)) && - (d.Metrics != nil ==> acc(d.Metrics.Mem(), _)) && - (d.forwardingMetrics != nil ==> acc(accForwardingMetrics(d.forwardingMetrics), _)) - fold acc(MutexInvariant!(), _) -} - /**** Acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/ ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) ensures acc(&d.internalNextHops, _) ensures d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), _) decreases func (d *DataPlane) getInternalNextHops() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) ensures acc(&d.forwardingMetrics, _) -ensures d.forwardingMetrics != nil ==> acc(accForwardingMetrics(d.forwardingMetrics), _) +ensures d.forwardingMetrics != nil ==> + acc(accForwardingMetrics(d.forwardingMetrics), _) decreases func (d *DataPlane) getForwardingMetrics() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) // The termination of this method is assumed. The reason is that the termination // proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) // followed by a fold of the same invariant with the same permission amount. -// As shown in methods SimplifyPermInv and ElaboratePermInv, Gobra requires intermediate -// assertions to make this verify, which is not easy to add here. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. decreases _ pure func (d *DataPlane) getValForwardingMetrics() map[uint16]forwardingMetrics { - return unfolding acc(MutexInvariant(d), _) in d.forwardingMetrics + return unfolding acc(d.Mem(), _) in d.forwardingMetrics } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) // The termination of this method is assumed. The reason is that the termination // proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) // followed by a fold of the same invariant with the same permission amount. -// As shown in methods SimplifyPermInv and ElaboratePermInv, Gobra requires intermediate -// assertions to make this verify, which is not easy to add here. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. decreases _ pure func (d *DataPlane) getDomForwardingMetrics() set[uint16] { - return unfolding acc(MutexInvariant(d), _) in + return unfolding acc(d.Mem(), _) in d.forwardingMetrics == nil ? set[uint16]{} : (unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in @@ -293,15 +226,31 @@ pure func (d *DataPlane) getDomForwardingMetrics() set[uint16] { } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) // The termination of this method is assumed. The reason is that the termination // proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) // followed by a fold of the same invariant with the same permission amount. -// As shown in methods SimplifyPermInv and ElaboratePermInv, Gobra requires intermediate -// assertions to make this verify, which is not easy to add here. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +pure func (d *DataPlane) GetDomInternalNextHops() set[uint16] { + return unfolding acc(d.Mem(), _) in + d.internalNextHops == nil ? + set[uint16]{} : + (unfolding acc(accAddr(d.internalNextHops), _) in + domain(d.internalNextHops)) +} + +ghost +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. decreases _ pure func (d *DataPlane) getDomExternal() set[uint16] { - return unfolding acc(MutexInvariant(d), _) in + return unfolding acc(d.Mem(), _) in d.external == nil ? set[uint16]{} : (unfolding acc(accBatchConn(d.external), _) in @@ -309,21 +258,31 @@ pure func (d *DataPlane) getDomExternal() set[uint16] { } ghost -requires acc(MutexInvariant(d), _) +opaque +requires acc(d.Mem(), _) decreases pure func (d *DataPlane) WellConfigured() bool { - return d.getDomExternal() == d.getDomForwardingMetrics() + // TODO: do not use subset, use union {0} + return d.getDomExternal() subset d.getDomForwardingMetrics() +} + +ghost +opaque +requires acc(d.Mem(), _) +decreases +pure func (d *DataPlane) PreWellConfigured() bool { + return d.getDomExternal() intersection d.GetDomInternalNextHops() == set[uint16]{} } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) requires id in d.getDomForwardingMetrics() ensures acc(&d.forwardingMetrics, _) ensures acc(d.forwardingMetrics, _) ensures acc(forwardingMetricsMem(d.forwardingMetrics[id], id), _) decreases func (d *DataPlane) getForwardingMetricsMem(id uint16) { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) assert id in d.getDomForwardingMetrics() assert d.getDomForwardingMetrics() == (d.forwardingMetrics == nil ? set[uint16]{} : @@ -338,82 +297,100 @@ func (d *DataPlane) getForwardingMetricsMem(id uint16) { } ghost -requires acc(MutexInvariant(d), _) -ensures acc(&d.external, _) && (d.external != nil ==> acc(accBatchConn(d.external), _)) +requires acc(d.Mem(), _) +ensures acc(&d.external, _) +ensures d.external != nil ==> acc(accBatchConn(d.external), _) decreases func (d *DataPlane) getExternalMem() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) -ensures acc(&d.linkTypes, _) && (d.linkTypes != nil ==> acc(d.linkTypes, _)) +requires acc(d.Mem(), _) +ensures acc(&d.linkTypes, _) +ensures d.linkTypes != nil ==> acc(d.linkTypes, _) decreases func (d *DataPlane) getLinkTypesMem() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) ensures acc(&d.localIA, _) decreases func (d *DataPlane) getLocalIA() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) -ensures acc(&d.neighborIAs, _) && (d.neighborIAs != nil ==> acc(d.neighborIAs, _)) +requires acc(d.Mem(), _) +ensures acc(&d.neighborIAs, _) +ensures d.neighborIAs != nil ==> acc(d.neighborIAs, _) decreases func (d *DataPlane) getNeighborIAs() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) && d.getValSvc() != nil -ensures acc(&d.svc, _) && d.svc != nil && acc(d.svc.Mem(), _) +requires acc(d.Mem(), _) && d.getValSvc() != nil +ensures acc(&d.svc, _) +ensures d.svc != nil && acc(d.svc.Mem(), _) decreases func (d *DataPlane) getSvcMem() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) // The termination of this method is assumed. The reason is that the termination // proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) // followed by a fold of the same invariant with the same permission amount. -// As shown in methods SimplifyPermInv and ElaboratePermInv, Gobra requires intermediate -// assertions to make this verify, which is not easy to add here. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. decreases _ pure func (d *DataPlane) getValSvc() *services { - return unfolding acc(MutexInvariant(d), _) in d.svc + return unfolding acc(d.Mem(), _) in d.svc +} + +ghost +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +pure func (d *DataPlane) SvcsAreSet() bool { + return unfolding acc(d.Mem(), _) in d.svc != nil } ghost -requires acc(MutexInvariant(d), _) -ensures acc(&d.bfdSessions, _) && (d.bfdSessions != nil ==> acc(accBfdSession(d.bfdSessions), _)) +requires acc(d.Mem(), _) +ensures acc(&d.bfdSessions, _) +ensures d.bfdSessions != nil ==> acc(accBfdSession(d.bfdSessions), _) decreases func (d *DataPlane) getBfdSessionsMem() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) -ensures acc(&d.internal, _) && (d.internal != nil ==> acc(d.internal.Mem(), _)) +requires acc(d.Mem(), _) +ensures acc(&d.internal, _) +ensures d.internal != nil ==> acc(d.internal.Mem(), _) decreases func (d *DataPlane) getInternal() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) ensures acc(&d.macFactory, _) decreases func (d *DataPlane) getMacFactoryMem() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) } ghost -requires acc(MutexInvariant(d), _) +requires acc(d.Mem(), _) requires acc(&d.macFactory, _) && d.macFactory != nil ensures acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _) ensures acc(sl.AbsSlice_Bytes(*d.key, 0, len(*d.key)), _) @@ -421,7 +398,117 @@ ensures scrypto.ValidKeyForHash(*d.key) ensures d.macFactory implements MacFactorySpec{d.key} decreases func (d *DataPlane) getNewPacketProcessorFootprint() { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) +} + +type Unit struct{} + +ghost +pure +requires acc(d.Mem(), _) +decreases _ +func (d *DataPlane) IsRunning() bool { + return unfolding acc(d.Mem(), _) in d.running +} + +ghost +// opaque +pure +requires acc(d.Mem(), _) +requires acc(&d.running, _) +ensures d.IsRunning() == d.running +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) isRunningEq() Unit { + return unfolding acc(d.Mem(), _) in Unit{} +} + +ghost +pure +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) InternalConnIsSet() bool { + return unfolding acc(d.Mem(), _) in d.internal != nil +} + +ghost +pure +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) MetricsAreSet() bool { + return unfolding acc(d.Mem(), _) in d.Metrics != nil +} + +ghost +// opaque +pure +requires acc(d.Mem(), _) +requires acc(&d.internal, _) +ensures d.InternalConnIsSet() == (d.internal != nil) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) internalIsSetEq() Unit { + return unfolding acc(d.Mem(), _) in Unit{} +} + +ghost +pure +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) KeyIsSet() bool { + return unfolding acc(d.Mem(), _) in d.macFactory != nil +} + +ghost +// opaque +pure +requires acc(d.Mem(), _) +requires acc(&d.macFactory, _) +ensures d.KeyIsSet() == (d.macFactory != nil) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) keyIsSetEq() Unit { + return unfolding acc(d.Mem(), _) in Unit{} +} + +ghost +pure +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +func (d *DataPlane) LocalIA() addr.IA { + return unfolding acc(d.Mem(), _) in d.localIA } /**** End of acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/ @@ -440,7 +527,6 @@ func getBfdSessionMem(v bfdSession, bfdSessions map[uint16]bfdSession) { } /** definitions used internally for the proof of Run **/ -// TODO: maybe drop and use the invariant of Messages instead now that we have IsActive? pred writeMsgInv(writeMsgs underlayconn.Messages) { len(writeMsgs) == 1 && @@ -557,8 +643,6 @@ pure func (s* scionPacketProcessor) sInitSegmentChange() (res bool) { /** end spec for newPacketProcessor **/ -/** **/ - ghost requires hasScionLayer ==> scionLayer.Mem(ubScionLayer) requires hasHbhLayer ==> hbhLayer.Mem(ubHbhLayer) @@ -589,9 +673,8 @@ func ResetDecodingLayers( } } -/** **/ pred (d *DataPlane) validResult(result processResult, addrAliasesPkt bool) { - acc(MutexInvariant(d), _) && + acc(d.Mem(), _) && // EgressID (result.EgressID != 0 ==> result.EgressID in d.getDomForwardingMetrics()) && // OutConn @@ -603,45 +686,63 @@ pred (d *DataPlane) validResult(result processResult, addrAliasesPkt bool) { } ghost -requires acc(MutexInvariant(d), _) && d.WellConfigured() +requires acc(d.Mem(), _) && d.WellConfigured() requires id in d.getDomExternal() -ensures acc(MutexInvariant(d), _) +ensures acc(d.Mem(), _) ensures id in d.getDomForwardingMetrics() decreases func (d *DataPlane) InDomainExternalInForwardingMetrics(id uint16) { - + reveal d.WellConfigured() } ghost -requires acc(MutexInvariant(d), _) && d.WellConfigured() +requires acc(d.Mem(), _) && d.WellConfigured() requires acc(&d.external, _) && acc(d.external, _) requires id in domain(d.external) -ensures acc(MutexInvariant(d), _) +ensures acc(d.Mem(), _) ensures id in d.getDomForwardingMetrics() decreases func (d *DataPlane) InDomainExternalInForwardingMetrics2(id uint16) { - unfold acc(MutexInvariant(d), _) + unfold acc(d.Mem(), _) + reveal d.WellConfigured() unfold acc(accBatchConn(d.external), _) } -// This lemma has the same exact spec as before, except for a fixed permission to d. -// external. Although simple, this requires some work to prove to avoid incompletnesses -// with MCE. ghost -requires acc(MutexInvariant(d), _) && d.WellConfigured() +requires acc(d.Mem(), _) && d.WellConfigured() requires acc(&d.external, _) && acc(d.external, R55) requires id in domain(d.external) -ensures acc(MutexInvariant(d), _) +ensures acc(d.Mem(), _) ensures acc(&d.external, _) && acc(d.external, R55) ensures id in d.getDomForwardingMetrics() decreases -func (d *DataPlane) InDomainExternalInForwardingMetrics3(id uint16) +func (d *DataPlane) InDomainExternalInForwardingMetrics3(id uint16) { + reveal d.WellConfigured() + assert unfolding acc(d.Mem(), _) in + (unfolding acc(accBatchConn(d.external), _) in true) +} ghost requires acc(&d.forwardingMetrics, _) requires acc(accForwardingMetrics(d.forwardingMetrics), _) decreases -pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] { +pure func (d *DataPlane) domainForwardingMetrics() set[uint16] { return unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in domain(d.forwardingMetrics) +} + +ghost +requires acc(d.Mem(), _) +// The termination of this method is assumed. The reason is that the termination +// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _) +// followed by a fold of the same invariant with the same permission amount. +// Gobra requires intermediate assertions to make this verify, +// which is not possible to add here. +decreases _ +pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] { + return unfolding acc(d.Mem(), _) in + d.forwardingMetrics != nil ? + unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in + domain(d.forwardingMetrics) : + set[uint16]{} } \ No newline at end of file diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index d34ff4569..b905bd4c6 100644 --- a/router/dataplane_spec_test.gobra +++ b/router/dataplane_spec_test.gobra @@ -21,10 +21,12 @@ import ( "github.com/scionproto/scion/pkg/addr" "github.com/scionproto/scion/pkg/slayers" + "github.com/scionproto/scion/private/topology" ) func foldMem_test() { d@ := DataPlane{} + fold d.Mem() fold MutexInvariant!<&d!>() // testing initialization with the operations from dataplane d.mtx.SetInv(MutexInvariant!<&d!>) @@ -39,3 +41,35 @@ func foldScionPacketProcessorInitMem_test() { fold d.scionLayer.NonInitMem() fold d.initMem() } + +ensures 0 < runningPerm +func runningPermIsPositive() {} + +ensures MutexInvariant(d) && acc(d.Mem(), OutMutexPerm) +decreases +func foldDataPlaneMem() (d *DataPlane) { + d = &DataPlane{} + d.external = make(map[uint16]BatchConn) + fold accBatchConn(d.external) + d.linkTypes = make(map[uint16]topology.LinkType) + d.neighborIAs = make(map[uint16]addr.IA) + d.internalNextHops = make(map[uint16]*net.UDPAddr) + fold accAddr(d.internalNextHops) + d.svc = newServices() + d.bfdSessions = make(map[uint16]bfdSession) + fold accBfdSession(d.bfdSessions) + d.forwardingMetrics = make(map[uint16]forwardingMetrics) + fold accForwardingMetrics(d.forwardingMetrics) + fold d.Mem() + fold MutexInvariant(d) +} + +requires MutexInvariant(d) && acc(d.Mem(), OutMutexPerm) +requires !d.IsRunning() +ensures acc(&d.running) +decreases +func canModifyRunning(d *DataPlane) { + unfold MutexInvariant(d) + d.isRunningEq() + unfold d.Mem() +} \ No newline at end of file diff --git a/verification/dependencies/context/context.gobra b/verification/dependencies/context/context.gobra index e2c3ec865..654f9d187 100644 --- a/verification/dependencies/context/context.gobra +++ b/verification/dependencies/context/context.gobra @@ -32,12 +32,11 @@ type Context interface { decreases Deadline() (deadline time.Time, ok bool) - preserves acc(Mem(), R20) - ensures isClosed ==> c.Closed() - ensures (!isClosed && c != nil) ==> - acc(c.RecvChannel(), _) + preserves acc(Mem(), _) + ensures acc(c.RecvChannel(), _) + ensures c.RecvGivenPerm() == PredTrue! decreases - Done() (c <-chan struct{}, ghost isClosed bool) + Done() (c <-chan struct{}) preserves acc(Mem(), R20) ensures isClosed ==> (e != nil && e.ErrorMem())