diff --git a/.gitignore b/.gitignore index bf68af4a1..f83e054de 100644 --- a/.gitignore +++ b/.gitignore @@ -100,4 +100,5 @@ target *.gobrafied *.internal .devcontainer +.metals .gobra diff --git a/private/underlay/conn/conn.go b/private/underlay/conn/conn.go index 3518125e0..dcdaaf045 100644 --- a/private/underlay/conn/conn.go +++ b/private/underlay/conn/conn.go @@ -44,29 +44,29 @@ type Messages []ipv4.Message type Conn interface { //@ pred Mem() // (VerifiedSCION) Reads a message to b. Returns the number of read bytes. - //@ preserves Mem() + //@ requires acc(Mem(), _) //@ preserves slices.AbsSlice_Bytes(b, 0, len(b)) //@ ensures err == nil ==> 0 <= n && n <= len(b) //@ ensures err == nil ==> acc(addr.Mem(), _) //@ ensures err != nil ==> err.ErrorMem() ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) - //@ preserves Mem() + //@ requires acc(Mem(), _) //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> m[i].Mem(1) //@ ensures err == nil ==> 0 <= n && n <= len(m) //@ ensures err != nil ==> err.ErrorMem() ReadBatch(m Messages) (n int, err error) - //@ preserves Mem() + //@ requires acc(Mem(), _) //@ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R10) //@ ensures err == nil ==> 0 <= n && n <= len(b) //@ ensures err != nil ==> err.ErrorMem() Write(b []byte) (n int, err error) //@ requires acc(u.Mem(), _) - //@ preserves Mem() + //@ requires acc(Mem(), _) //@ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R10) //@ ensures err == nil ==> 0 <= n && n <= len(b) //@ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, u *net.UDPAddr) (n int, err error) - //@ preserves Mem() + //@ requires acc(Mem(), _) //@ preserves forall i int :: { &m[i] } 0 <= i && i < len(m) ==> acc(m[i].Mem(1), R10) //@ ensures err == nil ==> 0 <= n && n <= len(m) //@ ensures err != nil ==> err.ErrorMem() @@ -163,25 +163,23 @@ 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. -// @ preserves c.Mem() +// @ requires acc(c.Mem(), _) // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) // @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs) // @ ensures errRet != nil ==> errRet.ErrorMem() func (c *connUDPIPv4) ReadBatch(msgs Messages) (nRet int, errRet error) { - //@ unfold c.Mem() + //@ 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 @*/) - //@ fold c.Mem() return n, err } -// @ preserves c.Mem() +// @ requires acc(c.Mem(), _) // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), 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 c.Mem() - //@ defer fold c.Mem() + //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/) } @@ -239,25 +237,23 @@ 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. -// @ preserves c.Mem() +// @ requires acc(c.Mem(), _) // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem(1) // @ ensures errRet == nil ==> 0 <= nRet && nRet <= len(msgs) // @ ensures errRet != nil ==> errRet.ErrorMem() func (c *connUDPIPv6) ReadBatch(msgs Messages) (nRet int, errRet error) { - //@ unfold c.Mem() + //@ 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 @*/) - //@ fold c.Mem() return n, err } -// @ preserves c.Mem() +// @ requires acc(c.Mem(), _) // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> acc(msgs[i].Mem(1), 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 c.Mem() - //@ defer fold c.Mem() + //@ unfold acc(c.Mem(), _) // (VerifiedSCION) 1 is the length of the buffers of the messages in msgs return c.pconn.WriteBatch(msgs, flags /*@, 1 @*/) } @@ -398,38 +394,35 @@ func (cc *connUDPBase) initConnUDP(network string, laddr, raddr *net.UDPAddr, cf return nil } -// @ preserves c.Mem() +// @ preserves acc(c.Mem(), _) // @ preserves slices.AbsSlice_Bytes(b, 0, len(b)) -// @ preserves unfolding c.Mem() in c.conn == underlyingConn +// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn // @ ensures err == nil ==> 0 <= n && n <= len(b) // @ ensures err == nil ==> acc(addr.Mem(), _) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPBase) ReadFrom(b []byte /*@, ghost underlyingConn *net.UDPConn @*/) (n int, addr *net.UDPAddr, err error) { - //@ unfold c.Mem() - //@ defer fold c.Mem() + //@ unfold acc(c.Mem(), _) return c.conn.ReadFromUDP(b) } -// @ preserves c.Mem() +// @ preserves acc(c.Mem(), _) // @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) -// @ preserves unfolding c.Mem() in c.conn == underlyingConn +// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn // @ ensures err == nil ==> 0 <= n && n <= len(b) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPBase) Write(b []byte /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) { - //@ unfold c.Mem() - //@ defer fold c.Mem() + //@ unfold acc(c.Mem(), _) return c.conn.Write(b) } // @ requires acc(dst.Mem(), _) -// @ preserves c.Mem() -// @ preserves unfolding c.Mem() in c.conn == underlyingConn +// @ preserves acc(c.Mem(), _) +// @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn // @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) // @ ensures err == nil ==> 0 <= n && n <= len(b) // @ ensures err != nil ==> err.ErrorMem() func (c *connUDPBase) WriteTo(b []byte, dst *net.UDPAddr /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) { - //@ unfold c.Mem() - //@ defer fold c.Mem() + //@ unfold acc(c.Mem(), _) if c.Remote != nil { return c.conn.Write(b) } @@ -475,7 +468,7 @@ func (c *connUDPBase) Close() (err error) { 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] } (i0 <= j && j < len(m)) ==> acc(&m[j]) + //@ 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 //@ decreases len(m) - i diff --git a/private/underlay/conn/conn_spec.gobra b/private/underlay/conn/conn_spec.gobra index 40829f4f1..298e98721 100644 --- a/private/underlay/conn/conn_spec.gobra +++ b/private/underlay/conn/conn_spec.gobra @@ -65,74 +65,55 @@ pred (c *Config) Mem() { /** Lift methods in *connUDPBase to *connUDPIPv4 **/ *connUDPIPv4 implements Conn -preserves c.Mem() +requires acc(c.Mem(), _) preserves slices.AbsSlice_Bytes(b, 0, len(b)) ensures err == nil ==> 0 <= n && n <= len(b) ensures err == nil ==> acc(addr.Mem(), _) ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv4) ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) { - unfold c.Mem() - unfold c.connUDPBase.MemWithoutConn() + unfold acc(c.Mem(), _) + unfold acc(c.connUDPBase.MemWithoutConn(), _) assert c.pconn.GetUnderlyingConn() == c.conn tmpImpl := c.conn - tmpItf := c.pconn.ExchangePerm() + tmpItf := c.pconn.ExchangeWildcardPerm() var packetconn *ipv4.PacketConn = c.pconn - assert tmpItf == c.conn - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.Mem() + fold acc(c.connUDPBase.Mem(), _) n1, addr1, err1 := c.connUDPBase.ReadFrom(b, tmpImpl) - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - unfold c.connUDPBase.Mem() - apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.MemWithoutConn() - fold c.Mem() return n1, addr1, err1 } -preserves c.Mem() +preserves acc(c.Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv4) Write(b []byte) (n int, err error) { - unfold c.Mem() - unfold c.connUDPBase.MemWithoutConn() + unfold acc(c.Mem(), _) + unfold acc(c.connUDPBase.MemWithoutConn(), _) assert c.pconn.GetUnderlyingConn() == c.conn tmpImpl := c.conn - tmpItf := c.pconn.ExchangePerm() + tmpItf := c.pconn.ExchangeWildcardPerm() var packetconn *ipv4.PacketConn = c.pconn assert tmpItf == c.conn - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.Mem() + fold acc(c.connUDPBase.Mem(), _) n1, err1 := c.connUDPBase.Write(b, tmpImpl) - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - unfold c.connUDPBase.Mem() - apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.MemWithoutConn() - fold c.Mem() return n1, err1 } requires acc(dst.Mem(), _) -preserves c.Mem() +preserves acc(c.Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv4) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) { - unfold c.Mem() - unfold c.connUDPBase.MemWithoutConn() + unfold acc(c.Mem(), _) + unfold acc(c.connUDPBase.MemWithoutConn(), _) assert c.pconn.GetUnderlyingConn() == c.conn tmpImpl := c.conn - tmpItf := c.pconn.ExchangePerm() + tmpItf := c.pconn.ExchangeWildcardPerm() var packetconn *ipv4.PacketConn = c.pconn assert tmpItf == c.conn - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.Mem() + fold acc(c.connUDPBase.Mem(), _) n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl) - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - unfold c.connUDPBase.Mem() - apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.MemWithoutConn() - fold c.Mem() return n1, err1 } @@ -169,74 +150,56 @@ func (c *connUDPIPv4) Close() (err error) { /** Lift methods in *connUDPBase to *connUDPIPv6 **/ *connUDPIPv6 implements Conn -preserves c.Mem() +preserves acc(c.Mem(), _) preserves slices.AbsSlice_Bytes(b, 0, len(b)) ensures err == nil ==> 0 <= n && n <= len(b) ensures err == nil ==> acc(addr.Mem(), _) ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv6) ReadFrom(b []byte) (n int, addr *net.UDPAddr, err error) { - unfold c.Mem() - unfold c.connUDPBase.MemWithoutConn() + unfold acc(c.Mem(), _) + unfold acc(c.connUDPBase.MemWithoutConn(), _) assert c.pconn.GetUnderlyingConn() == c.conn tmpImpl := c.conn - tmpItf := c.pconn.ExchangePerm() + tmpItf := c.pconn.ExchangeWildcardPerm() var packetconn *ipv6.PacketConn = c.pconn assert tmpItf == c.conn - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.Mem() + fold acc(c.connUDPBase.Mem(), _) n1, addr1, err1 := c.connUDPBase.ReadFrom(b, tmpImpl) - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - unfold c.connUDPBase.Mem() - apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.MemWithoutConn() - fold c.Mem() return n1, addr1, err1 } -preserves c.Mem() +preserves acc(c.Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv6) Write(b []byte) (n int, err error) { - unfold c.Mem() - unfold c.connUDPBase.MemWithoutConn() + unfold acc(c.Mem(), _) + unfold acc(c.connUDPBase.MemWithoutConn(), _) assert c.pconn.GetUnderlyingConn() == c.conn tmpImpl := c.conn - tmpItf := c.pconn.ExchangePerm() + tmpItf := c.pconn.ExchangeWildcardPerm() var packetconn *ipv6.PacketConn = c.pconn assert tmpItf == c.conn - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.Mem() + fold acc(c.connUDPBase.Mem(), _) n1, err1 := c.connUDPBase.Write(b, tmpImpl) - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - unfold c.connUDPBase.Mem() - apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.MemWithoutConn() - fold c.Mem() return n1, err1 } requires acc(dst.Mem(), _) -preserves c.Mem() +preserves acc(c.Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() func (c *connUDPIPv6) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) { - unfold c.Mem() - unfold c.connUDPBase.MemWithoutConn() + unfold acc(c.Mem(), _) + unfold acc(c.connUDPBase.MemWithoutConn(), _) assert c.pconn.GetUnderlyingConn() == c.conn tmpImpl := c.conn - tmpItf := c.pconn.ExchangePerm() + tmpItf := c.pconn.ExchangeWildcardPerm() var packetconn *ipv6.PacketConn = c.pconn assert tmpItf == c.conn - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.Mem() + fold acc(c.connUDPBase.Mem(), _) n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl) - assert tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - unfold c.connUDPBase.Mem() - apply tmpItf.Mem() --* (packetconn.Mem() && packetconn.GetUnderlyingConn() === tmpItf) - fold c.connUDPBase.MemWithoutConn() - fold c.Mem() return n1, err1 } diff --git a/router/assumptions.gobra b/router/assumptions.gobra new file mode 100644 index 000000000..b09b0613b --- /dev/null +++ b/router/assumptions.gobra @@ -0,0 +1,107 @@ +// Copyright 2022 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +// This file is used for declaring assumptions which we cannot currenlty do +// away with, due to Gobra's incompletnesses or lack of support for +// specific features, like post-initialization invariants or because +// Gobra does not currently infer that 'x' != nil if 'x.Mem()' holds, +// where 'x' is of an interface type. + +package router + +/**** Post-init invariants ****/ + +// All global variables of type 'error' declared in dataplane.go +// are duplicable. As such, we can always establish their invariants +// AFTER INITIALIZATION. + +ghost +ensures unsupportedPathType.ErrorMem() +decreases _ +func establishMemUnsupportedPathType() + +ghost +ensures malformedPath != nil +ensures malformedPath.ErrorMem() +decreases _ +func establishMemMalformedPath() + +ghost +ensures unsupportedPathTypeNextHeader.ErrorMem() +decreases _ +func establishMemUnsupportedPathTypeNextHeader() + +ghost +ensures noBFDSessionConfigured.ErrorMem() +decreases _ +func establishMemNoBFDSessionConfigured() + +ghost +ensures noBFDSessionFound.ErrorMem() +decreases _ +func establishMemNoBFDSessionFound() + +ghost +ensures invalidSrcAddrForTransit.ErrorMem() +decreases _ +func establishInvalidSrcAddrForTransit() + +ghost +ensures noSVCBackend.ErrorMem() +decreases _ +func establishNoSVCBackend() + +ghost +ensures cannotRoute.ErrorMem() +decreases _ +func establishCannotRoute() + +/**** End of post-init invariants ****/ + +/**** scmpError ghost members ****/ + +// Gobra currently runs into unexpected verification errors +// when trying to prove the termination of these methods +// ('IsDuplicableMem' and 'Duplicate'). +// https://github.com/viperproject/gobra/issues/702 + +ghost +trusted +requires acc(err.ErrorMem(), _) +decreases err.ErrorMem() +pure func (err scmpError) IsDuplicableMem() bool { + return unfolding acc(err.ErrorMem(), _) in + err.Cause.IsDuplicableMem() +} + +ghost +trusted +preserves err.ErrorMem() +ensures err.IsDuplicableMem() == old(err.IsDuplicableMem()) +ensures err.IsDuplicableMem() ==> err.ErrorMem() +decreases err.ErrorMem() +func (err scmpError) Duplicate() { + if err.IsDuplicableMem() { + unfold err.ErrorMem() + assert err.Cause.IsDuplicableMem() + err.Cause.Duplicate() + assert err.Cause.ErrorMem() && err.Cause.ErrorMem() + fold err.ErrorMem() + fold err.ErrorMem() + } +} + +/**** End of scmpError ghost members ****/ \ No newline at end of file diff --git a/router/dataplane.go b/router/dataplane.go index 92701013c..942b792fe 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -127,7 +127,7 @@ type BatchConn interface { // @ ensures err != nil ==> err.ErrorMem() WriteTo(b []byte, addr *net.UDPAddr) (n int, err error) // @ preserves Mem() - // @ preserves forall i int :: { msgs[i] } 0 <= i && i < len(msgs) ==> + // @ preserves forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> // @ acc(msgs[i].Mem(1), R10) // @ ensures err == nil ==> 0 <= n && n <= len(msgs) // @ ensures err != nil ==> err.ErrorMem() @@ -188,11 +188,13 @@ type scmpError struct { Cause error } +// Gobra cannot currently prove termination of this function, +// because it is not specified how the ErrorMem() of the result +// of serrors.New relates to that of e. +// @ trusted // @ preserves e.ErrorMem() -// (VerifiedSCION): Gobra can't prove termination here because we call Error -// to the result of New and right now it is not able to prove that this will -// not be a new scmpError. We assume it. -// @ decreases _ +// @ ensures e.IsDuplicableMem() == old(e.IsDuplicableMem()) +// @ decreases e.ErrorMem() func (e scmpError) Error() string { // @ unfold e.ErrorMem() // @ defer fold e.ErrorMem() @@ -1768,7 +1770,10 @@ func (p *scionPacketProcessor) verifyCurrentMAC() (respr processResult, reserr e // @ ensures acc(&p.d, R15) // @ ensures reserr != nil ==> reserr.ErrorMem() func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) (resaddr *net.UDPAddr, respr processResult, reserr error) { - a, err := p.d.resolveLocalDst(&p.scionLayer /*@, ubScionL @*/) // (VerifiedSCION) the parameter used to be only p.scionLayer + // (VerifiedSCION) the parameter used to be p.scionLayer, + // instead of &p.scionLayer. + a, err := p.d.resolveLocalDst(&p.scionLayer /*@, ubScionL @*/) + // @ establishNoSVCBackend() switch { case errors.Is(err, noSVCBackend): // @ TODO() diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index edb564f99..e24e07d75 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -19,6 +19,7 @@ package router import ( "net" "hash" + . "github.com/scionproto/scion/verification/utils/definitions" sl "github.com/scionproto/scion/verification/utils/slices" "github.com/scionproto/scion/pkg/scrypto" "github.com/scionproto/scion/pkg/addr" @@ -151,31 +152,6 @@ pred (err scmpError) ErrorMem() { err.Cause != nil ==> err.Cause.ErrorMem() } -// Currently assumed, as Gobra cannot currently prove termination -// of the code below -ghost -trusted -pure -decreases -func (err scmpError) IsDuplicableMem() bool { - return err != nil? err.cause.IsDuplicableMem() : true -} - -// Currently assumed, as Gobra cannot currently prove termination -// of the code below -ghost -trusted -preserves err.ErrorMem() -ensures err.IsDuplicableMem() ==> err.ErrorMem() -decreases -func (err scmpError) Duplicate() { - if err.IsDuplicableMem() { - unfold err.ErrorMem() - err.cause.Duplicate() - fold err.ErrorMem() - } -} - scmpError implements error type offsetPair struct { @@ -279,59 +255,6 @@ func (d *DataPlane) getNewPacketProcessorFootprint() { /**** End of acessor methods to avoid unfolding the Mem predicate of the dataplane so much ****/ -/**** Post-init invariants ****/ - -// unsupportedPathType is duplicable: we can always establish its invariant -ghost -ensures unsupportedPathType.ErrorMem() -decreases _ -func establishMemUnsupportedPathType() - -// malformedPath is duplicable: we can always establish its invariant -ghost -ensures malformedPath != nil -ensures malformedPath.ErrorMem() -decreases _ -func establishMemMalformedPath() - -// unsupportedPathTypeNextHeader is duplicable: we can always establish its invariant -ghost -ensures unsupportedPathTypeNextHeader.ErrorMem() -decreases _ -func establishMemUnsupportedPathTypeNextHeader() - -// noBFDSessionConfigured is duplicable: we can always establish its invariant -ghost -ensures noBFDSessionConfigured.ErrorMem() -decreases _ -func establishMemNoBFDSessionConfigured() - -// noBFDSessionFound is duplicable: we can always establish its invariant -ghost -ensures noBFDSessionFound.ErrorMem() -decreases _ -func establishMemNoBFDSessionFound() - -// invalidSrdAddrForTransit is duplicable: we can always establish its invariant -ghost -ensures invalidSrcAddrForTransit.ErrorMem() -decreases _ -func establishInvalidSrcAddrForTransit() - -// noSVCBackend is duplicable: we can always establish its invariant -ghost -ensures noSVCBackend.ErrorMem() -decreases _ -func establishNoSVCBackend() - -// cannotRoute is duplicable: we can always establish its invariant after init -ghost -ensures cannotRoute.ErrorMem() -decreases _ -func establishCannotRoute() - -/**** End of post-init invariants ****/ - /** Start of closure specs for the Run method **/ requires true func readClosureSpec(ingressID uint16, rd BatchConn) diff --git a/router/svc_spec.gobra b/router/svc_spec.gobra index ee1a808a6..fcce7542c 100644 --- a/router/svc_spec.gobra +++ b/router/svc_spec.gobra @@ -31,7 +31,7 @@ pred internalLockInv(s *services) { acc(&s.m) && acc(s.m) && // we can read all keys stored in the map - forall k addr.HostSVC :: { k in domain(s.m) }{ validMapValue(k, s.m[k]) } k in domain(s.m) ==> + forall k addr.HostSVC :: { k in domain(s.m) }{ k in s.m }{ s.m[k] } k in domain(s.m) ==> validMapValue(k, s.m[k]) } diff --git a/verification/dependencies/errors/errors_spec.gobra b/verification/dependencies/errors/errors_spec.gobra index c8e6843e2..74e5ef38d 100644 --- a/verification/dependencies/errors/errors_spec.gobra +++ b/verification/dependencies/errors/errors_spec.gobra @@ -12,20 +12,11 @@ package errors // Unwrap returns the result of calling the Unwrap method on err, if err's // type contains an Unwrap method returning error. // Otherwise, Unwrap returns nil. -trusted requires err.ErrorMem() ensures res.ErrorMem() -decreases _ // this is a simplifying assumption -func Unwrap(err error) (res error) { - u, ok := err.(interface { - // The function only terminates if this Unwrap terminates - Unwrap() error - }) - if !ok { - return nil - } - return u.Unwrap() -} +ensures res.ErrorMem() --* err.ErrorMem() +decreases err.ErrorMem() +func Unwrap(err error) (res error) // Is reports whether any error in err's chain matches target. // @@ -34,38 +25,10 @@ func Unwrap(err error) (res error) { // // An error is considered to match a target if it is equal to that target or if // it implements a method Is(error) bool such that Is(target) returns true. -// -// An error type might provide an Is method so it can be treated as equivalent -// to an existing error. For example, if MyError defines -// -// func (m MyError) Is(target error) bool { return target == fs.ErrExist } -// -// then Is(MyError{}, fs.ErrExist) returns true. See syscall.Errno.Is for -// an example in the standard library. An Is method should only shallowly -// compare err and the target and not call Unwrap on either. -trusted -decreases _ -func Is(err, target error) bool { - if target == nil { - return err == target - } - - isComp := reflectlite.TypeOf(target).Comparable() - for { - if isComp && err == target { - return true - } - if x, ok := err.(interface{ Is(error) bool }); ok && x.Is(target) { - return true - } - // TODO: consider supporting target.Is(err). This would allow - // user-definable predicates, but also may allow for coping with sloppy - // APIs, thereby making it easier to get away with them. - if err = Unwrap(err); err == nil { - return false - } - } -} +preserves err != nil ==> err.ErrorMem() +preserves target != nil ==> target.ErrorMem() +decreases err.ErrorMem() +func Is(err, target error) (res bool) // As finds the first error in err's chain that matches target, and if one is found, sets // target to that error value and returns true. Otherwise, it returns false. @@ -78,38 +41,50 @@ func Is(err, target error) bool { // As(target) returns true. In the latter case, the As method is responsible for // setting target. // -// An error type might provide an As method so it can be treated as if it were a -// different error type. -// // As panics if target is not a non-nil pointer to either a type that implements // error, or to any interface type. -trusted -requires target != nil -// Gobra cannot yet precisely capture the precondition "target must be a non-nil -// pointer to either a type that implements error, or to any interface type. -decreases _ -func As(err error, target interface{}) bool { - if target == nil { - panic("errors: target cannot be nil") - } - val := reflectlite.ValueOf(target) - typ := val.Type() - if typ.Kind() != reflectlite.Ptr || val.IsNil() { - panic("errors: target must be a non-nil pointer") - } - targetType := typ.Elem() - if targetType.Kind() != reflectlite.Interface && !targetType.Implements(errorType) { - panic("errors: *target must be interface or implement error") - } - for err != nil { - if reflectlite.TypeOf(err).AssignableTo(targetType) { - val.Elem().Set(reflectlite.ValueOf(err)) - return true - } - if x, ok := err.(interface{ As(any) bool }); ok && x.As(target) { - return true - } - err = Unwrap(err) - } - return false +requires err != nil ==> err.ErrorMem() +requires target != nil +preserves target.Mem() +ensures res ==> ( + let nestedErr := target.Get() in + err != nil && + nestedErr != nil && + nestedErr.ErrorMem() && + target.CanSet(nestedErr) && + (nestedErr.ErrorMem() --* err.ErrorMem())) +ensures !res ==> err.ErrorMem() +decreases err.ErrorMem() +func As(err error, target ErrorCell) (res bool) + +// Cell where one can store an error. This is used in the function +// 'As', for the type of 'target', instead of the type 'interface{}' +// used in the standard library. This way, we can capture the +// requirement that target must be able to store the error and make +// sure that no calls to this function can result in a panic. +type ErrorCell interface { + pred Mem() + + // This is not meant to be called. Instead, + // it shows that Mem() is strong enough to + // allow for the assignment of an error. + ghost + requires Mem() && CanSet(e) + ensures Mem() && Get() === e + decreases + Set(e error) + + ghost + pure + requires acc(Mem(), _) + decreases + Get() error + + // Determines if 'e' could be stored in the + // current cell. + ghost + pure + requires acc(Mem(), _) + decreases + CanSet(e error) bool } \ No newline at end of file diff --git a/verification/dependencies/github.com/google/gopacket/writer.gobra b/verification/dependencies/github.com/google/gopacket/writer.gobra index 17ac9c6bd..f20973514 100644 --- a/verification/dependencies/github.com/google/gopacket/writer.gobra +++ b/verification/dependencies/github.com/google/gopacket/writer.gobra @@ -102,7 +102,7 @@ type SerializeBuffer interface { PushLayer(LayerType) } -ensures res.Mem() +ensures res != nil && res.Mem() decreases func NewSerializeBuffer() (res SerializeBuffer) 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 4f676535c..d067a9da5 100644 --- a/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra +++ b/verification/dependencies/golang.org/x/net/internal/socket/socket.gobra @@ -41,7 +41,9 @@ pred (m *Message) Mem(lenBuffers int) { 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)) && - (m.Addr != nil ==> acc(m.Addr.Mem(), _)) + // typeOf(m.Addr) == type[*net.UDPAddr] && + (m.Addr != nil ==> acc(m.Addr.Mem(), _)) && + 0 <= m.N } pred (m *Message) MemWithoutHalf(lenBuffers int) { @@ -49,7 +51,21 @@ pred (m *Message) MemWithoutHalf(lenBuffers int) { 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)) && - (m.Addr != nil ==> acc(m.Addr.Mem(), _)) + // typeOf(m.Addr) == type[*net.UDPAddr] && + (m.Addr != nil ==> acc(m.Addr.Mem(), _)) && + 0 <= m.N +} + +ghost +requires acc(m.Mem(lenBuffers), _) +pure func (m *Message) GetAddr(lenBuffers int) net.Addr { + return unfolding acc(m.Mem(lenBuffers), _) in m.Addr +} + +ghost +requires acc(m.MemWithoutHalf(lenBuffers), _) +pure func (m *Message) GetAddrWithoutHalf(lenBuffers int) net.Addr { + return unfolding acc(m.MemWithoutHalf(lenBuffers), _) in m.Addr } ghost @@ -68,15 +84,42 @@ 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 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) +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) diff --git a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra index 44aa8769b..f5cf2e4db 100644 --- a/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra +++ b/verification/dependencies/golang.org/x/net/ipv4/endpoint.gobra @@ -120,13 +120,20 @@ requires acc(p.Mem(), _) pure func (p *PacketConn) GetUnderlyingConn() (c net.PacketConn) ghost -requires p.Mem() +requires acc(p.Mem(), _) ensures c === old(p.GetUnderlyingConn()) ensures c.Mem() ensures c.Mem() --* (p.Mem() && p.GetUnderlyingConn() === c) decreases _ func (p *PacketConn) ExchangePerm() (c net.PacketConn) +ghost +requires acc(p.Mem(), _) +ensures c === old(p.GetUnderlyingConn()) +ensures acc(c.Mem(), _) +decreases _ +func (p *PacketConn) ExchangeWildcardPerm() (c net.PacketConn) + // A RawConn represents a packet network endpoint that uses the IPv4 // transport. It is used to control several IP-level socket options // including IPv4 header manipulation. It also provides datagram @@ -219,9 +226,9 @@ func NewRawConn(c net.PacketConn) (r *RawConn, err error) { // On a successful read it returns the number of messages received, up // to len(ms). trusted +preserves acc(c.Mem(), _) preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> (&ms[i]).Mem(lenBuffers) -preserves c.Mem() ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> (0 <= n && n <= len(ms)) ensures err != nil ==> err.ErrorMem() @@ -235,7 +242,7 @@ func (c *PacketConn) ReadBatch(ms []socket.Message, flags int, ghost lenBuffers trusted preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> acc((&ms[i]).Mem(lenBuffers), R10) -preserves c.Mem() +preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> 0 <= n && n <= len(ms) ensures err != nil ==> err.ErrorMem() diff --git a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra index 0c23e243c..d2530666c 100644 --- a/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra +++ b/verification/dependencies/golang.org/x/net/ipv6/endpoint.gobra @@ -149,6 +149,13 @@ ensures c.Mem() --* (p.Mem() && p.GetUnderlyingConn() === c) decreases _ func (p *PacketConn) ExchangePerm() (c net.PacketConn) +ghost +requires acc(p.Mem(), _) +ensures c === old(p.GetUnderlyingConn()) +ensures acc(c.Mem(), _) +decreases _ +func (p *PacketConn) ExchangeWildcardPerm() (c net.PacketConn) + // (VerifiedSCION) Promote method from payloadHandler to PacketConn. // ReadBatch reads a batch of messages. // On a successful read it returns the number of messages received, up @@ -156,7 +163,7 @@ func (p *PacketConn) ExchangePerm() (c net.PacketConn) trusted preserves forall i int :: { &ms[i] } 0 <= i && i < len(ms) ==> (&ms[i]).Mem(lenBuffers) -preserves c.Mem() +preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> (0 <= n && n <= len(ms)) ensures err != nil ==> err.ErrorMem() @@ -169,7 +176,7 @@ 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) -preserves c.Mem() +preserves acc(c.Mem(), _) ensures c.GetUnderlyingConn() === old(c.GetUnderlyingConn()) ensures err == nil ==> 0 <= n && n <= len(ms) ensures err != nil ==> err.ErrorMem() diff --git a/verification/dependencies/net/net.gobra b/verification/dependencies/net/net.gobra index 937fcc6f6..e2ff126be 100644 --- a/verification/dependencies/net/net.gobra +++ b/verification/dependencies/net/net.gobra @@ -35,14 +35,14 @@ type Conn interface { pred Mem() // Read reads data from the connection. - preserves Mem() + requires acc(Mem(), _) preserves slices.AbsSlice_Bytes(b, 0, len(b)) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() Read(b []byte) (n int, err error) // Write writes data to the connection. - preserves Mem() + preserves acc(Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() @@ -92,7 +92,7 @@ type Conn interface { type PacketConn interface { pred Mem() - preserves Mem() + preserves acc(Mem(), _) preserves slices.AbsSlice_Bytes(p, 0, len(p)) ensures err == nil ==> 0 <= n && n <= len(p) ensures err == nil ==> acc(addr.Mem(), _) @@ -100,7 +100,7 @@ type PacketConn interface { ReadFrom(p []byte) (n int, addr Addr, err error) requires acc(addr.Mem(), _) - preserves Mem() + preserves acc(Mem(), _) preserves acc(slices.AbsSlice_Bytes(p, 0, len(p)), R15) ensures err == nil ==> 0 <= n && n <= len(p) ensures err != nil ==> err.ErrorMem() diff --git a/verification/dependencies/net/udpsock.gobra b/verification/dependencies/net/udpsock.gobra index 0b8079e8f..5b0706ddb 100644 --- a/verification/dependencies/net/udpsock.gobra +++ b/verification/dependencies/net/udpsock.gobra @@ -57,7 +57,7 @@ pred (u *UDPConn) Mem() { } // ReadFromUDP acts like ReadFrom but returns a UDPAddr. -preserves c.Mem() +preserves acc(c.Mem(), _) preserves slices.AbsSlice_Bytes(b, 0, len(b)) ensures err == nil ==> 0 <= n && n <= len(b) ensures err == nil ==> acc(addr.Mem(), _) @@ -65,7 +65,7 @@ ensures err != nil ==> err.ErrorMem() func (c *UDPConn) ReadFromUDP(b []byte) (n int, addr *UDPAddr, err error) // ReadFrom implements the PacketConn ReadFrom method. -preserves c.Mem() +preserves acc(c.Mem(), _) preserves slices.AbsSlice_Bytes(b, 0, len(b)) ensures err == nil ==> 0 <= n && n <= len(b) ensures err == nil ==> acc(addr.Mem(), _) @@ -73,7 +73,7 @@ ensures err != nil ==> err.ErrorMem() func (c *UDPConn) ReadFrom(b []byte) (n int, addr Addr, err error) // WriteToUDP acts like WriteTo but takes a UDPAddr. -requires c.Mem() && acc(addr.Mem(), 1/1000) +requires acc(c.Mem(), _) && acc(addr.Mem(), 1/1000) requires forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], 1/1000) ensures c.Mem() && acc(addr.Mem(), 1/1000) ensures forall i int :: {&b[i]} 0 <= i && i < len(b) ==> acc(&b[i], 1/1000) @@ -81,7 +81,7 @@ func (c *UDPConn) WriteToUDP(b []byte, addr *UDPAddr) (int, error) // WriteTo implements the PacketConn WriteTo method. requires acc(addr.Mem(), _) -preserves c.Mem() +preserves acc(c.Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() @@ -135,7 +135,7 @@ ensures err != nil ==> err.ErrorMem() decreases _ func (c *UDPConn) SetReadBuffer(bytes int) (err error) -preserves c.Mem() +preserves acc(c.Mem(), _) preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R15) ensures err == nil ==> 0 <= n && n <= len(b) ensures err != nil ==> err.ErrorMem() diff --git a/verification/dependencies/syscall/syscall_unix.gobra b/verification/dependencies/syscall/syscall_unix.gobra index e00a41e04..c0b53a89a 100644 --- a/verification/dependencies/syscall/syscall_unix.gobra +++ b/verification/dependencies/syscall/syscall_unix.gobra @@ -9,6 +9,8 @@ package syscall +import "errors" + // An Errno is an unsigned number describing an error condition. // It implements the error interface. The zero Errno is by convention // a non-error, so code to convert from Errno to error should use: @@ -17,17 +19,16 @@ package syscall // if errno != 0 { // err = errno // } -// -// Errno values can be tested against error values from the os package -// using errors.Is. For example: -// -// _, _, err := syscall.Syscall(...) -// if errors.Is(err, fs.ErrNotExist) ... + type Errno uintptr +Errno implements error +*Errno implements errors.ErrorCell + pred (e Errno) ErrorMem() { e != 0 } preserves e.ErrorMem() +ensures old(e.IsDuplicableMem()) == e.IsDuplicableMem() decreases func (e Errno) Error() string @@ -40,11 +41,41 @@ func (e Errno) IsDuplicableMem() (res bool) { ghost preserves e.ErrorMem() -ensures e.ErrorMem() +ensures e.ErrorMem() +ensures old(e.IsDuplicableMem()) == e.IsDuplicableMem() decreases func (e Errno) Duplicate() { assert unfolding e.ErrorMem() in true fold e.ErrorMem() } -Errno implements error +/** ErrorCell **/ +pred (s *Errno) Mem() { + acc(s) +} + +ghost +preserves s.Mem() && s.CanSet(e) +ensures s.Get() === e +decreases +func (s *Errno) Set(e error) { + unfold s.Mem() + defer fold s.Mem() + newErr := e.(Errno) + *s = newErr +} + +ghost +pure +requires acc(s.Mem(), _) +decreases +func (s *Errno) Get() error { + return unfolding acc(s.Mem(), _) in *s +} + +ghost +pure +decreases +func (s *Errno) CanSet(e error) bool { + return typeOf(e) == type[Errno] +} \ No newline at end of file diff --git a/verification/utils/floats/floats.gobra b/verification/utils/floats/floats.gobra new file mode 100644 index 000000000..059946c96 --- /dev/null +++ b/verification/utils/floats/floats.gobra @@ -0,0 +1,30 @@ +// Copyright 2022 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +// This package contains some lemmas that are useful to deal with floats. + +package floats + +ghost +requires l <= h +ensures float64(l) <= float64(h) +decreases _ +func CastPreservesOrder64(l, h int) + +ghost +ensures float64(0) < float64(1) +decreases _ +func ZeroLessOne64() \ No newline at end of file