From 32c592e25c6ff08d9868de71e4fca05a3de23375 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 26 Jan 2024 15:04:06 +0100 Subject: [PATCH] Verify core of `Run` method (#240) * start * backup change to interface * backup change to interface * backup * backup * backup of Run * backup of Run * fix error in auxiliary package * problematic files * deal with incompletnesses by abstracting properties in predicates * backup * drop commented assertions; blocked by Gobra incompletness * Fix specification error in the spec of processPkt * continue Run * continue Run * Fix a few errors * add fuller spec to processPkt * before modying Message.Mem() * backup * backup * backup * backup * backup * backup * backup * backup * drop unncessary invariant, performance improvements * perform obvious simplification in spec; continue verifying the main loop (almost done) * improves the postconditions of processPkt further * weaken predicate that is stronger than necessary * Fix ugly typo in an invariant * Backup * backup * fix contract * fix id erros * backup * Backup * undo unnecessary changes * backup * fix errors * Update router/dataplane_spec.gobra * backup * backup * backup * backup * backup * change the order of invariants to avoid incompletness with mce * drop dreaded comment * backup * fix names * fix a few verification errors * fix another verification error * kill problematic branch * progress towards proof * backup * fix verification error * backup * update socket.gobra spec * maybe problematic PR * start refactoring to decrease the amount of info provided to the smt solver * backup * fix type error * major clean-up * backup * fix a few errors due to the new encoding of socket * Backup * backup * backup * continue simplifying codebase * backup MemWithoutHalf * Drop MemWithoutHalf * Remove one assume false * settled on a spec for processPkt? * cleanup * further advance a goal * backup * backup, might not terminate * add necessary lemma calls * backup * remove unnecessary pre's * backup; things are still failing * backup * backup * backup * backup * backup * backup * fix error with OneHop * probably done with processOHP * fix bug * start adapting process * advances in processSCION * backup * continue advancing proof of process * backup * backup * backup * fix proof * rm file commited by mistake * fix tiny error --- pkg/slayers/scion.go | 77 +- private/underlay/conn/conn.go | 26 +- router/dataplane.go | 773 +++++++++++++----- router/dataplane_spec.gobra | 356 +++++++- .../x/net/internal/socket/socket.gobra | 112 +-- .../x/net/internal/socket/socket.gobra.old | 186 +++++ .../x/net/internal/socket/socket_test.gobra | 4 +- .../golang.org/x/net/ipv4/endpoint.gobra | 8 +- .../golang.org/x/net/ipv6/endpoint.gobra | 8 +- verification/dependencies/net/udpsock.gobra | 2 +- .../utils/definitions/definitions.gobra | 5 + 11 files changed, 1218 insertions(+), 339 deletions(-) create mode 100644 verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go index 95bb43f2c..0e44da293 100644 --- a/pkg/slayers/scion.go +++ b/pkg/slayers/scion.go @@ -575,18 +575,18 @@ func scionNextLayerTypeL4(t L4ProtocolType) gopacket.LayerType { // from the underlaying layer data. Changing the net.Addr object might lead to inconsistent layer // information and thus should be treated read-only. Instead, SetDstAddr should be used to update // the destination address. -// @ requires acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20) -// @ requires s.DstAddrType == T4Svc ==> len(s.RawDstAddr) >= addr.HostLenSVC -// @ requires acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) -// @ ensures acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20) -// @ ensures acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) -// @ ensures err == nil ==> (s.DstAddrType == T16Ip ==> typeOf(res) == *net.IPAddr) -// @ ensures err == nil ==> (s.DstAddrType == T16Ip ==> (acc(res.(*net.IPAddr)) && s.RawDstAddr === []byte(res.(*net.IPAddr).IP))) -// @ ensures err == nil ==> (s.DstAddrType == T4Ip ==> typeOf(res) == *net.IPAddr) -// @ ensures err == nil ==> (s.DstAddrType == T4Ip ==> (acc(res.(*net.IPAddr)) && s.RawDstAddr === []byte(res.(*net.IPAddr).IP))) -// @ ensures err == nil ==> (s.DstAddrType == T4Svc ==> typeOf(res) == addr.HostSVC) -// @ ensures err == nil == (s.DstAddrType == T4Ip || s.DstAddrType == T4Svc || s.DstAddrType == T16Ip) -// @ ensures err != nil ==> err.ErrorMem() +// @ requires acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20) +// @ requires s.DstAddrType == T4Svc ==> len(s.RawDstAddr) >= addr.HostLenSVC +// @ requires acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R15) +// @ ensures acc(&s.DstAddrType, R20) && acc(&s.RawDstAddr, R20) +// @ ensures err == nil ==> acc(res.Mem(), R15) +// @ ensures err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC +// @ ensures err == nil ==> +// @ let rawDstAddr := s.RawDstAddr in +// @ (acc(res.Mem(), R15) --* acc(sl.AbsSlice_Bytes(rawDstAddr, 0, len(rawDstAddr)), R15)) +// @ ensures err != nil ==> +// @ acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R15) +// @ ensures err != nil ==> err.ErrorMem() // @ decreases func (s *SCION) DstAddr() (res net.Addr, err error) { return parseAddr(s.DstAddrType, s.RawDstAddr) @@ -598,15 +598,15 @@ func (s *SCION) DstAddr() (res net.Addr, err error) { // address. // @ requires acc(&s.SrcAddrType, R20) && acc(&s.RawSrcAddr, R20) // @ requires s.SrcAddrType == T4Svc ==> len(s.RawSrcAddr) >= addr.HostLenSVC -// @ requires acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) +// @ requires acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R15) // @ ensures acc(&s.SrcAddrType, R20) && acc(&s.RawSrcAddr, R20) -// @ ensures acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20) -// @ ensures err == nil ==> (s.SrcAddrType == T16Ip ==> typeOf(res) == *net.IPAddr) -// @ ensures err == nil ==> (s.SrcAddrType == T16Ip ==> (acc(res.(*net.IPAddr)) && s.RawSrcAddr === []byte(res.(*net.IPAddr).IP))) -// @ ensures err == nil ==> (s.SrcAddrType == T4Ip ==> typeOf(res) == *net.IPAddr) -// @ ensures err == nil ==> (s.SrcAddrType == T4Ip ==> (acc(res.(*net.IPAddr)) && s.RawSrcAddr === []byte(res.(*net.IPAddr).IP))) -// @ ensures err == nil ==> (s.SrcAddrType == T4Svc ==> typeOf(res) == addr.HostSVC) -// @ ensures err == nil == (s.SrcAddrType == T4Ip || s.SrcAddrType == T4Svc || s.SrcAddrType == T16Ip) +// @ ensures err == nil ==> acc(res.Mem(), R15) +// @ ensures err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC +// @ ensures err == nil ==> +// @ let rawSrcAddr := s.RawSrcAddr in +// @ (acc(res.Mem(), R15) --* acc(sl.AbsSlice_Bytes(rawSrcAddr, 0, len(rawSrcAddr)), R15)) +// @ ensures err != nil ==> +// @ acc(sl.AbsSlice_Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R15) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (s *SCION) SrcAddr() (res net.Addr, err error) { @@ -687,28 +687,43 @@ func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error return err } -// @ requires addrType == T4Svc ==> len(raw) >= addr.HostLenSVC -// @ preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R20) -// @ ensures err == nil ==> (addrType == T16Ip ==> typeOf(res) == *net.IPAddr) -// @ ensures err == nil ==> (addrType == T16Ip ==> (acc(res.(*net.IPAddr)) && raw === []byte(res.(*net.IPAddr).IP))) -// @ ensures err == nil ==> (addrType == T4Ip ==> typeOf(res) == *net.IPAddr) -// @ ensures err == nil ==> (addrType == T4Ip ==> (acc(res.(*net.IPAddr)) && raw === []byte(res.(*net.IPAddr).IP))) -// @ ensures err == nil ==> (addrType == T4Svc ==> typeOf(res) == addr.HostSVC) -// @ ensures err == nil == (addrType == T4Ip || addrType == T4Svc || addrType == T16Ip) -// @ ensures err != nil ==> err.ErrorMem() +// @ requires addrType == T4Svc ==> len(raw) >= addr.HostLenSVC +// @ requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) +// @ ensures err == nil ==> acc(res.Mem(), R15) +// @ ensures err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC +// @ ensures err == nil ==> +// @ (acc(res.Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) +// @ ensures err != nil ==> acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) +// @ ensures err != nil ==> err.ErrorMem() // @ decreases func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) { switch addrType { case T4Ip: verScionTmp := &net.IPAddr{IP: net.IP(raw)} + // @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) + // @ fold acc(verScionTmp.Mem(), R15) + // @ package (acc((net.Addr)(verScionTmp).Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) { + // @ assert acc(&verScionTmp.IP, R50) && verScionTmp.IP === raw + // @ unfold acc(verScionTmp.Mem(), R15) + // @ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) + // @ } return verScionTmp, nil case T4Svc: - // @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R20) + // @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) verScionTmp := addr.HostSVC(binary.BigEndian.Uint16(raw[:addr.HostLenSVC])) - // @ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R20) + // @ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) + // @ fold acc(verScionTmp.Mem(), R15) + // @ package (acc((net.Addr)(verScionTmp).Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) { } return verScionTmp, nil case T16Ip: verScionTmp := &net.IPAddr{IP: net.IP(raw)} + // @ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) + // @ fold acc(verScionTmp.Mem(), R15) + // @ package (acc((net.Addr)(verScionTmp).Mem(), R15) --* acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15)) { + // @ assert acc(&verScionTmp.IP, R50) && verScionTmp.IP === raw + // @ unfold acc(verScionTmp.Mem(), R15) + // @ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R15) + // @ } return verScionTmp, nil } return nil, serrors.New("unsupported address type/length combination", diff --git a/private/underlay/conn/conn.go b/private/underlay/conn/conn.go index dcdaaf045..06d706d2a 100644 --- a/private/underlay/conn/conn.go +++ b/private/underlay/conn/conn.go @@ -51,7 +51,7 @@ type Conn interface { //@ ensures err != nil ==> err.ErrorMem() ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) //@ requires acc(Mem(), _) - //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem(1) + //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem() //@ ensures err == nil ==> 0 <= n && n <= len(m) //@ ensures err != nil ==> err.ErrorMem() ReadBatch(m Messages) (n int, err error) @@ -67,7 +67,7 @@ type Conn interface { //@ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, u *net.UDPAddr) (n int, err error) //@ requires acc(Mem(), _) - //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(1), R10) + //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(), R10) //@ ensures err == nil ==> 0 <= n && n <= len(m) //@ ensures err != nil ==> err.ErrorMem() WriteBatch(m Messages, k int) (n int, err error) @@ -164,24 +164,24 @@ func newConnUDPIPv4(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv4, // ReadBatch reads up to len(msgs) packets, and stores them in msgs. // It returns the number of packets read, and an error if any. // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs) // @ ensures errRet != nil ==> errRet.ErrorMem() func (c *connUDPIPv4) ReadBatch(msgs Messages) (nRet int, errRet error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/) + n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE) return n, err } // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R10) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv4) WriteBatch(msgs Messages, flags int) (n int, err error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/) + return c.pconn.WriteBatch(msgs, flags) } // SetReadDeadline sets the read deadline associated with the endpoint. @@ -238,24 +238,24 @@ func newConnUDPIPv6(listen, remote *net.UDPAddr, cfg *Config) (res *connUDPIPv6, // ReadBatch reads up to len(msgs) packets, and stores them in msgs. // It returns the number of packets read, and an error if any. // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() // @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs) // @ ensures errRet != nil ==> errRet.ErrorMem() func (c *connUDPIPv6) ReadBatch(msgs Messages) (nRet int, errRet error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE /*@, 1 @*/) + n, err := c.pconn.ReadBatch(msgs, syscall.MSG_WAITFORONE) return n, err } // @ requires acc(c.Mem(), _) -// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), R10) +// @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(), R10) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv6) WriteBatch(msgs Messages, flags int) (n int, err error) { //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs - return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/) + return c.pconn.WriteBatch(msgs, flags) } // SetReadDeadline sets the read deadline associated with the endpoint. @@ -463,11 +463,11 @@ func (c *connUDPBase) Close() (err error) { // messages. // @ requires 0 < n // @ ensures len(res) == n -// @ ensures forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem(1) +// @ ensures forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem() && res[i].GetAddr() == nil // @ decreases func NewReadMessages(n int) (res Messages) { m := make(Messages, n) - //@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem(1) + //@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem() && m[j].GetAddr() == nil //@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j]) && m[j].N == 0 //@ invariant forall j int :: { m[j].Addr } (i0 <= j && j < len(m)) ==> m[j].Addr == nil //@ invariant forall j int :: { m[j].OOB } (i0 <= j && j < len(m)) ==> m[j].OOB == nil @@ -477,7 +477,7 @@ func NewReadMessages(n int) (res Messages) { m[i].Buffers = make([][]byte, 1) //@ fold slices.AbsSlice_Bytes(m[i].Buffers[0], 0, len(m[i].Buffers[0])) //@ fold slices.AbsSlice_Bytes(m[i].OOB, 0, len(m[i].OOB)) - //@ fold m[i].Mem(1) + //@ fold m[i].Mem() } return m } diff --git a/router/dataplane.go b/router/dataplane.go index 2c1877968..74e16f30f 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -98,28 +98,32 @@ type bfdSession interface { // @ requires acc(Mem(), _) // @ ensures err != nil ==> err.ErrorMem() Run(ctx context.Context) (err error) - // @ requires acc(Mem(), _) - // @ requires msg.Mem(ub) - // @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) - // @ ensures msg.NonInitMem() // an implementation must copy the fields it needs from msg + // @ requires acc(Mem(), _) + // @ requires msg.Mem(ub) + // (VerifiedSCION) an implementation must copy the fields it needs from msg + // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) + // @ ensures msg.NonInitMem() ReceiveMessage(msg *layers.BFD /*@ , ghost ub []byte @*/) // @ requires acc(Mem(), _) IsUp() bool } // BatchConn is a connection that supports batch reads and writes. -// (VerifiedSCION) the spec of this interface exactly matches that of the same methods -// in private/underlay/conn/Conn -// TODO: add IO spec here +// (VerifiedSCION) the spec of this interface matches that of the methods +// with the same name in private/underlay/conn/Conn. type BatchConn interface { // @ pred Mem() // @ requires acc(Mem(), _) - // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> - // @ msgs[i].Mem(1) + // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + // @ msgs[i].Mem() + // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + // @ (msgs[i].Mem() && msgs[i].HasActiveAddr()) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err == nil ==> - // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> typeOf(msgs[i].GetAddr(1)) == type[*net.UDPAddr] + // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> ( + // @ typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr] && + // @ !msgs[i].HasWildcardPermAddr()) // @ ensures err == nil ==> // @ forall i int :: { &msgs[i] } 0 <= i && i < n ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) // @ ensures err != nil ==> err.ErrorMem() @@ -131,8 +135,8 @@ 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(1), R20) + // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + // @ (acc(msgs[i].Mem(), R50) && msgs[i].HasActiveAddr()) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() WriteBatch(msgs underlayconn.Messages, flags int) (n int, err error) @@ -282,7 +286,7 @@ func (d *DataPlane) SetKey(key []byte) (res error) { return mac } // (VerifiedSCION) Gobra cannot currently prove the following assertion, even though it must - // follow from the structure of the declaration of `verScionTemp`. + // follow from the structure of the declaration of `verScionTemp` (https://github.com/viperproject/gobra/issues/713). // @ assume verScionTemp != nil // @ proof verScionTemp implements MacFactorySpec{d.key} { // @ return verScionTemp() as f @@ -674,14 +678,14 @@ 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. -// @ trusted -// @ requires false // @ requires acc(&d.running, 1/2) && !d.running -// @ requires acc(&d.forwardingMetrics, 1/2) // @ requires acc(&d.Metrics, 1/2) && d.Metrics != nil // @ requires acc(&d.macFactory, 1/2) && d.macFactory != nil -// @ preserves d.mtx.LockP() -// @ preserves d.mtx.LockInv() == MutexInvariant!; +// @ requires acc(&d.forwardingMetrics, 1/2) && acc(d.forwardingMetrics, 1/2) +// @ requires 0 in domain(d.forwardingMetrics) +// @ requires d.mtx.LockP() +// @ requires d.mtx.LockInv() == MutexInvariant!; +// TODO: put well configured here func (d *DataPlane) Run(ctx context.Context) error { // @ share d, ctx d.mtx.Lock() @@ -691,59 +695,80 @@ func (d *DataPlane) Run(ctx context.Context) error { d.initMetrics() read /*@@@*/ := - // Note(VerifiedSCION): this precondition may cause problems ahead because of the lack of permissions to d.mtx // @ requires acc(&d, _) - // @ requires acc(&d.running, _) - // requires acc(&d.external, _) && (d.external != nil ==> acc(d.external, _)) - // requires ingressID in domain(d.external) - // @ requires acc(&d.macFactory, _) && d.macFactory != nil - // @ requires acc(MutexInvariant!(), _) + // @ 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 // @ requires rd != nil && acc(rd.Mem(), _) - // requires ingressID in domain(???) func /*@ rc @*/ (ingressID uint16, rd BatchConn) { - msgs := conn.NewReadMessages(inputBatchCnt) - // @ socketspec.SplitPermMsgs(msgs) - - // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf(1) - // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) + // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + // @ msgs[i].Mem() && msgs[i].GetAddr() == nil + // @ ensures forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> + // @ msgs[i].Mem() && + // @ msgs[i].HasActiveAddr() && + // @ msgs[i].GetAddr() == nil // @ decreases - // @ outline ( - // @ invariant len(msgs) != 0 ==> 0 <= i0 && i0 <= len(msgs) - // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> acc(&msgs[i], 1/2) - // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> i0 <= i && i < len(msgs) ==> msgs[i].MemWithoutHalf(1) - // @ invariant forall i int :: { &msgs[i] } 0 < len(msgs) ==> 0 <= i && i < i0 ==> msgs[i].Mem(1) + // @ outline( + // @ invariant 0 <= i0 && i0 <= len(msgs) + // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==> + // @ msgs[i].Mem() && msgs[i].GetAddr() == nil + // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < i0 ==> + // @ msgs[i].Mem() && msgs[i].GetAddr() == nil && msgs[i].HasActiveAddr() // @ decreases len(msgs) - i0 - for _, msg := range msgs /*@ with i0 @*/ { + for i0 := 0; i0 < len(msgs); i0 += 1 { + // (VerifiedSCION) changed a range loop in favor of a normal loop + // to be able to perform this unfold. + // @ unfold msgs[i0].Mem() + msg := msgs[i0] + // @ ensures sl.AbsSlice_Bytes(tmp, 0, len(tmp)) + // @ decreases + // @ outline( tmp := make([]byte, bufSize) // @ assert forall i int :: { &tmp[i] } 0 <= i && i < len(tmp) ==> acc(&tmp[i]) // @ fold sl.AbsSlice_Bytes(tmp, 0, len(tmp)) + // @ ) // @ assert msgs[i0] === msg - // @ unfold msgs[i0].MemWithoutHalf(1) msg.Buffers[0] = tmp - // @ fold msgs[i0].Mem(1) - // @ assert forall i int :: { &msgs[i] } 0 <= i && i < i0 ==> msgs[i].Mem(1) - // @ assert forall i int :: { &msgs[i] } i0 < i && i < len(msgs) ==> acc(&msgs[i], 1/2) && msgs[i].MemWithoutHalf(1) + // @ msgs[i0].IsActive = true + // @ fold msgs[i0].Mem() } // @ ) - // @ ensures writeMsgs[0].Mem(1) + // @ ensures writeMsgInv(writeMsgs) // @ decreases // @ outline ( writeMsgs := make(underlayconn.Messages, 1) writeMsgs[0].Buffers = make([][]byte, 1) // @ fold sl.AbsSlice_Bytes(writeMsgs[0].OOB, 0, len(writeMsgs[0].OOB)) // @ sl.NilAcc_Bytes() - // @ fold writeMsgs[0].Mem(1) + // @ fold writeMsgInv(writeMsgs) // @ ) processor := newPacketProcessor(d, ingressID) var scmpErr /*@@@*/ scmpError - // @ TODO() - // @ invariant acc(&d.running, _) && d.running + // @ 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 d.getValSvc() != nil + // @ invariant d.getValForwardingMetrics() != nil + // @ invariant 0 in d.getDomForwardingMetrics() + // @ invariant ingressID in d.getDomForwardingMetrics() // @ invariant acc(rd.Mem(), _) + // @ invariant processor.sInit() && processor.sInitD() === d for d.running { pkts, err := rd.ReadBatch(msgs) + // @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem() + // @ assert err == nil ==> + // @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) if err != nil { log.Debug("Failed to read batch", "err", err) // error metric @@ -752,66 +777,190 @@ func (d *DataPlane) Run(ctx context.Context) error { if pkts == 0 { continue } - for _, p := range msgs[:pkts] { + // @ assert pkts <= len(msgs) + // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> + // @ !msgs[i].HasWildcardPermAddr() + // @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> + // @ msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) + + // (VerifiedSCION) using regular for loop instead of range loop to avoid unnecessary + // complications with permissions + // @ 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 d.getValSvc() != nil + // @ invariant d.getValForwardingMetrics() != nil + // @ invariant 0 in d.getDomForwardingMetrics() + // @ invariant ingressID in d.getDomForwardingMetrics() + // @ invariant acc(rd.Mem(), _) + // @ invariant pkts <= len(msgs) + // @ invariant 0 <= i0 && i0 <= pkts + // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==> + // @ msgs[i].HasActiveAddr() + // @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==> + // @ typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr] + // @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> + // @ msgs[i].GetN() <= len(msgs[i].GetFstBuffer()) + // @ invariant processor.sInit() && processor.sInitD() === d + for i0 := 0; i0 < pkts; i0++ { + // @ assert &msgs[:pkts][i0] == &msgs[i0] + // @ preserves 0 <= i0 && i0 < pkts && pkts <= len(msgs) + // @ preserves acc(msgs[i0].Mem(), R1) + // @ ensures p === msgs[:pkts][i0].GetMessage() + // @ outline( + // @ unfold acc(msgs[i0].Mem(), R1) + p := msgs[:pkts][i0] + // @ fold acc(msgs[i0].Mem(), R1) + // @ ) + // @ assert msgs[i0].GetN() <= len(msgs[i0].GetFstBuffer()) + // @ d.getForwardingMetricsMem(ingressID) + // @ unfold acc(forwardingMetricsMem(d.forwardingMetrics[ingressID], ingressID), _) // input metric inputCounters := d.forwardingMetrics[ingressID] + // @ assert acc(inputCounters.InputPacketsTotal.Mem(), _) + // @ assert acc(inputCounters.InputBytesTotal.Mem(), _) + // @ prometheus.CounterMemImpliesNonNil(inputCounters.InputPacketsTotal) + // @ prometheus.CounterMemImpliesNonNil(inputCounters.InputBytesTotal) inputCounters.InputPacketsTotal.Inc() + // @ assert msgs[i0].GetN() == p.N + // (VerifiedSCION) Gobra still does not fully support floats + // @ fl.CastPreservesOrder64(0, p.N) inputCounters.InputBytesTotal.Add(float64(p.N)) srcAddr := p.Addr.(*net.UDPAddr) - result, err := processor.processPkt(p.Buffers[0][:p.N], srcAddr) - + // @ ghost m := &msgs[:pkts][i0] + // @ unfold m.Mem() + // @ assert p.Buffers === m.Buffers + // @ assert acc(&p.Buffers[0]) + // @ assert p.N <= len(p.Buffers[0]) + // @ sl.SplitRange_Bytes(p.Buffers[0], 0, p.N, writePerm) + tmpBuf := p.Buffers[0][:p.N] + // @ assert sl.AbsSlice_Bytes(tmpBuf, 0, p.N) + // @ assert sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)) + result, err /*@ , addrAliasesPkt @*/ := processor.processPkt(tmpBuf, srcAddr) + // @ fold scmpErr.Mem() switch { case err == nil: + // @ unfold scmpErr.Mem() case errors.As(err, &scmpErr): + // @ unfold d.validResult(result, addrAliasesPkt) + // @ ghost if addrAliasesPkt && result.OutAddr != nil { + // @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)), R15) + // @ } + // @ unfold scmpErr.Mem() if !scmpErr.TypeCode.InfoMsg() { log.Debug("SCMP", "err", scmpErr, "dst_addr", p.Addr) } // SCMP go back the way they came. result.OutAddr = srcAddr result.OutConn = rd + // @ addrAliasesPkt = false + // @ fold d.validResult(result, addrAliasesPkt) default: + // @ unfold d.validResult(result, addrAliasesPkt) + // @ ghost if addrAliasesPkt { + // @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)), R15) + // @ } + // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) + // @ assert acc(m) + // @ assert sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) + // @ assert (m.Addr != nil ==> acc(m.Addr.Mem(), _)) + // @ assert 0 <= m.N + // @ msgs[:pkts][i0].IsActive = false + // @ fold msgs[:pkts][i0].Mem() log.Debug("Error processing packet", "err", err) + // @ assert acc(inputCounters.DroppedPacketsTotal.Mem(), _) + // @ prometheus.CounterMemImpliesNonNil(inputCounters.DroppedPacketsTotal) inputCounters.DroppedPacketsTotal.Inc() + // @ unfold scmpErr.Mem() continue } if result.OutConn == nil { // e.g. BFD case no message is forwarded + // @ unfold d.validResult(result, addrAliasesPkt) + // @ ghost if addrAliasesPkt { + // @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)), R15) + // @ } + // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) + // @ msgs[:pkts][i0].IsActive = false + // @ fold msgs[:pkts][i0].Mem() continue } // Write to OutConn; drop the packet if this would block. // Use WriteBatch because it's the only available function that // supports MSG_DONTWAIT. + // @ unfold d.validResult(result, addrAliasesPkt) + // @ unfold writeMsgInv(writeMsgs) writeMsgs[0].Buffers[0] = result.OutPkt + // @ writeMsgs[0].WildcardPerm = !addrAliasesPkt + // @ writeMsgs[0].IsActive = true writeMsgs[0].Addr = nil if result.OutAddr != nil { // don't assign directly to net.Addr, typed nil! writeMsgs[0].Addr = result.OutAddr } - + // @ 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 { + // @ apply acc(result.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf)), R15) + // @ } + // @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm) + // @ msgs[:pkts][i0].IsActive = false + // @ fold msgs[:pkts][i0].Mem() + // @ fold writeMsgInv(writeMsgs) if err != nil { + // @ requires err != nil && err.ErrorMem() + // @ decreases + // @ outline ( var errno /*@@@*/ syscall.Errno - if !errors.As(err, &errno) || + // @ assert acc(&errno) + // @ fold errno.Mem() + errorsAs := errors.As(err, &errno) + // @ unfold errno.Mem() + if !errorsAs || !(errno == syscall.EAGAIN || errno == syscall.EWOULDBLOCK) { log.Debug("Error writing packet", "err", err) // error metric } + // @ ) + // @ assert acc(inputCounters.DroppedPacketsTotal.Mem(), _) + // @ prometheus.CounterMemImpliesNonNil(inputCounters.DroppedPacketsTotal) inputCounters.DroppedPacketsTotal.Inc() continue } + // @ requires acc(&d, _) + // @ requires acc(MutexInvariant(d), _) + // @ requires result.EgressID in d.getDomForwardingMetrics() + // @ decreases + // @ outline( // ok metric + // @ d.getForwardingMetricsMem(result.EgressID) + // @ unfold acc(forwardingMetricsMem(d.forwardingMetrics[result.EgressID], result.EgressID), _) outputCounters := d.forwardingMetrics[result.EgressID] + // @ assert acc(outputCounters.OutputPacketsTotal.Mem(), _) + // @ prometheus.CounterMemImpliesNonNil(outputCounters.OutputPacketsTotal) outputCounters.OutputPacketsTotal.Inc() + // @ assert acc(outputCounters.OutputBytesTotal.Mem(), _) + // @ prometheus.CounterMemImpliesNonNil(outputCounters.OutputBytesTotal) + // @ fl.CastPreservesOrder64(0, len(result.OutPkt)) outputCounters.OutputBytesTotal.Add(float64(len(result.OutPkt))) + // @ ) } } } + // (VerifiedSCION) Continue from here after adapting processPkt and processOHP // @ TODO() - // TODO: replace by acc(MutexInvariant(d), _) for the remainder of the proof? - makes proof obligations easier - // @ fold acc(MutexInvariant!(), _) for k, v := range d.bfdSessions { + // @ TODO() go func(ifID uint16, c bfdSession) { + // @ TODO() defer log.HandlePanic() if err := c.Run(ctx); err != nil && err != bfd.AlreadyRunning { log.Error("BFD session failed to start", "ifID", ifID, "err", err) @@ -820,18 +969,27 @@ func (d *DataPlane) Run(ctx context.Context) error { } for ifID, v := range d.external { go func(i uint16, c BatchConn) { + // @ TODO() defer log.HandlePanic() // TODO(VerifiedSCION): calling this may cause problems because of the lack of permissions to d.mtx // This should be easily addressable nonethelss - read(i, c) //@ as readClosureSpec + read(i, c) //@ as readClosureSpec // TODO: maybe use rc as the spec instead and delete readClosureSpec }(ifID, v) //@ as closureSpec2 } go func(c BatchConn) { + // @ TODO() defer log.HandlePanic() // TODO(VerifiedSCION): calling this may cause problems because of the lack of permissions to d.mtx - read(0, c) //@ as readClosureSpec + read(0, c) //@ as readClosureSpec // TODO: maybe use rc as the spec instead and delete readClosureSpec }(d.internal) //@ as closureSpec3 + // (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() @@ -920,23 +1078,8 @@ type processResult struct { } // @ requires acc(&d.macFactory, _) && d.macFactory != nil -// @ requires acc(MutexInvariant!(), _) -// @ ensures acc(&res.d) && res.d === d -// @ ensures acc(&res.ingressID) -// @ ensures acc(&res.buffer) -// @ ensures acc(&res.mac) -// @ ensures acc(res.scionLayer.NonInitMem()) -// @ ensures res.scionLayer.PathPoolInitializedNonInitMem() -// @ ensures acc(&res.hbhLayer) -// @ ensures acc(&res.e2eLayer) -// @ ensures acc(&res.lastLayer) -// @ ensures acc(&res.path) -// @ ensures acc(&res.hopField) -// @ ensures acc(&res.infoField) -// @ ensures acc(&res.segmentChange) -// @ ensures acc(&res.cachedMac) -// @ ensures acc(&res.macBuffers) -// @ ensures acc(&res.bfdLayer) +// @ requires acc(MutexInvariant(d), _) +// @ ensures res.sInit() && res.sInitD() == d // @ decreases func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcessor) { var verScionTmp gopacket.SerializeBuffer @@ -952,22 +1095,29 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess epicInput: make([]byte, libepic.MACBufferSize), }, } + // @ fold sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw) p.scionLayer.RecyclePaths() // @ fold p.scionLayer.NonInitMem() + // @ fold p.hbhLayer.NonInitMem() + // @ fold p.e2eLayer.NonInitMem() + // @ fold p.bfdLayer.NonInitMem() + // @ fold p.sInit() return p } -// @ preserves acc(&p.rawPkt) && acc(&p.path) && acc(&p.hopField) && acc(&p.infoField) -// @ preserves acc(&p.segmentChange) && acc(&p.buffer) && acc(&p.mac) && acc(&p.cachedMac) -// @ preserves p.buffer != nil && p.buffer.Mem() -// @ preserves p.mac != nil && p.mac.Mem() -// @ ensures p.rawPkt == nil && p.path == nil -// @ ensures p.hopField == path.HopField{} && p.infoField == path.InfoField{} -// @ ensures !p.segmentChange +// @ preserves p.sInit() +// @ ensures p.sInitD() == old(p.sInitD()) +// @ ensures p.sInitRawPkt() == nil +// @ ensures p.sInitPath() == nil +// @ ensures p.sInitHopField() == path.HopField{} +// @ ensures p.sInitInfoField() == path.InfoField{} +// @ ensures !p.sInitSegmentChange() // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (p *scionPacketProcessor) reset() (err error) { + // @ unfold p.sInit() + // @ defer fold p.sInit() p.rawPkt = nil //p.scionLayer // cannot easily be reset p.path = nil @@ -982,27 +1132,36 @@ func (p *scionPacketProcessor) reset() (err error) { return nil } -// @ requires p.scionLayer.NonInitMem() && p.hbhLayer.NonInitMem() && p.e2eLayer.NonInitMem() +// @ requires p.sInit() // @ requires sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)) -// @ requires acc(&p.d) && acc(MutexInvariant!(), _) -// @ requires acc(&p.d.svc, _) && p.d.svc != nil -// @ requires acc(&p.ingressID) -// @ requires acc(&p.rawPkt) && acc(&p.path) && acc(&p.hopField) && acc(&p.infoField) -// @ requires acc(&p.macBuffers.scionInput, R10) -// @ requires sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) -// @ requires acc(&p.segmentChange) && acc(&p.buffer) && acc(&p.mac) && acc(&p.cachedMac) -// @ requires acc(&p.srcAddr) && acc(&p.lastLayer) -// @ requires p.buffer != nil && p.buffer.Mem() -// @ requires p.mac != nil && p.mac.Mem() // @ requires acc(srcAddr.Mem(), _) -// @ requires p.bfdLayer.NonInitMem() +// @ requires let d := p.sInitD() in +// @ acc(MutexInvariant(d), _) && +// @ d.WellConfigured() && +// @ d.getValSvc() != nil && +// @ d.getValForwardingMetrics() != nil +// @ ensures p.sInit() +// @ ensures acc(MutexInvariant(p.sInitD()), _) +// @ ensures p.sInitD() == old(p.sInitD()) +// @ ensures p.sInitD().validResult(respr, addrAliasesPkt) +// @ ensures acc(sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)), 1 - R15) +// @ ensures addrAliasesPkt ==> ( +// @ respr.OutAddr != nil && +// @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)), R15))) +// @ ensures !addrAliasesPkt ==> acc(sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)), R15) +// @ ensures respr.OutPkt !== rawPkt && respr.OutPkt != nil ==> +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() func (p *scionPacketProcessor) processPkt(rawPkt []byte, - srcAddr *net.UDPAddr) (respr processResult, reserr error) { + srcAddr *net.UDPAddr) (respr processResult, reserr error /*@ , addrAliasesPkt bool @*/) { if err := p.reset(); err != nil { - return processResult{}, err + // @ fold p.sInitD().validResult(processResult{}, false) + return processResult{}, err /*@, false @*/ } + // @ assert p.sInitD().getValForwardingMetrics() != nil + // @ unfold p.sInit() + // @ ghost d := p.d p.rawPkt = rawPkt p.srcAddr = srcAddr @@ -1013,12 +1172,20 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ ghost var lastLayerIdx int p.lastLayer, err /*@ , processed, offsets, lastLayerIdx @*/ = decodeLayers(p.rawPkt, &p.scionLayer, &p.hbhLayer, &p.e2eLayer) if err != nil { - return processResult{}, err + // @ fold p.sInit() + // @ fold p.sInitD().validResult(processResult{}, false) + return processResult{}, err /*@, false @*/ } /*@ ghost var ub []byte + ghost var ubScionLayer []byte = p.rawPkt + ghost var ubHbhLayer []byte + ghost var ubE2eLayer []byte + ghost llStart := 0 ghost llEnd := 0 + ghost mustCombineRanges := lastLayerIdx != -1 && !offsets[lastLayerIdx].isNil + ghost var o offsetPair ghost if lastLayerIdx == -1 { ub = p.rawPkt } else { @@ -1026,13 +1193,21 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, ub = nil sl.NilAcc_Bytes() } else { - o := offsets[lastLayerIdx] + o = offsets[lastLayerIdx] ub = p.rawPkt[o.start:o.end] llStart = o.start llEnd = o.end sl.SplitRange_Bytes(p.rawPkt, o.start, o.end, writePerm) } } + hasHbhLayer := processed[0] + oHbh := offsets[0] + ubHbhLayer = hasHbhLayer && !oHbh.isNil ? p.rawPkt[oHbh.start:oHbh.end] : ([]byte)(nil) + hasE2eLayer := processed[1] + oE2e := offsets[1] + ubE2eLayer = hasE2eLayer && !oE2e.isNil ? p.rawPkt[oE2e.start:oE2e.end] : ([]byte)(nil) + assert processed[0] ==> p.hbhLayer.Mem(ubHbhLayer) + assert processed[1] ==> p.e2eLayer.Mem(ubE2eLayer) @*/ // @ assert sl.AbsSlice_Bytes(ub, 0, len(ub)) pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ub @*/ ) @@ -1042,23 +1217,39 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, pathType := /*@ unfolding p.scionLayer.Mem(rawPkt) in @*/ p.scionLayer.PathType switch pathType { case empty.PathType: + // @ ghost if mustCombineRanges { ghost defer sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, writePerm) } if p.lastLayer.NextLayerType( /*@ ub @*/ ) == layers.LayerTypeBFD { - // @ assert p.bfdLayer.NonInitMem() - return processResult{}, p.processIntraBFD(pld) + // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) + // @ defer fold p.sInit() + // @ defer fold p.d.validResult(processResult{}, false) + // @ ghost defer sl.CombineRange_Bytes(ub, start, end, writePerm) + return processResult{}, p.processIntraBFD(pld) /*@, false @*/ } // @ establishMemUnsupportedPathTypeNextHeader() + // @ defer fold p.sInit() + // @ defer fold p.d.validResult(processResult{}, false) + // @ ghost defer ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) + // @ ghost defer sl.CombineRange_Bytes(ub, start, end, writePerm) return processResult{}, serrors.WithCtx(unsupportedPathTypeNextHeader, - "type", pathType, "header", nextHdr(p.lastLayer /*@, ub @*/)) + "type", pathType, "header", nextHdr(p.lastLayer /*@, ub @*/)) /*@, false @*/ case onehop.PathType: if p.lastLayer.NextLayerType( /*@ ub @*/ ) == layers.LayerTypeBFD { + // @ ghost if mustCombineRanges { ghost defer sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, writePerm) } + // @ ghost defer sl.CombineRange_Bytes(ub, start, end, writePerm) // @ unfold acc(p.scionLayer.Mem(p.rawPkt), R10) ohp, ok := p.scionLayer.Path.(*onehop.Path) // @ fold acc(p.scionLayer.Mem(p.rawPkt), R10) if !ok { // @ establishMemMalformedPath() - return processResult{}, malformedPath + // @ defer fold p.sInit() + // @ defer fold p.d.validResult(processResult{}, false) + // @ ghost defer ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) + return processResult{}, malformedPath /*@, false @*/ } - return processResult{}, p.processInterBFD(ohp, pld) + // @ defer fold p.sInit() + // @ defer fold p.d.validResult(processResult{}, false) + // @ ghost defer ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) + return processResult{}, p.processInterBFD(ohp, pld) /*@, false @*/ } // @ sl.CombineRange_Bytes(ub, start, end, writePerm) // (VerifiedSCION) Nested if because short-circuiting && is not working @@ -1069,7 +1260,11 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ } // @ } // @ assert sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)) - return p.processOHP() + // @ unfold acc(MutexInvariant(p.d), _) + v1, v2 /*@, aliasesPkt @*/ := p.processOHP() + // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) + // @ fold p.sInit() + return v1, v2 /*@, aliasesPkt @*/ case scion.PathType: // @ sl.CombineRange_Bytes(ub, start, end, writePerm) // (VerifiedSCION) Nested if because short-circuiting && is not working @@ -1080,27 +1275,37 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // @ } // @ } // @ assert sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)) - return p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd @*/ ) + v1, v2 /*@ , addrAliasesPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd @*/ ) + // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer) + // @ fold p.sInit() + return v1, v2 /*@, addrAliasesPkt @*/ case epic.PathType: // @ TODO() - return p.processEPIC() + v1, v2 := p.processEPIC() + // @ fold p.sInit() + return v1, v2 /*@, false @*/ default: + // @ ghost if mustCombineRanges { ghost defer sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, writePerm) } + // @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer) + // @ sl.CombineRange_Bytes(ub, start, end, writePerm) + // @ fold p.d.validResult(processResult{}, false) + // @ fold p.sInit() // @ establishMemUnsupportedPathType() - return processResult{}, serrors.WithCtx(unsupportedPathType, "type", pathType) + return processResult{}, serrors.WithCtx(unsupportedPathType, "type", pathType) /*@, false @*/ } } // @ requires acc(&p.d, R20) // @ requires acc(&p.ingressID, R20) -// @ requires acc(MutexInvariant!(), _) +// @ requires acc(MutexInvariant(p.d), _) // @ requires p.bfdLayer.NonInitMem() -// @ requires sl.AbsSlice_Bytes(data, 0, len(data)) +// @ preserves sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures acc(&p.d, R20) // @ ensures acc(&p.ingressID, R20) // @ ensures p.bfdLayer.NonInitMem() // @ ensures err != nil ==> err.ErrorMem() func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (err error) { - // @ unfold acc(MutexInvariant!(), _) + // @ unfold acc(MutexInvariant(p.d), _) // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } if len(p.d.bfdSessions) == 0 { // @ establishMemNoBFDSessionConfigured() @@ -1127,13 +1332,15 @@ 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!(), _) +// @ requires acc(MutexInvariant(p.d), _) // @ requires sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures acc(&p.d, R20) // @ ensures acc(&p.srcAddr, R20) +// @ ensures p.bfdLayer.NonInitMem() +// @ ensures sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures res != nil ==> res.ErrorMem() func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { - // @ unfold acc(MutexInvariant!(), _) + // @ unfold acc(MutexInvariant(p.d), _) // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } if len(p.d.bfdSessions) == 0 { // @ establishMemNoBFDSessionConfigured() @@ -1150,6 +1357,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ ghost if p.d.internalNextHops != nil { unfold acc(accAddr(p.d.internalNextHops), _) } // (VerifiedSCION) establish ability to use range loop (requires a fixed permission) + // (VerifiedSCION) TODO: Rewrite this to use regular loop instead to avoid complications with permissions. // @ ghost m := p.d.internalNextHops // @ assert m != nil ==> acc(m, _) // @ inhale m != nil ==> acc(m, R19) @@ -1183,13 +1391,14 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { return nil } + // @ bfd.DowngradePerm(data) // @ establishMemNoBFDSessionFound() return noBFDSessionFound } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires acc(&p.d, R5) && acc(MutexInvariant!(), _) -// @ requires acc(&p.d.svc, _) && p.d.svc != nil +// @ requires acc(&p.d, R5) && acc(MutexInvariant(p.d), _) && 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 // @ requires acc(&p.rawPkt, R1) && ub === p.rawPkt @@ -1211,14 +1420,21 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) -// @ ensures acc(&p.d, R20) +// @ ensures acc(&p.d, R5) // @ ensures acc(&p.path) // @ ensures acc(&p.rawPkt, R1) // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() -// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), 1 - R15) +// @ ensures p.d.validResult(respr, addrAliasesPkt) +// @ ensures addrAliasesPkt ==> ( +// @ respr.OutAddr != nil && +// @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15))) +// @ ensures !addrAliasesPkt ==> acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) +// @ ensures respr.OutPkt !== ub && respr.OutPkt != nil ==> +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() -func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error /*@ , addrAliasesPkt bool @*/) { var ok bool // @ unfold acc(p.scionLayer.Mem(ub), R20) @@ -1228,7 +1444,8 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil // TODO(lukedirtwalker) parameter problem invalid path? // @ p.scionLayer.DowngradePerm(ub) // @ establishMemMalformedPath() - return processResult{}, malformedPath + // @ fold p.d.validResult(processResult{}, false) + return processResult{}, malformedPath /*@ , false @*/ } return p.process( /*@ ub, llIsNil, startLL, endLL @*/ ) } @@ -1360,11 +1577,13 @@ func (p *scionPacketProcessor) packSCMP( return processResult{OutPkt: rawSCMP}, err } +// @ requires acc(&p.d, R50) && acc(MutexInvariant(p.d), _) // @ requires acc(p.scionLayer.Mem(ub), R5) // @ requires acc(&p.path, R20) // @ requires p.path === p.scionLayer.GetPath(ub) // @ requires acc(&p.hopField) && acc(&p.infoField) // @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R1) +// @ ensures acc(&p.d, R50) // @ ensures acc(p.scionLayer.Mem(ub), R6) // @ ensures acc(&p.path, R20) // @ ensures p.path === p.scionLayer.GetPath(ub) @@ -1375,6 +1594,7 @@ func (p *scionPacketProcessor) packSCMP( // @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrHF(ubPath) < p.path.GetNumHops(ubPath)) // @ ensures acc(p.scionLayer.Mem(ub), R6) +// @ ensures p.d.validResult(respr, false) // @ ensures reserr == nil ==> ( // @ let ubPath := p.scionLayer.UBPath(ub) in // @ unfolding acc(p.scionLayer.Mem(ub), R10) in @@ -1391,6 +1611,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ sl.SplitRange_Bytes(ub, startP, endP, R1) // @ ghost defer sl.CombineRange_Bytes(ub, startP, endP, R1) p.hopField, err = p.path.GetCurrentHopField( /*@ ubPath @*/ ) + // @ fold p.d.validResult(processResult{}, false) if err != nil { // TODO(lukedirtwalker) parameter problem invalid path? return processResult{}, err @@ -1405,6 +1626,10 @@ 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), _) +// @ 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() // @ decreases func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr error) { @@ -1412,9 +1637,20 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr Add(path.ExpTimeToDuration(p.hopField.ExpTime)) expired := expiration.Before(time.Now()) if !expired { + // @ fold p.d.validResult(respr, false) return processResult{}, nil } // @ TODO() + // TODO: adapt; note that packSCMP always returns an empty addr and conn and + // when the err is nil, it returns the bytes of p.buffer. This should be a magic wand + // that is consumed after sending the reply. For now, we are making this simplifying + // assumption, but in the future, we should elaborate the proof for this to not be + // necessary. To do this, we need to return a flag everywhere that says whether the + // pkt overlaps with p.buffer and, if so, a wand from AbsSlice of its underlying slice + // to p.buffer.Mem(). This is very similar to what we did with the address. + // The flag would be added to processPkt, processSCION, process. Only when processing + // SCION could this flag be true. In all other cases, it will be false. The processResult + // that is returned never overlaps with the rawPkt return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodePathExpired, @@ -1427,6 +1663,9 @@ 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), _) +// @ 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() // @ ensures reserr == nil && p.infoField.ConsDir ==> ( // @ p.ingressID == 0 || p.hopField.ConsIngress == p.ingressID) @@ -1450,10 +1689,11 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr "pkt_ingress", pktIngressID, "router_ingress", p.ingressID), ) } + // @ fold p.d.validResult(respr, false) return processResult{}, nil } -// @ requires acc(&p.d, R20) && acc(MutexInvariant!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ requires acc(p.scionLayer.Mem(ubScionL), R19) // @ requires acc(&p.path, R20) // @ requires p.path === p.scionLayer.GetPath(ubScionL) @@ -1461,6 +1701,9 @@ func (p *scionPacketProcessor) validateIngressID() (respr processResult, reserr // @ ensures acc(p.scionLayer.Mem(ubScionL), R19) // @ ensures acc(&p.path, R20) // @ ensures acc(&p.d, R20) +// @ 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() // @ decreases func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) (respr processResult, reserr error) { @@ -1496,6 +1739,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) return p.invalidDstIA() } } + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } @@ -1539,7 +1783,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!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ requires acc(&p.srcAddr, R20) && acc(p.srcAddr.Mem(), _) // @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R4) // @ ensures acc(&p.path, R15) @@ -1548,6 +1792,8 @@ func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { // @ ensures acc(&p.infoField, R4) && acc(&p.hopField, R4) // @ ensures acc(&p.d, R20) // @ ensures acc(&p.srcAddr, R20) +// @ ensures p.d.validResult(respr, false) +// @ ensures respr.OutPkt == nil // @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @*/ ) (respr processResult, reserr error) { @@ -1560,9 +1806,10 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ // @ ghost defer sl.CombineRange_Bytes(ub, startP, endP, R5) // (VerifiedSCION) Gobra cannot prove this property yet, even though it follows // from the type system - // @ assume 0 <= p.path.GetCurrHF(ubPath) + // @ assume 0 <= p.path.GetCurrHF(ubPath) // TODO: drop assumptions like this if p.path.IsFirstHop( /*@ ubPath @*/ ) || p.ingressID != 0 { // not a transit packet, nothing to check + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } pktIngressID := p.ingressInterface( /*@ ubPath @*/ ) @@ -1577,17 +1824,22 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @ if !ok || !expectedSrc.IP.Equal(p.srcAddr.IP) { // Drop // @ establishInvalidSrcAddrForTransit() + // @ fold p.d.validResult(processResult{}, false) return processResult{}, invalidSrcAddrForTransit } + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } -// @ requires acc(&p.d, R20) && acc(MutexInvariant!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ preserves acc(&p.ingressID, R20) // @ preserves acc(&p.segmentChange, R20) // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ ensures acc(&p.d, R20) +// @ ensures p.d.validResult(respr, false) +// @ ensures reserr == nil ==> respr === processResult{} +// @ ensures reserr != nil ==> sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr error) { @@ -1619,12 +1871,16 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e // No check required if the packet is received from an internal interface. switch { case p.ingressID == 0: + // @ fold p.d.validResult(respr, false) return processResult{}, nil case ingress == topology.Core && egress == topology.Core: + // @ fold p.d.validResult(respr, false) return processResult{}, nil case ingress == topology.Child && egress == topology.Parent: + // @ fold p.d.validResult(respr, false) return processResult{}, nil case ingress == topology.Parent && egress == topology.Child: + // @ fold p.d.validResult(respr, false) return processResult{}, nil default: // malicious // @ TODO() @@ -1640,10 +1896,13 @@ func (p *scionPacketProcessor) validateEgressID() (respr processResult, reserr e // Having a segment change received from the internal interface is never valid. switch { case ingress == topology.Core && egress == topology.Child: + // @ fold p.d.validResult(respr, false) return processResult{}, nil case ingress == topology.Child && egress == topology.Core: + // @ fold p.d.validResult(respr, false) return processResult{}, nil case ingress == topology.Child && egress == topology.Child: + // @ fold p.d.validResult(respr, false) return processResult{}, nil default: // @ TODO() @@ -1736,6 +1995,10 @@ 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), _) +// @ ensures p.d.validResult(respr, false) +// @ ensures respr.OutPkt != nil ==> +// @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures len(p.cachedMac) == path.MACBufferSize // @ ensures sl.AbsSlice_Bytes(p.cachedMac, 0, len(p.cachedMac)) // @ ensures reserr != nil ==> reserr.ErrorMem() @@ -1764,33 +2027,45 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e // such that EPIC does not need to recalculate it. p.cachedMac = fullMac + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } // @ requires acc(&p.d, R15) -// @ requires acc(MutexInvariant!(), _) -// (VerifiedSCION) permission to acc(&p.d.svc, _) would not be necessary -// if one was using something other than a predicate expression instance. -// @ requires acc(&p.d.svc, _) && p.d.svc != nil +// @ requires acc(MutexInvariant(p.d), _) +// @ requires p.d.getValSvc() != nil +// @ requires acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) // @ preserves acc(p.scionLayer.Mem(ubScionL), R10) -// @ preserves acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R10) // @ ensures acc(&p.d, R15) +// @ ensures p.d.validResult(respr, addrAliasesUb) +// @ ensures !addrAliasesUb ==> acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) +// @ ensures !addrAliasesUb && resaddr != nil ==> acc(resaddr.Mem(), _) +// @ ensures addrAliasesUb ==> resaddr != nil +// @ ensures addrAliasesUb ==> acc(resaddr.Mem(), R15) +// @ ensures addrAliasesUb ==> (acc(resaddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15)) +// @ ensures respr.OutPkt != nil ==> +// @ reserr != nil && sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> !addrAliasesUb // @ ensures reserr != nil ==> reserr.ErrorMem() -func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) (resaddr *net.UDPAddr, respr processResult, reserr error) { +func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) (resaddr *net.UDPAddr, respr processResult, reserr error /*@ , addrAliasesUb bool @*/) { // (VerifiedSCION) the parameter used to be p.scionLayer, // instead of &p.scionLayer. - a, err := p.d.resolveLocalDst(&p.scionLayer /*@, ubScionL @*/) + a, err /*@ , addrAliases @*/ := p.d.resolveLocalDst(&p.scionLayer /*@, ubScionL @*/) // @ establishNoSVCBackend() switch { case errors.Is(err, noSVCBackend): + // @ ghost if addrAliases { + // @ apply acc(a.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) + // @ } // @ TODO() r, err := p.packSCMP( slayers.SCMPTypeDestinationUnreachable, slayers.SCMPCodeNoRoute, &slayers.SCMPDestinationUnreachable{}, err) - return nil, r, err + return nil, r, err /*@ , false @*/ default: - return a, processResult{}, nil + // @ fold p.d.validResult(respr, addrAliases) + return a, processResult{}, nil /*@ , addrAliases @*/ } } @@ -1848,6 +2123,7 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte @*/ ) (reserr // @ ensures reserr == nil ==> (p.scionLayer.Mem(ub) && p.scionLayer.UBPath(ub) === old(p.scionLayer.UBPath(ub)) && p.scionLayer.GetPath(ub) === old(p.scionLayer.GetPath(ub))) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() // @ ensures p.segmentChange +// @ ensures respr === processResult{} // @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte @*/ ) (respr processResult, reserr error) { @@ -1923,11 +2199,14 @@ func (p *scionPacketProcessor) egressInterface() uint16 { return p.hopField.ConsIngress } -// @ requires acc(&p.d, R20) && acc(MutexInvariant!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) // @ preserves acc(&p.ingressID, R20) // @ ensures acc(&p.d, R20) +// @ 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() func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr error) { egressID := p.egressInterface() @@ -1955,6 +2234,7 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down")) } } + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } @@ -1962,7 +2242,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!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ preserves acc(&p.lastLayer, R19) // @ preserves p.lastLayer != nil @@ -1976,6 +2256,9 @@ func (p *scionPacketProcessor) validateEgressUp() (respr processResult, reserr e // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ub), R10) // @ ensures acc(&p.d, R20) +// @ 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() // @ decreases func (p *scionPacketProcessor) handleIngressRouterAlert( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { @@ -1984,10 +2267,12 @@ func (p *scionPacketProcessor) handleIngressRouterAlert( /*@ ghost ub []byte, gh // @ ghost endP := p.scionLayer.PathEndIdx(ub) // @ assert ub[startP:endP] === ubPath if p.ingressID == 0 { + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } alert := p.ingressRouterAlertFlag() if !*alert { + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } *alert = false @@ -1998,6 +2283,7 @@ func (p *scionPacketProcessor) handleIngressRouterAlert( /*@ ghost ub []byte, gh // @ sl.SplitRange_Bytes(ub, startP, endP, writePerm) if err := p.path.SetHopField(p.hopField, int( /*@ unfolding acc(p.path.Mem(ubPath), R50) in (unfolding acc(p.path.Base.Mem(), R55) in @*/ p.path.PathMeta.CurrHF /*@ ) @*/) /*@ , ubPath @*/); err != nil { // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("update hop field", err) } // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) @@ -2031,7 +2317,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!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ preserves sl.AbsSlice_Bytes(ub, 0, len(ub)) // @ preserves acc(&p.lastLayer, R19) // @ preserves p.lastLayer != nil @@ -2045,6 +2331,9 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ub), R14) // @ ensures acc(&p.d, R20) +// @ 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() // @ decreases func (p *scionPacketProcessor) handleEgressRouterAlert( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { @@ -2055,12 +2344,14 @@ func (p *scionPacketProcessor) handleEgressRouterAlert( /*@ ghost ub []byte, gho alert := p.egressRouterAlertFlag() if !*alert { + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } egressID := p.egressInterface() // @ p.d.getExternalMem() // @ if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) } if _, ok := p.d.external[egressID]; !ok { + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } *alert = false @@ -2072,6 +2363,7 @@ func (p *scionPacketProcessor) handleEgressRouterAlert( /*@ ghost ub []byte, gho // @ sl.SplitRange_Bytes(ub, startP, endP, writePerm) if err := p.path.SetHopField(p.hopField, int( /*@ unfolding acc(p.path.Mem(ubPath), R50) in (unfolding acc(p.path.Base.Mem(), R55) in @*/ p.path.PathMeta.CurrHF /*@ ) @*/) /*@ , ubPath @*/); err != nil { // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("update hop field", err) } // @ sl.CombineRange_Bytes(ub, startP, endP, writePerm) @@ -2103,11 +2395,14 @@ 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!(), _) +// @ requires acc(&p.d, R20) && acc(MutexInvariant(p.d), _) // @ preserves sl.AbsSlice_Bytes(ubLastLayer, 0, len(ubLastLayer)) // @ ensures acc(&p.lastLayer, R20) // @ ensures acc(p.lastLayer.Mem(ubLastLayer), R15) // @ ensures acc(&p.d, R20) +// @ 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() // @ decreases func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( @@ -2115,6 +2410,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( if p.lastLayer.NextLayerType( /*@ ubLastLayer @*/ ) != slayers.LayerTypeSCMP { log.Debug("Packet with router alert, but not SCMP") + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } scionPld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLastLayer @*/ ) @@ -2128,11 +2424,13 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ fold scmpH.NonInitMem() if err := scmpH.DecodeFromBytes(scionPld, gopacket.NilDecodeFeedback); err != nil { log.Debug("Parsing SCMP header of router alert", "err", err) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } if /*@ (unfolding acc(scmpH.Mem(scionPld), R55) in @*/ scmpH.TypeCode /*@ ) @*/ != slayers.CreateSCMPTypeCode(slayers.SCMPTypeTracerouteRequest, 0) { log.Debug("Packet with router alert, but not traceroute request", "type_code", ( /*@ unfolding acc(scmpH.Mem(scionPld), R55) in @*/ scmpH.TypeCode)) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } var scmpP /*@@@*/ slayers.SCMPTraceroute @@ -2143,6 +2441,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( // @ ghost defer sl.CombineRange_Bytes(scionPld, 4, len(scionPld), writePerm) if err := scmpP.DecodeFromBytes(scmpH.Payload, gopacket.NilDecodeFeedback); err != nil { log.Debug("Parsing SCMPTraceroute", "err", err) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } // @ unfold scmpP.Mem(scmpH.Payload) @@ -2159,6 +2458,9 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( } // @ preserves acc(p.scionLayer.Mem(ubScionL), R20) +// @ preserves acc(&p.d, R50) && acc(MutexInvariant(p.d), _) +// @ 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)) // @ ensures reserr != nil ==> reserr.ErrorMem() // @ decreases @@ -2166,6 +2468,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ unfold acc(p.scionLayer.Mem(ubScionL), R20) // @ defer fold acc(p.scionLayer.Mem(ubScionL), R20) if int(p.scionLayer.PayloadLen) == len(p.scionLayer.Payload) { + // @ fold p.d.validResult(processResult{}, false) return processResult{}, nil } // @ TODO() @@ -2179,8 +2482,8 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) -// @ requires acc(&p.d, R5) && acc(MutexInvariant!(), _) -// @ requires acc(&p.d.svc, _) && p.d.svc != nil +// @ requires acc(&p.d, R5) && acc(MutexInvariant(p.d), _) && 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 // @ requires acc(&p.rawPkt, R1) && ub === p.rawPkt @@ -2203,61 +2506,71 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ preserves acc(&p.macBuffers.scionInput, R10) // @ preserves sl.AbsSlice_Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) -// @ ensures acc(&p.d, R20) +// @ ensures acc(&p.d, R5) // @ ensures acc(&p.path, R10) // @ ensures acc(&p.rawPkt, R1) -// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), 1 - R15) +// @ ensures p.d.validResult(respr, addrAliasesPkt) +// @ ensures addrAliasesPkt ==> ( +// @ respr.OutAddr != nil && +// @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15))) +// @ ensures !addrAliasesPkt ==> acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) +// @ ensures respr.OutPkt !== ub && respr.OutPkt != nil ==> +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr == nil ==> p.scionLayer.Mem(ub) // @ ensures reserr != nil ==> p.scionLayer.NonInitMem() // @ ensures reserr != nil ==> reserr.ErrorMem() -func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error /*@, addrAliasesPkt bool @*/) { if r, err := p.parsePath( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.validateHopExpiry(); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.validateIngressID(); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.validatePktLen( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.validateTransitUnderlaySrc( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.validateSrcDstIA( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if err := p.updateNonConsDirIngressSegID( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return processResult{}, err + return processResult{}, err /*@, false @*/ } if r, err := p.verifyCurrentMAC(); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.handleIngressRouterAlert( /*@ ub, llIsNil, startLL, endLL @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } // Inbound: pkts destined to the local IA. // @ p.d.getLocalIA() if /*@ unfolding acc(p.scionLayer.Mem(ub), R50) in (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in @*/ p.scionLayer.DstIA /*@ ) @*/ == p.d.localIA { - a, r, err := p.resolveInbound( /*@ ub @*/ ) + a, r, err /*@, aliasesUb @*/ := p.resolveInbound( /*@ ub @*/ ) if err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, aliasesUb @*/ } // @ p.d.getInternal() - return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil + // @ unfold p.d.validResult(r, aliasesUb) + // @ fold p.d.validResult(processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, aliasesUb) + // @ assert ub === p.rawPkt + return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil /*@, aliasesUb @*/ } // Outbound: pkts leaving the local IA. @@ -2268,44 +2581,47 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, if p.path.IsXover( /*@ ubPath @*/ ) { // @ fold acc(p.scionLayer.Mem(ub), R3) if r, err := p.doXover( /*@ ub @*/ ); err != nil { - return r, err + // @ fold p.d.validResult(r, false) + return r, err /*@, false @*/ } if r, err := p.validateHopExpiry(); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, serrors.WithCtx(err, "info", "after xover") + return r, serrors.WithCtx(err, "info", "after xover") /*@, false @*/ } // verify the new block if r, err := p.verifyCurrentMAC(); err != nil { // fold acc(p.scionLayer.Mem(ub), R3) // @ p.scionLayer.DowngradePerm(ub) - return r, serrors.WithCtx(err, "info", "after xover") + return r, serrors.WithCtx(err, "info", "after xover") /*@, false @*/ } } // @ fold acc(p.scionLayer.Mem(ub), R3) if r, err := p.validateEgressID(); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } // handle egress router alert before we check if it's up because we want to // send the reply anyway, so that trace route can pinpoint the exact link // that failed. if r, err := p.handleEgressRouterAlert( /*@ ub, llIsNil, startLL, endLL @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } if r, err := p.validateEgressUp(); err != nil { // @ p.scionLayer.DowngradePerm(ub) - return r, err + return r, err /*@, false @*/ } - egressID := p.egressInterface() // @ p.d.getExternalMem() // @ if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) } if c, ok := p.d.external[egressID]; ok { if err := p.processEgress( /*@ ub @*/ ); err != nil { - return processResult{}, err + // @ fold p.d.validResult(processResult{}, false) + return processResult{}, err /*@, false @*/ } - return processResult{EgressID: egressID, OutConn: c, OutPkt: p.rawPkt}, nil + // @ p.d.InDomainExternalInForwardingMetrics2(egressID) + // @ fold p.d.validResult(processResult{EgressID: egressID, OutConn: c, OutPkt: p.rawPkt}, false) + return processResult{EgressID: egressID, OutConn: c, OutPkt: p.rawPkt}, nil /*@, false @*/ } // ASTransit: pkts leaving from another AS BR. @@ -2313,7 +2629,8 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ ghost if p.d.internalNextHops != nil { unfold acc(accAddr(p.d.internalNextHops), _) } if a, ok := p.d.internalNextHops[egressID]; ok { // @ p.d.getInternal() - return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil + // @ fold p.d.validResult(processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, false) + return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil /*@, false @*/ } errCode := slayers.SCMPCodeUnknownHopFieldEgress if !p.infoField.ConsDir { @@ -2321,20 +2638,21 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, } // @ TODO() // @ p.scionLayer.DowngradePerm(ub) - return p.packSCMP( + tmp, err := p.packSCMP( slayers.SCMPTypeParameterProblem, errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, ) + return tmp, err /*@, false @*/ } // @ requires acc(&p.rawPkt, R15) // @ requires p.scionLayer.Mem(p.rawPkt) // @ requires acc(&p.ingressID, R15) -// @ requires acc(&p.d, R15) && acc(MutexInvariant!(), _) +// @ requires acc(&p.d, R15) && acc(MutexInvariant(p.d), _) && p.d.WellConfigured() +// @ requires p.d.getValSvc() != nil // @ requires sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)) -// @ requires acc(&p.d.svc, _) && p.d.svc != nil // @ preserves acc(&p.mac, R10) // @ preserves p.mac != nil && p.mac.Mem() // @ preserves acc(&p.macBuffers.scionInput, R10) @@ -2344,9 +2662,17 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ ensures p.scionLayer.Mem(p.rawPkt) // @ ensures acc(&p.ingressID, R15) // @ ensures acc(&p.d, R15) -// @ ensures sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)) -// @ ensures reserr != nil ==> reserr.ErrorMem() -func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) { +// @ ensures p.d.validResult(respr, addrAliasesPkt) +// @ ensures acc(sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)), 1 - R15) +// @ ensures addrAliasesPkt ==> ( +// @ respr.OutAddr != nil && +// @ let rawPkt := p.rawPkt in +// @ (acc(respr.OutAddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(rawPkt, 0, len(rawPkt)), R15))) +// @ ensures !addrAliasesPkt ==> acc(sl.AbsSlice_Bytes(p.rawPkt, 0, len(p.rawPkt)), R15) +// @ ensures respr.OutPkt !== p.rawPkt && respr.OutPkt != nil ==> +// @ sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() +func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /*@ , addrAliasesPkt bool @*/) { // @ ghost ubScionL := p.rawPkt // @ p.scionLayer.ExtractAcc(ubScionL) s := p.scionLayer @@ -2361,15 +2687,17 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // TODO parameter problem -> invalid path // @ establishMemMalformedPath() // @ fold p.scionLayer.Mem(ubScionL) - return processResult{}, malformedPath + // @ fold p.d.validResult(processResult{}, false) + return processResult{}, malformedPath /*@ , false @*/ } if /*@ unfolding acc(s.Path.Mem(ubPath), R50) in @*/ !ohp.Info.ConsDir { // TODO parameter problem -> invalid path // @ establishMemMalformedPath() // @ defer fold p.scionLayer.Mem(ubScionL) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr( "OneHop path in reverse construction direction is not allowed", - malformedPath, "srcIA", s.SrcIA, "dstIA", s.DstIA) + malformedPath, "srcIA", s.SrcIA, "dstIA", s.DstIA) /*@ , false @*/ } // OHP leaving our IA @@ -2379,9 +2707,10 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // @ establishCannotRoute() // TODO parameter problem -> invalid path // @ defer fold p.scionLayer.Mem(ubScionL) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("bad source IA", cannotRoute, "type", "ohp", "egress", ( /*@ unfolding acc(ohp.Mem(ubPath), R50) in (unfolding acc(ohp.FirstHop.Mem(), R55) in @*/ ohp.FirstHop.ConsEgress /*@ ) @*/), - "localIA", p.d.localIA, "srcIA", s.SrcIA) + "localIA", p.d.localIA, "srcIA", s.SrcIA) /*@ , false @*/ } // @ p.d.getNeighborIAs() neighborIA, ok := p.d.neighborIAs[ /*@ unfolding acc(ohp.Mem(ubPath), R50) in (unfolding acc(ohp.FirstHop.Mem(), R55) in @*/ ohp.FirstHop.ConsEgress /*@ ) @*/] @@ -2389,15 +2718,17 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // @ establishCannotRoute() // TODO parameter problem invalid interface // @ defer fold p.scionLayer.Mem(ubScionL) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WithCtx(cannotRoute, - "type", "ohp", "egress", ( /*@ unfolding acc(ohp.Mem(ubPath), R50) in (unfolding acc(ohp.FirstHop.Mem(), R55) in @*/ ohp.FirstHop.ConsEgress /*@ ) @*/)) + "type", "ohp", "egress", ( /*@ unfolding acc(ohp.Mem(ubPath), R50) in (unfolding acc(ohp.FirstHop.Mem(), R55) in @*/ ohp.FirstHop.ConsEgress /*@ ) @*/)) /*@ , false @*/ } if !neighborIA.Equal(s.DstIA) { // @ establishCannotRoute() // @ defer fold p.scionLayer.Mem(ubScionL) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("bad destination IA", cannotRoute, "type", "ohp", "egress", ( /*@ unfolding acc(ohp.Mem(ubPath), R50) in (unfolding acc(ohp.FirstHop.Mem(), R55) in @*/ ohp.FirstHop.ConsEgress /*@ ) @*/), - "neighborIA", neighborIA, "dstIA", s.DstIA) + "neighborIA", neighborIA, "dstIA", s.DstIA) /*@ , false @*/ } // @ unfold s.Path.Mem(ubPath) // @ unfold ohp.FirstHop.Mem() @@ -2420,8 +2751,9 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // @ defer fold s.Path.Mem(ubPath) // @ defer fold ohp.FirstHop.Mem() // TODO parameter problem -> invalid MAC + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.New("MAC", "expected", fmt.Sprintf("%x", macCopy), - "actual", fmt.Sprintf("%x", ohp.FirstHop.Mac), "type", "ohp") + "actual", fmt.Sprintf("%x", ohp.FirstHop.Mac), "type", "ohp") /*@ , false @*/ } ohp.Info.UpdateSegID(ohp.FirstHop.Mac) // @ fold ohp.FirstHop.Mem() @@ -2431,7 +2763,8 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // (VerifiedSCION) the second parameter was changed from 's' to 'p.scionLayer' due to the // changes made to 'updateSCIONLayer'. if err := updateSCIONLayer(p.rawPkt, &p.scionLayer /* s */, p.buffer); err != nil { - return processResult{}, err + // @ fold p.d.validResult(processResult{}, false) + return processResult{}, err /*@ , false @*/ } // @ unfold p.scionLayer.Mem(ubScionL) // @ defer fold p.scionLayer.Mem(ubScionL) @@ -2443,14 +2776,23 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // @ p.d.getExternalMem() // @ ghost if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) } if c, ok := p.d.external[ohp.FirstHop.ConsEgress]; ok { + // (VerifiedSCION) the following must hold, obviously. + // Unfortunately, Gobra struggles with instantiating the body + // of the function. + // @ assume ohp.FirstHop.ConsEgress in p.d.getDomExternal() // buffer should already be correct + // (VerifiedSCION) TODO: we need to add a pre to run that says that the + // domain of forwardingMetrics is the same as the one for external + // @ p.d.InDomainExternalInForwardingMetrics(ohp.FirstHop.ConsEgress) + // @ fold p.d.validResult(processResult{EgressID: ohp.FirstHop.ConsEgress, OutConn: c, OutPkt: p.rawPkt}, false) return processResult{EgressID: ohp.FirstHop.ConsEgress, OutConn: c, OutPkt: p.rawPkt}, - nil + nil /*@ , false @*/ } // TODO parameter problem invalid interface // @ establishCannotRoute() + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WithCtx(cannotRoute, "type", "ohp", - "egress", ohp.FirstHop.ConsEgress, "consDir", ohp.Info.ConsDir) + "egress", ohp.FirstHop.ConsEgress, "consDir", ohp.Info.ConsDir) /*@ , false @*/ } // OHP entering our IA @@ -2458,18 +2800,20 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) if !p.d.localIA.Equal(s.DstIA) { // @ establishCannotRoute() // @ defer fold p.scionLayer.Mem(ubScionL) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("bad destination IA", cannotRoute, "type", "ohp", "ingress", p.ingressID, - "localIA", p.d.localIA, "dstIA", s.DstIA) + "localIA", p.d.localIA, "dstIA", s.DstIA) /*@ , false @*/ } // @ p.d.getNeighborIAs() neighborIA := p.d.neighborIAs[p.ingressID] if !neighborIA.Equal(s.SrcIA) { // @ establishCannotRoute() // @ defer fold p.scionLayer.Mem(ubScionL) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("bad source IA", cannotRoute, "type", "ohp", "ingress", p.ingressID, - "neighborIA", neighborIA, "srcIA", s.SrcIA) + "neighborIA", neighborIA, "srcIA", s.SrcIA) /*@ , false @*/ } // @ unfold s.Path.Mem(ubPath) @@ -2492,38 +2836,49 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error) // changes made to 'updateSCIONLayer'. // @ fold p.scionLayer.Mem(ubScionL) if err := updateSCIONLayer(p.rawPkt, &p.scionLayer /* s */, p.buffer); err != nil { - return processResult{}, err + // @ fold p.d.validResult(processResult{}, false) + return processResult{}, err /*@ , false @*/ } - // @ p.d.getSvcMem() // (VerifiedSCION) the parameter was changed from 's' to '&p.scionLayer' due to the // changes made to 'resolveLocalDst'. - a, err := p.d.resolveLocalDst(&p.scionLayer /* s */ /*@ , ubScionL @*/) + a, err /*@ , addrAliases @*/ := p.d.resolveLocalDst(&p.scionLayer /* s */ /*@ , ubScionL @*/) if err != nil { - return processResult{}, err + // @ ghost if addrAliases { + // @ apply acc(a.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ubScionL, 0, len(ubScionL)), R15) + // @ } + // @ fold p.d.validResult(processResult{}, false) + return processResult{}, err /*@ , false @*/ } // @ p.d.getInternal() - return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil + // @ assert p.d.internal != nil ==> acc(p.d.internal.Mem(), _) + // @ fold p.d.validResult(processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, addrAliases) + return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil /*@ , addrAliases @*/ } -// @ requires acc(MutexInvariant!(), _) -// @ requires acc(&d.svc, _) && d.svc != nil -// @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) +// @ requires acc(MutexInvariant(d), _) +// @ requires d.getValSvc() != nil +// @ requires acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) // @ preserves acc(s.Mem(ub), R14) +// @ ensures !addrAliasesUb ==> acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) +// @ ensures !addrAliasesUb && resaddr != nil ==> acc(resaddr.Mem(), _) +// @ ensures addrAliasesUb ==> resaddr != nil +// @ ensures addrAliasesUb ==> acc(resaddr.Mem(), R15) +// @ ensures addrAliasesUb ==> (acc(resaddr.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15)) // @ ensures reserr != nil ==> reserr.ErrorMem() // (VerifiedSCION) the type of 's' was changed from slayers.SCION to *slayers.SCION. This makes // specs a lot easier and, makes the implementation faster as well by avoiding passing large data-structures // by value. We should consider porting merging this in upstream SCION. -func (d *DataPlane) resolveLocalDst(s *slayers.SCION /*@, ghost ub []byte @*/) (resaddr *net.UDPAddr, reserr error) { +func (d *DataPlane) resolveLocalDst(s *slayers.SCION /*@, ghost ub []byte @*/) (resaddr *net.UDPAddr, reserr error /*@ , addrAliasesUb bool @*/) { // @ ghost start, end := s.ExtractAcc(ub) // @ assert s.RawDstAddr === ub[start:end] // @ sl.SplitRange_Bytes(ub, start, end, R15) // @ assert acc(sl.AbsSlice_Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R15) dst, err := s.DstAddr() - // @ sl.CombineRange_Bytes(ub, start, end, R15) // @ apply acc(s, R16) --* acc(s.Mem(ub), R15) if err != nil { + // @ sl.CombineRange_Bytes(ub, start, end, R15) // TODO parameter problem. - return nil, err + return nil, err /*@ , false @*/ } switch v := dst.(type) { case addr.HostSVC: @@ -2532,24 +2887,54 @@ func (d *DataPlane) resolveLocalDst(s *slayers.SCION /*@, ghost ub []byte @*/) ( // @ d.getSvcMem() a, ok := d.svc.Any(v.Base()) if !ok { + // @ apply acc(dst.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub[start:end], 0, len(ub[start:end])), R15) + // @ sl.CombineRange_Bytes(ub, start, end, R15) // @ establishNoSVCBackend() - return nil, noSVCBackend + return nil, noSVCBackend /*@ , false @*/ } - return a, nil + // @ apply acc(dst.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub[start:end], 0, len(ub[start:end])), R15) + // @ sl.CombineRange_Bytes(ub, start, end, R15) + return a, nil /*@ , false @*/ case *net.IPAddr: - return addEndhostPort(v), nil + tmp := addEndhostPort(v) + // @ package acc(tmp.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R15) { + // @ apply acc(tmp.Mem(), R15) --* acc(v.Mem(), R15) + // @ assert acc(dst.Mem(), R15) + // @ apply acc(dst.Mem(), R15) --* acc(sl.AbsSlice_Bytes(ub[start:end], 0, len(ub[start:end])), R15) + // @ sl.CombineRange_Bytes(ub, start, end, R15) + // @ } + return tmp, nil /*@ , true @*/ default: panic("unexpected address type returned from DstAddr") } } -// @ preserves acc(&dst.IP, R20) -// @ ensures acc(res) -// @ ensures res.IP === dst.IP -// @ ensures res.Port == topology.EndhostPort +// (VerifiedSCION) marked as trusted due to an incompletness in silicon, +// where it is failing to prove the body of a predicate right after unfolding it. +// @ trusted +// @ requires acc(dst.Mem(), R15) +// @ ensures res != nil && acc(res.Mem(), R15) +// @ ensures acc(res.Mem(), R15) --* acc(dst.Mem(), R15) // @ decreases func addEndhostPort(dst *net.IPAddr) (res *net.UDPAddr) { - return &net.UDPAddr{IP: dst.IP, Port: topology.EndhostPort} + // @ unfold acc(dst.Mem(), R15) + tmp := &net.UDPAddr{IP: dst.IP, Port: topology.EndhostPort} + // @ assert forall i int :: { &tmp.IP[i] } 0 <= i && i < len(tmp.IP) ==> acc(&tmp.IP[i], R15) + // @ fold acc(sl.AbsSlice_Bytes(tmp.IP, 0, len(tmp.IP)), R15) + // @ fold acc(tmp.Mem(), R15) + // @ package (acc(tmp.Mem(), R15) --* acc(dst.Mem(), R15)) { + // @ assert acc(dst, R15) + // @ assert acc(tmp, R50) + // @ assert dst.IP === tmp.IP + // @ unfold acc(tmp.Mem(), R15) + // @ unfold acc(sl.AbsSlice_Bytes(tmp.IP, 0, len(tmp.IP)), R15) + // (VerifiedSCION) this is the failling assertion; + // TODO: report it! + // @ assert forall i int :: { &tmp.IP[i] } 0 <= i && i < len(tmp.IP) ==> acc(&tmp.IP[i], R15) + // @ assert forall i int :: { &dst.IP[i] } 0 <= i && i < len(dst.IP) ==> acc(&dst.IP[i], R15) + // @ fold acc(dst.Mem(), R15) + // @ } + return tmp } // TODO(matzf) this function is now only used to update the OneHop-path. @@ -2686,7 +3071,7 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { return err } -// @ requires acc(&p.d, _) && acc(MutexInvariant!(), _) +// @ requires acc(&p.d, _) && acc(MutexInvariant(p.d), _) // @ 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 b499388ca..da6a122f6 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -21,8 +21,13 @@ import ( "hash" "net" + "github.com/google/gopacket" + "github.com/scionproto/scion/pkg/addr" "github.com/scionproto/scion/pkg/scrypto" + "github.com/scionproto/scion/pkg/slayers" + "github.com/scionproto/scion/pkg/slayers/path" + "github.com/scionproto/scion/pkg/slayers/path/scion" underlayconn "github.com/scionproto/scion/private/underlay/conn" . "github.com/scionproto/scion/verification/utils/definitions" @@ -162,90 +167,253 @@ ensures forall i int :: {res[i]} 0 <= i && i < len(res) ==> res[i] == offsetPai decreases func newOffsetPair(n int) (res seq[offsetPair]) -/**** Acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/ 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), _) ensures acc(&d.internalNextHops, _) ensures d.internalNextHops != nil ==> acc(accAddr(d.internalNextHops), _) decreases func (d *DataPlane) getInternalNextHops() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) ensures acc(&d.forwardingMetrics, _) ensures d.forwardingMetrics != nil ==> acc(accForwardingMetrics(d.forwardingMetrics), _) decreases func (d *DataPlane) getForwardingMetrics() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) +// 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. +decreases _ +pure func (d *DataPlane) getValForwardingMetrics() map[uint16]forwardingMetrics { + return unfolding acc(MutexInvariant(d), _) in d.forwardingMetrics +} + +ghost +requires acc(MutexInvariant(d), _) +// 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. +decreases _ +pure func (d *DataPlane) getDomForwardingMetrics() set[uint16] { + return unfolding acc(MutexInvariant(d), _) in + d.forwardingMetrics == nil ? + set[uint16]{} : + (unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in + domain(d.forwardingMetrics)) +} + +ghost +requires acc(MutexInvariant(d), _) +// 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. +decreases _ +pure func (d *DataPlane) getDomExternal() set[uint16] { + return unfolding acc(MutexInvariant(d), _) in + d.external == nil ? + set[uint16]{} : + (unfolding acc(accBatchConn(d.external), _) in + domain(d.external)) +} + +ghost +requires acc(MutexInvariant(d), _) +decreases +pure func (d *DataPlane) WellConfigured() bool { + return d.getDomExternal() == d.getDomForwardingMetrics() +} + +ghost +requires acc(MutexInvariant(d), _) +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), _) + assert id in d.getDomForwardingMetrics() + assert d.getDomForwardingMetrics() == (d.forwardingMetrics == nil ? + set[uint16]{} : + (unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in + domain(d.forwardingMetrics))) + assert id in (d.forwardingMetrics == nil ? + set[uint16]{} : + (unfolding acc(accForwardingMetrics(d.forwardingMetrics), _) in + domain(d.forwardingMetrics))) + unfold acc(accForwardingMetrics(d.forwardingMetrics), _) + assert id in domain(d.forwardingMetrics) +} + +ghost +requires acc(MutexInvariant(d), _) ensures acc(&d.external, _) && (d.external != nil ==> acc(accBatchConn(d.external), _)) decreases func (d *DataPlane) getExternalMem() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) ensures acc(&d.linkTypes, _) && (d.linkTypes != nil ==> acc(d.linkTypes, _)) decreases func (d *DataPlane) getLinkTypesMem() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) ensures acc(&d.localIA, _) decreases func (d *DataPlane) getLocalIA() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) ensures acc(&d.neighborIAs, _) && (d.neighborIAs != nil ==> acc(d.neighborIAs, _)) decreases func (d *DataPlane) getNeighborIAs() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) -ensures acc(&d.svc, _) && (d.svc != nil ==> acc(d.svc.Mem(), _)) +requires acc(MutexInvariant(d), _) && d.getValSvc() != nil +ensures acc(&d.svc, _) && d.svc != nil && acc(d.svc.Mem(), _) decreases func (d *DataPlane) getSvcMem() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) +// 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. +decreases _ +pure func (d *DataPlane) getValSvc() *services { + return unfolding acc(MutexInvariant(d), _) in d.svc +} + +ghost +requires acc(MutexInvariant(d), _) ensures acc(&d.bfdSessions, _) && (d.bfdSessions != nil ==> acc(accBfdSession(d.bfdSessions), _)) decreases func (d *DataPlane) getBfdSessionsMem() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) ensures acc(&d.internal, _) && (d.internal != nil ==> acc(d.internal.Mem(), _)) decreases func (d *DataPlane) getInternal() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) ensures acc(&d.macFactory, _) decreases func (d *DataPlane) getMacFactoryMem() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } ghost -requires acc(MutexInvariant!(), _) +requires acc(MutexInvariant(d), _) 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)), _) @@ -253,7 +421,7 @@ ensures scrypto.ValidKeyForHash(*d.key) ensures d.macFactory implements MacFactorySpec{d.key} decreases func (d *DataPlane) getNewPacketProcessorFootprint() { - unfold acc(MutexInvariant!(), _) + unfold acc(MutexInvariant(d), _) } /**** End of acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/ @@ -273,6 +441,8 @@ func closureSpec3(c BatchConn) /** End of closure specs for the Run method **/ /** 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 && acc(&writeMsgs[0]) && @@ -313,4 +483,144 @@ pure decreases func (s *scmpError) CanSet(e error) bool { return typeOf(e) == type[scmpError] +} + +/** spec for newPacketProcessor **/ + +// initial state, established after allocating with newPacketProcessor. +pred (s* scionPacketProcessor) sInit() { + acc(&s.d) && + acc(&s.ingressID) && + acc(&s.buffer) && s.buffer != nil && + s.buffer.Mem() && + acc(&s.mac) && s.mac != nil && s.mac.Mem() && + s.scionLayer.NonInitMem() && + // The following is not necessary + // s.scionLayer.PathPoolInitializedNonInitMem() && + s.hbhLayer.NonInitMem() && + s.e2eLayer.NonInitMem() && + acc(&s.lastLayer) && + acc(&s.path) && + acc(&s.hopField) && + acc(&s.infoField) && + acc(&s.segmentChange) && + acc(&s.cachedMac) && + acc(&s.macBuffers) && + sl.AbsSlice_Bytes(s.macBuffers.scionInput, 0, len(s.macBuffers.scionInput)) && + s.bfdLayer.NonInitMem() && + acc(&s.srcAddr) && + acc(&s.rawPkt) +} + +// each ghost method on *scionPacketProcessor has, in the name, the state in which it +// expects to find the packet processor. In the case below, the state `Init` is expected. +ghost +requires acc(s.sInit(), _) +decreases +pure func (s* scionPacketProcessor) sInitD() (res *DataPlane) { + return unfolding acc(s.sInit(), _) in s.d +} + +ghost +requires acc(s.sInit(), _) +decreases +pure func (s* scionPacketProcessor) sInitRawPkt() (res []byte) { + return unfolding acc(s.sInit(), _) in s.rawPkt +} + +ghost +requires acc(s.sInit(), _) +decreases +pure func (s* scionPacketProcessor) sInitPath() (res *scion.Raw) { + return unfolding acc(s.sInit(), _) in s.path +} + +ghost +requires acc(s.sInit(), _) +decreases +pure func (s* scionPacketProcessor) sInitHopField() (res path.HopField) { + return unfolding acc(s.sInit(), _) in s.hopField +} + +ghost +requires acc(s.sInit(), _) +decreases +pure func (s* scionPacketProcessor) sInitInfoField() (res path.InfoField) { + return unfolding acc(s.sInit(), _) in s.infoField +} + +ghost +requires acc(s.sInit(), _) +decreases +pure func (s* scionPacketProcessor) sInitSegmentChange() (res bool) { + return unfolding acc(s.sInit(), _) in s.segmentChange +} + +/** end spec for newPacketProcessor **/ + +/** **/ + +ghost +requires hasScionLayer ==> scionLayer.Mem(ubScionLayer) +requires hasHbhLayer ==> hbhLayer.Mem(ubHbhLayer) +requires hasE2eLayer ==> e2eLayer.Mem(ubE2eLayer) +ensures hasScionLayer ==> scionLayer.NonInitMem() +ensures hasHbhLayer ==> hbhLayer.NonInitMem() +ensures hasE2eLayer ==> e2eLayer.NonInitMem() +decreases +func ResetDecodingLayers( + scionLayer *slayers.SCION, + hbhLayer *slayers.HopByHopExtnSkipper, + e2eLayer *slayers.EndToEndExtnSkipper, + ubScionLayer []byte, + ubHbhLayer []byte, + ubE2eLayer []byte, + hasScionLayer bool, + hasHbhLayer bool, + hasE2eLayer bool, +) { + if hasScionLayer { + scionLayer.DowngradePerm(ubScionLayer) + } + if hasHbhLayer { + hbhLayer.DowngradePerm(ubHbhLayer) + } + if hasE2eLayer { + e2eLayer.DowngradePerm(ubE2eLayer) + } +} + +/** **/ +pred (d *DataPlane) validResult(result processResult, addrAliasesPkt bool) { + acc(MutexInvariant(d), _) && + // EgressID + (result.EgressID != 0 ==> result.EgressID in d.getDomForwardingMetrics()) && + // OutConn + (result.OutConn != nil ==> acc(result.OutConn.Mem(), _)) && + // OutAddr + (addrAliasesPkt && result.OutAddr != nil ==> acc(result.OutAddr.Mem(), R15)) && + (!addrAliasesPkt && result.OutAddr != nil ==> acc(result.OutAddr.Mem(), _)) + // OutPkt moved out +} + +ghost +requires acc(MutexInvariant(d), _) && d.WellConfigured() +requires id in d.getDomExternal() +ensures acc(MutexInvariant(d), _) +ensures id in d.getDomForwardingMetrics() +decreases +func (d *DataPlane) InDomainExternalInForwardingMetrics(id uint16) { + +} + +ghost +requires acc(MutexInvariant(d), _) && d.WellConfigured() +requires acc(&d.external, _) && acc(d.external, _) +requires id in domain(d.external) +ensures acc(MutexInvariant(d), _) +ensures id in d.getDomForwardingMetrics() +decreases +func (d *DataPlane) InDomainExternalInForwardingMetrics2(id uint16) { + unfold acc(MutexInvariant(d), _) + unfold acc(accBatchConn(d.external), _) } \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra index 90ab85a07..4d28c738d 100644 --- a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra @@ -1,6 +1,13 @@ // Specification for package "golang.org/x/net/internal/socket" // Based on file https://github.com/golang/net/blob/master/internal/socket/socket.go +// This file is specialized for the case where all instances m of message +// satisfy the property len(m.Buffers) == 1, which is the case in the router. +// The old file (socket.gobra.old) contains more general definitions, +// but this is unnecessary for the SCION router and requires us proving +// many additional lemmas, e.g., that the following is injective: +// forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i]) + // +gobra package socket @@ -8,7 +15,7 @@ package socket import ( "net" - "github.com/scionproto/scion/verification/utils/slices" + sl "github.com/scionproto/scion/verification/utils/slices" ) @@ -34,104 +41,73 @@ type Message struct { N int // # of bytes read or written from/to Buffers NN int // # of bytes read or written from/to OOB Flags int // protocol-specific information on the received message -} -pred (m *Message) Mem(lenBuffers int) { - acc(m) && - len(m.Buffers) == lenBuffers && - (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> (acc(&m.Buffers[i]) && slices.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && - slices.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && - // typeOf(m.Addr) == type[*net.UDPAddr] && - (m.Addr != nil ==> acc(m.Addr.Mem(), _)) && - 0 <= m.N + // (VerifiedSCION) the following are, morally, ghost fields: + // is it still ok to read the Addr of the Message? + IsActive bool + // do we have a fixed amount of perms to the Addr or a wildcard amount? + WildcardPerm bool } -pred (m *Message) MemWithoutHalf(lenBuffers int) { - acc(m, 1/2) && - len(m.Buffers) == lenBuffers && - (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> (acc(&m.Buffers[i]) && slices.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && - slices.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && +pred (m *Message) Mem() { + acc(m) && + len(m.Buffers) == 1 && + acc(&m.Buffers[0]) && + sl.AbsSlice_Bytes(m.Buffers[0], 0, len(m.Buffers[0])) && + sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && // typeOf(m.Addr) == type[*net.UDPAddr] && - (m.Addr != nil ==> acc(m.Addr.Mem(), _)) && + ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && + ((m.Addr != nil && m.IsActive && m.WildcardPerm) ==> acc(m.Addr.Mem(), _)) && 0 <= m.N } ghost -requires acc(m.Mem(lenBuffers), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetAddr(lenBuffers int) net.Addr { - return unfolding acc(m.Mem(lenBuffers), _) in m.Addr +pure func (m *Message) HasWildcardPermAddr() bool { + return unfolding acc(m.Mem(), _) in m.WildcardPerm } ghost -requires acc(m.MemWithoutHalf(lenBuffers), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetAddrWithoutHalf(lenBuffers int) net.Addr { - return unfolding acc(m.MemWithoutHalf(lenBuffers), _) in m.Addr +pure func (m *Message) HasActiveAddr() bool { + return unfolding acc(m.Mem(), _) in m.IsActive } ghost -requires acc(m.Mem(lenBuffers), _) -requires 0 <= i && i < lenBuffers +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetBuffer(lenBuffers int, i int) []byte { - return unfolding acc(m.Mem(lenBuffers), _) in m.Buffers[i] +pure func (m *Message) GetAddr() net.Addr { + return unfolding acc(m.Mem(), _) in m.Addr } -// Only defined for the case where lenBuffers == 1 ghost -requires acc(m.Mem(1), _) +requires acc(m.Mem(), _) decreases -pure func (m *Message) GetFstBuffer() []byte { - return unfolding acc(m.Mem(1), _) in m.Buffers[0] +pure func (m *Message) GetMessage() Message { + return unfolding acc(m.Mem(), _) in *m } -// Only defined for the case where lenBuffers == 1 -ghost -requires acc(m.Mem(1), _) -decreases -pure func (m *Message) GetN() int { - return unfolding acc(m.Mem(1), _) in m.N -} ghost -requires m.Mem(1) -ensures acc(m, 1/2) && m.MemWithoutHalf(1) -ensures old(m.GetAddr(1)) === m.GetAddrWithoutHalf(1) -ensures m.N == old(unfolding m.Mem(1) in m.N) -ensures m.Buffers === old(unfolding m.Mem(1) in m.Buffers) -ensures old(m.GetFstBuffer()) === unfolding m.MemWithoutHalf(1) in m.Buffers[0] -ensures old(m.GetN()) == m.N +requires acc(m.Mem(), _) decreases -func (m *Message) SplitPerm() { - unfold m.Mem(1) - fold m.MemWithoutHalf(1) +pure func (m *Message) GetBuffer() []byte { + return unfolding acc(m.Mem(), _) in m.Buffers[0] } ghost -requires acc(m, 1/2) && m.MemWithoutHalf(1) -ensures m.Mem(1) -ensures m.GetAddr(1) === old(m.GetAddrWithoutHalf(1)) -ensures old(m.N) == unfolding m.Mem(1) in m.N -ensures m.GetFstBuffer() === old(unfolding m.MemWithoutHalf(1) in m.Buffers[0]) -ensures unfolding m.Mem(1) in m.Buffers === old(m.Buffers) -ensures m.GetN() == old(m.N) +requires acc(m.Mem(), _) decreases -func (m *Message) CombinePerm() { - unfold m.MemWithoutHalf(1) - fold m.Mem(1) +pure func (m *Message) GetFstBuffer() []byte { + return unfolding acc(m.Mem(), _) in m.Buffers[0] } ghost -requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].Mem(1) -ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) +requires acc(m.Mem(), _) +ensures 0 <= res decreases -func SplitPermMsgs(msgs []Message) { - invariant 0 <= i && i <= len(msgs) - invariant forall j int :: { &msgs[j] } i <= j && j < len(msgs) ==> msgs[j].Mem(1) - invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) - decreases len(msgs) - i - for i := 0; i < len(msgs); i++ { - msgs[i].SplitPerm() - } -} \ No newline at end of file +pure func (m *Message) GetN() (res int) { + return unfolding acc(m.Mem(), _) in m.N +} diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old new file mode 100644 index 000000000..e61f20e9f --- /dev/null +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra.old @@ -0,0 +1,186 @@ +// Specification for package "golang.org/x/net/internal/socket" +// Based on file https://github.com/golang/net/blob/master/internal/socket/socket.go + +package socket + +import ( + "net" + + sl "github.com/scionproto/scion/verification/utils/slices" +) + + +// A Message represents an IO message. +type Message struct { + // When writing, the Buffers field must contain at least one + // byte to write. + // When reading, the Buffers field will always contain a byte + // to read. + Buffers [][]byte + + // OOB contains protocol-specific control or miscellaneous + // ancillary data known as out-of-band data. + OOB []byte + + // Addr specifies a destination address when writing. + // It can be nil when the underlying protocol of the raw + // connection uses connection-oriented communication. + // After a successful read, it may contain the source address + // on the received packet. + Addr net.Addr + + N int // # of bytes read or written from/to Buffers + NN int // # of bytes read or written from/to OOB + Flags int // protocol-specific information on the received message + + // (VerifiedSCION) the following are, morally, ghost fields: + // is it still ok to read the buffers and Addr of the Message? + IsActive bool + // do we have a fixed amount of perms to the Addr a wildcard amount? + WildcardPerm bool +} + +pred (m *Message) Mem(lenBuffers int) { + acc(m) && + len(m.Buffers) == lenBuffers && + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i])) && + (m.IsActive ==> + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> + sl.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && + sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && + // typeOf(m.Addr) == type[*net.UDPAddr] && + ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && + ((m.Addr != nil && m.IsActive && m.WildcardPerm) ==> acc(m.Addr.Mem(), _)) && + 0 <= m.N +} + +pred (m *Message) MemWithoutHalf(lenBuffers int) { + acc(m, 1/2) && + len(m.Buffers) == lenBuffers && + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> acc(&m.Buffers[i])) && + (m.IsActive ==> + (forall i int :: { &m.Buffers[i] } 0 <= i && i < len(m.Buffers) ==> + sl.AbsSlice_Bytes(m.Buffers[i], 0, len(m.Buffers[i])))) && + sl.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) && + // typeOf(m.Addr) == type[*net.UDPAddr] && + ((m.Addr != nil && m.IsActive && !m.WildcardPerm) ==> m.Addr.Mem()) && + ((m.Addr != nil && m.IsActive && m.WildcardPerm) ==> acc(m.Addr.Mem(), _)) && + 0 <= m.N +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) HasWildcardPermAddr(lenBuffers int) bool { + return unfolding acc(m.Mem(lenBuffers), _) in m.WildcardPerm +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) HasActiveBuffers(lenBuffers int) bool { + return unfolding acc(m.Mem(lenBuffers), _) in m.IsActive +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) GetAddr(lenBuffers int) net.Addr { + return unfolding acc(m.Mem(lenBuffers), _) in m.Addr +} + +ghost +requires acc(m.Mem(lenBuffers), _) +decreases +pure func (m *Message) GetMessage(lenBuffers int) Message { + return unfolding acc(m.Mem(lenBuffers), _) in *m +} + +ghost +requires acc(m.MemWithoutHalf(lenBuffers), _) +decreases +pure func (m *Message) GetAddrWithoutHalf(lenBuffers int) net.Addr { + return unfolding acc(m.MemWithoutHalf(lenBuffers), _) in m.Addr +} + +ghost +requires acc(m.Mem(lenBuffers), _) +requires 0 <= i && i < lenBuffers +decreases +pure func (m *Message) GetBuffer(lenBuffers int, i int) []byte { + return unfolding acc(m.Mem(lenBuffers), _) in m.Buffers[i] +} + +// Only defined for the case where lenBuffers == 1 +ghost +requires acc(m.Mem(1), _) +decreases +pure func (m *Message) GetFstBuffer() []byte { + return unfolding acc(m.Mem(1), _) in m.Buffers[0] +} + +// Only defined for the case where lenBuffers == 1 +ghost +requires acc(m.Mem(1), _) +decreases +pure func (m *Message) GetN() int { + return unfolding acc(m.Mem(1), _) in m.N +} + +ghost +requires m.Mem(1) +ensures acc(m, 1/2) && m.MemWithoutHalf(1) +ensures old(m.GetAddr(1)) === m.GetAddrWithoutHalf(1) +ensures m.N == old(unfolding m.Mem(1) in m.N) +ensures m.Buffers === old(unfolding m.Mem(1) in m.Buffers) +ensures old(m.GetFstBuffer()) === unfolding m.MemWithoutHalf(1) in m.Buffers[0] +ensures old(m.GetN()) == m.N +ensures old(m.HasWildcardPermAddr(1)) == m.WildcardPerm +ensures old(m.HasActiveBuffers(1)) == m.IsActive +ensures old(m.GetMessage(1)) === *m +decreases +func (m *Message) SplitPerm() { + unfold m.Mem(1) + fold m.MemWithoutHalf(1) +} + +ghost +requires acc(m, 1/2) && m.MemWithoutHalf(1) +ensures m.Mem(1) +ensures m.GetAddr(1) === old(m.GetAddrWithoutHalf(1)) +ensures old(m.N) == unfolding m.Mem(1) in m.N +ensures m.GetFstBuffer() === old(unfolding m.MemWithoutHalf(1) in m.Buffers[0]) +ensures unfolding m.Mem(1) in m.Buffers === old(m.Buffers) +ensures m.GetN() == old(m.N) +ensures m.HasWildcardPermAddr(1) == old(m.WildcardPerm) +ensures m.HasActiveBuffers(1) == old(m.IsActive) +ensures m.GetMessage(1) === old(*m) +decreases +func (m *Message) CombinePerm() { + unfold m.MemWithoutHalf(1) + fold m.Mem(1) +} + +ghost +requires forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].Mem(1) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> old(msgs[j].GetMessage(1)) === msgs[j] +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) +ensures forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==> msgs[j].IsActive == old(msgs[j].HasActiveBuffers(1)) +decreases +func SplitPermMsgs(msgs []Message) { + invariant 0 <= i && i <= len(msgs) + invariant forall j int :: { &msgs[j] } i <= j && j < len(msgs) ==> msgs[j].Mem(1) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> acc(&msgs[j], 1/2) && msgs[j].MemWithoutHalf(1) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].IsActive == old(msgs[j].HasActiveBuffers(1)) + invariant forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j] === old(msgs[j].GetMessage(1)) + invariant forall j int :: { &msgs[j] } i <= j && j < len(msgs) ==> msgs[j].GetMessage(1) === old(msgs[j].GetMessage(1)) + decreases len(msgs) - i + for i := 0; i < len(msgs); i++ { + assert forall j int :: { &msgs[j] }{ &msgs[j].WildcardPerm } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) + msgs[i].SplitPerm() + assert forall j int :: { &msgs[j] } 0 <= j && j < i ==> msgs[j].WildcardPerm == old(msgs[j].HasWildcardPermAddr(1)) + assert msgs[i].WildcardPerm == old(msgs[i].HasWildcardPermAddr(1)) + } +} \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra b/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra index c045b5147..21b652166 100644 --- a/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket_test.gobra @@ -21,5 +21,7 @@ import "github.com/scionproto/scion/verification/utils/slices" func foldMem_test() { var m@ Message fold slices.AbsSlice_Bytes(m.OOB, 0, len(m.OOB)) - fold m.Mem(0) + m.Buffers = make([][]byte, 1) + fold slices.AbsSlice_Bytes(m.Buffers[0], 0, len(m.Buffers[0])) + fold m.Mem() } \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra index 39557db4d..38c0cf5e7 100644 --- a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra +++ b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra @@ -229,11 +229,11 @@ func NewRawConn(c net.PacketConn) (r *RawConn, err error) { trusted preserves acc(c.Mem(), _) preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> - (&ms[i]).Mem(lenBuffers) + (&ms[i]).Mem() ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> (0 <= n && n <= len(ms)) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) ReadBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.ReadBatch(ms, flags) } @@ -242,11 +242,11 @@ func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers // It returns the number of messages written on a successful write. trusted preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> - acc((&ms[i]).Mem(lenBuffers), R10) + acc((&ms[i]).Mem(), R10) preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> 0 <= n && n <= len(ms) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) WriteBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) WriteBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.WriteBatch(ms, flags) } \ No newline at end of file diff --git a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra index b5744863e..aee3a6c80 100644 --- a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra +++ b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra @@ -163,12 +163,12 @@ func (p *PacketConn) ExchangeWildcardPerm() (c net.PacketConn) // to len(ms). trusted preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> - (&ms[i]).Mem(lenBuffers) + (&ms[i]).Mem() preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> (0 <= n && n <= len(ms)) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) ReadBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.ReadBatch(ms, flags) } @@ -176,11 +176,11 @@ func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers // WriteBatch writes a batch of messages. // It returns the number of messages written on a successful write. trusted -preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> acc((&ms[i]).Mem(lenBuffers), R10) +preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> acc((&ms[i]).Mem(), R10) preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> 0 <= n && n <= len(ms) ensures err != nil ==> err.ErrorMem() -func (c *PacketConn) WriteBatch(ms []socket.Message, flags int, ghost lenBuffers int) (n int, err error) { +func (c *PacketConn) WriteBatch(ms []socket.Message, flags int) (n int, err error) { return c.payloadHandler.WriteBatch(ms, flags) } \ No newline at end of file diff --git a/verification/dependencies/net/udpsock.gobra b/verification/dependencies/net/udpsock.gobra index 5b0706ddb..20d23a34e 100644 --- a/verification/dependencies/net/udpsock.gobra +++ b/verification/dependencies/net/udpsock.gobra @@ -24,7 +24,7 @@ type UDPAddr struct { pred (a *UDPAddr) Mem() { // The second conjunct should be eventually replaced by a.IP.Mem(). // However, doing this at the moment requires changes in the VerifiedSCION codebase. - acc(a) && slices.AbsSlice_Bytes(a.IP, 0, len(a.IP)) + acc(a, R5) && slices.AbsSlice_Bytes(a.IP, 0, len(a.IP)) } (*UDPAddr) implements Addr { diff --git a/verification/utils/definitions/definitions.gobra b/verification/utils/definitions/definitions.gobra index 910e8c3e9..b7086de2a 100644 --- a/verification/utils/definitions/definitions.gobra +++ b/verification/utils/definitions/definitions.gobra @@ -96,6 +96,11 @@ ensures false decreases _ func IgnoreBranch() +ghost +ensures false +decreases _ +func IgnoreFromHere() + ghost ensures false decreases _