From acd1b2210ce946f71bbb1dc5c1d0ef48f205e120 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 2 May 2024 16:24:19 +0200 Subject: [PATCH 1/8] proof of scionfix #4502 --- router/dataplane.go | 28 ++++++------ router/io-spec-non-proven-lemmas.gobra | 62 ++++++++++++++++++++++++++ 2 files changed, 75 insertions(+), 15 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index e452a52f5..9795d8dc3 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2233,7 +2233,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 +2248,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 +2281,7 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost oldPkt io.IO_pkt2, gh /*@ dp, @*/ ) } - + // @ p.EstablishNoBouncingPkt(oldPkt, pktEgressID) // @ p.d.getLinkTypesMem() ingress, egress := p.d.linkTypes[p.ingressID], p.d.linkTypes[pktEgressID] // @ p.d.LinkTypesLemma(dp) @@ -3316,26 +3317,23 @@ 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.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) { + // 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) // @ } - // @ newAbsPkt = reveal absIO_val(dp, p.rawPkt, 0) - // @ } else { - // @ ToDoAfterScionFix("https://github.com/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 @*/ } diff --git a/router/io-spec-non-proven-lemmas.gobra b/router/io-spec-non-proven-lemmas.gobra index 6edcde280..d4eb52869 100644 --- a/router/io-spec-non-proven-lemmas.gobra +++ b/router/io-spec-non-proven-lemmas.gobra @@ -166,6 +166,68 @@ 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 := (currseg.ConsDir ? currseg.Future[0].EgIF2 : currseg.Future[0].InIF2) in + let egressID := OptEgressID != none[io.IO_ifs] ? uint16(get(OptEgressID)) : 0 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 acc(&p.d.external, _) +requires p.d.external == nil ==> p.ingressID != 0 +requires p.d.external != nil ==> acc(p.d.external, _) +requires p.d.external != nil ==> + (egressID in domain(p.d.external)) || 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) { + if(p.d.external != nil) { + p.d.getDomExternalLemma() + assert p.d.getDomExternal() == domain(p.d.external) + } + 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 acc(&p.d.external, _) +requires p.d.external != nil ==> acc(p.d.external, _) +requires p.d.external != nil ==> !(egressID in domain(p.d.external)) +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) { + if(p.d.external != nil) { + p.d.getDomExternalLemma() + assert p.d.getDomExternal() == domain(p.d.external) + } else { + assert p.d.getDomExternal() == unfolding acc(p.d.Mem(), _) in + set[uint16]{} + } + assert !(egressID in p.d.getDomExternal()) + reveal AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID)) + reveal p.NoBouncingPkt(pkt) +} + // TODO prove ghost requires 0 <= start && start <= end && end <= len(ub) From e095c62b9c94aec172227085f3f573272e6499e4 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 2 May 2024 19:18:20 +0200 Subject: [PATCH 2/8] feedback --- pkg/slayers/path/hopfield_spec.gobra | 6 ++++++ router/dataplane.go | 2 -- router/io-spec-non-proven-lemmas.gobra | 8 +++----- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/pkg/slayers/path/hopfield_spec.gobra b/pkg/slayers/path/hopfield_spec.gobra index e93e22f39..7100c8b9e 100644 --- a/pkg/slayers/path/hopfield_spec.gobra +++ b/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 ifsToIO_ifsInv(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) diff --git a/router/dataplane.go b/router/dataplane.go index 9795d8dc3..3c81de64d 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3326,10 +3326,8 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ 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) // @ } // @ } diff --git a/router/io-spec-non-proven-lemmas.gobra b/router/io-spec-non-proven-lemmas.gobra index d4eb52869..2b865920d 100644 --- a/router/io-spec-non-proven-lemmas.gobra +++ b/router/io-spec-non-proven-lemmas.gobra @@ -175,7 +175,7 @@ decreases pure func (p *scionPacketProcessor) NoBouncingPkt(pkt io.IO_pkt2) bool { return let currseg := pkt.CurrSeg in let OptEgressID := (currseg.ConsDir ? currseg.Future[0].EgIF2 : currseg.Future[0].InIF2) in - let egressID := OptEgressID != none[io.IO_ifs] ? uint16(get(OptEgressID)) : 0 in + let egressID := path.ifsToIO_ifsInv(OptEgressID) in ((egressID in p.d.getDomExternal()) || p.ingressID != 0) } @@ -185,10 +185,8 @@ requires acc(&p.ingressID, R55) requires len(pkt.CurrSeg.Future) > 0 requires AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID)) requires acc(&p.d.external, _) -requires p.d.external == nil ==> p.ingressID != 0 requires p.d.external != nil ==> acc(p.d.external, _) -requires p.d.external != nil ==> - (egressID in domain(p.d.external)) || p.ingressID != 0 +requires (egressID in domain(p.d.external)) || p.ingressID != 0 ensures acc(&p.d, R55) && acc(p.d.Mem(), _) ensures acc(&p.ingressID, R55) ensures p.NoBouncingPkt(pkt) @@ -210,7 +208,7 @@ requires AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID)) requires p.NoBouncingPkt(pkt) requires acc(&p.d.external, _) requires p.d.external != nil ==> acc(p.d.external, _) -requires p.d.external != nil ==> !(egressID in domain(p.d.external)) +requires !(egressID in domain(p.d.external)) ensures acc(&p.d, R55) && acc(p.d.Mem(), _) ensures acc(&p.ingressID, R55) ensures p.ingressID != 0 From fcea9d0cb22f2d73a9bcf89c9fad02c8d1600c1b Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 2 May 2024 20:01:55 +0200 Subject: [PATCH 3/8] drop assume in processOHP() --- router/dataplane.go | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/router/dataplane.go b/router/dataplane.go index 3c81de64d..cc793083b 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3492,7 +3492,8 @@ func (p *scionPacketProcessor) processOHP( /* @ ghost dp io.DataPlaneSpec @ */ ) // (VerifiedSCION) the following must hold, obviously. // Unfortunately, Gobra struggles with instantiating the body // of the function. - // @ assume ohp.FirstHop.ConsEgress in p.d.getDomExternal() + // @ p.d.getDomExternalLemma() + // @ assert 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 From 1447f24d047750754703fbb836c534a83a44ff86 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 2 May 2024 23:08:45 +0200 Subject: [PATCH 4/8] change getDomExternal() to opaque --- pkg/slayers/path/hopfield_spec.gobra | 2 +- router/dataplane.go | 11 +++------ router/dataplane_spec.gobra | 3 ++- router/dataplane_spec_test.gobra | 6 ++--- router/io-spec-abstract-transitions.gobra | 27 +++++++++++++++++--- router/io-spec-non-proven-lemmas.gobra | 24 +++--------------- router/io-spec.gobra | 30 +++++++++++------------ 7 files changed, 51 insertions(+), 52 deletions(-) diff --git a/pkg/slayers/path/hopfield_spec.gobra b/pkg/slayers/path/hopfield_spec.gobra index 7100c8b9e..311a60a66 100644 --- a/pkg/slayers/path/hopfield_spec.gobra +++ b/pkg/slayers/path/hopfield_spec.gobra @@ -36,7 +36,7 @@ pure func ifsToIO_ifs(ifs uint16) option[io.IO_ifs]{ ghost decreases -pure func ifsToIO_ifsInv(ifs option[io.IO_ifs]) uint16{ +pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16{ return ifs == none[io.IO_ifs] ? 0 : uint16(get(ifs)) } diff --git a/router/dataplane.go b/router/dataplane.go index cc793083b..53441f15f 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -2281,6 +2281,7 @@ 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] @@ -3295,6 +3296,7 @@ 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) @@ -3307,7 +3309,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ 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) @@ -3317,6 +3319,7 @@ 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() @@ -3489,14 +3492,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. // @ p.d.getDomExternalLemma() // @ assert 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.InDomainExternalInForwardingMetrics(ohp.FirstHop.ConsEgress) // @ fold p.d.validResult(processResult{EgressID: ohp.FirstHop.ConsEgress, OutConn: c, OutPkt: p.rawPkt}, false) // @ TemporaryAssumeForIO(!slayers.IsSupportedPkt(p.rawPkt)) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 4fdf29163..72630e7fb 100644 --- a/router/dataplane_spec.gobra +++ b/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() } diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra index 26c4fe81d..49b421d64 100644 --- a/router/dataplane_spec_test.gobra +++ b/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() diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index ebb4aeb92..b25e5d784 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/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 +// withhin 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] diff --git a/router/io-spec-non-proven-lemmas.gobra b/router/io-spec-non-proven-lemmas.gobra index 2b865920d..b3b5f0adb 100644 --- a/router/io-spec-non-proven-lemmas.gobra +++ b/router/io-spec-non-proven-lemmas.gobra @@ -174,8 +174,8 @@ 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 := (currseg.ConsDir ? currseg.Future[0].EgIF2 : currseg.Future[0].InIF2) in - let egressID := path.ifsToIO_ifsInv(OptEgressID) in + let OptEgressID := CurrSegIO_ifs(pkt, false) in + let egressID := path.IO_ifsToIfs(OptEgressID) in ((egressID in p.d.getDomExternal()) || p.ingressID != 0) } @@ -184,18 +184,12 @@ 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 acc(&p.d.external, _) -requires p.d.external != nil ==> acc(p.d.external, _) -requires (egressID in domain(p.d.external)) || p.ingressID != 0 +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) { - if(p.d.external != nil) { - p.d.getDomExternalLemma() - assert p.d.getDomExternal() == domain(p.d.external) - } reveal AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID)) reveal p.NoBouncingPkt(pkt) } @@ -206,22 +200,12 @@ requires acc(&p.ingressID, R55) requires len(pkt.CurrSeg.Future) > 0 requires AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID)) requires p.NoBouncingPkt(pkt) -requires acc(&p.d.external, _) -requires p.d.external != nil ==> acc(p.d.external, _) -requires !(egressID in domain(p.d.external)) +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) { - if(p.d.external != nil) { - p.d.getDomExternalLemma() - assert p.d.getDomExternal() == domain(p.d.external) - } else { - assert p.d.getDomExternal() == unfolding acc(p.d.Mem(), _) in - set[uint16]{} - } - assert !(egressID in p.d.getDomExternal()) reveal AbsEgressInterfaceConstraint(pkt, path.ifsToIO_ifs(egressID)) reveal p.NoBouncingPkt(pkt) } diff --git a/router/io-spec.gobra b/router/io-spec.gobra index 456e9f73b..10dbfe229 100644 --- a/router/io-spec.gobra +++ b/router/io-spec.gobra @@ -159,37 +159,35 @@ 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.getDomExternal() == domain(d.external) +ensures d.external != nil ==> acc(d.external, _) && + d.getDomExternal() == domain(d.external) +ensures d.external == nil ==> + d.getDomExternal() == set[uint16]{} 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 From de2157fcae35a29252969d846f49b1b699558f62 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Thu, 2 May 2024 23:12:51 +0200 Subject: [PATCH 5/8] fix comment --- router/io-spec-abstract-transitions.gobra | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/router/io-spec-abstract-transitions.gobra b/router/io-spec-abstract-transitions.gobra index b25e5d784..4faa43b52 100644 --- a/router/io-spec-abstract-transitions.gobra +++ b/router/io-spec-abstract-transitions.gobra @@ -179,8 +179,8 @@ func InternalEnterEvent(oldPkt io.IO_pkt2, ingressID option[io.IO_ifs], newPkt i // 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 -// withhin the AS (ingressID == none[io.IO_ifs]) -// and will leave the AS (egressID == none[io.IO_ifs]) +// 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] From 29fc9ed2858a8dd771f0a1df624da5802628cd70 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Fri, 3 May 2024 00:24:32 +0200 Subject: [PATCH 6/8] verification fix and simplification --- router/dataplane.go | 2 +- router/dataplane_spec.gobra | 14 +------------- 2 files changed, 2 insertions(+), 14 deletions(-) diff --git a/router/dataplane.go b/router/dataplane.go index 53441f15f..e7d1b531b 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -3302,7 +3302,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ 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)) diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 72630e7fb..5a5e28fc5 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -684,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) @@ -707,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) } From 54ba395bb32cc887ec45b2f6682dc7c88c2e1326 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Fri, 3 May 2024 08:42:29 +0200 Subject: [PATCH 7/8] fix verification errors --- router/dataplane.go | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/router/dataplane.go b/router/dataplane.go index e7d1b531b..520d61858 100644 --- a/router/dataplane.go +++ b/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!() // @ 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) } From 11a901c9a060c8f04ea3668739543a0c48c25a4f Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Fri, 3 May 2024 11:12:57 +0200 Subject: [PATCH 8/8] feedback --- router/io-spec.gobra | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/router/io-spec.gobra b/router/io-spec.gobra index 10dbfe229..9b77fe93a 100644 --- a/router/io-spec.gobra +++ b/router/io-spec.gobra @@ -174,10 +174,8 @@ requires acc(&d.external, _) requires d.external != nil ==> acc(d.external, _) ensures acc(d.Mem(), _) ensures acc(&d.external, _) -ensures d.external != nil ==> acc(d.external, _) && - d.getDomExternal() == domain(d.external) -ensures d.external == nil ==> - d.getDomExternal() == set[uint16]{} +ensures d.external != nil ==> acc(d.external, _) +ensures d.getDomExternal() == domain(d.external) decreases func (d *DataPlane) getDomExternalLemma() { if (d.external != nil) {