Skip to content

Commit

Permalink
Verify send guard in Run (#263)
Browse files Browse the repository at this point in the history 
* remove send operation

* lemma for smaller buffer result in same abstract pkt

* progress send guard

* progress send guard

* Fix incompleteness and continue with send guard (#273)

* backup

* backup

* backup

* backup

* backup

* drop space

* pick better triggers

* add necessary lemma and call to it; contains an assume false that needs to be dropped

* backup

* backup

* add missing loop invariant about ingressID

* backup

* backup

* fix verification error

* try out a simpler trigger

* widen lemma for absIO_val (#268)

* widen lemma for abspkt (non termianting)

* abspkt proven

* renamed io-spec-lemmas

* io val also proven

* cleanup

* merged markus' abspkt improvements

* consdir lemma

* proved

* reinstate lemma4

* fix verification error

* Simplify widen lemma from #268 (#282)

* start simplifying

* continue simplifying

* continue simplifying stuff

* continue simplifying

* continue simplifying

* simplify further

* finish for now

* Update router/io-spec.gobra

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>

* Continue send (#283)

* widen lemma for abspkt (non termianting)

* abspkt proven

* renamed io-spec-lemmas

* io val also proven

* cleanup

* merged markus' abspkt improvements

* consdir lemma

* proved

* reinstate lemma4

* fix verification error

* Simplify widen lemma from #268 (#282)

* start simplifying

* continue simplifying

* continue simplifying stuff

* continue simplifying

* continue simplifying

* simplify further

* finish for now

* Update router/io-spec.gobra

* finish send in Run

* propagate changes to processSCION

---------

Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>

* backup

* adapt to the new syntax of backend annotations

* clean-up

* changes according to feedback

---------

Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>
Co-authored-by: Dspil <dennisspiliopoylos@gmail.com>
  • Loading branch information
@mlimbeck @jcp19 @Dspil
4 people committed Apr 26, 2024
1 parent e276398 commit 1e85796
Show file tree
Hide file tree
Showing 5 changed files with 828 additions and 276 deletions.
70 changes: 45 additions & 25 deletions router/dataplane.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,9 +141,8 @@ type BatchConn interface {
// @ io.token(old(MultiReadBioNext(place, n))) &&
// @ old(MultiReadBioCorrectIfs(place, n, ifsToIO_ifs(ingressID)))
// @ ensures err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==>
// @ unfolding acc(msgs[i].Mem(), R56) in absIO_val(dp, msgs[i].Buffers[0], ingressID) ==
// @ old(MultiReadBioIO_val(place, n)[i])
// @ forall i int :: { &msgs[i] } 0 <= i && i < n ==>
// @ MsgToAbsVal(dp, &msgs[i], ingressID) == old(MultiReadBioIO_val(place, n)[i])
// TODO (Markus): uint16 or option[io.IO_ifs] for ingress
ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place, ghost dp io.DataPlaneSpec @*/) (n int, err error)
// @ requires acc(addr.Mem(), _)
Expand Down Expand Up @@ -755,8 +754,7 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro
// @ requires dp.Valid()
// @ requires d.DpAgreesWithSpec(dp)
// @ requires io.token(place) && dp.dp3s_iospec_ordered(state, place)
// @ preserves d.mtx.LockP()
// @ preserves d.mtx.LockInv() == MutexInvariant!<d!>;
// @ #backend[moreJoins()]
func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost state io.IO_dp3s_state_local, ghost dp io.DataPlaneSpec @*/) error {
// @ share d, ctx
d.mtx.Lock()
Expand Down Expand Up @@ -815,9 +813,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// @ requires let d := *dPtr in
// @ acc(d.Mem(), _) && d.DpAgreesWithSpec(dp)
// @ requires acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>;
func /*@ rc @*/ (ingressID uint16, rd BatchConn /*@, ghost ioLock *sync.Mutex, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) {
// @ ghost ioIngressID := ifsToIO_ifs(ingressID)

// @ #backend[moreJoins()]
func /*@ rc @*/ (ingressID uint16, rd BatchConn, dPtr **DataPlane /*@, ghost ioLock *sync.Mutex, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) {
d := *dPtr
msgs := conn.NewReadMessages(inputBatchCnt)
// @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
// @ msgs[i].Mem() && msgs[i].GetAddr() == nil
Expand Down Expand Up @@ -878,22 +876,41 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// @ invariant 0 in d.getDomForwardingMetrics()
// @ invariant ingressID in d.getDomForwardingMetrics()
// @ invariant acc(rd.Mem(), _)
// @ invariant acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, sharedArg !>

// @ invariant processor.sInit() && processor.sInitD() === d
// @ invariant processor.getIngressID() == ingressID
// @ invariant acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
// @ invariant d.DpAgreesWithSpec(dp) && dp.Valid()
for d.running {
// @ ghost ioIngressID := ifsToIO_ifs(ingressID)
// Multi recv event
// @ ghost ioLock.Lock()
// @ unfold SharedInv!< dp, sharedArg !>()
// @ ghost t, s := *sharedArg.Place, *sharedArg.State
// @ ghost numberOfReceivedPacketsProphecy := AllocProphecy()
// @ ExtractMultiReadBio(dp, t, numberOfReceivedPacketsProphecy, s)
// @ MultiUpdateElemWitness(t, numberOfReceivedPacketsProphecy, ioIngressID, s, ioSharedArg)
// @ ghost ioValSeq := MultiReadBioIO_val(t,numberOfReceivedPacketsProphecy)
// @ ghost ioValSeq := MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)

// @ ghost sN := MultiReadBioUpd(t, numberOfReceivedPacketsProphecy, s)
// @ ghost tN := MultiReadBioNext(t, numberOfReceivedPacketsProphecy)
// @ assert dp.dp3s_iospec_ordered(sN, tN)
// @ BeforeReadBatch:
pkts, err := rd.ReadBatch(msgs /*@, ingressID, numberOfReceivedPacketsProphecy, t , dp @*/)
// @ assert old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)) == ioValSeq
// @ assert err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==>
// @ ioValSeq[i] == old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)[i])
// @ assert err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==> MsgToAbsVal(dp, &msgs[i], ingressID) == ioValSeq[i]
// @ ghost *ioSharedArg.State = sN
// @ ghost *ioSharedArg.Place = tN
// @ assert err == nil ==>
// @ forall i int :: { &msgs[i] } 0 <= i && i < pkts ==>
// @ MsgToAbsVal(dp, &msgs[i], ingressID) == old[BeforeReadBatch](MultiReadBioIO_val(t, numberOfReceivedPacketsProphecy)[i])
// @ MultiElemWitnessConv(ioSharedArg.IBufY, ioIngressID, ioValSeq)
// @ fold SharedInv!< dp, ioSharedArg !>()
// @ ioLock.Unlock()
// End of multi recv event

// @ assert forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
// @ assert err == nil ==>
Expand Down Expand Up @@ -939,12 +956,11 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// contracts for IO-spec
// @ invariant pkts <= len(ioValSeq)
// @ invariant d.DpAgreesWithSpec(dp) && dp.Valid()
// @ invariant ioIngressID == path.ifsToIO_ifs(ingressID)
// @ invariant ioIngressID == ifsToIO_ifs(ingressID)
// @ invariant acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>;
// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==>
// @ MsgToAbsVal(dp, &msgs[i], ingressID) == ioValSeq[i]
// @ invariant MultiElemWitnessWithIndex(ioSharedArg.IBufY, ioIngressID, ioValSeq, i0)
// @ decreases pkts - i0
for i0 := 0; i0 < pkts; i0++ {
// @ assert &msgs[:pkts][i0] == &msgs[i0]
// @ preserves 0 <= i0 && i0 < pkts && pkts <= len(msgs)
Expand Down Expand Up @@ -987,11 +1003,11 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
// @ assert ioValSeq[i0].isIO_val_Pkt2 ==>
// @ ElemWitness(ioSharedArg.IBufY, ioIngressID, ioValSeq[i0].IO_val_Pkt2_2)
// @ assert absPktTmpBuf.isIO_val_Pkt2 ==> absPktTmpBuf == ioValSeq[i0]
// @ assert path.ifsToIO_ifs(processor.getIngressID()) == ioIngressID
// @ assert ifsToIO_ifs(processor.getIngressID()) == ioIngressID
// @ sl.SplitRange_Bytes(p.Buffers[0], 0, p.N, HalfPerm)
// @ assert sl.AbsSlice_Bytes(tmpBuf, 0, p.N)
// @ assert sl.AbsSlice_Bytes(tmpBuf, 0, len(tmpBuf))
result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioLock, ioSharedArg, dp@*/)
result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioLock, ioSharedArg, dp @*/)
// @ fold scmpErr.Mem()

switch {
Expand Down Expand Up @@ -1415,7 +1431,7 @@ func (p *scionPacketProcessor) reset() (err error) {
// @ d.WellConfigured() &&
// @ d.getValSvc() != nil &&
// @ d.getValForwardingMetrics() != nil &&
// @ d.DpAgreesWithSpec(dp)
// @ d.DpAgreesWithSpec(dp)
// @ ensures p.sInit()
// @ ensures acc(p.sInitD().Mem(), _)
// @ ensures p.sInitD() == old(p.sInitD())
Expand All @@ -1433,13 +1449,15 @@ func (p *scionPacketProcessor) reset() (err error) {
// @ requires dp.Valid()
// @ requires acc(ioLock.LockP(), _) && ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>;
// @ requires let absPkt := absIO_val(dp, rawPkt, p.getIngressID()) in
// @ absPkt.isIO_val_Pkt2 ==> ElemWitness(ioSharedArg.IBufY, ifsToIO_ifs(p.getIngressID()), absPkt.IO_val_Pkt2_2)
// @ ensures reserr == nil && newAbsPkt.isIO_val_Pkt2 ==>
// @ ElemWitness(ioSharedArg.OBufY, newAbsPkt.IO_val_Pkt2_1, newAbsPkt.IO_val_Pkt2_2)
// @ ensures reserr == nil && newAbsPkt.isIO_val_Pkt2 ==> respr.OutPkt != nil &&
// @ newAbsPkt == absIO_val(dp, respr.OutPkt, respr.EgressID)
// TODO: On a first step, we will prove that whenever we have a valid scion packet in processSCION,
// the correct "next packet" is computed
// @ absPkt.isIO_val_Pkt2 ==> ElemWitness(ioSharedArg.IBufY, ifsToIO_ifs(p.getIngressID()), absPkt.IO_val_Pkt2_2)
// @ ensures dp.Valid()
// @ ensures respr.OutPkt != nil ==>
// @ newAbsPkt == absIO_val(dp, respr.OutPkt, respr.EgressID)
// @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{})
// @ ensures newAbsPkt.isIO_val_Pkt2 ==>
// @ ElemWitness(ioSharedArg.OBufY, newAbsPkt.IO_val_Pkt2_1, newAbsPkt.IO_val_Pkt2_2)
// @ ensures reserr != nil && respr.OutPkt != nil ==> newAbsPkt.isIO_val_Unsupported
// @ ensures respr.OutPkt != nil ==> newAbsPkt == absIO_val(dp, respr.OutPkt, respr.EgressID)
func (p *scionPacketProcessor) processPkt(rawPkt []byte,
srcAddr *net.UDPAddr /*@, ghost ioLock *sync.Mutex, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/) (respr processResult, reserr error /*@ , addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) {

Expand Down Expand Up @@ -1734,8 +1752,10 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) {
// @ absPkt.isIO_val_Pkt2 ==> ElemWitness(ioSharedArg.IBufY, ifsToIO_ifs(p.ingressID), absPkt.IO_val_Pkt2_2)
// @ ensures reserr == nil && newAbsPkt.isIO_val_Pkt2 ==>
// @ ElemWitness(ioSharedArg.OBufY, newAbsPkt.IO_val_Pkt2_1, newAbsPkt.IO_val_Pkt2_2)
// @ ensures reserr == nil && newAbsPkt.isIO_val_Pkt2 ==> respr.OutPkt != nil &&
// @ ensures respr.OutPkt != nil ==>
// @ newAbsPkt == absIO_val(dp, respr.OutPkt, respr.EgressID)
// @ ensures reserr != nil && respr.OutPkt != nil ==>
// @ newAbsPkt.isIO_val_Unsupported
func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock *sync.Mutex, ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) {

var ok bool
Expand Down Expand Up @@ -3215,7 +3235,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool,
return r, serrors.WithCtx(err, "info", "after xover") /*@, false, io.IO_val_Unit{} @*/
}
// verify the new block
if r, err := p.verifyCurrentMAC( /*@ nextPkt, dp @*/ ); err != nil {
if r, err := p.verifyCurrentMAC(); err != nil {
// @ p.scionLayer.DowngradePerm(ub)
return r, serrors.WithCtx(err, "info", "after xover") /*@, false, io.IO_val_Unit{} @*/
}
Expand Down
55 changes: 34 additions & 21 deletions router/dataplane_concurrency_model.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,29 +160,32 @@ requires ElemAuth(s.ibuf, y.IBufY) && ElemAuth(s.obuf, y.OBufY)
ensures MultiReadBio(t, n)
ensures MultiReadBioUpd(t, n, s) == old(MultiReadBioUpd(t, n, s))
ensures MultiReadBioNext(t, n) == old(MultiReadBioNext(t, n))
ensures ElemAuth(MultiReadBioUpd(t, n, s).ibuf, y.IBufY) && ElemAuth(MultiReadBioUpd(t, n, s).obuf, y.OBufY)
ensures 0 <= n && MultiReadBioCorrectIfs(t, n, k) ==> MultiElemWitness(y.IBufY, k, MultiReadBioIO_val(t, n))
ensures ElemAuth(MultiReadBioUpd(t, n, s).ibuf, y.IBufY)
ensures ElemAuth(MultiReadBioUpd(t, n, s).obuf, y.OBufY)
ensures 0 <= n && MultiReadBioCorrectIfs(t, n, k) ==>
MultiElemWitness(y.IBufY, k, MultiReadBioIO_val(t, n))
decreases n
func MultiUpdateElemWitness(
t io.Place,
n int,
k Key,
s io.IO_dp3s_state_local,
y SharedArg) {
if n > 0 {
unfold MultiReadBio(t, n)
val := io.dp3s_iospec_bio3s_recv_R(t)
next := io.dp3s_iospec_bio3s_recv_T(t)
if val.isIO_val_Pkt2{
UpdateElemWitness(s.ibuf, y.IBufY, val.IO_val_Pkt2_1, val.IO_val_Pkt2_2)
}
MultiUpdateElemWitness(next, n-1, k, addIbuf(s, val), y)
fold MultiReadBio(t, n)
}

if 0 <= n && MultiReadBioCorrectIfs(t, n, k) {
fold MultiElemWitness(y.IBufY, k, MultiReadBioIO_val(t, n))
}
t io.Place,
n int,
k Key,
s io.IO_dp3s_state_local,
y SharedArg) {
if n > 0 {
unfold MultiReadBio(t, n)
val := io.dp3s_iospec_bio3s_recv_R(t)
next := io.dp3s_iospec_bio3s_recv_T(t)
if val.isIO_val_Pkt2{
UpdateElemWitness(s.ibuf, y.IBufY, val.IO_val_Pkt2_1, val.IO_val_Pkt2_2)
}
MultiUpdateElemWitness(next, n-1, k, addIbuf(s, val), y)
fold MultiReadBio(t, n)
}

if 0 <= n && MultiReadBioCorrectIfs(t, n, k) {
reveal MultiReadBioIO_val(t, n)
fold MultiElemWitness(y.IBufY, k, MultiReadBioIO_val(t, n))
}
}

// Every well-formed packet is accompanied by a witness. Establishing the MultiElemWitness
Expand Down Expand Up @@ -226,6 +229,16 @@ func MultiElemWitnessStep(y ElemRA, k Key, es seq[io.IO_val], currIdx int) {
unfold MultiElemWitnessWithIndex(y, k, es, currIdx)
}

ghost
requires 0 <= currIdx && currIdx < len(es)
requires MultiElemWitnessWithIndex(y, k, es, currIdx)
ensures es[currIdx].isIO_val_Pkt2 ==> ElemWitness(y, k, es[currIdx].IO_val_Pkt2_2)
ensures MultiElemWitnessWithIndex(y, k, es, currIdx + 1)
decreases
func MultiElemWitnessStep(y ElemRA, k Key, es seq[io.IO_val], currIdx int) {
unfold MultiElemWitnessWithIndex(y, k, es, currIdx)
}

ghost
requires i >= 0
requires MultiElemWitness(y,k,es[i:])
Expand Down
18 changes: 15 additions & 3 deletions router/io-spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,14 @@
package router

import (
sl "verification/utils/slices"
"verification/io"
"verification/dependencies/encoding/binary"
"github.com/scionproto/scion/pkg/slayers/path"
"github.com/scionproto/scion/pkg/slayers/path/scion"
"github.com/scionproto/scion/private/topology"
"golang.org/x/net/ipv4"

"verification/dependencies/encoding/binary"
"verification/io"
sl "verification/utils/slices"
. "verification/utils/definitions"
)

Expand Down Expand Up @@ -652,3 +654,13 @@ pure func (d *DataPlane) DpAgreesWithSpec(dp io.DataPlaneSpec) bool {
d.dpSpecWellConfiguredNeighborIAs(dp) &&
d.dpSpecWellConfiguredLinkTypes(dp)
}

ghost
requires dp.Valid()
requires acc(msg.Mem(), R50)
decreases
pure func MsgToAbsVal(dp io.DataPlaneSpec, msg *ipv4.Message, ingressID uint16) (res io.IO_val) {
return unfolding acc(msg.Mem(), R50) in
absIO_val(dp, msg.Buffers[0], ingressID)
}

Loading

0 comments on commit 1e85796

Please sign in to comment.