Skip to content

Commit

Permalink
Verify core of Run method (#240)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@jcp19
jcp19 authored Jan 26, 2024
1 parent bcc5ca8 commit 32c592e
Show file tree
Hide file tree
Showing 11 changed files with 1,218 additions and 339 deletions.
77 changes: 46 additions & 31 deletions pkg/slayers/scion.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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) {
Expand Down Expand Up @@ -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",
Expand Down
26 changes: 13 additions & 13 deletions private/underlay/conn/conn.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -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
}
Loading

0 comments on commit 32c592e

Please sign in to comment.