Merge branch 'master' into temp

.github/workflows/gobra.yml

@@ -265,7 +265,7 @@ jobs:
  uses: viperproject/gobra-action@main
  with:
  packages: 'pkg/slayers/path/scion'
- timeout: 5m
+ timeout: 30m
  headerOnly: ${{ env.headerOnly }}
  module: ${{ env.module }}
  includePaths: ${{ env.includePaths }}
@@ -415,16 +415,20 @@ jobs:
  includePaths: ${{ env.includePaths }}
  assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
  checkConsistency: ${{ env.checkConsistency }}
+ # Due to a bug introduced in https:/viperproject/gobra/pull/776,
+ # we must currently disable the chopper, otherwise we well-founded orders
+ # for termination checking are not available at the chopped Viper parts.
+ # We should reenable it whenever possible, as it reduces verification time in
+ # ~8 min (20%).
+ # chop: 10
  parallelizeBranches: '1'
- # The following flag has a significant influence on the number of branches verified.
- # Without it, verification would take a lot longer.
  conditionalizePermissions: '1'
+ moreJoins: 'impure'
  imageVersion: ${{ env.imageVersion }}
  mceMode: 'on'
  requireTriggers: ${{ env.requireTriggers }}
  overflow: ${{ env.overflow }}
  useZ3API: ${{ env.useZ3API }}
  disableNL: '0'
  viperBackend: ${{ env.viperBackend }}
- unsafeWildcardOptimization: '0'
-
+ unsafeWildcardOptimization: '0'

.gitignore

@@ -101,3 +101,5 @@ target
 *.internal
 .devcontainer
 .metals
+.bazelbsp
+.bazel

README.md

@@ -1,6 +1,6 @@
 # VerifiedSCION
 
-This package contains the **verified** implementation of the
+This package contains the **verified** implementation of the router from the
 [SCION](http://www.scion-architecture.net) protocol, a future Internet architecture.
 SCION is the first
 clean-slate Internet architecture designed to provide route control, failure
@@ -10,7 +10,7 @@ isolation, and explicit trust information for end-to-end communication.
 
 To find out more about the project, please visit the [official project page](https://www.pm.inf.ethz.ch/research/verifiedscion.html).
 
-> We are currently in the process of migrating the specifications and other annotations from the [original VerifiedSCION repository](https:/jcp19/VerifiedSCION) to this one. This repository contains an up-to-date version of SCION (which we plan to keep updated), as well as improvements resulting from our experience from our first efforts on verifying SCION.
+> This repository contains a recent version of SCION (which we plan to keep updated), as well as fixes to the bugs we report as a result of verifying the SCION router from the mainline SCION repository.
 
 ## Methodology
 We focus on verifying the main implementation of SCION, written in the *Go* programming language.

pkg/addr/host.go

@@ -28,7 +28,7 @@ import (
 
  "github.com/scionproto/scion/pkg/private/serrors"
  //@ . "github.com/scionproto/scion/verification/utils/definitions"
- //@ "github.com/scionproto/scion/verification/utils/slices"
+ //@ sl "github.com/scionproto/scion/verification/utils/slices"
 )
 
 type HostAddrType uint8
@@ -196,7 +196,7 @@ func (h HostIPv4) Pack() (res []byte) {
 func (h HostIPv4) IP() (res net.IP) {
  // XXX(kormat): ensure the reply is the 4-byte representation.
  //@ unfold acc(h.Mem(), R13)
- //@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
  return net.IP(h).To4( /*@ false @*/ )
 }
 
@@ -205,10 +205,10 @@ func (h HostIPv4) IP() (res net.IP) {
 // @ decreases
 func (h HostIPv4) Copy() (res HostAddr) {
  //@ unfold acc(h.Mem(), R13)
- //@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
  var tmp HostIPv4 = HostIPv4(append( /*@ R13, @*/ net.IP(nil), h...))
- //@ fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
- //@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+ //@ fold acc(sl.Bytes(h, 0, len(h)), R13)
+ //@ fold sl.Bytes(tmp, 0, len(tmp))
  //@ fold acc(h.Mem(), R13)
  //@ fold tmp.Mem()
  return tmp
@@ -231,7 +231,7 @@ func (h HostIPv4) Equal(o HostAddr) bool {
 func (h HostIPv4) String() string {
  //@ assert unfolding acc(h.Mem(), R13) in len(h) == HostLenIPv4
  //@ ghost defer fold acc(h.Mem(), R13)
- //@ ghost defer fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ ghost defer fold acc(sl.Bytes(h, 0, len(h)), R13)
  return h.IP().String()
 }
 
@@ -254,7 +254,7 @@ func (h HostIPv6) Type() HostAddrType {
 // @ decreases
 func (h HostIPv6) Pack() (res []byte) {
  //@ unfold acc(h.Mem(), R13)
- //@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
  return []byte(h)[:HostLenIPv6]
 }
 
@@ -264,7 +264,7 @@ func (h HostIPv6) Pack() (res []byte) {
 // @ decreases
 func (h HostIPv6) IP() (res net.IP) {
  //@ unfold acc(h.Mem(), R13)
- //@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
  return net.IP(h)
 }
 
@@ -273,10 +273,10 @@ func (h HostIPv6) IP() (res net.IP) {
 // @ decreases
 func (h HostIPv6) Copy() (res HostAddr) {
  //@ unfold acc(h.Mem(), R13)
- //@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
  var tmp HostIPv6 = HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...))
- //@ fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
- //@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+ //@ fold acc(sl.Bytes(h, 0, len(h)), R13)
+ //@ fold sl.Bytes(tmp, 0, len(tmp))
  //@ fold acc(h.Mem(), R13)
  //@ fold tmp.Mem()
  return tmp
@@ -299,7 +299,7 @@ func (h HostIPv6) Equal(o HostAddr) bool {
 func (h HostIPv6) String() string {
  //@ assert unfolding acc(h.Mem(), R13) in len(h) == HostLenIPv6
  //@ ghost defer fold acc(h.Mem(), R13)
- //@ ghost defer fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+ //@ ghost defer fold acc(sl.Bytes(h, 0, len(h)), R13)
  return h.IP().String()
 }
 
@@ -442,7 +442,7 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
  }
  //@ assert forall i int :: { &b[:HostLenIPv4][i] } 0 <= i && i < len(b[:HostLenIPv4]) ==> &b[:HostLenIPv4][i] == &b[i]
  tmp := HostIPv4(b[:HostLenIPv4])
- //@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+ //@ fold sl.Bytes(tmp, 0, len(tmp))
  //@ fold tmp.Mem()
  return tmp, nil
  case HostTypeIPv6:
@@ -451,7 +451,7 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
  }
  //@ assert forall i int :: { &b[:HostLenIPv4][i] } 0 <= i && i < len(b[:HostLenIPv4]) ==> &b[:HostLenIPv4][i] == &b[i]
  tmp := HostIPv6(b[:HostLenIPv6])
- //@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+ //@ fold sl.Bytes(tmp, 0, len(tmp))
  //@ fold tmp.Mem()
  return tmp, nil
  case HostTypeSVC:
@@ -473,12 +473,12 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
 func HostFromIP(ip net.IP) (res HostAddr) {
  if ip4 := ip.To4( /*@ false @*/ ); ip4 != nil {
  tmp := HostIPv4(ip4)
- //@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+ //@ fold sl.Bytes(tmp, 0, len(tmp))
  //@ fold tmp.Mem()
  return tmp
  }
  tmp := HostIPv6(ip)
- //@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+ //@ fold sl.Bytes(tmp, 0, len(tmp))
  //@ fold tmp.Mem()
  return tmp
 }

pkg/addr/host_spec.gobra

@@ -28,14 +28,14 @@ HostNone implements HostAddr
 
 pred (h HostIPv4) Mem() {
  len(h) == HostLenIPv4 &&
- slices.AbsSlice_Bytes(h, 0, len(h))
+ slices.Bytes(h, 0, len(h))
 }
 
 HostIPv4 implements HostAddr
 
 pred (h HostIPv6) Mem() {
  len(h) == HostLenIPv6 &&
- slices.AbsSlice_Bytes(h, 0, len(h))
+ slices.Bytes(h, 0, len(h))
 }
 
 HostIPv6 implements HostAddr

pkg/experimental/epic/epic.go

@@ -48,13 +48,11 @@ const (
 
 var zeroInitVector /*@@@*/ [16]byte
 
-/*@
 // ghost init
-func init() {
- fold acc(sl.AbsSlice_Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
- fold acc(postInitInvariant(), _)
-}
-@*/
+// @ func init() {
+// @ fold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
+// @ fold acc(postInitInvariant(), _)
+// @ }
 
 // CreateTimestamp returns the epic timestamp, which encodes the current time (now) relative to the
 // input timestamp. The input timestamp must not be in the future (compared to the current time),
@@ -107,26 +105,24 @@ func VerifyTimestamp(timestamp time.Time, epicTS uint32, now time.Time) (err err
 // If the same buffer is provided in subsequent calls to this function, the previously returned
 // EPIC MAC may get overwritten. Only the most recently returned EPIC MAC is guaranteed to be
 // valid.
-// (VerifiedSCION) ::OVERRIDE:: the following function is marked as trusted, even though it is verified,
-// due to an incompletness of Gobra that keeps it from being able to prove that we have
-// the magic wand at the end of a successful run.
-// @ trusted
 // @ requires len(auth) == 16
-// @ requires sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+// @ requires sl.Bytes(buffer, 0, len(buffer))
 // @ preserves acc(s.Mem(ub), R20)
-// @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R20)
-// @ preserves acc(sl.AbsSlice_Bytes(auth, 0, len(auth)), R30)
-// @ ensures reserr == nil ==> sl.AbsSlice_Bytes(res, 0, len(res))
-// @ ensures reserr == nil ==> (sl.AbsSlice_Bytes(res, 0, len(res)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer)))
+// @ preserves acc(sl.Bytes(ub, 0, len(ub)), R20)
+// @ preserves acc(sl.Bytes(auth, 0, len(auth)), R30)
+// @ ensures reserr == nil ==> sl.Bytes(res, 0, len(res))
+// @ ensures reserr == nil ==> (sl.Bytes(res, 0, len(res)) --* sl.Bytes(buffer, 0, len(buffer)))
 // @ ensures reserr != nil ==> reserr.ErrorMem()
-// @ ensures reserr != nil ==> sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+// @ ensures reserr != nil ==> sl.Bytes(buffer, 0, len(buffer))
 // @ decreases
 func CalcMac(auth []byte, pktID epic.PktID, s *slayers.SCION,
  timestamp uint32, buffer []byte /*@ , ghost ub []byte @*/) (res []byte, reserr error) {
 
+ // @ ghost oldBuffer := buffer
+ // @ ghost allocatesNewBuffer := len(buffer) < MACBufferSize
  if len(buffer) < MACBufferSize {
  buffer = make([]byte, MACBufferSize)
- // @ fold sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+ // @ fold sl.Bytes(buffer, 0, len(buffer))
  }
 
  // Initialize cryptographic MAC function
@@ -149,11 +145,14 @@ func CalcMac(auth []byte, pktID epic.PktID, s *slayers.SCION,
  // @ ghost end := start + 4
  result := input[len(input)-f.BlockSize() : len(input)-f.BlockSize()+4]
  // @ sl.SplitRange_Bytes(input, start, end, writePerm)
- // @ package (sl.AbsSlice_Bytes(result, 0, len(result)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer))) {
- // @ sl.CombineRange_Bytes(input, start, end, writePerm)
- // @ sl.CombineRange_Bytes(buffer, 0, inputLength, writePerm)
+ // @ package (sl.Bytes(result, 0, len(result)) --* sl.Bytes(oldBuffer, 0, len(oldBuffer))) {
+ // @ ghost if !allocatesNewBuffer {
+ // @ assert oldBuffer === buffer
+ // @ sl.CombineRange_Bytes(input, start, end, writePerm)
+ // @ sl.CombineRange_Bytes(oldBuffer, 0, inputLength, writePerm)
+ // @ }
  // @ }
- // @ assert (sl.AbsSlice_Bytes(result, 0, len(result)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer)))
+ // @ assert (sl.Bytes(result, 0, len(result)) --* sl.Bytes(oldBuffer, 0, len(oldBuffer)))
  return result, nil
 }
 
@@ -162,11 +161,11 @@ func CalcMac(auth []byte, pktID epic.PktID, s *slayers.SCION,
 // bytes of the SCION path type MAC, has invalid length, or if the MAC calculation gives an error,
 // also VerifyHVF returns an error. The verification was successful if and only if VerifyHVF
 // returns nil.
-// @ preserves sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+// @ preserves sl.Bytes(buffer, 0, len(buffer))
 // @ preserves acc(s.Mem(ub), R20)
-// @ preserves acc(sl.AbsSlice_Bytes(hvf, 0, len(hvf)), R50)
-// @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R20)
-// @ preserves acc(sl.AbsSlice_Bytes(auth, 0, len(auth)), R30)
+// @ preserves acc(sl.Bytes(hvf, 0, len(hvf)), R50)
+// @ preserves acc(sl.Bytes(ub, 0, len(ub)), R20)
+// @ preserves acc(sl.Bytes(auth, 0, len(auth)), R30)
 // @ ensures reserr != nil ==> reserr.ErrorMem()
 // @ decreases
 func VerifyHVF(auth []byte, pktID epic.PktID, s *slayers.SCION,
@@ -182,11 +181,11 @@ func VerifyHVF(auth []byte, pktID epic.PktID, s *slayers.SCION,
  }
 
  if subtle.ConstantTimeCompare(hvf, mac) == 0 {
- // @ apply sl.AbsSlice_Bytes(mac, 0, len(mac)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+ // @ apply sl.Bytes(mac, 0, len(mac)) --* sl.Bytes(buffer, 0, len(buffer))
  return serrors.New("epic hop validation field verification failed",
  "hvf in packet", hvf, "calculated mac", mac, "auth", auth)
  }
- // @ apply sl.AbsSlice_Bytes(mac, 0, len(mac)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+ // @ apply sl.Bytes(mac, 0, len(mac)) --* sl.Bytes(buffer, 0, len(buffer))
  return nil
 }
 
@@ -205,7 +204,7 @@ func CoreFromPktCounter(counter uint32) (uint8, uint32) {
 }
 
 // @ requires len(key) == 16
-// @ preserves acc(sl.AbsSlice_Bytes(key, 0, len(key)), R50)
+// @ preserves acc(sl.Bytes(key, 0, len(key)), R50)
 // @ ensures reserr == nil ==> res != nil && res.Mem() && res.BlockSize() == 16
 // @ ensures reserr != nil ==> reserr.ErrorMem()
 // @ decreases
@@ -224,8 +223,8 @@ func initEpicMac(key []byte) (res cipher.BlockMode, reserr error) {
 
 // @ requires MACBufferSize <= len(inputBuffer)
 // @ preserves acc(s.Mem(ub), R20)
-// @ preserves acc(sl.AbsSlice_Bytes(ub, 0, len(ub)), R20)
-// @ preserves sl.AbsSlice_Bytes(inputBuffer, 0, len(inputBuffer))
+// @ preserves acc(sl.Bytes(ub, 0, len(ub)), R20)
+// @ preserves sl.Bytes(inputBuffer, 0, len(inputBuffer))
 // @ ensures reserr == nil ==> 16 <= res && res <= len(inputBuffer)
 // @ ensures reserr != nil ==> reserr.ErrorMem()
 // @ decreases
@@ -264,30 +263,30 @@ func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
  inputLength := 16 * nrBlocks
 
  // Fill input
- // @ unfold sl.AbsSlice_Bytes(inputBuffer, 0, len(inputBuffer))
+ // @ unfold sl.Bytes(inputBuffer, 0, len(inputBuffer))
  offset := 0
  inputBuffer[0] = uint8(s.SrcAddrType & 0x3) // extract length bits
  offset += 1
  // @ assert forall i int :: { &inputBuffer[offset:][i] } 0 <= i && i < len(inputBuffer[offset:]) ==>
  // @ &inputBuffer[offset:][i] == &inputBuffer[offset+i]
  binary.BigEndian.PutUint32(inputBuffer[offset:], timestamp)
  offset += 4
- // @ fold sl.AbsSlice_Bytes(inputBuffer, 0, len(inputBuffer))
+ // @ fold sl.Bytes(inputBuffer, 0, len(inputBuffer))
  // @ sl.SplitRange_Bytes(inputBuffer, offset, len(inputBuffer), writePerm)
  pktID.SerializeTo(inputBuffer[offset:])
  // @ sl.CombineRange_Bytes(inputBuffer, offset, len(inputBuffer), writePerm)
  offset += epic.PktIDLen
- // @ unfold sl.AbsSlice_Bytes(inputBuffer, 0, len(inputBuffer))
+ // @ unfold sl.Bytes(inputBuffer, 0, len(inputBuffer))
  // @ assert forall i int :: { &inputBuffer[offset:][i] } 0 <= i && i < len(inputBuffer[offset:]) ==>
  // @ &inputBuffer[offset:][i] == &inputBuffer[offset+i]
  binary.BigEndian.PutUint64(inputBuffer[offset:], uint64(s.SrcIA))
  offset += addr.IABytes
  // @ assert forall i int :: { &inputBuffer[offset:][i] } 0 <= i && i < len(inputBuffer[offset:]) ==>
  // @ &inputBuffer[offset:][i] == &inputBuffer[offset+i]
  // @ sl.SplitRange_Bytes(ub, start, end, R20)
- // @ unfold acc(sl.AbsSlice_Bytes(srcAddr, 0, len(srcAddr)), R20)
+ // @ unfold acc(sl.Bytes(srcAddr, 0, len(srcAddr)), R20)
  copy(inputBuffer[offset:], srcAddr /*@ , R20 @*/)
- // @ fold acc(sl.AbsSlice_Bytes(srcAddr, 0, len(srcAddr)), R20)
+ // @ fold acc(sl.Bytes(srcAddr, 0, len(srcAddr)), R20)
  // @ sl.CombineRange_Bytes(ub, start, end, R20)
  offset += l
  // @ assert forall i int :: { &inputBuffer[offset:][i] } 0 <= i && i < len(inputBuffer[offset:]) ==>
@@ -303,15 +302,15 @@ func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
  // @ acc(&inputBuffer[offset:inputLength][i])
  // @ establishPostInitInvariant()
  // @ unfold acc(postInitInvariant(), _)
- // @ assert acc(sl.AbsSlice_Bytes(zeroInitVector[:], 0, 16), _)
+ // @ assert acc(sl.Bytes(zeroInitVector[:], 0, 16), _)
  // (VerifiedSCION) From the package invariant, we learn that we have a wildcard access to zeroInitVector.
  // Unfortunately, it is not possible to call `copy` with a wildcard amount, even though
  // that would be perfectly fine. The spec of `copy` would need to be adapted to allow for that case.
- // @ inhale acc(sl.AbsSlice_Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), R55)
- // @ unfold acc(sl.AbsSlice_Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), R55)
+ // @ inhale acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), R55)
+ // @ unfold acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), R55)
  // @ assert forall i int :: { &zeroInitVector[:][i] } 0 <= i && i < len(zeroInitVector[:]) ==>
  // @ &zeroInitVector[:][i] == &zeroInitVector[i]
  copy(inputBuffer[offset:inputLength], zeroInitVector[:] /*@ , R55 @*/)
- // @ fold sl.AbsSlice_Bytes(inputBuffer, 0, len(inputBuffer))
+ // @ fold sl.Bytes(inputBuffer, 0, len(inputBuffer))
  return inputLength, nil
 }

pkg/experimental/epic/epic_spec.gobra

@@ -21,7 +21,7 @@ import sl "github.com/scionproto/scion/verification/utils/slices"
 pred postInitInvariant() {
  acc(&zeroInitVector, _) &&
  len(zeroInitVector[:]) == 16 &&
- acc(sl.AbsSlice_Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
+ acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
 }
 
 // learn the invariant established by init

pkg/private/serrors/serrors_spec.gobra

@@ -76,12 +76,12 @@ func Wrap(msg, cause error, errCtx ...interface{}) (res error)
 // Elements of errCtx are limited to "primitive types" at the moment.
 // This is a safe but strict under-approximation of what can be done
 // with this method.
-requires cause.ErrorMem()
+requires cause != nil ==> cause.ErrorMem()
 preserves forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> acc(&errCtx[i], R15)
 // The following precondition cannot be adequately captured in Gobra.
 // requires forall i int :: 0 <= i && i < len(errCtx) ==> IsOfPrimitiveType(errCtx[i])
 ensures res != nil && res.ErrorMem()
-ensures res.ErrorMem() --* cause.ErrorMem()
+ensures cause != nil ==> (res.ErrorMem() --* cause.ErrorMem())
 decreases
 func WrapStr(msg string, cause error, errCtx ...interface{}) (res error)