Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Proof of Internal Packet Bouncing fix (#4502) #333

Merged
merged 8 commits into from
May 6, 2024
Merged

Proof of Internal Packet Bouncing fix (#4502) #333

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
acd1b22
proof of scionfix #4502
mlimbeck May 2, 2024
e095c62
feedback
mlimbeck May 2, 2024
fcea9d0
drop assume in processOHP()
mlimbeck May 2, 2024
1447f24
change getDomExternal() to opaque
mlimbeck May 2, 2024
de2157f
fix comment
mlimbeck May 2, 2024
29fc9ed
verification fix and simplification
mlimbeck May 2, 2024
54ba395
fix verification errors
mlimbeck May 3, 2024
11a901c
feedback
mlimbeck May 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions pkg/slayers/path/hopfield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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{
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
return ifs == none[io.IO_ifs] ? 0 : uint16(get(ifs))
}

ghost
requires 0 <= start && start <= middle
requires middle + HopLen <= end && end <= len(raw)
Expand Down
29 changes: 13 additions & 16 deletions router/dataplane.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -3316,26 +3317,21 @@ 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) {
// @ 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 @*/
}
Expand Down Expand Up @@ -3496,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
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
Expand Down
60 changes: 60 additions & 0 deletions router/io-spec-non-proven-lemmas.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,66 @@ pure func (p* scionPacketProcessor) GetIsXoverSpec(ub []byte) bool {
p.path.GetIsXoverSpec(ubPath)
}

ghost
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
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
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
let egressID := path.ifsToIO_ifsInv(OptEgressID) in
((egressID in p.d.getDomExternal()) || p.ingressID != 0)
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
}

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 ==> acc(p.d.external, _)
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)
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 !(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)
Expand Down
Loading