Merge branch 'try-diff-trigger-scion-path' of https://github.com/vipe…

…rproject/VerifiedSCION into try-diff-trigger-scion-path

.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 }}

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://github.com/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/slayers/path/scion/raw.go

@@ -557,32 +557,72 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/)
 	// https://github.com/viperproject/gobra/issues/192
 	//@ assume 0 <= tmpHopField.ConsIngress && 0 <= tmpHopField.ConsEgress
 	//@ fold acc(tmpHopField.Mem(), R9)
-	//@ unfold acc(s.Mem(ubuf), R20)
-	//@ unfold acc(s.Base.Mem(), R20)
+	//@ reveal validPktMetaHdr(ubuf)
+	//@ unfold acc(s.Mem(ubuf), R50)
+	//@ unfold acc(s.Base.Mem(), R50)
+	//@ ghost currInfIdx := int(s.PathMeta.CurrINF)
+	//@ ghost currHfIdx := int(s.PathMeta.CurrHF)
+	//@ ghost seg1Len := int(s.PathMeta.SegLen[0])
+	//@ ghost seg2Len := int(s.PathMeta.SegLen[1])
+	//@ ghost seg3Len := int(s.PathMeta.SegLen[2])
+	//@ ghost segLens := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
+	//@ ghost segLen := segLens.LengthOfCurrSeg(idx)
+	//@ ghost prevSegLen := segLens.LengthOfPrevSeg(idx)
+	//@ ghost offset := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
+	//@ ghost hopfieldOffset := MetaLen + s.NumINF*path.InfoLen
 	if idx >= s.NumHops {
 		// (VerifiedSCION) introduced `err`
 		err := serrors.New("HopField index out of bounds", "max", s.NumHops-1, "actual", idx)
-		//@ fold acc(s.Base.Mem(), R20)
-		//@ fold acc(s.Mem(ubuf), R20)
+		//@ fold acc(s.Base.Mem(), R50)
+		//@ fold acc(s.Mem(ubuf), R50)
 		return err
 	}
 	hopOffset := MetaLen + s.NumINF*path.InfoLen + idx*path.HopLen
-	//@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm)
-	//@ assert sl.Bytes(s.Raw, 0, len(s.Raw))
-	//@ sl.SplitRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm)
+
+	//@ SliceBytesIntoSegments(ubuf, segLens, HalfPerm)
+	//@ SliceBytesIntoInfoFields(ubuf[:hopfieldOffset], s.NumINF, segLens, R40)
+
+	//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
+	//@ ghost inf := path.BytesToAbsInfoField(InfofieldByteSlice(ubuf, currInfIdx), 0)
+	//@ ghost hfIdxSeg := idx-prevSegLen
+	//@ ghost currHopfields := HopfieldsByteSlice(ubuf, currInfIdx, segLens)
+	//@ ghost if idx == currHfIdx {
+	//@ 	CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
+	//@ 	LeftSegEquality(ubuf, currInfIdx+1, segLens)
+	//@ 	MidSegEquality(ubuf, currInfIdx+2, segLens)
+	//@ 	RightSegEquality(ubuf, currInfIdx-1, segLens)
+	//@ 	reveal s.absPkt(ubuf)
+	//@ 	SplitHopfields(currHopfields, hfIdxSeg, segLen, R0)
+	//@ 	EstablishBytesStoreCurrSeg(currHopfields, hfIdxSeg, segLen, inf)
+	//@ 	SplitHopfields(currHopfields, hfIdxSeg, segLen, R0)
+	//@ } else {
+	//@ 	sl.SplitRange_Bytes(ubuf[offset:offset+segLen*path.HopLen], hfIdxSeg*path.HopLen,
+	//@ 		(hfIdxSeg+1)*path.HopLen, HalfPerm)
+	//@ }
+	//@ sl.SplitRange_Bytes(ubuf, hopOffset, hopOffset+path.HopLen, HalfPerm)
 	ret := tmpHopField.SerializeTo(s.Raw[hopOffset : hopOffset+path.HopLen])
-	//@ sl.CombineRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm)
-	//@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm)
-	//@ fold acc(s.Base.Mem(), R20)
-	//@ fold acc(s.Mem(ubuf), R20)
-	// (VerifiedSCION) The proof for these assumptions is provided in PR #361
-	// (https://github.com/viperproject/VerifiedSCION/pull/361), which will
-	// be merged once the performance issues are resolved.
-	//@ TemporaryAssumeForIO(validPktMetaHdr(ubuf) && s.GetBase(ubuf).EqAbsHeader(ubuf))
-	//@ TemporaryAssumeForIO(idx == int(old(s.GetCurrHF(ubuf))) ==>
-	//@  	let oldPkt := old(s.absPkt(ubuf)) in
-	//@  	let newPkt := oldPkt.UpdateHopField(hop.ToIO_HF()) in
-	//@  	s.absPkt(ubuf) == newPkt)
+	//@ sl.CombineRange_Bytes(ubuf, hopOffset, hopOffset+path.HopLen, HalfPerm)
+	//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
+	//@ assert reveal validPktMetaHdr(ubuf)
+	//@ ghost if idx == currHfIdx {
+	//@ 	CombineHopfields(currHopfields, hfIdxSeg, segLen, R0)
+	//@ 	EstablishBytesStoreCurrSeg(currHopfields, hfIdxSeg, segLen, inf)
+	//@ 	CombineHopfields(currHopfields, hfIdxSeg, segLen, R0)
+	//@ 	CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
+	//@ 	LeftSegEquality(ubuf, currInfIdx+1, segLens)
+	//@ 	MidSegEquality(ubuf, currInfIdx+2, segLens)
+	//@ 	RightSegEquality(ubuf, currInfIdx-1, segLens)
+	//@ 	reveal s.absPkt(ubuf)
+	//@ 	assert s.absPkt(ubuf).CurrSeg.Future ==
+	//@ 		seq[io.IO_HF]{tmpHopField.ToIO_HF()} ++ old(s.absPkt(ubuf).CurrSeg.Future[1:])
+	//@ } else {
+	//@ 	sl.CombineRange_Bytes(ubuf[offset:offset+segLen*path.HopLen], hfIdxSeg*path.HopLen,
+	//@ 		(hfIdxSeg+1)*path.HopLen, HalfPerm)
+	//@ }
+	//@ CombineBytesFromInfoFields(ubuf[:hopfieldOffset], s.NumINF, segLens, R40)
+	//@ CombineBytesFromSegments(ubuf, segLens, HalfPerm)
+	//@ fold acc(s.Base.Mem(), R50)
+	//@ fold acc(s.Mem(ubuf), R50)
 	return ret
 }
 

verification/dependencies/github.com/google/gopacket/base.gobra

@@ -60,8 +60,8 @@ ensures   len(res) != 0 ==> res === ub[start:end]
 decreases
 func (p Payload) Payload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
 	res = []byte(p)
-    assert unfolding acc(p.Mem(ub), R20) in true
-    return res, 0, len(p)
+	assert unfolding acc(p.Mem(ub), R20) in true
+	return res, 0, len(p)
 }
 
 requires b != nil && b.Mem()

verification/io/dataplane_abstract.gobra

@@ -21,16 +21,16 @@ package io
 //     to the interface y of AS a2.
 type DataPlaneSpec adt {
 	DataPlaneSpec_{
-		linkTypes		dict[IO_ifs]IO_Link
-		neighborIAs		dict[IO_ifs]IO_as
-		localIA			IO_as
-		links			dict[AsIfsPair]AsIfsPair
+		linkTypes   dict[IO_ifs]IO_Link
+		neighborIAs dict[IO_ifs]IO_as
+		localIA     IO_as
+		links       dict[AsIfsPair]AsIfsPair
 	}
 }
 
 type AsIfsPair struct {
-	asid	IO_as
-	ifs		IO_ifs
+	asid IO_as
+	ifs  IO_ifs
 }
 
 ghost

verification/io/other_defs.gobra

@@ -200,6 +200,7 @@ type IO_dp2_state adt {
 }
 
 ghost
+opaque
 decreases
 pure func (m IO_msgterm) extract_asid() IO_as {
 	return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_

verification/io/router.gobra

@@ -27,47 +27,72 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm {
 		case none[IO_ifs]:
 			MsgTerm_Empty{}
 		default:
-			IO_msgterm(MsgTerm_AS{IO_as(get(ifs))})
+			MsgTerm_AS{IO_as(get(ifs))}
 	}
 }
 
 ghost
 decreases
 pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool {
+	return hf_valid_impl(dp.Asid(), ts, uinfo, hf)
+}
+
+ghost
+decreases
+pure func hf_valid_impl(asid IO_as, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool {
 	return let inif := hf.InIF2 in
 		let egif := hf.EgIF2 in
-		let x := hf.HVF in
-		let l := IO_msgterm(MsgTerm_L{
-			seq[IO_msgterm]{
-				IO_msgterm(MsgTerm_Num{ts}),
-				if2term(inif),
-				if2term(egif),
-				IO_msgterm(MsgTerm_FS{uinfo})}}) in
-		x == mac(macKey(asidToKey(dp.Asid())), l)
+		let hvf := hf.HVF in
+		let next := nextMsgtermSpec(asid, inif, egif, ts, uinfo) in
+		hvf == next
+}
+
+ghost
+opaque
+ensures result.extract_asid() == asid
+decreases
+pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) (result IO_msgterm) {
+	return let l := plaintextToMac(inif, egif, ts, uinfo) in
+		let res := mac(macKey(asidToKey(asid)), l) in
+		let _ := reveal res.extract_asid() in
+		res
+}
+
+ghost
+decreases
+pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm {
+	return MsgTerm_L {
+		seq[IO_msgterm]{
+			MsgTerm_Num{ts},
+			if2term(inif),
+			if2term(egif),
+			MsgTerm_FS{uinfo},
+		},
+	}
 }
 
 ghost
 decreases
 pure func macKey(key IO_key) IO_msgterm {
-	return IO_msgterm(MsgTerm_Key{key})
+	return MsgTerm_Key{key}
 }
 
 ghost
 decreases
 pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm {
-	return IO_msgterm( MsgTerm_Hash {
-		MsgTerm_Hash_ : IO_msgterm( MsgTerm_MPair{
-			MsgTerm_MPair_1 : fst,
-			MsgTerm_MPair_2 : snd,
-		}),
-	})
+	return MsgTerm_Hash {
+		MsgTerm_Hash_: MsgTerm_MPair {
+			MsgTerm_MPair_1: fst,
+			MsgTerm_MPair_2: snd,
+		},
+	}
 }
 
 // helper function, not defined in IO spec
 ghost
 decreases
-pure func asidToKey(asid IO_as) IO_key{
-	return IO_key(Key_macK{asid})
+pure func asidToKey(asid IO_as) IO_key {
+	return Key_macK{asid}
 }
 
 ghost

verification/utils/definitions/definitions.gobra

@@ -129,8 +129,3 @@ ghost
 ensures b
 decreases
 func AssumeForIO(b bool)
-
-ghost
-ensures b
-decreases
-func TemporaryAssumeForIO(b bool)