Streamline the assumptions about MsgTerms

pkg/slayers/path/hopfield_spec.gobra

@@ -42,6 +42,7 @@ decreases
 pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) {
 	return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle + 2 + k]) in
 		let _ := Asserting(forall k int :: {&raw[middle+4:middle+6][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+6][k] == &raw[middle + 4 + k]) in
+		let _ := Asserting(forall k int :: {&raw[middle+6:middle+6+MacLen][k]} 0 <= k && k < MacLen ==> &raw[middle+6:middle+6+MacLen][k] == &raw[middle + 6 + k]) in
 		unfolding acc(slices.AbsSlice_Bytes(raw, start, end), _) in
 		let inif2 := binary.BigEndian.Uint16(raw[middle+2:middle+4]) in
 		let egif2 := binary.BigEndian.Uint16(raw[middle+4:middle+6]) in
@@ -50,7 +51,7 @@ pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) {
 		io.IO_HF(io.IO_HF_{
 			InIF2 : op_inif2,
 			EgIF2 : op_egif2,
-			HVF : AbsMac(raw[6:6+MacLen]),
+			HVF : AbsMac(FromSliceToMacArray(raw[middle+6:middle+6+MacLen])),
 		})
 }
 
@@ -60,16 +61,6 @@ pure func (h HopField) ToIO_HF() (io.IO_HF) {
 	return io.IO_HF(io.IO_HF_{
 			InIF2 : ifsToIO_ifs(h.ConsIngress),
 			EgIF2 : ifsToIO_ifs(h.ConsEgress),
-			HVF : AbsMac2(h.Mac),
+			HVF : AbsMac(h.Mac),
 		})
 }
-
-ghost
-decreases
-pure func AbsMac(mac []byte) (io.IO_msgterm)
-
-
-ghost
-decreases
-pure func AbsMac2(mac [MacLen]byte) (io.IO_msgterm)
-

pkg/slayers/path/infofield.go

@@ -131,16 +131,15 @@ func (inf *InfoField) SerializeTo(b []byte) (err error) {
 // UpdateSegID updates the SegID field by XORing the SegID field with the 2
 // first bytes of the MAC. It is the beta calculation according to
 // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation
+// @ requires hf.HVF == AbsMac(hfMac)
 // @ preserves acc(&inf.SegID)
-// requires hf.HVF == AbsMac(hfMac[:])
-// @ ensures absUinfo_(inf.SegID) == old(io.upd_uinfo(absUinfo_(inf.SegID), hf))
+// @ ensures AbsUInfoFromUint16(inf.SegID) ==
+// @ 	old(io.upd_uinfo(AbsUInfoFromUint16(inf.SegID), hf))
 // @ decreases
 func (inf *InfoField) UpdateSegID(hfMac [MacLen]byte /* @, ghost hf io.IO_HF @ */) {
 	//@ share hfMac
 	inf.SegID = inf.SegID ^ binary.BigEndian.Uint16(hfMac[:2])
-	// TODO: (Markus) How to argue that we need to assume this
-	// upd_uinfo equivalent to xor in the protocol
-	// @ assume absUinfo_(inf.SegID) == old(io.upd_uinfo(absUinfo_(inf.SegID), hf))
+	// @ AssumeForIO(AbsUInfoFromUint16(inf.SegID) == old(io.upd_uinfo(AbsUInfoFromUint16(inf.SegID), hf)))
 }
 
 // @ decreases

pkg/slayers/path/infofield_spec.gobra

@@ -74,13 +74,9 @@ pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm]
 		unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in
 		let _ := Asserting(forall k int :: {&raw[idx:idx+2][k]} 0 <= k && k < 2 ==>
 			&raw[idx:idx+4][k] == &raw[idx + k]) in
-		absUinfo_(binary.BigEndian.Uint16(raw[idx:idx+2]))
+		AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2]))
 }
 
-ghost
-decreases
-pure func absUinfo_(SegID uint16) set[io.IO_msgterm]
-
 // This type simplifies the infoField, making it easier
 // to use than the IO_seg3 from the IO-spec.
 type IntermediateAbsInfoField adt {
@@ -113,7 +109,7 @@ pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int
 		let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
 		IntermediateAbsInfoField(IntermediateAbsInfoField_{
 			AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
-			UInfo : absUinfo_(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
+			UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
 			ConsDir : raw[middle] & 0x1 == 0x1,
 			Peer : raw[middle] & 0x2  == 0x2,
 		})
@@ -124,7 +120,7 @@ decreases
 pure func (inf InfoField) ToIntermediateAbsInfoField() (IntermediateAbsInfoField) {
 	return IntermediateAbsInfoField(IntermediateAbsInfoField_{
 		AInfo : io.IO_ainfo(inf.Timestamp),
-		UInfo : absUinfo_(inf.SegID),
+		UInfo : AbsUInfoFromUint16(inf.SegID),
 		ConsDir : inf.ConsDir,
 		Peer : inf.Peer,
 	})

pkg/slayers/path/io_msgterm_spec.gobra

@@ -0,0 +1,46 @@
+// Copyright 2020 Anapaya Systems
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package path
+
+import "verification/io"
+
+// At the moment, we assume that all cryptographic operations performed at the code level
+// imply the desired properties at the IO spec level because we cannot currently prove in
+// Gobra the correctness of these operations. Given that we do not prove any properties
+// about this function, we currently do not provide a definition for it.
+
+ghost
+decreases
+pure func AbsUInfoFromUint16(SegID uint16) set[io.IO_msgterm]
+
+ghost
+decreases
+pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm)
+
+// The following function converts a slice with at least `MacLen` elements into
+// an (exclusive) array containing the mac. Note that there are no permissions
+// involved for accessing exclusive arrays. This functions is abstract for now
+// because Gobra does not allow for array literals in pure functions, even though
+// they are no more side-effectful than creating an instance of a struct type.
+// This will soon be fixed in Gobra.
+ghost
+requires MacLen <= len(mac)
+requires forall i int :: { &mac[i] } 0 <= i && i < MacLen ==> acc(&mac[i], _)
+ensures  len(res) == MacLen
+ensures  forall i int :: { res[i] } 0 <= i && i < MacLen ==> mac[i] == res[i]
+decreases
+pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte)

router/dataplane.go

@@ -2328,7 +2328,7 @@ func (p *scionPacketProcessor) updateNonConsDirIngressSegID( /*@ ghost ub []byte
 	// @ reveal p.EqAbsHopField(absPkt(dp, ub))
 	if !p.infoField.ConsDir && p.ingressID != 0 {
 		p.infoField.UpdateSegID(p.hopField.Mac /*@, p.hopField.ToIO_HF() @*/)
-		// @ assert path.absUinfo_(p.infoField.SegID) == old(io.upd_uinfo(path.absUinfo_(p.infoField.SegID), p.hopField.ToIO_HF()))
+		// @ assert path.AbsUInfoFromUint16(p.infoField.SegID) == old(io.upd_uinfo(path.AbsUInfoFromUint16(p.infoField.SegID), p.hopField.ToIO_HF()))
 		// (VerifiedSCION) the following property is guaranteed by the type system, but Gobra cannot infer it yet
 		// @ assume 0 <= p.path.GetCurrINF(ubPath)
 		// @ sl.SplitRange_Bytes(ub, start, end, HalfPerm)
@@ -2342,7 +2342,7 @@ func (p *scionPacketProcessor) updateNonConsDirIngressSegID( /*@ ghost ub []byte
 		// @ p.SubSliceAbsPktToAbsPkt(ub, start, end, dp)
 		// @ ghost sl.CombineRange_Bytes(ub, start, end, HalfPerm)
 		// @ absPktFutureLemma(dp, ub)
-		// @ assert  absPkt(dp, ub).CurrSeg.UInfo == old(io.upd_uinfo(path.absUinfo_(p.infoField.SegID), p.hopField.ToIO_HF()))
+		// @ assert  absPkt(dp, ub).CurrSeg.UInfo == old(io.upd_uinfo(path.AbsUInfoFromUint16(p.infoField.SegID), p.hopField.ToIO_HF()))
 		// @ assert reveal p.EqAbsInfoField(absPkt(dp, ub))
 		// @ assert reveal p.EqAbsHopField(absPkt(dp, ub))
 	}
@@ -2528,7 +2528,7 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte, ghost dp io.D
 	// need to update the SegID.
 	if p.infoField.ConsDir {
 		p.infoField.UpdateSegID(p.hopField.Mac /*@, p.hopField.ToIO_HF() @*/)
-		// @ assert path.absUinfo_(p.infoField.SegID) == old(io.upd_uinfo(path.absUinfo_(p.infoField.SegID), p.hopField.ToIO_HF()))
+		// @ assert path.AbsUInfoFromUint16(p.infoField.SegID) == old(io.upd_uinfo(path.AbsUInfoFromUint16(p.infoField.SegID), p.hopField.ToIO_HF()))
 		// @ assume 0 <= p.path.GetCurrINF(ubPath)
 		if err := p.path.SetInfoField(p.infoField, int( /*@ unfolding acc(p.path.Mem(ubPath), R45) in (unfolding acc(p.path.Base.Mem(), R50) in @*/ p.path.PathMeta.CurrINF /*@ ) @*/) /*@ , ubPath, dp @*/); err != nil {
 			// TODO parameter problem invalid path

verification/io/router.gobra

@@ -72,7 +72,7 @@ pure func asidToKey(asid IO_as) IO_key{
 
 ghost
 decreases
-pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm]{
+pure func upd_uinfo(segid set[IO_msgterm], hf IO_HF) set[IO_msgterm] {
 	return let setHVF := set[IO_msgterm]{hf.HVF} in
 		(segid union setHVF) setminus (segid intersection setHVF)
 }