Proof of Internal Packet Bouncing fix (#4502)

pkg/slayers/path/hopfield_spec.gobra

@@ -34,6 +34,12 @@ pure func ifsToIO_ifs(ifs uint16) option[io.IO_ifs]{
  return ifs == 0 ? none[io.IO_ifs] : some(io.IO_ifs(ifs))
 }
 
+ghost
+decreases
+pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16{
+ return ifs == none[io.IO_ifs] ? 0 : uint16(get(ifs))
+}
+
 ghost
 requires 0 <= start && start <= middle
 requires middle + HopLen <= end && end <= len(raw)

router/dataplane.go

@@ -781,11 +781,13 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
  // @ decreases
  // @ outline (
  // @ reveal d.PreWellConfigured()
+ // @ reveal d.getDomExternal()
  // @ reveal d.DpAgreesWithSpec(dp)
  // @ unfold d.Mem()
  d.running = true
  // @ fold MutexInvariant!<d!>()
  // @ fold d.Mem()
+ // @ reveal d.getDomExternal()
  // @ reveal d.PreWellConfigured()
  // @ reveal d.DpAgreesWithSpec(dp)
  // @ )
@@ -1279,6 +1281,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 // @ decreases
 func (d *DataPlane) initMetrics( /*@ ghost dp io.DataPlaneSpec @*/ ) {
  // @ assert reveal d.PreWellConfigured()
+ // @ reveal d.getDomExternal()
  // @ assert reveal d.DpAgreesWithSpec(dp)
  // @ assert unfolding acc(d.Mem(), _) in
  // @ d.dpSpecWellConfiguredLocalIA(dp) &&
@@ -1351,6 +1354,7 @@ func (d *DataPlane) initMetrics( /*@ ghost dp io.DataPlaneSpec @*/ ) {
  // @ assert d.dpSpecWellConfiguredNeighborIAs(dp)
  // @ assert d.dpSpecWellConfiguredLinkTypes(dp)
  // @ fold d.Mem()
+ // @ reveal d.getDomExternal()
  // @ reveal d.WellConfigured()
  // @ assert reveal d.DpAgreesWithSpec(dp)
 }
@@ -2233,7 +2237,7 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @
 // @ ensures acc(&p.hopField, R20)
 // @ ensures acc(&p.ingressID, R21)
 // @ ensures acc(&p.segmentChange, R20)
-// @ ensures acc(&p.d, R20)
+// @ ensures acc(&p.d, R20) && acc(p.d.Mem(), _)
 // @ ensures p.d.validResult(respr, false)
 // @ ensures reserr == nil ==> respr === processResult{}
 // @ ensures reserr != nil ==> sl.AbsSlice_Bytes(respr.OutPkt, 0, len(respr.OutPkt))
@@ -2248,6 +2252,7 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @
 // @ requires p.segmentChange ==> oldPkt.RightSeg != none[io.IO_seg2] && len(get(oldPkt.RightSeg).Past) > 0
 // @ requires !p.segmentChange ==> AbsValidateIngressIDConstraint(oldPkt, path.ifsToIO_ifs(p.ingressID))
 // @ requires p.segmentChange ==> AbsValidateIngressIDConstraintXover(oldPkt, path.ifsToIO_ifs(p.ingressID))
+// @ ensures reserr == nil ==> p.NoBouncingPkt(oldPkt)
 // @ ensures reserr == nil && !p.segmentChange ==> AbsValidateEgressIDConstraint(oldPkt, (p.ingressID != 0), dp)
 // @ ensures reserr == nil && p.segmentChange ==> oldPkt.RightSeg != none[io.IO_seg2] && len(get(oldPkt.RightSeg).Past) > 0
 // @ ensures reserr == nil && p.segmentChange ==> p.ingressID != 0 && AbsValidateEgressIDConstraintXover(oldPkt, dp)
@@ -2280,7 +2285,8 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost oldPkt io.IO_pkt2, gh
  /*@ dp, @*/
  )
  }
-
+ // @ p.d.getDomExternalLemma()
+ // @ p.EstablishNoBouncingPkt(oldPkt, pktEgressID)
  // @ p.d.getLinkTypesMem()
  ingress, egress := p.d.linkTypes[p.ingressID], p.d.linkTypes[pktEgressID]
  // @ p.d.LinkTypesLemma(dp)
@@ -3294,19 +3300,20 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool,
  // @ p.d.getExternalMem()
  // @ if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) }
  if c, ok := p.d.external[egressID]; ok {
+ // @ p.d.getDomExternalLemma()
  // @ p.d.EgressIDNotZeroLemma(egressID, dp)
  if err := p.processEgress( /*@ ub, dp @*/ ); err != nil {
  // @ fold p.d.validResult(processResult{}, false)
  return processResult{}, err /*@, false, absReturnErr(dp, processResult{}) @*/
  }
- // @ p.d.InDomainExternalInForwardingMetrics2(egressID)
+ // @ p.d.InDomainExternalInForwardingMetrics(egressID)
  // @ assert absPkt(dp, ub) == AbsProcessEgress(nextPkt)
  // @ nextPkt = absPkt(dp, ub)
  // @ TemporaryAssumeForIO(old(slayers.IsSupportedPkt(ub)) == slayers.IsSupportedPkt(ub))
  // @ ghost if(slayers.IsSupportedPkt(ub)) {
  // @ ghost if(!p.segmentChange) {
  // enter/exit event
- // @ ExternalEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioLock, ioSharedArg, dp)
+ // @ ExternalEnterOrExitEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioLock, ioSharedArg, dp)
  // @ } else {
  // xover event
  // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, path.ifsToIO_ifs(egressID), ioLock, ioSharedArg, dp)
@@ -3316,26 +3323,22 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool,
  // @ fold p.d.validResult(processResult{EgressID: egressID, OutConn: c, OutPkt: p.rawPkt}, false)
  return processResult{EgressID: egressID, OutConn: c, OutPkt: p.rawPkt}, nil /*@, false, newAbsPkt @*/
  }
+ // @ p.d.getDomExternalLemma()
+ // @ p.IngressIDNotZeroLemma(nextPkt, egressID)
  // ASTransit: pkts leaving from another AS BR.
  // @ p.d.getInternalNextHops()
  // @ ghost if p.d.internalNextHops != nil { unfold acc(accAddr(p.d.internalNextHops), _) }
  if a, ok := p.d.internalNextHops[egressID]; ok {
  // @ p.d.getInternal()
- // @ ghost if(path.ifsToIO_ifs(p.ingressID) != none[io.IO_ifs]) {
- // @ TemporaryAssumeForIO(old(slayers.IsSupportedPkt(ub)) == slayers.IsSupportedPkt(ub))
- // @ ghost if(slayers.IsSupportedPkt(ub)) {
- // @ if(!p.segmentChange) {
- // enter event
- // @ InternalEnterEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.IO_ifs], ioLock, ioSharedArg, dp)
- // @ } else {
- // xover event
- // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.IO_ifs], ioLock, ioSharedArg, dp)
- // @ }
+ // @ TemporaryAssumeForIO(old(slayers.IsSupportedPkt(ub)) == slayers.IsSupportedPkt(ub))
+ // @ ghost if(slayers.IsSupportedPkt(ub)) {
+ // @ if(!p.segmentChange) {
+ // @ InternalEnterEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.IO_ifs], ioLock, ioSharedArg, dp)
+ // @ } else {
+ // @ XoverEvent(oldPkt, path.ifsToIO_ifs(p.ingressID), nextPkt, none[io.IO_ifs], ioLock, ioSharedArg, dp)
  // @ }
- // @ newAbsPkt = reveal absIO_val(dp, p.rawPkt, 0)
- // @ } else {
- // @ ToDoAfterScionFix("https:/scionproto/scion/issues/4497")
  // @ }
+ // @ newAbsPkt = reveal absIO_val(dp, p.rawPkt, 0)
  // @ fold p.d.validResult(processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, false)
  return processResult{OutConn: p.d.internal, OutAddr: a, OutPkt: p.rawPkt}, nil /*@, false, newAbsPkt @*/
  }
@@ -3493,13 +3496,8 @@ func (p *scionPacketProcessor) processOHP( /* @ ghost dp io.DataPlaneSpec @ */ )
  // @ p.d.getExternalMem()
  // @ ghost if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) }
  if c, ok := p.d.external[ohp.FirstHop.ConsEgress]; ok {
- // (VerifiedSCION) the following must hold, obviously.
- // Unfortunately, Gobra struggles with instantiating the body
- // of the function.
- // @ assume ohp.FirstHop.ConsEgress in p.d.getDomExternal()
- // buffer should already be correct
- // (VerifiedSCION) TODO: we need to add a pre to run that says that the
- // domain of forwardingMetrics is the same as the one for external
+ // @ p.d.getDomExternalLemma()
+ // @ assert ohp.FirstHop.ConsEgress in p.d.getDomExternal()
  // @ p.d.InDomainExternalInForwardingMetrics(ohp.FirstHop.ConsEgress)
  // @ fold p.d.validResult(processResult{EgressID: ohp.FirstHop.ConsEgress, OutConn: c, OutPkt: p.rawPkt}, false)
  // @ TemporaryAssumeForIO(!slayers.IsSupportedPkt(p.rawPkt))

router/dataplane_spec.gobra

@@ -242,6 +242,7 @@ pure func (d *DataPlane) GetDomInternalNextHops() set[uint16] {
 }
 
 ghost
+opaque
 requires acc(d.Mem(), _)
 decreases
 pure func (d *DataPlane) getDomExternal() set[uint16] {
@@ -276,7 +277,7 @@ requires acc(d.Mem(), _)
 decreases
 pure func (d *DataPlane) WellConfigured() bool {
  return d.getDomNeighborIAs() == d.getDomExternal() &&
- d.getDomExternal() == d.getDomLinkTypes() &&
+ d.getDomNeighborIAs() == d.getDomLinkTypes() &&
  !(0 in d.getDomNeighborIAs()) &&
  d.getDomExternal() subset d.getDomForwardingMetrics()
 }
@@ -683,19 +684,6 @@ func (d *DataPlane) InDomainExternalInForwardingMetrics(id uint16) {
  reveal d.WellConfigured()
 }
 
-ghost
-requires acc(d.Mem(), _) && d.WellConfigured()
-requires acc(&d.external, _) && acc(d.external, _)
-requires id in domain(d.external)
-ensures acc(d.Mem(), _)
-ensures id in d.getDomForwardingMetrics()
-decreases
-func (d *DataPlane) InDomainExternalInForwardingMetrics2(id uint16) {
- unfold acc(d.Mem(), _)
- reveal d.WellConfigured()
- unfold acc(accBatchConn(d.external), _)
-}
-
 ghost
 requires acc(d.Mem(), _) && d.WellConfigured()
 requires acc(&d.external, _) && acc(d.external, R55)
@@ -706,6 +694,7 @@ ensures id in d.getDomForwardingMetrics()
 decreases
 func (d *DataPlane) InDomainExternalInForwardingMetrics3(id uint16) {
  reveal d.WellConfigured()
+ reveal d.getDomExternal()
  assert unfolding acc(d.Mem(), _) in
  (unfolding acc(accBatchConn(d.external), _) in true)
 }

router/dataplane_spec_test.gobra

@@ -207,10 +207,10 @@ func testRun(
  assert d.dpSpecWellConfiguredLinkTypes(dp)
 
  fold d.Mem()
- assert d.getDomNeighborIAs() == d.getDomExternal()
- assert d.getDomExternal() == d.getDomLinkTypes()
+ assert d.getDomNeighborIAs() == reveal d.getDomExternal()
+ assert d.getDomNeighborIAs() == d.getDomLinkTypes()
  assert !(0 in d.getDomNeighborIAs())
- assert d.getDomExternal() intersection d.GetDomInternalNextHops() == set[uint16]{}
+ assert reveal d.getDomExternal() intersection d.GetDomInternalNextHops() == set[uint16]{}
  assert reveal d.DpAgreesWithSpec(dp)
 
  assert reveal d.PreWellConfigured()

router/io-spec-abstract-transitions.gobra

@@ -25,6 +25,14 @@ import (
  . "verification/utils/definitions"
 )
 
+ghost
+requires len(pkt.CurrSeg.Future) > 0
+decreases
+pure func CurrSegIO_ifs(pkt io.IO_pkt2, dir bool) option[io.IO_ifs] {
+ return let currseg := pkt.CurrSeg in
+ (currseg.ConsDir == dir ? currseg.Future[0].InIF2 : currseg.Future[0].EgIF2)
+}
+
 ghost
 opaque
 requires len(oldPkt.CurrSeg.Future) > 0
@@ -47,7 +55,7 @@ decreases
 pure func AbsValidateIngressIDConstraint(pkt io.IO_pkt2, ingressID option[io.IO_ifs]) bool {
  return let currseg := pkt.CurrSeg in
  ingressID != none[io.IO_ifs] ==>
- ingressID == (currseg.ConsDir ? currseg.Future[0].InIF2 : currseg.Future[0].EgIF2)
+ ingressID == CurrSegIO_ifs(pkt, true)
 }
 
 ghost
@@ -67,7 +75,7 @@ requires len(pkt.CurrSeg.Future) > 0
 decreases
 pure func AbsEgressInterfaceConstraint(pkt io.IO_pkt2, egressID option[io.IO_ifs]) bool {
  return let currseg := pkt.CurrSeg in
- egressID == (currseg.ConsDir ? currseg.Future[0].EgIF2 : currseg.Future[0].InIF2)
+ egressID == CurrSegIO_ifs(pkt, false)
 }
 
 ghost
@@ -140,7 +148,9 @@ pure func AbsVerifyCurrentMACConstraint(pkt io.IO_pkt2, dp io.DataPlaneSpec) boo
  let uinfo := currseg.UInfo in
  dp.hf_valid(d, ts, uinfo, hf)
 }
-
+// This executes the IO enter event whenever a pkt was received
+// from a different AS (ingressID != none[io.IO_ifs])
+// and will be forwarded to another border router within the AS (egressID == none[io.IO_ifs])
 ghost
 requires dp.Valid()
 requires ingressID != none[io.IO_ifs]
@@ -165,6 +175,12 @@ func InternalEnterEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt i
  AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
 }
 
+// Either this executes the IO enter event whenever a pkt was received
+// from a different AS (ingressID != none[io.IO_ifs])
+// and will leave the AS (egressID != none[io.IO_ifs]) or
+// it executes the IO exit event whenever a pkt was received from
+// within the AS (ingressID == none[io.IO_ifs])
+// and will leave the AS (egressID != none[io.IO_ifs])
 ghost
 requires dp.Valid()
 requires egressID != none[io.IO_ifs]
@@ -180,7 +196,7 @@ preserves acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioShared
 ensures dp.Valid()
 ensures ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
 decreases
-func ExternalEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt2, egressID option[io.IO_ifs], ioLock *sync.Mutex, ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+func ExternalEnterOrExitEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_pkt2, egressID option[io.IO_ifs], ioLock *sync.Mutex, ioSharedArg SharedArg, dp io.DataPlaneSpec) {
  reveal dp.Valid()
  nextPkt := reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)
  reveal AbsValidateIngressIDConstraint(oldPkt, ingressID)
@@ -195,6 +211,9 @@ func ExternalEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt io.IO_
  }
 }
 
+// This executes the IO xover event whenever a pkt was received
+// from a different AS (ingressID != none[io.IO_ifs])
+// and a segment switch was performed.
 ghost
 requires dp.Valid()
 requires ingressID != none[io.IO_ifs]

router/io-spec-non-proven-lemmas.gobra

@@ -166,6 +166,50 @@ pure func (p* scionPacketProcessor) GetIsXoverSpec(ub []byte) bool {
  p.path.GetIsXoverSpec(ubPath)
 }
 
+ghost
+opaque
+requires acc(&p.d, R55) && acc(p.d.Mem(), _)
+requires acc(&p.ingressID, R55)
+requires len(pkt.CurrSeg.Future) > 0
+decreases
+pure func (p *scionPacketProcessor) NoBouncingPkt(pkt io.IO_pkt2) bool {
+ return let currseg := pkt.CurrSeg in
+ let OptEgressID := CurrSegIO_ifs(pkt, false) in
+ let egressID := path.IO_ifsToIfs(OptEgressID) in
+ ((egressID in p.d.getDomExternal()) || p.ingressID != 0)
+}
+
+ghost
+requires acc(&p.d, R55) && acc(p.d.Mem(), _)
+requires acc(&p.ingressID, R55)
+requires len(pkt.CurrSeg.Future) > 0
+requires AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID))
+requires (egressID in p.d.getDomExternal()) || p.ingressID != 0
+ensures acc(&p.d, R55) && acc(p.d.Mem(), _)
+ensures acc(&p.ingressID, R55)
+ensures p.NoBouncingPkt(pkt)
+decreases
+func (p *scionPacketProcessor) EstablishNoBouncingPkt(pkt io.IO_pkt2, egressID uint16) {
+ reveal AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID))
+ reveal p.NoBouncingPkt(pkt)
+}
+
+ghost
+requires acc(&p.d, R55) && acc(p.d.Mem(), _)
+requires acc(&p.ingressID, R55)
+requires len(pkt.CurrSeg.Future) > 0
+requires AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID))
+requires p.NoBouncingPkt(pkt)
+requires !(egressID in p.d.getDomExternal())
+ensures acc(&p.d, R55) && acc(p.d.Mem(), _)
+ensures acc(&p.ingressID, R55)
+ensures p.ingressID != 0
+decreases
+func (p *scionPacketProcessor) IngressIDNotZeroLemma(pkt io.IO_pkt2, egressID uint16) {
+ reveal AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID))
+ reveal p.NoBouncingPkt(pkt)
+}
+
 // TODO prove
 ghost
 requires 0 <= start && start <= end && end <= len(ub)

router/io-spec.gobra

@@ -159,37 +159,33 @@ ghost
 requires acc(d.Mem(), _)
 requires d.DpAgreesWithSpec(dp)
 requires d.WellConfigured()
-requires acc(&d.external, _)
-requires acc(d.external, _)
-requires egressID in domain(d.external)
+requires egressID in d.getDomExternal()
 ensures egressID != 0
 ensures io.IO_ifs(egressID) in domain(dp.GetNeighborIAs())
 decreases
 func (d *DataPlane) EgressIDNotZeroLemma(egressID uint16, dp io.DataPlaneSpec) {
  reveal d.WellConfigured()
  reveal d.DpAgreesWithSpec(dp)
- d.getDomExternalLemma()
- assert d.getDomExternal() == domain(d.external)
- assert egressID in d.getDomExternal()
- assert d.getDomNeighborIAs() == d.getDomExternal()
- assert io.IO_ifs(egressID) in domain(dp.GetNeighborIAs())
- assert egressID != 0
 }
 
 ghost
 requires acc(d.Mem(), _)
 requires acc(&d.external, _)
-requires acc(d.external, _)
+requires d.external != nil ==> acc(d.external, _)
 ensures acc(d.Mem(), _)
 ensures acc(&d.external, _)
-ensures acc(d.external, _)
+ensures d.external != nil ==> acc(d.external, _)
 ensures d.getDomExternal() == domain(d.external)
 decreases
 func (d *DataPlane) getDomExternalLemma() {
- assert d.external != nil
- assert d.getDomExternal() == unfolding acc(d.Mem(), _) in
- (unfolding acc(accBatchConn(d.external), _) in
- domain(d.external))
+ if (d.external != nil) {
+ assert reveal d.getDomExternal() == unfolding acc(d.Mem(), _) in
+ (unfolding acc(accBatchConn(d.external), _) in
+ domain(d.external))
+ } else {
+ assert reveal d.getDomExternal() ==
+ unfolding acc(d.Mem(), _) in set[uint16]{}
+ }
 }
 
 ghost