processEpic

pkg/experimental/epic/epic.go

@@ -304,7 +304,7 @@ func prepareMacInput(pktID epic.PktID, s *slayers.SCION, timestamp uint32,
 	// @ establishPostInitInvariant()
 	// @ unfold acc(postInitInvariant(), _)
 	// @ assert acc(sl.Bytes(zeroInitVector[:], 0, 16), _)
-	// (VerifiedSCION) From the pkg invariant, we learn that we have a wildcard access to zeroInitVector.
+	// (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.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), R55)

pkg/slayers/path/epic/epic_spec.gobra

@@ -102,4 +102,11 @@ pure func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 
+ghost
+pure
+decreases
+func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+	return true
+}
+
 (*Path) implements path.Path

pkg/slayers/path/path.go

@@ -90,6 +90,7 @@ type Path interface {
 	//@ ensures   err == nil ==> IsValidResultOfDecoding(b)
 	//@ ensures   err != nil ==> err.ErrorMem()
 	//@ ensures   err != nil ==> NonInitMem()
+	//@ ensures   err == nil ==> IsValidResultOfDecoding(b, err)
 	//@ decreases
 	DecodeFromBytes(b []byte) (err error)
 	//@ ghost

pkg/slayers/path/scion/base_spec.gobra

@@ -146,6 +146,13 @@ pure func (s *Base) GetBase() Base {
 ghost
 requires s.Mem()
 decreases
+pure func (s *Base) GetBase() Base {
+	return unfolding acc(s.Mem(), _) in *s
+}
+
+ghost
+requires acc(s.Mem(), _)
+decreases
 pure func (s *Base) GetCurrHF() uint8 {
 	return s.GetMetaHdr().CurrHF
 }

pkg/slayers/path/scion/raw_spec.gobra

@@ -157,6 +157,13 @@ pure func (r *Raw) GetBase(ub []byte) Base {
 ghost
 requires r.Mem(ub)
 decreases
+pure func (r *Raw) GetBase(ub []byte) Base {
+	return unfolding acc(r.Mem(ub), _) in r.Base.GetBase()
+}
+
+ghost
+requires acc(r.Mem(ub), _)
+decreases
 pure func (r *Raw) GetNumINF(ghost ub []byte) int {
 	return unfolding r.Mem(ub) in
 		(unfolding r.Base.Mem() in r.NumINF)

router/dataplane.go

@@ -1654,10 +1654,21 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte,
 		// @ fold p.sInit()
 		return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/
 	case epic.PathType:
-		// @ TODO()
-		v1, v2 := p.processEPIC()
+		// @ sl.CombineRange_Bytes(ub, start, end, HalfPerm)
+		// @ ghost if lastLayerIdx >= 0 {
+		// @ 	ghost if !offsets[lastLayerIdx].isNil {
+		// @ 		o := offsets[lastLayerIdx]
+		// @ 		sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm)
+		// @ 	}
+		// @ }
+		// @ unfold acc(p.d.Mem(), _)
+		// @ assert reveal p.scionLayer.EqPathType(p.rawPkt)
+		// @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt))
+		// @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt))
+		v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ )
+		// @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer)
 		// @ fold p.sInit()
-		return v1, v2 /*@, false, io.ValUnit{} @*/
+		return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/
 	default:
 		// @ ghost if mustCombineRanges { ghost defer sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm) }
 		// @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer)
@@ -1853,54 +1864,124 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil
 	return p.process( /*@ ub, llIsNil, startLL, endLL , ioLock, ioSharedArg, dp @*/ )
 }
 
-// @ trusted
-// @ requires false
-func (p *scionPacketProcessor) processEPIC() (processResult, error) {
-
+// @ requires  0 <= startLL && startLL <= endLL && endLL <= len(ub)
+// @ requires  acc(&p.d, R5) && acc(p.d.Mem(), _) && p.d.WellConfigured()
+// @ requires  p.d.getValSvc() != nil
+// The ghost param ub here allows us to introduce a bound variable to p.rawPkt,
+// which slightly simplifies the spec
+// @ requires  acc(&p.rawPkt, R1) && ub === p.rawPkt
+// @ requires  acc(&p.path)
+// @ requires  p.scionLayer.Mem(ub)
+// @ requires  sl.Bytes(ub, 0, len(ub))
+// @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _)
+// @ preserves acc(&p.lastLayer, R10)
+// @ preserves p.lastLayer != nil
+// @ preserves (p.lastLayer !== &p.scionLayer && llIsNil) ==>
+// @ 	acc(p.lastLayer.Mem(nil), R10)
+// @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==>
+// @ 	acc(p.lastLayer.Mem(ub[startLL:endLL]), R10)
+// @ preserves acc(&p.ingressID, R20)
+// @ preserves acc(&p.infoField)
+// @ preserves acc(&p.hopField)
+// @ preserves acc(&p.segmentChange) && !p.segmentChange
+// @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem()
+// @ preserves acc(&p.macBuffers.scionInput, R10)
+// @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
+// @ preserves acc(&p.cachedMac)
+// @ ensures   acc(&p.d, R5)
+// @ ensures   acc(&p.path)
+// @ ensures   acc(&p.rawPkt, R1)
+// @ ensures   reserr == nil ==> p.scionLayer.Mem(ub)
+// @ ensures   reserr != nil ==> p.scionLayer.NonInitMem()
+// @ ensures   acc(sl.Bytes(ub, 0, len(ub)), 1 - R15)
+// @ ensures   p.d.validResult(respr, addrAliasesPkt)
+// @ ensures   addrAliasesPkt ==> (
+// @ 	respr.OutAddr != nil &&
+// @ 	(acc(respr.OutAddr.Mem(), R15) --* acc(sl.Bytes(ub, 0, len(ub)), R15)))
+// @ ensures   !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15)
+// @ ensures   respr.OutPkt !== ub && respr.OutPkt != nil ==>
+// @ 	sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt))
+// @ ensures   reserr != nil ==> reserr.ErrorMem()
+// contracts for IO-spec
+// @ requires p.scionLayer.EqPathType(p.rawPkt)
+// @ requires !slayers.IsSupportedPkt(p.rawPkt)
+// @ requires  p.d.DpAgreesWithSpec(dp)
+// @ requires  dp.Valid()
+// @ requires  acc(ioLock.LockP(), _)
+// @ requires  ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
+// @ ensures  (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{})
+// @ ensures  respr.OutPkt != nil ==>
+// @ 	newAbsPkt == absIO_val(respr.OutPkt, respr.EgressID) &&
+// @ 	newAbsPkt.isIO_val_Unsupported
+// @ decreases 0 if sync.IgnoreBlockingForTermination()
+func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) {
+	// @ TODO()
+	// @ unfold acc(p.scionLayer.Mem(ub), R10)
 	epicPath, ok := p.scionLayer.Path.(*epic.Path)
 	if !ok {
-		return processResult{}, malformedPath
+		// @ fold acc(p.scionLayer.Mem(ub), R10)
+		// @ p.scionLayer.DowngradePerm(ub)
+		// @ establishMemMalformedPath()
+		// @ fold p.d.validResult(respr, false)
+		return processResult{}, malformedPath /*@ , false, io.IO_val_Unit{}  @*/
 	}
 
+	// @ ghost startP := p.scionLayer.PathStartIdx(ub)
+	// @ ghost endP := p.scionLayer.PathEndIdx(ub)
+	// @ ghost ubPath := ub[startP:endP]
+	// @ unfold acc(epicPath.Mem(ubPath), R10)
 	p.path = epicPath.ScionPath
 	if p.path == nil {
-		return processResult{}, malformedPath
+		// @ fold acc(epicPath.Mem(ubPath), R10)
+		// @ fold acc(p.scionLayer.Mem(ub), R10)
+		// @ p.scionLayer.DowngradePerm(ub)
+		// @ establishMemMalformedPath()
+		// @ fold p.d.validResult(respr, false)
+		return processResult{}, malformedPath /*@ , false, io.IO_val_Unit{} @*/
 	}
 
-	isPenultimate := p.path.IsPenultimateHop()
-	isLast := p.path.IsLastHop()
+	isPenultimate := p.path.IsPenultimateHop( /*@ ubPath[epic.MetadataLen:] @*/ )
+	isLast := p.path.IsLastHop( /*@ ubPath[epic.MetadataLen:] @*/ )
+	// @ fold acc(epicPath.Mem(ubPath), R10)
+	// @ fold acc(p.scionLayer.Mem(ub), R10)
 
-	result, err := p.process()
+	result, err /*@ , addrAliases, newAbsPkt @*/ := p.process( /*@ ub, llIsNil, startLL, endLL, ioLock, ioSharedArg, dp @*/ )
 	if err != nil {
-		return result, err
+		return result, err /*@ , addrAliases, newAbsPkt @*/
 	}
+	// @ TODO()
 
 	if isPenultimate || isLast {
-		firstInfo, err := p.path.GetInfoField(0)
+		firstInfo, err := p.path.GetInfoField(0 /*@ , ubPath[epic.MetadataLen:] @*/)
 		if err != nil {
-			return processResult{}, err
+			// @ p.scionLayer.DowngradePerm(ub)
+			// @ fold p.d.validResult(respr, false)
+			return processResult{}, err /*@ , false, io.IO_val_Unit{} @*/
 		}
 
 		timestamp := time.Unix(int64(firstInfo.Timestamp), 0)
 		err = libepic.VerifyTimestamp(timestamp, epicPath.PktID.Timestamp, time.Now())
 		if err != nil {
+			// @ p.scionLayer.DowngradePerm(ub)
+			// @ fold p.d.validResult(respr, false)
 			// TODO(mawyss): Send back SCMP packet
-			return processResult{}, err
+			return processResult{}, err /*@ , false, io.IO_val_Unit{} @*/
 		}
 
 		HVF := epicPath.PHVF
 		if isLast {
 			HVF = epicPath.LHVF
 		}
 		err = libepic.VerifyHVF(p.cachedMac, epicPath.PktID,
-			&p.scionLayer, firstInfo.Timestamp, HVF, p.macBuffers.epicInput)
+			&p.scionLayer, firstInfo.Timestamp, HVF, p.macBuffers.epicInput /*@ , ub @*/)
 		if err != nil {
+			// @ p.scionLayer.DowngradePerm(ub)
 			// TODO(mawyss): Send back SCMP packet
-			return processResult{}, err
+			return processResult{}, err /*@ , false, io.IO_val_Unit{} @*/
 		}
 	}
 
-	return result, nil
+	return result, nil /*@ , false, io.IO_val_Unit{} @*/
 }
 
 // scionPacketProcessor processes packets. It contains pre-allocated per-packet
@@ -2044,7 +2125,7 @@ func (p *scionPacketProcessor) packSCMP(
 // @ requires  acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ requires  acc(p.scionLayer.Mem(ub), R5)
 // @ requires  acc(&p.path, R20)
-// @ requires  p.path === p.scionLayer.GetPath(ub)
+// @ requires  p.path === p.scionLayer.GetScionPath(ub)
 // @ requires  acc(&p.hopField) && acc(&p.infoField)
 // Preconditions for IO:
 // @ requires  p.scionLayer.EqAbsHeader(ub)
@@ -2053,7 +2134,7 @@ func (p *scionPacketProcessor) packSCMP(
 // @ ensures   acc(&p.d, R50)
 // @ ensures   acc(p.scionLayer.Mem(ub), R5)
 // @ ensures   acc(&p.path, R20)
-// @ ensures   p.path === p.scionLayer.GetPath(ub)
+// @ ensures   p.path === p.scionLayer.GetScionPath(ub)
 // @ ensures   acc(&p.hopField) && acc(&p.infoField)
 // @ ensures   respr === processResult{}
 // @ ensures   reserr == nil ==>
@@ -2096,7 +2177,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce
 		// TODO(lukedirtwalker) parameter problem invalid path?
 		return processResult{}, err
 	}
-	p.infoField, err = p.path.GetCurrentInfoField( /*@ ubPath @*/ )
+	p.infoField, err = p.path.GetCurrentInfoField( /*@ ubScionPath @*/ )
 	if err != nil {
 		// TODO(lukedirtwalker) parameter problem invalid path?
 		return processResult{}, err
@@ -2526,20 +2607,28 @@ func (p *scionPacketProcessor) invalidDstIA(
 func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @*/ ) (respr processResult, reserr error) {
 	// @ ghost startP := p.scionLayer.PathStartIdx(ub)
 	// @ ghost endP := p.scionLayer.PathEndIdx(ub)
-	// @ unfold acc(p.scionLayer.Mem(ub), R4)
-	// @ defer fold acc(p.scionLayer.Mem(ub), R4)
+	// @ ghost startScionP := p.scionLayer.PathScionStartIdx(ub)
+	// @ ghost endScionP := p.scionLayer.PathScionEndIdx(ub)
+	// @ unfold acc(p.scionLayer.Mem(ub), R5)
+	// @ defer fold acc(p.scionLayer.Mem(ub), R5)
 	// @ ghost ubPath := ub[startP:endP]
-	// @ sl.SplitRange_Bytes(ub, startP, endP, R5)
-	// @ ghost defer sl.CombineRange_Bytes(ub, startP, endP, R5)
+	// @ ghost ubScionPath := ub[startScionP:endScionP]
+
+	// @ ghost if typeOf(p.scionLayer.Path) == *epic.Path {
+	// @ 	unfold acc(p.scionLayer.Path.Mem(ubPath), R5)
+	// @ 	defer fold acc(p.scionLayer.Path.Mem(ubPath), R5)
+	// @ }
+	// @ sl.SplitRange_Bytes(ub, startScionP, endScionP, R5)
+	// @ ghost defer sl.CombineRange_Bytes(ub, startScionP, endScionP, R5)
 	// (VerifiedSCION) Gobra cannot prove this property yet, even though it follows
 	// from the type system
-	// @ assume 0 <= p.path.GetCurrHF(ubPath) // TODO: drop assumptions like this
-	if p.path.IsFirstHop( /*@ ubPath @*/ ) || p.ingressID != 0 {
+	// @ assume 0 <= p.path.GetCurrHF(ubScionPath) // TODO: drop assumptions like this
+	if p.path.IsFirstHop( /*@ ubScionPath @*/ ) || p.ingressID != 0 {
 		// not a transit packet, nothing to check
 		// @ fold p.d.validResult(processResult{}, false)
 		return processResult{}, nil
 	}
-	pktIngressID := p.ingressInterface( /*@ ubPath @*/ )
+	pktIngressID := p.ingressInterface( /*@ ubScionPath @*/ )
 	// @ p.d.getInternalNextHops()
 	// @ ghost if p.d.internalNextHops != nil { unfold acc(accAddr(p.d.internalNextHops), _) }
 	expectedSrc, ok := p.d.internalNextHops[pktIngressID]
@@ -2727,7 +2816,7 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost dp io.DataPlaneSpec,
 // @ requires  acc(&p.infoField)
 // @ requires  acc(&p.path, R20)
 // @ requires  acc(p.scionLayer.Mem(ub), R19)
-// @ requires  p.path === p.scionLayer.GetPath(ub)
+// @ requires  p.path === p.scionLayer.GetScionPath(ub)
 // @ requires  acc(&p.hopField,  R20)
 // @ requires  sl.Bytes(ub, 0, len(ub))
 // @ requires  acc(&p.ingressID, R21)
@@ -2758,12 +2847,16 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost dp io.DataPlaneSpec,
 // @ decreases
 func (p *scionPacketProcessor) updateNonConsDirIngressSegID( /*@ ghost ub []byte @*/ ) (err error) {
 	// @ ghost ubPath := p.scionLayer.UBPath(ub)
-	// @ ghost start := p.scionLayer.PathStartIdx(ub)
-	// @ ghost end   := p.scionLayer.PathEndIdx(ub)
-	// @ assert ub[start:end] === ubPath
+	// @ ghost ubScionPath := p.scionLayer.UBScionPath(ub)
+	// @ ghost startScionP := p.scionLayer.PathScionStartIdx(ub)
+	// @ ghost endScionP   := p.scionLayer.PathScionEndIdx(ub)
 
 	// @ unfold acc(p.scionLayer.Mem(ub), R20)
 	// @ defer fold acc(p.scionLayer.Mem(ub), R20)
+	// @ ghost if typeOf(p.scionLayer.Path) == *epic.Path {
+	// @ 	unfold acc(p.scionLayer.Path.Mem(ubPath), R20)
+	// @ 	defer fold acc(p.scionLayer.Path.Mem(ubPath), R20)
+	// @ }
 	// against construction dir the ingress router updates the SegID, ifID == 0
 	// means this comes from this AS itself, so nothing has to be done.
 	// TODO(lukedirtwalker): For packets destined to peer links this shouldn't
@@ -3048,6 +3141,9 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte @*/ ) (reserr
 	// @ ghost startP := p.scionLayer.PathStartIdx(ub)
 	// @ ghost endP   := p.scionLayer.PathEndIdx(ub)
 	// @ assert ub[startP:endP] === ubPath
+	// @ ghost ubScionPath := p.scionLayer.UBScionPath(ub)
+	// @ ghost startScionP := p.scionLayer.PathScionStartIdx(ub)
+	// @ ghost endScionP := p.scionLayer.PathScionEndIdx(ub)
 
 	// @ unfold acc(p.scionLayer.Mem(ub), 1-R55)
 	// @ sl.SplitRange_Bytes(ub, startP, endP, HalfPerm)
@@ -3445,6 +3541,9 @@ func (p *scionPacketProcessor) handleIngressRouterAlert( /*@ ghost ub []byte, gh
 	// @ ghost ubPath := p.scionLayer.UBPath(ub)
 	// @ ghost startP := p.scionLayer.PathStartIdx(ub)
 	// @ ghost endP   := p.scionLayer.PathEndIdx(ub)
+	// @ ghost ubScionPath := p.scionLayer.UBScionPath(ub)
+	// @ ghost startScionP := p.scionLayer.PathScionStartIdx(ub)
+	// @ ghost endScionP   := p.scionLayer.PathScionEndIdx(ub)
 	// @ assert ub[startP:endP] === ubPath
 	if p.ingressID == 0 {
 		// @ fold p.d.validResult(processResult{}, false)
@@ -3556,9 +3655,9 @@ func (p *scionPacketProcessor) handleEgressRouterAlert( /*@ ghost ub []byte, gho
 	// @ assert let fut := absPkt(ub).CurrSeg.Future in
 	// @ 	fut == seq[io.HF]{p.hopField.Abs()} ++ fut[1:]
 	// @ ghost ubPath := p.scionLayer.UBPath(ub)
-	// @ ghost startP := p.scionLayer.PathStartIdx(ub)
-	// @ ghost endP   := p.scionLayer.PathEndIdx(ub)
-	// @ assert ub[startP:endP] === ubPath
+	// @ ghost ubScionPath := p.scionLayer.UBScionPath(ub)
+	// @ ghost startScionP := p.scionLayer.PathScionStartIdx(ub)
+	// @ ghost endScionP   := p.scionLayer.PathScionEndIdx(ub)
 
 	alert := p.egressRouterAlertFlag()
 	if !*alert {
@@ -3843,6 +3942,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost
 // @ ensures   !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15)
 // @ ensures   acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem()
 // @ ensures   reserr == nil ==> p.scionLayer.Mem(ub)
+// @ ensures   reserr == nil ==> p.path == p.scionLayer.GetScionPath(ub)
 // @ ensures   reserr != nil ==> p.scionLayer.NonInitMem()
 // @ ensures   sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ ensures   respr.OutPkt != nil ==>

verification/io/packets.gobra

@@ -26,4 +26,4 @@ ghost type Pkt ghost struct {
 	LeftSeg  option[Seg]
 	MidSeg   option[Seg]
 	RightSeg option[Seg]
-}
+}

verification/utils/definitions/definitions.gobra

@@ -92,6 +92,16 @@ ensures false
 decreases _
 func TODO()
 
+// Does the same as TODO, but should be used when it kills a branch
+// that cannot be verified until an issue in SCION is fixed and ported
+// to our branch of SCION.
+ghost
+ensures false
+decreases _
+func ToDoAfterScionFix(url string)
+
+/**** End of functions to introduce temporary assumptions **/
+
 // type to be used as a stub for sets of private fields in formalizations of
 // third party libs
 type PrivateField *int