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

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 1 commit
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
28 changes: 13 additions & 15 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,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
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
// @ 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 @*/
}
Expand Down
62 changes: 62 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,68 @@ 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 := OptEgressID != none[io.IO_ifs] ? uint16(get(OptEgressID)) : 0 in
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
((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 ==> 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
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
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))
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
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