Bring changes of libepic from PR #261

pkg/experimental/epic/epic.go

@@ -107,13 +107,26 @@ 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) 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 Uncallable()
+// @ requires  len(auth) == 16
+// @ requires  sl.AbsSlice_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)))
+// @ ensures   reserr != nil ==> reserr.ErrorMem()
+// @ ensures   reserr != nil ==> sl.AbsSlice_Bytes(buffer, 0, len(buffer))
+// @ decreases
 func CalcMac(auth []byte, pktID epic.PktID, s *slayers.SCION,
-	timestamp uint32, buffer []byte) ([]byte, error) {
+	timestamp uint32, buffer []byte /*@ , ghost ub []byte @*/) (res []byte, reserr error) {
 
 	if len(buffer) < MACBufferSize {
 		buffer = make([]byte, MACBufferSize)
+		// @ fold sl.AbsSlice_Bytes(buffer, 0, len(buffer))
 	}
 
 	// Initialize cryptographic MAC function
@@ -122,39 +135,58 @@ func CalcMac(auth []byte, pktID epic.PktID, s *slayers.SCION,
 		return nil, err
 	}
 	// Prepare the input for the MAC function
-	inputLength, err := prepareMacInput(pktID, s, timestamp, buffer)
+	inputLength, err := prepareMacInput(pktID, s, timestamp, buffer /*@, ub @*/)
 	if err != nil {
 		return nil, err
 	}
+	// @ assert 16 <= inputLength
+	// @ assert f.BlockSize() == 16
 	// Calculate Epic MAC = first 4 bytes of the last CBC block
+	// @ sl.SplitRange_Bytes(buffer, 0, inputLength, writePerm)
 	input := buffer[:inputLength]
 	f.CryptBlocks(input, input)
-	return input[len(input)-f.BlockSize() : len(input)-f.BlockSize()+4], nil
+	// @ ghost start := len(input)-f.BlockSize()
+	// @ 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)
+	// @ }
+	// @ assert (sl.AbsSlice_Bytes(result, 0, len(result)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer)))
+	return result, nil
 }
 
 // VerifyHVF verifies the correctness of the HVF (PHVF or the LHVF) field in the EPIC packet by
 // recalculating and comparing it. If the EPIC authenticator (auth), which denotes the full 16
 // 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.
-// @ trusted
-// @ requires Uncallable()
+// @ preserves sl.AbsSlice_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)
+// @ ensures   reserr != nil ==> reserr.ErrorMem()
+// @ decreases
 func VerifyHVF(auth []byte, pktID epic.PktID, s *slayers.SCION,
-	timestamp uint32, hvf []byte, buffer []byte) error {
+	timestamp uint32, hvf []byte, buffer []byte /*@ , ghost ub []byte @*/) (reserr error) {
 
 	if s == nil || len(auth) != AuthLen {
 		return serrors.New("invalid input")
 	}
 
-	mac, err := CalcMac(auth, pktID, s, timestamp, buffer)
+	mac, err := CalcMac(auth, pktID, s, timestamp, buffer /*@ , ub @*/)
 	if err != nil {
 		return err
 	}
 
 	if subtle.ConstantTimeCompare(hvf, mac) == 0 {
+		// @ apply sl.AbsSlice_Bytes(mac, 0, len(mac)) --* sl.AbsSlice_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))
 	return nil
 }
 
@@ -172,12 +204,9 @@ func CoreFromPktCounter(counter uint32) (uint8, uint32) {
 	return coreID, coreCounter
 }
 
-// (VerifiedSCION) The following verifies if we remove `Uncallable()“
-// from the precondition, but it seems to suffer from perf. problems.
-// @ requires  Uncallable()
 // @ requires  len(key) == 16
-// @ requires  sl.AbsSlice_Bytes(key, 0, len(key))
-// @ ensures   reserr == nil ==> res.Mem()
+// @ preserves acc(sl.AbsSlice_Bytes(key, 0, len(key)), R50)
+// @ ensures   reserr == nil ==> res != nil && res.Mem() && res.BlockSize() == 16
 // @ ensures   reserr != nil ==> reserr.ErrorMem()
 // @ decreases
 func initEpicMac(key []byte) (res cipher.BlockMode, reserr error) {
@@ -193,13 +222,11 @@ func initEpicMac(key []byte) (res cipher.BlockMode, reserr error) {
 	return mode, nil
 }
 
-// (VerifiedSCION) This function is mostly verified, but needs to be revisited before
-// dropping the precondition `Uncallable()`.
-// @ requires  Uncallable()
 // @ 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))
+// @ ensures   reserr == nil ==> 16 <= res && res <= len(inputBuffer)
 // @ ensures   reserr != nil ==> reserr.ErrorMem()
 // @ decreases
 func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
@@ -230,6 +257,10 @@ func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
 
 	// Calculate a multiple of 16 such that the input fits in
 	nrBlocks := int(math.Ceil((float64(23) + float64(l)) / float64(16)))
+	// (VerifiedSCION) The following assumptions cannot be currently proven due to Gobra's incomplete
+	// support for floats.
+	// @ assume 23 + l <= nrBlocks * 16
+	// @ assume nrBlocks * 16 <= 23 + l + 16
 	inputLength := 16 * nrBlocks
 
 	// Fill input
@@ -263,9 +294,24 @@ func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
 	// @ 	&inputBuffer[offset:][i] == &inputBuffer[offset+i]
 	binary.BigEndian.PutUint16(inputBuffer[offset:], s.PayloadLen)
 	offset += 2
+	// @ assert offset == 23 + l
+	// @ assert offset <= inputLength
+	// @ assert inputLength <= len(inputBuffer)
 	// @ assert forall i int :: { &inputBuffer[offset:inputLength][i] } 0 <= i && i < len(inputBuffer[offset:inputLength]) ==>
 	// @ 	&inputBuffer[offset:inputLength][i] == &inputBuffer[offset+i]
-	copy(inputBuffer[offset:inputLength], zeroInitVector[:] /*@ , R20 @*/)
+	// @ assert forall i int :: { &inputBuffer[offset:inputLength][i] } 0 <= i && i < len(inputBuffer[offset:inputLength]) ==>
+	// @ 	acc(&inputBuffer[offset:inputLength][i])
+	// @ establishPostInitInvariant()
+	// @ unfold acc(postInitInvariant(), _)
+	// @ assert acc(sl.AbsSlice_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)
+	// @ 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))
 	return inputLength, nil
 }

pkg/slayers/scion_spec.gobra

@@ -281,6 +281,18 @@ func (s *SCION) UBPath(ub []byte) []byte {
 		ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]
 }
 
+ghost
+pure
+requires acc(s.Mem(ub), _)
+decreases
+func (s *SCION) UBScionPath(ub []byte) []byte {
+	return unfolding acc(s.Mem(ub), _) in
+		let ubPath := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
+		typeOf(s.Path) == *epic.Path ?
+			unfolding acc(s.Path.Mem(ubPath), _) in ubPath[epic.MetadataLen:] :
+			ubPath
+}
+
 ghost
 pure
 requires acc(s.Mem(ub), _)
@@ -297,6 +309,26 @@ func (s *SCION) PathEndIdx(ub []byte) int {
 	return unfolding acc(s.Mem(ub), _) in int(s.HdrLen*LineLen)
 }
 
+ghost
+pure
+requires acc(s.Mem(ub), _)
+decreases
+func (s *SCION) PathScionStartIdx(ub []byte) int {
+	return unfolding acc(s.Mem(ub), _) in
+		let offset := CmnHdrLen+s.AddrHdrLenSpecInternal() in
+		typeOf(s.Path) == *epic.Path ?
+			offset + epic.MetadataLen :
+			offset
+}
+
+ghost
+pure
+requires acc(s.Mem(ub), _)
+decreases
+func (s *SCION) PathScionEndIdx(ub []byte) int {
+	return unfolding acc(s.Mem(ub), _) in int(s.HdrLen*LineLen)
+}
+
 ghost
 requires  0 < p
 preserves acc(s.Mem(ub), p)
@@ -317,6 +349,19 @@ func (s *SCION) GetPath(ub []byte) path.Path {
 	return unfolding acc(s.Mem(ub), _) in s.Path
 }
 
+ghost
+pure
+requires acc(s.Mem(ub), _)
+decreases
+func (s *SCION) GetScionPath(ub []byte) path.Path {
+	return unfolding acc(s.Mem(ub), _) in (
+	typeOf(s.Path) == *epic.Path ?
+		(let ubPath := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
+			unfolding acc(s.Path.Mem(ubPath), _) in
+			(path.Path)(s.Path.(*epic.Path).ScionPath)) :
+		s.Path)
+}
+
 ghost
 requires  acc(s.Mem(ub), _)
 decreases

verification/dependencies/crypto/aes/cipher.gobra

@@ -10,6 +10,7 @@ package aes
 
 import "crypto/cipher"
 import "github.com/scionproto/scion/verification/utils/slices"
+import . "github.com/scionproto/scion/verification/utils/definitions"
 
 // The AES block size in bytes.
 const BlockSize = 16
@@ -19,10 +20,13 @@ const BlockSize = 16
 // either 16, 24, or 32 bytes to select
 // AES-128, AES-192, or AES-256.
 trusted
-requires  len(key) == 16 || len(key) == 24 || len(key) == 32
-preserves slices.AbsSlice_Bytes(key, 0, len(key))
+preserves acc(slices.AbsSlice_Bytes(key, 0, len(key)), R50)
 ensures   err == nil ==>
-	(result != nil && result.Mem() && result.BlockSize() == len(key))
+	len(key) == 16 || len(key) == 24 || len(key) == 32
+ensures   err == nil ==>
+	(result != nil &&
+	result.Mem()   &&
+	result.BlockSize() == len(key))
 ensures   err != nil ==> err.ErrorMem()
 decreases
 func NewCipher(key []byte) (result cipher.Block, err error) {

verification/dependencies/crypto/cipher/cbc.gobra

@@ -21,10 +21,11 @@ import "github.com/scionproto/scion/verification/utils/slices"
 // mode, using the given Block. The length of iv must be the same as the
 // Block's block size.
 trusted
-requires b != nil && b.Mem()
-requires len(iv) == b.BlockSize()
-requires slices.AbsSlice_Bytes(iv, 0, len(iv))
-ensures  result.Mem()
+requires  b != nil && b.Mem()
+requires  len(iv) == b.BlockSize()
+preserves acc(slices.AbsSlice_Bytes(iv, 0, len(iv)), _)
+ensures   result != nil && result.Mem()
+ensures   result.BlockSize() == old(b.BlockSize())
 decreases _
 func NewCBCEncrypter(b Block, iv []byte) (result BlockMode) {
 	if len(iv) != b.BlockSize() {

verification/dependencies/crypto/cipher/cipher.gobra

@@ -94,8 +94,10 @@ type BlockMode interface {
 	// maintains state and does not reset at each CryptBlocks call.
 	requires  len(src) <= len(dst)
 	preserves Mem()
-	preserves slices.AbsSlice_Bytes(dst, 0, len(dst))
+	preserves acc(slices.AbsSlice_Bytes(dst, 0, len(dst)), 1 - R10)
+	preserves dst !== src ==> acc(slices.AbsSlice_Bytes(dst, 0, len(dst)), R10)
 	preserves acc(slices.AbsSlice_Bytes(src, 0, len(src)), R10)
+	ensures   BlockSize() == old(BlockSize())
 	decreases
 	CryptBlocks(dst, src []byte)
 }