Verify packSCMP (#243)

* start

* make type-check

* backup

* fix syntax errors

* establish necessary precondition of DecodeFromBytes

* remove TODOs

* backup

* move on with proof obligations

* verify packSCMP; reinstate TODO()s for doing the proof step by step

* backup

* backup

* fix parse and type errors

* fix packscmp

* backup

* backup

* kill branches for now

* backup

* backup

* remove files pushed by mistake

* del file

* fix verification error

* change comment format

* backup

* reset changes to scion_spec.gobra

* continue making progress

* backup

* simplify spec

* backup

* non-termination again

* backup

* packSCMP Continued (#373)

* fix missing precondition for packSCMP

* progress scmp

* further progress

* further scmp fixes

* fix syntax error and strengthen spec of erros.Is function

* fix verification error

* fix verification errors in process()

* drop last scmp assumption

* fix verification errors in process()

* add missing postconditions to resolveInbound

* fix p.d permissions

* remove wrong precondition from validateEgressUp()

* clean up

* feedback

* Update router/dataplane.go

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Move ownership of underlying slice of `SerializableBuffer` to outside of `Mem()` (#374)

* fix missing precondition for packSCMP

* progress scmp

* further progress

* further scmp fixes

* fix syntax error and strengthen spec of erros.Is function

* fix verification error

* fix verification errors in process()

* drop last scmp assumption

* fix verification errors in process()

* add missing postconditions to resolveInbound

* fix p.d permissions

* save

* remove wrong precondition from validateEgressUp()

* clean up

* feedback

* change dependencies to new buffer approach

* remove buffWithFullPerm flag from scionPacketProcessor

* fix verification errors

* fix permission mistake

* Apply suggestions from code review

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* pass underlying buffer slice to prepareSCMP

* remove deep ownership of buffer slice in message

* fix verification error in run

* fix injectivity issue in run() and verification error in newPacketProcessor

* different trigger

* proves injectivity for message buffer directly without sets

* test: remove unnecessary invariants in run()

* improvements to injectivity lemma for messages

* introduce new lemma PermsImplyIneq()

* fixed missing preconditions

* minor fixes and feedback

* fix verification error

* fmt

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

---------

Co-authored-by: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com>

.gitignore

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

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)
 

pkg/slayers/path/scion/raw_spec.gobra

@@ -373,15 +373,15 @@ requires validPktMetaHdr(raw)
 decreases
 pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
 	return let _ := reveal validPktMetaHdr(raw) in
-		let metaHdr := RawBytesToMetaHdr(raw) in
+		let metaHdr := RawBytesToMetaHdr(raw)  in
 		let currInfIdx := int(metaHdr.CurrINF) in
-		let currHfIdx := int(metaHdr.CurrHF) in
-		let seg1Len := int(metaHdr.SegLen[0]) in
-		let seg2Len := int(metaHdr.SegLen[1]) in
-		let seg3Len := int(metaHdr.SegLen[2]) in
+		let currHfIdx := int(metaHdr.CurrHF)   in
+		let seg1Len := int(metaHdr.SegLen[0])  in
+		let seg2Len := int(metaHdr.SegLen[1])  in
+		let seg3Len := int(metaHdr.SegLen[2])  in
 		let segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len) in
-		let segLen := segs.LengthOfCurrSeg(currHfIdx) in
-		let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in
+		let segLen := segs.LengthOfCurrSeg(currHfIdx)            in
+		let prevSegLen := segs.LengthOfPrevSeg(currHfIdx)        in
 		let numINF := segs.NumInfoFields() in
 		let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in
 		io.IO_Packet2 {
@@ -428,7 +428,7 @@ pure func validPktMetaHdr(raw []byte) bool {
 		let segs := io.CombineSegLens(seg1, seg2, seg3) in
 		let base := RawBytesToBase(raw)       in
 		0 < metaHdr.SegLen[0] &&
-		base.Valid()     &&
+		base.Valid()          &&
 		PktLen(segs, MetaLen) <= len(raw)
 }
 

pkg/slayers/scion.go

@@ -218,9 +218,11 @@ func (s *SCION) NetworkFlow() (res gopacket.Flow) {
 // @ requires  b != nil && b.Mem()
 // @ requires  acc(s.Mem(ubuf), R0)
 // @ requires  sl.Bytes(ubuf, 0, len(ubuf))
+// @ requires  sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
 // @ ensures   b.Mem()
 // @ ensures   acc(s.Mem(ubuf), R0)
 // @ ensures   sl.Bytes(ubuf, 0, len(ubuf))
+// @ ensures   sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
 // TODO: hide internal spec details
 // @ ensures   e == nil && s.HasOneHopPath(ubuf) ==>
 // @	len(b.UBuf()) == old(len(b.UBuf())) + unfolding acc(s.Mem(ubuf), R55) in
@@ -257,7 +259,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
 	}
 	// @ ghost uSerBufN := b.UBuf()
 	// @ assert buf === uSerBufN[:scnLen]
-	// @ b.ExchangePred()
 
 	// @ unfold acc(sl.Bytes(uSerBufN, 0, len(uSerBufN)), writePerm)
 	// Serialize common header.
@@ -287,7 +288,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
 		// @ sl.Unslice_Bytes(uSerBufN, 0, CmnHdrLen, R54)
 		// @ sl.CombineRange_Bytes(uSerBufN, CmnHdrLen, scnLen, writePerm)
 		// @ sl.CombineRange_Bytes(ubuf, CmnHdrLen, len(ubuf), R10)
-		// @ b.RestoreMem(uSerBufN)
 		return err
 	}
 	offset := CmnHdrLen + s.AddrHdrLen( /*@ nil, true @*/ )
@@ -320,7 +320,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
 	// @ sl.CombineRange_Bytes(uSerBufN, offset, scnLen, HalfPerm)
 	// @ sl.CombineRange_Bytes(ubuf, startP, endP, HalfPerm)
 	// @ reveal IsSupportedPkt(uSerBufN)
-	// @ b.RestoreMem(uSerBufN)
 	// @ reveal IsSupportedRawPkt(b.View())
 	return tmp
 }

pkg/slayers/scion_spec.gobra

@@ -336,8 +336,8 @@ ghost
 requires  0 < p
 preserves acc(s.Mem(ub), p)
 ensures   let start := s.PathStartIdx(ub) in
-		  let end   := s.PathEndIdx(ub) in
-		  0 <= start && start <= end && end <= len(ub)
+	let end := s.PathEndIdx(ub) in
+	0 <= start && start <= end && end <= len(ub)
 decreases
 func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) {
 	unfold acc(s.Mem(ub), p)
@@ -462,7 +462,7 @@ pure func ValidPktMetaHdr(raw []byte) bool {
 		let length := GetLength(raw) in
 		length <= len(raw) &&
 		unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
-	 	let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in
+		let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in
 		let hdr := binary.BigEndian.Uint32(rawHdr) in
 		let metaHdr := scion.DecodedFrom(hdr)      in
 		let seg1 := int(metaHdr.SegLen[0])         in

pkg/slayers/scmp.go

@@ -111,6 +111,7 @@ func (s *SCMP) NextLayerType( /*@ ghost ub []byte @*/ ) gopacket.LayerType {
 // @ requires  b != nil
 // @ requires  s.Mem(ubufMem)
 // @ preserves b.Mem()
+// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
 // @ ensures   err == nil ==> s.Mem(ubufMem)
 // @ ensures   err != nil ==> err.ErrorMem()
 // @ decreases
@@ -121,15 +122,6 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp
 		return err
 	}
 	// @ unfold s.Mem(ubufMem)
-
-	// @ requires len(underlyingBufRes) >= 4
-	// @ requires bytes === underlyingBufRes[:4]
-	// @ requires b != nil
-	// @ preserves acc(&s.TypeCode)
-	// @ preserves b.Mem() && b.UBuf() === underlyingBufRes
-	// @ decreases
-	// @ outline (
-	// @ b.ExchangePred()
 	// @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm)
 	// @ unfold sl.Bytes(underlyingBufRes, 0, 2)
 	// @ assert forall i int :: { &bytes[i] } 0 <= i && i < 2 ==> &bytes[i] == &underlyingBufRes[i]
@@ -138,59 +130,37 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp
 	// @ unfold sl.Bytes(bytes, 0, 2)
 	// @ fold sl.Bytes(underlyingBufRes, 0, 2)
 	// @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm)
-	// @ b.RestoreMem(underlyingBufRes)
-	// @ )
 
 	if opts.ComputeChecksums {
 		if s.scn == nil {
 			// @ fold s.Mem(ubufMem)
 			return serrors.New("can not calculate checksum without SCION header")
 		}
 		// zero out checksum bytes
-		// @ requires len(underlyingBufRes) >= 4
-		// @ requires bytes === underlyingBufRes[:4]
-		// @ requires b != nil
-		// @ preserves b.Mem() && b.UBuf() === underlyingBufRes
-		// @ decreases
-		// @ outline (
-		// @ b.ExchangePred()
 		// @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
 		// @ unfold sl.Bytes(underlyingBufRes, 0, 4)
 		// @ assert forall i int :: { &bytes[i] } 0 <= i && i < 4 ==> &bytes[i] == &underlyingBufRes[i]
 		bytes[2] = 0
 		bytes[3] = 0
 		// @ fold sl.Bytes(underlyingBufRes, 0, 4)
 		// @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
-		// @ b.RestoreMem(underlyingBufRes)
-		// @ )
 		verScionTmp := b.Bytes()
 		// @ unfold s.scn.ChecksumMem()
 		s.Checksum, err = s.scn.computeChecksum(verScionTmp, uint8(L4SCMP))
 		// @ fold s.scn.ChecksumMem()
-		// @ b.RestoreMem(verScionTmp)
 		if err != nil {
 			// @ fold s.Mem(ubufMem)
 			return err
 		}
 
 	}
-	// @ requires len(underlyingBufRes) >= 4
-	// @ requires bytes === underlyingBufRes[:4]
-	// @ requires b != nil
-	// @ preserves acc(&s.Checksum)
-	// @ preserves b.Mem() && b.UBuf() === underlyingBufRes
-	// @ decreases
-	// @ outline (
-	// @ b.ExchangePred()
 	// @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
 	// @ unfold sl.Bytes(underlyingBufRes, 0, 4)
 	// @ assert forall i int :: { &bytes[i] } 0 <= i && i < 4 ==> &bytes[i] == &underlyingBufRes[i]
 	// @ assert forall i int :: { &bytes[2:][i] } 0 <= i && i < 2 ==> &bytes[2:][i] == &bytes[i + 2]
 	binary.BigEndian.PutUint16(bytes[2:], s.Checksum)
 	// @ fold sl.Bytes(underlyingBufRes, 0, 4)
 	// @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
-	// @ b.RestoreMem(underlyingBufRes)
-	// @ )
 	// @ fold s.Mem(ubufMem)
 	return nil
 }