diff --git a/.gitignore b/.gitignore index 89f277b5d..098a44ecb 100644 --- a/.gitignore +++ b/.gitignore @@ -101,3 +101,5 @@ target *.internal .devcontainer .metals +.bazelbsp +.bazel diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra index 5fd0ba9a6..df7b48e19 100644 --- a/pkg/slayers/path/scion/raw_spec.gobra +++ b/pkg/slayers/path/scion/raw_spec.gobra @@ -382,15 +382,15 @@ requires validPktMetaHdr(raw) decreases pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) { return let _ := reveal validPktMetaHdr(raw) in - let metaHdr := RawBytesToMetaHdr(raw) in + let metaHdr := RawBytesToMetaHdr(raw) in let currInfIdx := int(metaHdr.CurrINF) in - let currHfIdx := int(metaHdr.CurrHF) in - let seg1Len := int(metaHdr.SegLen[0]) in - let seg2Len := int(metaHdr.SegLen[1]) in - let seg3Len := int(metaHdr.SegLen[2]) in + let currHfIdx := int(metaHdr.CurrHF) in + let seg1Len := int(metaHdr.SegLen[0]) in + let seg2Len := int(metaHdr.SegLen[1]) in + let seg3Len := int(metaHdr.SegLen[2]) in let segs := io.CombineSegLens(seg1Len, seg2Len, seg3Len) in - let segLen := segs.LengthOfCurrSeg(currHfIdx) in - let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in + let segLen := segs.LengthOfCurrSeg(currHfIdx) in + let prevSegLen := segs.LengthOfPrevSeg(currHfIdx) in let numINF := segs.NumInfoFields() in let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in io.IO_Packet2 { @@ -407,7 +407,7 @@ requires acc(sl.Bytes(raw, 0, len(raw)), R56) decreases pure func RawBytesToMetaHdr(raw []byte) MetaHdr { return unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in - let hdr := binary.BigEndian.Uint32(raw[:MetaLen]) in + let hdr := binary.BigEndian.Uint32(raw[:MetaLen]) in DecodedFrom(hdr) } @@ -436,9 +436,8 @@ pure func validPktMetaHdr(raw []byte) bool { let seg3 := int(metaHdr.SegLen[2]) in let segs := io.CombineSegLens(seg1, seg2, seg3) in let base := RawBytesToBase(raw) in - 0 < metaHdr.SegLen[0] && - base.StronglyValid() && - base.CurrInfMatchesCurrHF() && + 0 < metaHdr.SegLen[0] && + base.FullyValid() && PktLen(segs, MetaLen) <= len(raw) } diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 9d5689d17..56c1dbbba 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -335,8 +335,8 @@ ghost requires 0 < p preserves acc(s.Mem(ub), p) ensures let start := s.PathStartIdx(ub) in - let end := s.PathEndIdx(ub) in - 0 <= start && start <= end && end <= len(ub) + let end := s.PathEndIdx(ub) in + 0 <= start && start <= end && end <= len(ub) decreases func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) { unfold acc(s.Mem(ub), p) @@ -461,7 +461,7 @@ pure func ValidPktMetaHdr(raw []byte) bool { let length := GetLength(raw) in length <= len(raw) && unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in - let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in + let _ := Asserting(forall k int :: {&rawHdr[k]} 0 <= k && k < scion.MetaLen ==> &rawHdr[k] == &raw[start + k]) in let hdr := binary.BigEndian.Uint32(rawHdr) in let metaHdr := scion.DecodedFrom(hdr) in let seg1 := int(metaHdr.SegLen[0]) in diff --git a/router/assumptions.gobra b/router/assumptions.gobra index f8811b007..17716e7fc 100644 --- a/router/assumptions.gobra +++ b/router/assumptions.gobra @@ -75,6 +75,16 @@ ensures cannotRoute.ErrorMem() decreases _ func establishCannotRoute() +ghost +ensures invalidSrcIA.ErrorMem() +decreases _ +func establishInvalidSrcIA() + +ghost +ensures invalidDstIA.ErrorMem() +decreases _ +func establishInvalidDstIA() + /**** End of post-init invariants ****/ /**** scmpError ghost members ****/ diff --git a/router/dataplane.go b/router/dataplane.go index 3ce5d8f6d..3d9370488 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1426,6 +1426,7 @@ func (p *scionPacketProcessor) reset() (err error) { return nil } +// @ trusted // TODO: drop // @ requires p.sInit() // @ requires sl.Bytes(rawPkt, 0, len(rawPkt)) // @ requires acc(srcAddr.Mem(), _) @@ -1479,7 +1480,7 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte, // parse SCION header and skip extensions; var err error // @ ghost var processed seq[bool] - // @ ghost var offsets seq[offsetPair] + // ghost var offsets seq[offsetPair] // @ ghost var lastLayerIdx int p.lastLayer, err /*@ , processed, offsets, lastLayerIdx @*/ = decodeLayers(p.rawPkt, &p.scionLayer, &p.hbhLayer, &p.e2eLayer) if err != nil { @@ -1724,7 +1725,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ acc(p.lastLayer.Mem(nil), R10) // @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==> // @ acc(p.lastLayer.Mem(ub[startLL:endLL]), R10) -// @ requires acc(&p.ingressID, R20) +// @ requires acc(&p.ingressID, R10) // @ preserves acc(&p.infoField) // @ preserves acc(&p.hopField) // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem() @@ -1732,7 +1733,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) { // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures acc(&p.segmentChange) -// @ ensures acc(&p.ingressID, R20) +// @ ensures acc(&p.ingressID, R10) // @ ensures acc(&p.d, R5) // @ ensures acc(&p.path) // @ ensures acc(&p.rawPkt, R1) @@ -1883,42 +1884,104 @@ type macBuffersT struct { epicInput []byte } -// @ trusted -// @ requires false +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R45) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ requires cause.ErrorMem() +// @ ensures acc(&p.d, R20) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures sl.Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R45) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() // @ ensures reserr != nil && respr.OutPkt != nil ==> -// @ absIO_val(respr.OutPkt, respr.EgressID).isIO_val_Unsupported +// @ !slayers.IsSupportedPkt(respr.OutPkt) +// @ decreases func (p *scionPacketProcessor) packSCMP( typ slayers.SCMPType, code slayers.SCMPCode, scmpP gopacket.SerializableLayer, cause error, + // @ ghost ub []byte, + // @ ghost ubLL []byte, + // @ ghost startLL int, + // @ ghost endLL int, ) (respr processResult, reserr error) { - + // @ ghost llIsScmp := false + // @ ghost scmpPldIsNil := false + // @ ghost maybeStartPld := 0 + // @ ghost maybeEndPld := 0 // check invoking packet was an SCMP error: - if p.lastLayer.NextLayerType() == slayers.LayerTypeSCMP { - var scmpLayer slayers.SCMP - err := scmpLayer.DecodeFromBytes(p.lastLayer.LayerPayload(), gopacket.NilDecodeFeedback) + if p.lastLayer.NextLayerType( /*@ ubLL @*/ ) == slayers.LayerTypeSCMP { + // @ llIsScmp = true + var scmpLayer /*@@@*/ slayers.SCMP + // @ fold scmpLayer.NonInitMem() + pld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ ) + // @ sl.SplitRange_Bytes(ub, startLL, endLL, writePerm) + // @ maybeStartPld = start + // @ maybeEndPld = end + // @ if pld == nil { + // @ scmpPldIsNil = true + // @ fold sl.Bytes(nil, 0, 0) + // @ } else { + // @ sl.SplitRange_Bytes(ubLL, start, end, writePerm) + // @ } + // @ gopacket.AssertInvariantNilDecodeFeedback() + err := scmpLayer.DecodeFromBytes(pld, gopacket.NilDecodeFeedback) if err != nil { + // @ ghost if !scmpPldIsNil { sl.CombineRange_Bytes(ubLL, start, end, writePerm) } + // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("decoding SCMP layer", err) } - if !scmpLayer.TypeCode.InfoMsg() { + if /*@ unfolding scmpLayer.Mem(pld) in @*/ !scmpLayer.TypeCode.InfoMsg() { + // @ ghost if !scmpPldIsNil { sl.CombineRange_Bytes(ubLL, start, end, writePerm) } + // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + // @ fold p.d.validResult(processResult{}, false) return processResult{}, serrors.WrapStr("SCMP error for SCMP error pkt -> DROP", cause) } } - rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , nil @*/) // (VerifiedSCION) replace nil by sth else + // @ ghost if llIsScmp { + // @ ghost if !scmpPldIsNil { + // @ sl.CombineRange_Bytes(ubLL, maybeStartPld, maybeEndPld, writePerm) + // @ } + // @ sl.CombineRange_Bytes(ub, startLL, endLL, writePerm) + // @ } + rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , ub @*/) + // @ ghost result := processResult{OutPkt: rawSCMP} + // @ fold p.d.validResult(result, false) return processResult{OutPkt: rawSCMP}, err } +// @ requires acc(sl.Bytes(ub, 0, len(ub)), R1) // @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R5) // @ requires acc(&p.path, R20) // @ requires p.path === p.scionLayer.GetPath(ub) // @ requires acc(&p.hopField) && acc(&p.infoField) -// @ requires acc(sl.Bytes(ub, 0, len(ub)), R1) +// @ requires p.scionLayer.EqAbsHeader(ub) +// @ requires p.scionLayer.ValidScionInitSpec(ub) // @ ensures acc(sl.Bytes(ub, 0, len(ub)), R1) // @ ensures acc(&p.d, R50) -// @ ensures acc(p.scionLayer.Mem(ub), R6) +// @ ensures acc(p.scionLayer.Mem(ub), R5) // @ ensures acc(&p.path, R20) // @ ensures p.path === p.scionLayer.GetPath(ub) // @ ensures acc(&p.hopField) && acc(&p.infoField) @@ -1927,16 +1990,16 @@ func (p *scionPacketProcessor) packSCMP( // @ let ubPath := p.scionLayer.UBPath(ub) in // @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrHF(ubPath) < p.path.GetNumHops(ubPath)) -// @ ensures acc(p.scionLayer.Mem(ub), R6) // @ ensures p.d.validResult(respr, false) // @ ensures reserr == nil ==> ( // @ let ubPath := p.scionLayer.UBPath(ub) in // @ unfolding acc(p.scionLayer.Mem(ub), R10) in // @ p.path.GetCurrINF(ubPath) < p.path.GetNumINF(ubPath)) // @ ensures reserr != nil ==> reserr.ErrorMem() -// contracts for IO-spec -// @ requires p.scionLayer.EqAbsHeader(ub) && p.scionLayer.ValidScionInitSpec(ub) -// @ ensures reserr == nil ==> slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub) +// @ ensures reserr == nil ==> +// @ slayers.ValidPktMetaHdr(ub) && +// @ p.scionLayer.EqAbsHeader(ub) && +// @ p.scionLayer.ValidPathMetaData(ub) // @ ensures reserr == nil ==> len(absPkt(ub).CurrSeg.Future) > 0 // @ ensures reserr == nil ==> p.EqAbsHopField(absPkt(ub)) // @ ensures reserr == nil ==> p.EqAbsInfoField(absPkt(ub)) @@ -1987,18 +2050,23 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce return processResult{}, nil } +// HERE // @ preserves acc(&p.infoField, R20) // @ preserves acc(&p.hopField, R20) +// @ preserves acc(&p.path, R20) +// @ preserves acc(&p.ingressID, R20) // @ preserves acc(&p.d, R50) && acc(p.d.Mem(), _) +// @ preserves acc(p.scionLayer.Mem(ubScionL), R3) +// @ preserves p.path == p.scionLayer.GetPath(ubScionL) // @ ensures p.d.validResult(respr, false) // @ ensures respr.OutPkt != nil ==> // @ reserr != nil && sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() -// contracts for IO-spec +// posts for IO // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isIO_val_Unsupported // @ decreases -func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr error) { +func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte @*/ ) (respr processResult, reserr error) { expiration := util.SecsToTime(p.infoField.Timestamp). Add(path.ExpTimeToDuration(p.hopField.ExpTime)) expired := expiration.Before(time.Now()) @@ -2020,9 +2088,18 @@ func (p *scionPacketProcessor) validateHopExpiry() (respr processResult, reserr return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodePathExpired, - &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, - serrors.New("expired hop", "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, - "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF), + &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ ubScionL @*/ )}, + serrors.New( + "expired hop", + "cons_dir", + /*@ unfolding acc(p.scionLayer.Mem(ubScionL), R20) in @*/ p.infoField.ConsDir, + "if_id", + p.ingressID, + "curr_inf", + /*@ unfolding acc(p.scionLayer.Mem(ubScionL), R20) in @*/ p.path.PathMeta.CurrINF, + "curr_hf", + /*@ unfolding acc(p.scionLayer.Mem(ubScionL), R20) in @*/ p.path.PathMeta.CurrHF), + /*@ nil , nil, 0, 0, @*/ ) } @@ -2065,6 +2142,7 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost oldPkt io.IO_pkt2 @* &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.New("ingress interface invalid", "pkt_ingress", pktIngressID, "router_ingress", p.ingressID), + /*@ nil , nil, 0, 0, @*/ ) } // @ reveal p.EqAbsHopField(oldPkt) @@ -2117,22 +2195,22 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) // Note: SCMP error messages triggered by the sibling router may use paths that // don't start with the first hop. if p.path.IsFirstHop( /*@ ubPath @*/ ) && !srcIsLocal { - // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP - return p.invalidSrcIA() + // @ TODO() + return p.invalidSrcIA( /*@ nil, nil, 0, 0 @*/ ) } if dstIsLocal { - // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP - return p.invalidDstIA() + // @ TODO() + return p.invalidDstIA( /*@ nil, nil, 0, 0 @*/ ) } } else { // Inbound if srcIsLocal { - // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP - return p.invalidSrcIA() + // @ TODO() + return p.invalidSrcIA( /*@ nil, nil, 0, 0 @*/ ) } if p.path.IsLastHop( /*@ ubPath @*/ ) != dstIsLocal { - // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP - return p.invalidDstIA() + // @ TODO() + return p.invalidDstIA( /*@ nil, nil, 0, 0 @*/ ) } // @ ghost if(p.path.IsLastHopSpec(ubPath)) { // @ p.path.LastHopLemma(ubPath) @@ -2154,26 +2232,94 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte @*/ ) } // invalidSrcIA is a helper to return an SCMP error for an invalid SrcIA. -// @ trusted -// @ requires false -func (p *scionPacketProcessor) invalidSrcIA() (processResult, error) { +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer === p.lastLayer ==> +// @ ub === ubLL +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, R20) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures sl.Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases +func (p *scionPacketProcessor) invalidSrcIA( +// @ ghost ub []byte, +// @ ghost ubLL []byte, +// @ ghost startLL int, +// @ ghost endLL int, +) (respr processResult, reserr error) { + // @ establishInvalidSrcIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidSourceAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen + addr.IABytes)}, invalidSrcIA, + /*@ ub , ubLL, startLL, endLL, @*/ ) } // invalidDstIA is a helper to return an SCMP error for an invalid DstIA. -// @ trusted -// @ requires false -func (p *scionPacketProcessor) invalidDstIA() (processResult, error) { +// @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ requires &p.scionLayer === p.lastLayer ==> +// @ ub === ubLL +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() +// @ ensures acc(&p.d, R20) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures &p.scionLayer !== p.lastLayer ==> +// @ acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures sl.Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ ensures p.d.validResult(respr, false) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// @ ensures reserr != nil ==> reserr.ErrorMem() +// @ decreases +func (p *scionPacketProcessor) invalidDstIA( +// @ ghost ub []byte, +// @ ghost ubLL []byte, +// @ ghost startLL int, +// @ ghost endLL int, +) (respr processResult, reserr error) { + // @ establishInvalidDstIA() return p.packSCMP( slayers.SCMPTypeParameterProblem, slayers.SCMPCodeInvalidDestinationAddress, &slayers.SCMPParameterProblem{Pointer: uint16(slayers.CmnHdrLen)}, invalidDstIA, + /*@ ub , ubLL, startLL, endLL, @*/ ) } @@ -2298,6 +2444,7 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost oldPkt io.IO_pkt2, gh errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, + /*@ nil, nil, 0, 0, @*/ ) } // @ p.d.getDomExternalLemma() @@ -2333,7 +2480,8 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost oldPkt io.IO_pkt2, gh slayers.SCMPCodeInvalidPath, // XXX(matzf) new code InvalidHop? &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, serrors.WithCtx(cannotRoute, "ingress_id", p.ingressID, "ingress_type", ingress, - "egress_id", pktEgressID, "egress_type", egress)) + "egress_id", pktEgressID, "egress_type", egress), + /*@ nil, nil, 0, 0, @*/) } } // @ assert reveal AbsValidateIngressIDConstraintXover(oldPkt, path.ifsToIO_ifs(p.ingressID)) @@ -2359,7 +2507,8 @@ func (p *scionPacketProcessor) validateEgressID( /*@ ghost oldPkt io.IO_pkt2, gh slayers.SCMPCodeInvalidSegmentChange, &slayers.SCMPParameterProblem{Pointer: p.currentInfoPointer( /*@ nil @*/ )}, serrors.WithCtx(cannotRoute, "ingress_id", p.ingressID, "ingress_type", ingress, - "egress_id", pktEgressID, "egress_type", egress)) + "egress_id", pktEgressID, "egress_type", egress), + /*@ nil, nil, 0, 0, @*/) } } @@ -2517,6 +2666,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost oldPkt io.IO_pkt2, gh "cons_dir", p.infoField.ConsDir, "if_id", p.ingressID, "curr_inf", p.path.PathMeta.CurrINF, "curr_hf", p.path.PathMeta.CurrHF, "seg_id", p.infoField.SegID), + /*@ nil, nil, 0, 0, @*/ ) } // Add the full MAC to the SCION packet processor, @@ -2567,7 +2717,9 @@ func (p *scionPacketProcessor) resolveInbound( /*@ ghost ubScionL []byte @*/ ) ( r, err := p.packSCMP( slayers.SCMPTypeDestinationUnreachable, slayers.SCMPCodeNoRoute, - &slayers.SCMPDestinationUnreachable{}, err) + &slayers.SCMPDestinationUnreachable{}, + err, + /*@ nil, nil, 0, 0, @*/) return nil, r, err /*@ , false @*/ default: // @ fold p.d.validResult(respr, addrAliases) @@ -2680,6 +2832,8 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte @*/ ) (reserr // @ ensures reserr == nil ==> p.EqAbsHopField(absPkt(ub)) // @ ensures reserr == nil ==> p.EqAbsInfoField(absPkt(ub)) // @ ensures reserr == nil ==> absPkt(ub) == AbsDoXover(old(absPkt(ub))) +// @ ensures reserr == nil ==> +// @ p.scionLayer.ValidPathMetaData(ub) == old(p.scionLayer.ValidPathMetaData(ub)) // @ decreases func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte @*/ ) (respr processResult, reserr error) { p.segmentChange = true @@ -2769,12 +2923,13 @@ func (p *scionPacketProcessor) ingressInterface( /*@ ghost ubPath []byte @*/ ) u // @ requires acc(&p.infoField, R21) // @ requires acc(&p.hopField, R21) -// @ ensures acc(&p.infoField, R21) -// @ ensures acc(&p.hopField, R21) -// contracts for IO-spec +// pres for IO: // @ requires len(oldPkt.CurrSeg.Future) > 0 // @ requires p.EqAbsInfoField(oldPkt) // @ requires p.EqAbsHopField(oldPkt) +// @ ensures acc(&p.infoField, R21) +// @ ensures acc(&p.hopField, R21) +// posts for IO: // @ ensures p.EqAbsInfoField(oldPkt) // @ ensures p.EqAbsHopField(oldPkt) // @ ensures AbsEgressInterfaceConstraint(oldPkt, path.ifsToIO_ifs(egress)) @@ -2791,24 +2946,47 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.IO_pkt2 @*/ } // @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) +// @ requires ubLL == nil || ubLL === ub[startLL:endLL] +// @ requires acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ requires acc(p.lastLayer.Mem(ubLL), R15) +// @ requires acc(&p.buffer, R50) && p.buffer.Mem() // @ requires acc(&p.infoField, R20) // @ requires acc(&p.hopField, R20) -// @ preserves acc(&p.ingressID, R21) +// @ requires acc(&p.ingressID, R21) +// pres for IO: +// @ requires len(oldPkt.CurrSeg.Future) > 0 +// @ requires p.EqAbsInfoField(oldPkt) +// @ requires p.EqAbsHopField(oldPkt) // @ ensures acc(&p.infoField, R20) // @ ensures acc(&p.hopField, R20) +// @ ensures acc(&p.ingressID, R21) +// @ preserves sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.d, R20) // @ ensures p.d.validResult(respr, false) -// @ ensures respr.OutPkt != nil ==> -// @ reserr != nil && sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() -// contracts for IO-spec -// @ requires len(oldPkt.CurrSeg.Future) > 0 -// @ requires p.EqAbsInfoField(oldPkt) -// @ requires p.EqAbsHopField(oldPkt) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures acc(&p.lastLayer, R55) && p.lastLayer != nil +// @ ensures acc(p.lastLayer.Mem(ubLL), R15) +// @ ensures acc(&p.buffer, R50) +// @ ensures respr === processResult{} ==> +// @ p.buffer.Mem() +// @ ensures respr !== processResult{} ==> +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) +// posts for IO: // @ ensures reserr != nil && respr.OutPkt != nil ==> // @ absIO_val(respr.OutPkt, respr.EgressID).isIO_val_Unsupported // @ decreases 0 if sync.IgnoreBlockingForTermination() -func (p *scionPacketProcessor) validateEgressUp( /*@ ghost oldPkt io.IO_pkt2 @*/ ) (respr processResult, reserr error) { +func (p *scionPacketProcessor) validateEgressUp( +// @ ghost ub []byte, +// @ ghost ubLL []byte, +// @ ghost startLL int, +// @ ghost endLL int, +// @ ghost oldPkt io.IO_pkt2, +) (respr processResult, reserr error) { egressID := p.egressInterface( /*@ oldPkt @ */ ) // @ p.d.getBfdSessionsMem() // @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) } @@ -2830,8 +3008,11 @@ func (p *scionPacketProcessor) validateEgressUp( /*@ ghost oldPkt io.IO_pkt2 @*/ Egress: uint64(egressID), } } - // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP - return p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down")) + tmpRes, tmpErr := p.packSCMP(typ, 0, scmpP, serrors.New("bfd session down") /*@, ub , ubLL, startLL, endLL, @*/) + // @ ghost if tmpErr != nil && tmpRes.OutPkt != nil { + // @ AbsUnsupportedPktIsUnsupportedVal(tmpRes.OutPkt, tmpRes.EgressID) + // @ } + return tmpRes, tmpErr } } // @ fold p.d.validResult(processResult{}, false) @@ -2949,9 +3130,9 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ requires acc(p.scionLayer.Mem(ub), R13) // @ requires p.path === p.scionLayer.GetPath(ub) // @ requires acc(&p.d, R20) && acc(p.d.Mem(), _) -// @ requires sl.Bytes(ub, 0, len(ub)) -// @ requires acc(&p.infoField, R20) -// @ requires acc(&p.hopField) +// @ requires sl.Bytes(ub, 0, len(ub)) +// @ requires acc(&p.infoField, R20) +// @ requires acc(&p.hopField) // @ preserves acc(&p.lastLayer, R19) // @ preserves p.lastLayer != nil // @ preserves (&p.scionLayer !== p.lastLayer && llIsNil) ==> @@ -2959,9 +3140,9 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) { // @ preserves (&p.scionLayer !== p.lastLayer && !llIsNil) ==> // @ acc(p.lastLayer.Mem(ub[startLL:endLL]), R15) // @ preserves acc(&p.ingressID, R21) -// @ ensures acc(&p.infoField, R20) -// @ ensures acc(&p.hopField) -// @ ensures sl.Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.infoField, R20) +// @ ensures acc(&p.hopField) +// @ ensures sl.Bytes(ub, 0, len(ub)) // @ ensures acc(&p.path, R20) // @ ensures acc(p.scionLayer.Mem(ub), R13) // @ ensures acc(&p.d, R20) @@ -3113,7 +3294,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest( Interface: uint64(interfaceID), } // @ ToDoAfterScionFix("https://github.com/scionproto/scion/issues/4482") // depends on packSCMP - return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, nil) + return p.packSCMP(slayers.SCMPTypeTracerouteReply, 0, &scmpP, (error)(nil) /*@ , nil, nil, 0, 0, @*/) } // @ preserves acc(p.scionLayer.Mem(ubScionL), R20) @@ -3142,21 +3323,21 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( &slayers.SCMPParameterProblem{Pointer: 0}, serrors.New("bad packet size", "header", p.scionLayer.PayloadLen, "actual", len(p.scionLayer.Payload)), + /*@ nil, nil, 0, 0, @*/ ) } // @ requires 0 <= startLL && startLL <= endLL && endLL <= len(ub) // @ requires acc(&p.d, R5) && acc(p.d.Mem(), _) && p.d.WellConfigured() // @ requires p.d.getValSvc() != nil -// The ghost param ub here allows us to introduce a bound variable to p.rawPkt, -// which slightly simplifies the spec // @ requires acc(&p.rawPkt, R1) && ub === p.rawPkt // @ requires acc(&p.path, R10) // @ requires p.scionLayer.Mem(ub) // @ requires p.path == p.scionLayer.GetPath(ub) // @ requires sl.Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R20) +// @ requires acc(&p.ingressID, R15) // @ requires acc(&p.segmentChange) && !p.segmentChange +// @ requires acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem() // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _) // @ preserves acc(&p.lastLayer, R10) // @ preserves p.lastLayer != nil @@ -3171,7 +3352,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput)) // @ preserves acc(&p.cachedMac) // @ ensures acc(&p.segmentChange) -// @ ensures acc(&p.ingressID, R20) +// @ ensures acc(&p.ingressID, R15) // @ ensures acc(&p.d, R5) // @ ensures acc(&p.path, R10) // @ ensures acc(&p.rawPkt, R1) @@ -3183,8 +3364,11 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ ensures !addrAliasesPkt ==> acc(sl.Bytes(ub, 0, len(ub)), R15) // @ ensures respr.OutPkt !== ub && respr.OutPkt != nil ==> // @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) -// @ ensures reserr == nil ==> p.scionLayer.Mem(ub) -// @ ensures reserr != nil ==> p.scionLayer.NonInitMem() +// @ ensures acc(&p.buffer, R10) +// @ ensures reserr == nil ==> p.scionLayer.Mem(ub) && p.buffer.Mem() +// @ ensures reserr != nil ==> p.scionLayer.NonInitMem() && +// @ p.buffer.MemWithoutUBuf(respr.OutPkt) && +// @ sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)) // @ ensures reserr != nil ==> reserr.ErrorMem() // contracts for IO-spec // @ requires p.d.DpAgreesWithSpec(dp) @@ -3203,7 +3387,15 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte @*/ ) ( // @ ensures (respr.OutPkt == nil) == (newAbsPkt == io.IO_val_Unit{}) // @ decreases 0 if sync.IgnoreBlockingForTermination() // @ #backend[stateConsolidationMode(6)] -func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { +func (p *scionPacketProcessor) process( +// @ ghost ub []byte, +// @ ghost llIsNil bool, +// @ ghost startLL int, +// @ ghost endLL int, +// @ ghost ioLock gpointer[gsync.GhostMutex], +// @ ghost ioSharedArg SharedArg, +// @ ghost dp io.DataPlaneSpec, +) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.IO_val @*/) { if r, err := p.parsePath( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(r) @*/ @@ -3217,7 +3409,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ oldPkt = absPkt(ub) // @ } // @ nextPkt := oldPkt - if r, err := p.validateHopExpiry(); err != nil { + if r, err := p.validateHopExpiry( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(r) @*/ } @@ -3259,7 +3451,9 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ p.d.getLocalIA() if /*@ unfolding acc(p.scionLayer.Mem(ub), R50) in (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in @*/ p.scionLayer.DstIA /*@ ) @*/ == p.d.localIA { // @ assert p.DstIsLocalIngressID(ub) - // @ assert unfolding acc(p.scionLayer.Mem(ub), R50) in (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in p.scionLayer.DstIA) == p.d.localIA + // @ assert unfolding acc(p.scionLayer.Mem(ub), R50) in + // @ (unfolding acc(p.scionLayer.HeaderMem(ub[slayers.CmnHdrLen:]), R55) in + // @ p.scionLayer.DstIA) == p.d.localIA // @ p.LocalDstLemma(ub) // @ assert p.ingressID != 0 // @ assert len(nextPkt.CurrSeg.Future) == 1 @@ -3293,7 +3487,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, // @ assert absPkt(ub) == AbsDoXover(nextPkt) // @ AbsValidateIngressIDXoverLemma(nextPkt, AbsDoXover(nextPkt), path.ifsToIO_ifs(p.ingressID)) // @ nextPkt = absPkt(ub) - if r, err := p.validateHopExpiry(); err != nil { + if r, err := p.validateHopExpiry( /*@ ub @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, serrors.WithCtx(err, "info", "after xover") /*@, false, absReturnErr(r) @*/ } @@ -3321,7 +3515,12 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, return r, err /*@, false, absReturnErr(r) @*/ } // @ assert nextPkt == absPkt(ub) - if r, err := p.validateEgressUp( /*@ nextPkt @*/ ); err != nil { + // @ ghost ubLL := llIsNil ? []byte(nil) : (p.lastLayer === &p.scionLayer ? ub : ub[startLL:endLL]) + // @ ghost if !llIsNil && p.lastLayer === &p.scionLayer { + // @ startLL = 0 + // @ endLL = len(ub) + // @ } + if r, err := p.validateEgressUp( /*@ ub, ubLL, startLL, endLL, nextPkt, @*/ ); err != nil { // @ p.scionLayer.DowngradePerm(ub) return r, err /*@, false, absReturnErr(r) @*/ } @@ -3384,6 +3583,7 @@ func (p *scionPacketProcessor) process( /*@ ghost ub []byte, ghost llIsNil bool, errCode, &slayers.SCMPParameterProblem{Pointer: p.currentHopPointer( /*@ nil @*/ )}, cannotRoute, + /*@ nil, nil, 0, 0, @*/ ) return tmp, err /*@, false, absReturnErr(tmp) @*/ } @@ -3813,14 +4013,25 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { return err } -// @ requires acc(&p.d, _) && acc(p.d.Mem(), _) +// @ requires acc(&p.d, R50) && acc(p.d.Mem(), _) // @ requires acc(p.scionLayer.Mem(ub), R4) // @ requires p.scionLayer.ValidPathMetaData(ub) // @ requires sl.Bytes(ub, 0, len(ub)) -// @ requires acc(&p.ingressID, R15) +// @ requires acc(&p.ingressID, R50) +// @ requires acc(&p.buffer, R55) && p.buffer.Mem() +// @ ensures acc(&p.d, R50) // @ ensures acc(p.scionLayer.Mem(ub), R4) // @ ensures sl.Bytes(ub, 0, len(ub)) -// @ ensures acc(&p.ingressID, R15) +// @ ensures acc(&p.ingressID, R50) +// @ ensures acc(&p.buffer, R55) +// @ ensures result != nil ==> +// @ sl.Bytes(result, 0, len(result)) && +// @ p.buffer.MemWithoutUBuf(result) +// @ ensures result == nil ==> +// @ p.buffer.Mem() +// @ ensures reserr != nil && reserr.ErrorMem() +// @ ensures reserr != nil && result != nil ==> +// @ !slayers.IsSupportedPkt(result) // @ decreases func (p *scionPacketProcessor) prepareSCMP( typ slayers.SCMPType, @@ -3828,7 +4039,7 @@ func (p *scionPacketProcessor) prepareSCMP( scmpP gopacket.SerializableLayer, cause error, // @ ghost ub []byte, -) ([]byte, error) { +) (result []byte, reserr error) { // *copy* and reverse path -- the original path should not be modified as this writes directly // back to rawPkt (quote). @@ -4044,31 +4255,36 @@ func (p *scionPacketProcessor) prepareSCMP( // @ ensures -1 <= idx && idx < len(opts) // @ ensures len(processed) == len(opts) // @ ensures len(offsets) == len(opts) -// @ ensures reterr == nil && 0 <= idx ==> processed[idx] +// @ ensures reterr == nil && 0 <= idx ==> processed[idx] // @ ensures reterr == nil && idx == -1 ==> retl === base -// @ ensures reterr == nil && 0 <= idx ==> retl === opts[idx] +// @ ensures reterr == nil && 0 <= idx ==> retl === opts[idx] // @ ensures reterr == nil ==> retl != nil // @ ensures reterr == nil ==> base.Mem(data) // @ ensures reterr == nil && typeOf(base.GetPath(data)) == *scion.Raw ==> // @ base.EqAbsHeader(data) && base.ValidScionInitSpec(data) // @ ensures reterr == nil ==> base.EqPathType(data) -// @ ensures forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ (processed[i] ==> (0 <= offsets[i].start && offsets[i].start <= offsets[i].end && offsets[i].end <= len(data))) -// @ ensures reterr == nil ==> forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ ((processed[i] && !offsets[i].isNil) ==> opts[i].Mem(data[offsets[i].start:offsets[i].end])) -// @ ensures reterr == nil ==> forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ ((processed[i] && offsets[i].isNil) ==> opts[i].Mem(nil)) -// @ ensures reterr == nil ==> forall i int :: {&opts[i]}{processed[i]} 0 <= i && i < len(opts) ==> -// @ (!processed[i] ==> opts[i].NonInitMem()) -// @ ensures reterr != nil ==> base.NonInitMem() -// @ ensures reterr != nil ==> (forall i int :: { &opts[i] } 0 <= i && i < len(opts) ==> opts[i].NonInitMem()) -// @ ensures reterr != nil ==> reterr.ErrorMem() +// @ ensures reterr == nil ==> +// @ forall i int :: { &opts[i] } 0 <= i && i < len(opts) && processed[i] ==> +// @ decRelations[i].IsValid(data) && +// @ opts[i].Mem(decRelations[i].LayerSlice(data)) +// @ ensures reterr == nil ==> +// @ forall i int :: { &opts[i] } 0 <= i && i < len(opts) && !processed[i] ==> +// @ opts[i].NonInitMem() +// @ ensures reterr != nil ==> +// @ base.NonInitMem() && reterr.ErrorMem() +// @ ensures reterr != nil ==> +// @ (forall i int :: { &opts[i] } 0 <= i && i < len(opts) ==> opts[i].NonInitMem()) // @ decreases -// (VerifiedSCION) originally, `base` was declared with type `gopacket.DecodingLayer`. This is unnecessarily complicated for a private function -// that is only called once with a parameter of type `*SCION`, and leads to more annyoing post-conditions. -func decodeLayers(data []byte, base *slayers.SCION, - opts ...gopacket.DecodingLayer) (retl gopacket.DecodingLayer, reterr error /*@ , ghost processed seq[bool], ghost offsets seq[offsetPair], ghost idx int @*/) { - +// (VerifiedSCION) originally, `base` was declared with type `gopacket.DecodingLayer`. This is unnecessarily +// complicated for a private function that is only called once with a parameter of type `*SCION`, and leads +// to more annyoing post-conditions. +func decodeLayers(data []byte, base *slayers.SCION, opts ...gopacket.DecodingLayer) ( + retl gopacket.DecodingLayer, + reterr error, + // @ ghost processed seq[bool], + // @ ghost decRelations seq[decodedLayerRelation], + // @ ghost idx int, +) { // @ processed = seqs.NewSeqBool(len(opts)) // @ offsets = newOffsetPair(len(opts)) // @ idx = -1 diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra index 5361ad9c2..1288494f2 100644 --- a/router/dataplane_spec.gobra +++ b/router/dataplane_spec.gobra @@ -164,6 +164,7 @@ pred (err scmpError) ErrorMem() { scmpError implements error +// TODO: drop type offsetPair struct { start int end int @@ -718,3 +719,42 @@ pure func (d *DataPlane) DomainForwardingMetrics() set[uint16] { domain(d.forwardingMetrics) : set[uint16]{} } + +/**** Abstractions for `decodeLayers` and dealing with SCMP packets ****/ +type decodedLayerRelation adt { + decodedLayerIsNil {} + decodedLayerIsBaseLayer {} + decodedLayerIsSubsliceOfBase { + start int + end int + } +} + +ghost +decreases +pure func (l decodedLayerRelation) IsValid(base []byte) bool { + return (match l { + case decodedLayerIsNil{}: + true + case decodedLayerIsBaseLayer{}: + true + case decodedLayerIsSubsliceOfBase{?start, ?end}: + 0 <= start && + start <= end && + end <= len(base) + }) +} + +ghost +requires l.IsValid(base) +decreases +pure func (l decodedLayerRelation) LayerSlice(base []byte) []byte { + return (match l { + case decodedLayerIsNil{}: + nil + case decodedLayerIsBaseLayer{}: + base + case decodedLayerIsSubsliceOfBase{?start, ?end}: + base[start:end] + }) +} \ No newline at end of file diff --git a/router/io-spec.gobra b/router/io-spec.gobra index 6aeed7678..8fb6b9023 100644 --- a/router/io-spec.gobra +++ b/router/io-spec.gobra @@ -83,6 +83,16 @@ pure func absIO_val(raw []byte, ingressID uint16) (val io.IO_val) { absIO_val_Unsupported(raw, ingressID) } +ghost +requires acc(sl.Bytes(raw, 0, len(raw)), R56) +requires !slayers.IsSupportedPkt(raw) +ensures acc(sl.Bytes(raw, 0, len(raw)), R56) +ensures absIO_val(raw, ingressID).isIO_val_Unsupported +decreases +func AbsUnsupportedPktIsUnsupportedVal(raw []byte, ingressID uint16) { + reveal absIO_val(raw, ingressID) +} + ghost requires respr.OutPkt != nil ==> acc(sl.Bytes(respr.OutPkt, 0, len(respr.OutPkt)), R56)