From c17ec5802c3ca975053734be47ad6c8d5f92b3dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 1 Mar 2024 22:10:40 +0100 Subject: [PATCH 1/2] libepic --- pkg/experimental/epic/epic.go | 80 +++++++++++++++---- .../dependencies/crypto/aes/cipher.gobra | 10 ++- .../dependencies/crypto/cipher/cbc.gobra | 9 ++- .../dependencies/crypto/cipher/cipher.gobra | 4 +- 4 files changed, 78 insertions(+), 25 deletions(-) diff --git a/pkg/experimental/epic/epic.go b/pkg/experimental/epic/epic.go index c72529bbf..2a3c083f6 100644 --- a/pkg/experimental/epic/epic.go +++ b/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,14 +135,26 @@ 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 @@ -137,24 +162,31 @@ 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. -// @ 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 } diff --git a/verification/dependencies/crypto/aes/cipher.gobra b/verification/dependencies/crypto/aes/cipher.gobra index fdab1c7e8..3dd4949b5 100644 --- a/verification/dependencies/crypto/aes/cipher.gobra +++ b/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) { diff --git a/verification/dependencies/crypto/cipher/cbc.gobra b/verification/dependencies/crypto/cipher/cbc.gobra index d27cd4e79..a195b0260 100644 --- a/verification/dependencies/crypto/cipher/cbc.gobra +++ b/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() { diff --git a/verification/dependencies/crypto/cipher/cipher.gobra b/verification/dependencies/crypto/cipher/cipher.gobra index 8573aae95..76c9d6364 100644 --- a/verification/dependencies/crypto/cipher/cipher.gobra +++ b/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) } From f892670323b5ce7c68ab67f86e2bcec789927932 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 1 Mar 2024 22:14:32 +0100 Subject: [PATCH 2/2] add changes to scion_spec.gobra --- pkg/slayers/scion_spec.gobra | 45 ++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index f464b6951..632535619 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/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