diff --git a/pkg/slayers/path/infofield.go b/pkg/slayers/path/infofield.go index 754b44846..f3488e768 100644 --- a/pkg/slayers/path/infofield.go +++ b/pkg/slayers/path/infofield.go @@ -62,16 +62,16 @@ type InfoField struct { // path.InfoLen. // @ requires len(raw) >= InfoLen // @ preserves acc(inf) -// @ preserves acc(slices.Bytes(raw, 0, InfoLen), R45) +// @ preserves acc(slices.Bytes(raw, 0, len(raw)), R45) // @ ensures err == nil -// @ ensures BytesToIntermediateAbsInfoField(raw, 0, 0, InfoLen) == -// @ inf.ToIntermediateAbsInfoField() +// @ ensures BytesToAbsInfoField(raw, 0) == +// @ inf.ToAbsInfoField() // @ decreases func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) { if len(raw) < InfoLen { return serrors.New("InfoField raw too short", "expected", InfoLen, "actual", len(raw)) } - //@ unfold acc(slices.Bytes(raw, 0, InfoLen), R50) + //@ unfold acc(slices.Bytes(raw, 0, len(raw)), R50) inf.ConsDir = raw[0]&0x1 == 0x1 inf.Peer = raw[0]&0x2 == 0x2 //@ assert &raw[2:4][0] == &raw[2] && &raw[2:4][1] == &raw[3] @@ -79,7 +79,9 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) { //@ assert &raw[4:8][0] == &raw[4] && &raw[4:8][1] == &raw[5] //@ assert &raw[4:8][2] == &raw[6] && &raw[4:8][3] == &raw[7] inf.Timestamp = binary.BigEndian.Uint32(raw[4:8]) - //@ fold acc(slices.Bytes(raw, 0, InfoLen), R50) + //@ fold acc(slices.Bytes(raw, 0, len(raw)), R50) + //@ assert reveal BytesToAbsInfoField(raw, 0) == + //@ inf.ToAbsInfoField() return nil } @@ -87,30 +89,30 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) { // path.InfoLen. // @ requires len(b) >= InfoLen // @ preserves acc(inf, R10) -// @ preserves slices.Bytes(b, 0, InfoLen) +// @ preserves slices.Bytes(b, 0, len(b)) // @ ensures err == nil -// @ ensures inf.ToIntermediateAbsInfoField() == -// @ BytesToIntermediateAbsInfoField(b, 0, 0, InfoLen) +// @ ensures inf.ToAbsInfoField() == +// @ BytesToAbsInfoField(b, 0) // @ decreases func (inf *InfoField) SerializeTo(b []byte) (err error) { if len(b) < InfoLen { return serrors.New("buffer for InfoField too short", "expected", InfoLen, "actual", len(b)) } - //@ ghost targetAbsInfo := inf.ToIntermediateAbsInfoField() - //@ unfold slices.Bytes(b, 0, InfoLen) + //@ ghost targetAbsInfo := inf.ToAbsInfoField() + //@ unfold slices.Bytes(b, 0, len(b)) b[0] = 0 if inf.ConsDir { b[0] |= 0x1 } - //@ ghost tmpInfo1 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen) + //@ ghost tmpInfo1 := BytesToAbsInfoFieldHelper(b, 0) //@ bits.InfoFieldFirstByteSerializationLemmas() //@ assert tmpInfo1.ConsDir == targetAbsInfo.ConsDir //@ ghost firstByte := b[0] if inf.Peer { b[0] |= 0x2 } - //@ tmpInfo2 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen) + //@ tmpInfo2 := BytesToAbsInfoFieldHelper(b, 0) //@ assert tmpInfo2.Peer == (b[0] & 0x2 == 0x2) //@ assert tmpInfo2.ConsDir == (b[0] & 0x1 == 0x1) //@ assert tmpInfo2.Peer == targetAbsInfo.Peer @@ -119,14 +121,16 @@ func (inf *InfoField) SerializeTo(b []byte) (err error) { b[1] = 0 // reserved //@ assert &b[2:4][0] == &b[2] && &b[2:4][1] == &b[3] binary.BigEndian.PutUint16(b[2:4], inf.SegID) - //@ ghost tmpInfo3 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen) + //@ ghost tmpInfo3 := BytesToAbsInfoFieldHelper(b, 0) //@ assert tmpInfo3.UInfo == targetAbsInfo.UInfo //@ assert &b[4:8][0] == &b[4] && &b[4:8][1] == &b[5] //@ assert &b[4:8][2] == &b[6] && &b[4:8][3] == &b[7] binary.BigEndian.PutUint32(b[4:8], inf.Timestamp) - //@ ghost tmpInfo4 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen) + //@ ghost tmpInfo4 := BytesToAbsInfoFieldHelper(b, 0) //@ assert tmpInfo4.AInfo == targetAbsInfo.AInfo - //@ fold slices.Bytes(b, 0, InfoLen) + //@ fold slices.Bytes(b, 0, len(b)) + //@ assert inf.ToAbsInfoField() == + //@ reveal BytesToAbsInfoField(b, 0) return nil } diff --git a/pkg/slayers/path/infofield_spec.gobra b/pkg/slayers/path/infofield_spec.gobra index 3b52222d2..da554ab37 100644 --- a/pkg/slayers/path/infofield_spec.gobra +++ b/pkg/slayers/path/infofield_spec.gobra @@ -75,39 +75,29 @@ pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm] AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2])) } -// This type simplifies the infoField, making it easier -// to use than the IO_seg3 from the IO-spec. -type IntermediateAbsInfoField adt { - IntermediateAbsInfoField_ { - AInfo io.IO_ainfo - UInfo set[io.IO_msgterm] - ConsDir bool - Peer bool - } -} - ghost -requires 0 <= start && start <= middle -requires middle+InfoLen <= end && end <= len(raw) -requires acc(sl.Bytes(raw, start, end), _) +opaque +requires 0 <= middle +requires middle+InfoLen <= len(raw) +requires acc(sl.Bytes(raw, 0, len(raw)), _) decreases -pure func BytesToIntermediateAbsInfoField(raw [] byte, start int, middle int, end int) (IntermediateAbsInfoField) { - return unfolding acc(sl.Bytes(raw, start, end), _) in - BytesToIntermediateAbsInfoFieldHelper(raw, middle, end) +pure func BytesToAbsInfoField(raw [] byte, middle int) (io.AbsInfoField) { + return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in + BytesToAbsInfoFieldHelper(raw, middle) } ghost requires 0 <= middle -requires middle+InfoLen <= end && end <= len(raw) -requires forall i int :: { &raw[i] } middle <= i && i < end ==> +requires middle+InfoLen <= len(raw) +requires forall i int :: { &raw[i] } middle <= i && i < len(raw) ==> acc(&raw[i], _) decreases -pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int) (IntermediateAbsInfoField) { +pure func BytesToAbsInfoFieldHelper(raw [] byte, middle int) (io.AbsInfoField) { return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in - IntermediateAbsInfoField(IntermediateAbsInfoField_{ + io.AbsInfoField(io.AbsInfoField_{ AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])), UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])), ConsDir : raw[middle] & 0x1 == 0x1, @@ -117,8 +107,8 @@ pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int ghost decreases -pure func (inf InfoField) ToIntermediateAbsInfoField() (IntermediateAbsInfoField) { - return IntermediateAbsInfoField(IntermediateAbsInfoField_{ +pure func (inf InfoField) ToAbsInfoField() (io.AbsInfoField) { + return io.AbsInfoField(io.AbsInfoField_{ AInfo : io.IO_ainfo(inf.Timestamp), UInfo : AbsUInfoFromUint16(inf.SegID), ConsDir : inf.ConsDir, diff --git a/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra new file mode 100644 index 000000000..2ec25d54a --- /dev/null +++ b/pkg/slayers/path/scion/info_hop_setter_lemmas.gobra @@ -0,0 +1,546 @@ +// Copyright 2022 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package scion + +import ( + "github.com/scionproto/scion/pkg/slayers/path" + . "verification/utils/definitions" + sl "verification/utils/slices" + "verification/io" +) + +/*** This file contains helpful lemmas for proving SetInfoField and SetHopfield. ***/ +// Our abstract translation functions (CurrSeg, LeftSeg, RightSeg, MidSeg) are defined based on the +// entire byte slice of the concrete packet. This approach makes proving updates to the bytes very difficult. +// In this file, we introduce new translation functions that rely only on the hopfields byte slice and +// the infofield of a segment. We prove that these new functions are equivalent to the original ones +// and can be translated to each other. With these new functions, the proofs for SetInfoField and SetHopfield +// are greatly simplified. + + +// InfofieldByteSlice returns the byte slice of the infofield corresponding to the +// specified currInfIdx argument. Although a packet can have only three infofields, +// we use currInfIdx == 4 to represent the first infofield in our translation from +// concrete packets to abstract packets. This requires the special case that +// currInfIdx == 4 returns the same as currInfIdx == 0. +ghost +requires 0 <= currInfIdx +requires path.InfoFieldOffset(currInfIdx, MetaLen) + path.InfoLen <= len(raw) +decreases +pure func InfofieldByteSlice(raw []byte, currInfIdx int) ([]byte) { + return let infOffset := currInfIdx == 4 ? + path.InfoFieldOffset(0, MetaLen) : + path.InfoFieldOffset(currInfIdx, MetaLen) in + raw[infOffset:infOffset+path.InfoLen] +} + +// HopfieldsStartIdx returns index of the first byte of the hopfields of a segment +// specified by the currInfIdx argument. Although a packet can have only three segments, +// we use currInfIdx == 4 to represent the first segment in our translation from +// concrete packets to abstract packets. This requires the special case that +// currInfIdx == 4 returns the same as currInfIdx == 0. +ghost +requires s.Valid() +requires 0 <= currInfIdx +decreases +pure func HopfieldsStartIdx(currInfIdx int, s io.SegLens) int { + return let numInf := s.NumInfoFields() in + let infOffset := path.InfoFieldOffset(numInf, MetaLen) in + (currInfIdx == 0 || currInfIdx == 4) ? infOffset : + currInfIdx == 1 ? infOffset+s.Seg1Len*path.HopLen : + infOffset+(s.Seg1Len+s.Seg2Len)*path.HopLen +} + +// HopfieldsStartIdx returns index of the last byte of the hopfields of a segment +// specified by the currInfIdx argument. Although a packet can have only three segments, +// we use currInfIdx == 4 to represent the first segment in our translation from +// concrete packets to abstract packets. This requires the special case that +// currInfIdx == 4 returns the same as currInfIdx == 0. +ghost +requires s.Valid() +requires 0 <= currInfIdx +decreases +pure func HopfieldsEndIdx(currInfIdx int, s io.SegLens) int { + return let numInf := s.NumInfoFields() in + let infOffset := path.InfoFieldOffset(numInf, MetaLen) in + (currInfIdx == 0 || currInfIdx == 4) ? infOffset+s.Seg1Len*path.HopLen : + currInfIdx == 1 ? infOffset+(s.Seg1Len+s.Seg2Len)*path.HopLen : + infOffset+(s.Seg1Len+s.Seg2Len+s.Seg3Len)*path.HopLen +} + +// HopfieldsStartIdx returns returns the byte slice of the hopfields of a segment +// specified by the currInfIdx argument. Although a packet can have only three segments, +// we use currInfIdx == 4 to represent the first segment in our translation from +// concrete packets to abstract packets. This requires the special case that +// currInfIdx == 4 returns the same as currInfIdx == 0. +ghost +requires s.Valid() +requires 0 <= currInfIdx +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +decreases +pure func HopfieldsByteSlice(raw []byte, currInfIdx int, s io.SegLens) ([]byte) { + return let numInf := s.NumInfoFields() in + let infOffset := path.InfoFieldOffset(numInf, MetaLen) in + let start := HopfieldsStartIdx(currInfIdx, s) in + let end := HopfieldsEndIdx(currInfIdx, s) in + raw[start:end] +} + +// SliceBytesIntoSegments splits the raw bytes of a packet into its hopfield segments +ghost +requires 0 < p +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires acc(sl.Bytes(raw, 0, len(raw)), p) +ensures acc(sl.Bytes(raw[:HopfieldsStartIdx(0, s)], 0, HopfieldsStartIdx(0, s)), p) +ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 0, s), 0, s.Seg1Len*path.HopLen), p) +ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 1, s), 0, s.Seg2Len*path.HopLen), p) +ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 2, s), 0, s.Seg3Len*path.HopLen), p) +ensures acc(sl.Bytes(raw[HopfieldsEndIdx(2, s):], 0, len(raw[HopfieldsEndIdx(2, s):])), p) +decreases +func SliceBytesIntoSegments(raw []byte, s io.SegLens, p perm) { + sl.SplitByIndex_Bytes(raw, 0, len(raw), HopfieldsStartIdx(0, s), p) + sl.SplitByIndex_Bytes(raw, HopfieldsStartIdx(0, s), len(raw), HopfieldsEndIdx(0, s), p) + sl.SplitByIndex_Bytes(raw, HopfieldsStartIdx(1, s), len(raw), HopfieldsEndIdx(1, s), p) + sl.SplitByIndex_Bytes(raw, HopfieldsStartIdx(2, s), len(raw), HopfieldsEndIdx(2, s), p) + sl.Reslice_Bytes(raw, 0, HopfieldsStartIdx(0, s), p) + sl.Reslice_Bytes(raw, HopfieldsStartIdx(0, s), HopfieldsEndIdx(0, s), p) + sl.Reslice_Bytes(raw, HopfieldsStartIdx(1, s), HopfieldsEndIdx(1, s), p) + sl.Reslice_Bytes(raw, HopfieldsStartIdx(2, s), HopfieldsEndIdx(2, s), p) + sl.Reslice_Bytes(raw, HopfieldsEndIdx(2, s), len(raw), p) +} + +// CombineBytesFromSegments combines the three hopfield segments of a packet into a single slice of bytes. +ghost +requires 0 < p +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires acc(sl.Bytes(raw[:HopfieldsStartIdx(0, s)], 0, HopfieldsStartIdx(0, s)), p) +requires acc(sl.Bytes(HopfieldsByteSlice(raw, 0, s), 0, s.Seg1Len*path.HopLen), p) +requires acc(sl.Bytes(HopfieldsByteSlice(raw, 1, s), 0, s.Seg2Len*path.HopLen), p) +requires acc(sl.Bytes(HopfieldsByteSlice(raw, 2, s), 0, s.Seg3Len*path.HopLen), p) +requires acc(sl.Bytes(raw[HopfieldsEndIdx(2, s):], 0, len(raw[HopfieldsEndIdx(2, s):])), p) +ensures acc(sl.Bytes(raw, 0, len(raw)), p) +decreases +func CombineBytesFromSegments(raw []byte, s io.SegLens, p perm) { + sl.Unslice_Bytes(raw, HopfieldsEndIdx(2, s), len(raw), p) + sl.Unslice_Bytes(raw, HopfieldsStartIdx(2, s), HopfieldsEndIdx(2, s), p) + sl.Unslice_Bytes(raw, HopfieldsStartIdx(1, s), HopfieldsEndIdx(1, s), p) + sl.Unslice_Bytes(raw, HopfieldsStartIdx(0, s), HopfieldsEndIdx(0, s), p) + sl.Unslice_Bytes(raw, 0, HopfieldsStartIdx(0, s), p) + sl.CombineAtIndex_Bytes(raw, HopfieldsStartIdx(2, s), len(raw), HopfieldsEndIdx(2, s), p) + sl.CombineAtIndex_Bytes(raw, HopfieldsStartIdx(1, s), len(raw), HopfieldsEndIdx(1, s), p) + sl.CombineAtIndex_Bytes(raw, HopfieldsStartIdx(0, s), len(raw), HopfieldsEndIdx(0, s), p) + sl.CombineAtIndex_Bytes(raw, 0, len(raw), HopfieldsStartIdx(0, s), p) +} + +// SliceBytesIntoInfoFields splits the raw bytes of a packet into its infofields +ghost +requires 0 < p +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires numInf == s.NumInfoFields() +requires acc(sl.Bytes(raw, 0, len(raw)), p) +ensures acc(sl.Bytes(raw[:MetaLen], 0, MetaLen), p) +ensures acc(sl.Bytes(InfofieldByteSlice(raw, 0), 0, path.InfoLen), p) +ensures 1 < numInf ==> acc(sl.Bytes(InfofieldByteSlice(raw, 1), 0, path.InfoLen), p) +ensures 2 < numInf ==> acc(sl.Bytes(InfofieldByteSlice(raw, 2), 0, path.InfoLen), p) +ensures acc(sl.Bytes(raw[HopfieldsStartIdx(0, s):], 0, len(raw[HopfieldsStartIdx(0, s):])), p) +decreases +func SliceBytesIntoInfoFields(raw []byte, numInf int, s io.SegLens, p perm) { + sl.SplitByIndex_Bytes(raw, 0, len(raw), MetaLen, p) + sl.SplitByIndex_Bytes(raw, MetaLen, len(raw), path.InfoFieldOffset(1, MetaLen), p) + sl.Reslice_Bytes(raw, 0, MetaLen, p) + sl.Reslice_Bytes(raw, MetaLen, path.InfoFieldOffset(1, MetaLen), p) + if(numInf > 1) { + sl.SplitByIndex_Bytes(raw, path.InfoFieldOffset(1, MetaLen), len(raw), + path.InfoFieldOffset(2, MetaLen), p) + sl.Reslice_Bytes(raw, path.InfoFieldOffset(1, MetaLen), + path.InfoFieldOffset(2, MetaLen), p) + } + if(numInf > 2) { + sl.SplitByIndex_Bytes(raw, path.InfoFieldOffset(2, MetaLen), len(raw), + HopfieldsStartIdx(0, s), p) + sl.Reslice_Bytes(raw, path.InfoFieldOffset(2, MetaLen), HopfieldsStartIdx(0, s), p) + } + sl.Reslice_Bytes(raw, HopfieldsStartIdx(0, s), len(raw), p) +} + +// CombineBytesFromInfoFields combines the infofields of a packet into a single slice of bytes. +ghost +requires 0 < p +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires numInf == s.NumInfoFields() +requires acc(sl.Bytes(raw[:MetaLen], 0, MetaLen), p) +requires acc(sl.Bytes(InfofieldByteSlice(raw, 0), 0, path.InfoLen), p) +requires 1 < numInf ==> acc(sl.Bytes(InfofieldByteSlice(raw, 1), 0, path.InfoLen), p) +requires 2 < numInf ==> acc(sl.Bytes(InfofieldByteSlice(raw, 2), 0, path.InfoLen), p) +requires acc(sl.Bytes(raw[HopfieldsStartIdx(0, s):], 0, len(raw[HopfieldsStartIdx(0, s):])), p) +ensures acc(sl.Bytes(raw, 0, len(raw)), p) +decreases +func CombineBytesFromInfoFields(raw []byte, numInf int, s io.SegLens, p perm) { + sl.Unslice_Bytes(raw, HopfieldsStartIdx(0, s), len(raw), p) + if(numInf > 2) { + sl.Unslice_Bytes(raw, path.InfoFieldOffset(2, MetaLen), HopfieldsStartIdx(0, s), p) + sl.CombineAtIndex_Bytes(raw, path.InfoFieldOffset(2, MetaLen), len(raw), + HopfieldsStartIdx(0, s), p) + } + if(numInf > 1) { + sl.Unslice_Bytes(raw, path.InfoFieldOffset(1, MetaLen), + path.InfoFieldOffset(2, MetaLen), p) + sl.CombineAtIndex_Bytes(raw, path.InfoFieldOffset(1, MetaLen), len(raw), + path.InfoFieldOffset(2, MetaLen), p) + } + sl.Unslice_Bytes(raw, MetaLen, path.InfoFieldOffset(1, MetaLen), p) + sl.Unslice_Bytes(raw, 0, MetaLen, p) + sl.CombineAtIndex_Bytes(raw, MetaLen, len(raw), path.InfoFieldOffset(1, MetaLen), p) + sl.CombineAtIndex_Bytes(raw, 0, len(raw), MetaLen, p) +} + +// CurrSegWithInfo returns the abstract representation of the current segment of a packet. +// Unlike CurrSeg, it relies solely on the hopfield byte slice and an infofield instead of +// the entire raw bytes of the packet. This approach simplifies the verification of changes +// within a segment after updates to the packet's raw bytes. +ghost +opaque +requires 0 < SegLen +requires 0 <= currHfIdx && currHfIdx <= SegLen +requires SegLen*path.HopLen == len(hopfields) +requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R56) +decreases +pure func CurrSegWithInfo(hopfields []byte, currHfIdx int, SegLen int, inf io.AbsInfoField) io.IO_seg3 { + return segment(hopfields, 0, currHfIdx, inf.AInfo, inf.UInfo, inf.ConsDir, inf.Peer, SegLen) +} + + +// LeftSegWithInfo returns the abstract representation of the next segment of a packet. +// Unlike LeftSeg, it relies solely on the hopfields byte slice and an infofield instead of +// the entire bytes of the packet. Whenever the return value is not none, LeftSegWithInfo +// requires permissions to the hopfields byte slice of the segment specified by currInfIdx. +ghost +opaque +requires s.Valid() +requires (currInfIdx == 1 && s.Seg2Len > 0) || + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) ==> + let start := HopfieldsStartIdx(currInfIdx, s) in + let end := HopfieldsEndIdx(currInfIdx, s) in + inf != none[io.AbsInfoField] && + len(hopfields) == end-start && + acc(sl.Bytes(hopfields, 0, len(hopfields)), R49) +decreases +pure func LeftSegWithInfo( + hopfields []byte, + currInfIdx int, + s io.SegLens, + inf option[io.AbsInfoField]) option[io.IO_seg3] { + return (currInfIdx == 1 && s.Seg2Len > 0) ? + some(CurrSegWithInfo(hopfields, 0, s.Seg2Len, get(inf))) : + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) ? + some(CurrSegWithInfo(hopfields, 0, s.Seg3Len, get(inf))) : + none[io.IO_seg3] +} + +// RightSegWithInfo returns the abstract representation of the previous segment of a packet. +// Unlike RightSeg, it relies solely on the hopfields byte slice and an infofield instead of +// the entire bytes of the packet. Whenever the return value is not none, RightSegWithInfo +// requires permissions to the hopfields byte slice of the segment specified by currInfIdx. +ghost +opaque +requires s.Valid() +requires (currInfIdx == 0 && s.Seg2Len > 0) || + (currInfIdx == 1 && s.Seg2Len > 0 && s.Seg3Len > 0) ==> + let start := HopfieldsStartIdx(currInfIdx, s) in + let end := HopfieldsEndIdx(currInfIdx, s) in + inf != none[io.AbsInfoField] && + len(hopfields) == end-start && + acc(sl.Bytes(hopfields, 0, len(hopfields)), R49) +decreases +pure func RightSegWithInfo( + hopfields []byte, + currInfIdx int, + s io.SegLens, + inf option[io.AbsInfoField]) option[io.IO_seg3] { + return (currInfIdx == 1 && s.Seg2Len > 0 && s.Seg3Len > 0) ? + some(CurrSegWithInfo(hopfields, s.Seg2Len, s.Seg2Len, get(inf))) : + (currInfIdx == 0 && s.Seg2Len > 0) ? + some(CurrSegWithInfo(hopfields, s.Seg1Len, s.Seg1Len, get(inf))) : + none[io.IO_seg3] +} + +// MidSegWithInfo returns the abstract representation of the last or first segment of a packet. +// Unlike MidSeg, it relies solely on the hopfields byte slice and an infofield instead of +// the entire bytes of the packet. Whenever the return value is not none, MidSegWithInfo +// requires permissions to the hopfields byte slice of the segment specified by currInfIdx. +ghost +opaque +requires s.Valid() +requires (s.Seg2Len > 0 && s.Seg3Len > 0 && + (currInfIdx == 2 || currInfIdx == 4)) ==> + let start := HopfieldsStartIdx(currInfIdx, s) in + let end := HopfieldsEndIdx(currInfIdx, s) in + inf != none[io.AbsInfoField] && + len(hopfields) == end-start && + acc(sl.Bytes(hopfields, 0, len(hopfields)), R49) +decreases +pure func MidSegWithInfo( + hopfields []byte, + currInfIdx int, + s io.SegLens, + inf option[io.AbsInfoField]) option[io.IO_seg3] { + return (currInfIdx == 4 && s.Seg2Len > 0 && s.Seg3Len > 0) ? + some(CurrSegWithInfo(hopfields, s.Seg1Len, s.Seg1Len, get(inf))) : + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) ? + some(CurrSegWithInfo(hopfields, 0, s.Seg3Len, get(inf))) : + none[io.IO_seg3] +} + +// CurrSegEquality ensures that the two definitions of abstract segments, CurrSegWithInfo(..) +// and CurrSeg(..), represent the same abstract segment. +ghost +requires path.InfoFieldOffset(currInfIdx, MetaLen) + path.InfoLen <= offset +requires 0 < SegLen +requires offset + path.HopLen * SegLen <= len(raw) +requires 0 <= currHfIdx && currHfIdx <= SegLen +requires 0 <= currInfIdx && currInfIdx < 3 +preserves acc(sl.Bytes(raw, 0, len(raw)), R50) +preserves acc(sl.Bytes(raw[offset:offset+SegLen*path.HopLen], 0, SegLen*path.HopLen), R50) +preserves acc(sl.Bytes(InfofieldByteSlice(raw, currInfIdx), 0, path.InfoLen), R50) +ensures let inf := path.BytesToAbsInfoField(InfofieldByteSlice(raw, currInfIdx), 0) in + CurrSegWithInfo(raw[offset:offset+SegLen*path.HopLen], currHfIdx, SegLen, inf) == + CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen) +decreases +func CurrSegEquality(raw []byte, offset int, currInfIdx int, currHfIdx int, SegLen int) { + infoBytes := InfofieldByteSlice(raw, currInfIdx) + inf := path.BytesToAbsInfoField(infoBytes, 0) + infOffset := path.InfoFieldOffset(currInfIdx, MetaLen) + unfold acc(sl.Bytes(raw, 0, len(raw)), R56) + unfold acc(sl.Bytes(infoBytes, 0, path.InfoLen), R56) + assert reveal path.BytesToAbsInfoField(raw, infOffset) == + reveal path.BytesToAbsInfoField(infoBytes, 0) + reveal CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen) + reveal CurrSegWithInfo(raw[offset:offset+SegLen*path.HopLen], currHfIdx, SegLen, inf) + fold acc(sl.Bytes(raw, 0, len(raw)), R56) + fold acc(sl.Bytes(infoBytes, 0, path.InfoLen), R56) + widenSegment(raw, offset, currHfIdx, inf.AInfo, inf.UInfo, inf.ConsDir, + inf.Peer, SegLen, offset, offset+SegLen*path.HopLen) +} + +// UpdateCurrSegInfo proves that updating the infofield from inf1 to inf2 does not alter the hopfields +// of the current segment. +ghost +requires 0 < SegLen +requires 0 <= currHfIdx && currHfIdx <= SegLen +requires SegLen*path.HopLen == len(raw) +preserves acc(sl.Bytes(raw, 0, len(raw)), R50) +ensures CurrSegWithInfo(raw, currHfIdx, SegLen, inf1).UpdateCurrSeg(inf2) == + CurrSegWithInfo(raw, currHfIdx, SegLen, inf2) +decreases +func UpdateCurrSegInfo(raw []byte, currHfIdx int, SegLen int, + inf1 io.AbsInfoField, inf2 io.AbsInfoField) { + seg1 := reveal CurrSegWithInfo(raw, currHfIdx, SegLen, inf1) + seg2 := reveal CurrSegWithInfo(raw, currHfIdx, SegLen, inf2) +} + + +// LeftSegEqualitySpec defines the conditions that must hold for LeftSegWithInfo(..) +// and LeftSeg(..) to represent the same abstract segment. +ghost +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires 1 <= currInfIdx && currInfIdx < 4 +requires acc(sl.Bytes(raw, 0, len(raw)), R49) +requires (currInfIdx == 1 && s.Seg2Len > 0) || + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) ==> + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && + acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) +decreases +pure func LeftSegEqualitySpec(raw []byte, currInfIdx int, s io.SegLens) bool { + return (currInfIdx == 1 && s.Seg2Len > 0) || + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) ? + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + let inf := some(path.BytesToAbsInfoField(infoBytes, 0)) in + LeftSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) == + LeftSegWithInfo(hopBytes, currInfIdx, s, inf) : + LeftSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) == + LeftSegWithInfo(nil, currInfIdx, s, none[io.AbsInfoField]) +} + +// LeftSegEquality ensures that the two definitions of abstract segments, LeftSegWithInfo(..) +// and LeftSeg(..), represent the same abstract segment. +// The left segment corresponds to different segments of the packet depending on the currInfIdx. +// To address this, we need to consider all possible cases of currInfIdx. This results in fairly +// complex preconditions and postconditions because, for every currInfIdx, we need an offset for +// its infofield and one for its hopfields. +ghost +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires 1 <= currInfIdx && currInfIdx < 4 +preserves acc(sl.Bytes(raw, 0, len(raw)), R49) +preserves (currInfIdx == 1 && s.Seg2Len > 0) || + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) ==> + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && + acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) +ensures LeftSegEqualitySpec(raw, currInfIdx, s) +decreases +func LeftSegEquality(raw []byte, currInfIdx int, s io.SegLens) { + reveal LeftSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) + if ((currInfIdx == 1 && s.Seg2Len > 0) || + (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0)) { + infoBytes := InfofieldByteSlice(raw, currInfIdx) + hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) + inf := some(reveal path.BytesToAbsInfoField(infoBytes, 0)) + offset := HopfieldsStartIdx(currInfIdx, s) + segLen := currInfIdx == 1 ? s.Seg2Len : s.Seg3Len + reveal LeftSegWithInfo(hopBytes, currInfIdx, s, inf) + CurrSegEquality(raw, offset, currInfIdx, 0, segLen) + } else { + reveal LeftSegWithInfo(nil, currInfIdx, s, none[io.AbsInfoField]) + } +} + +// RightSegEqualitySpec defines the conditions that must hold for RightSegWithInfo(..) +// and RightSeg(..) to represent the same abstract segment. +ghost +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires -1 <= currInfIdx && currInfIdx < 2 +requires acc(sl.Bytes(raw, 0, len(raw)), R49) +requires (currInfIdx == 0 && s.Seg2Len > 0) || + (currInfIdx == 1 && s.Seg2Len > 0 && s.Seg3Len > 0) ==> + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && + acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) +decreases +pure func RightSegEqualitySpec(raw []byte, currInfIdx int, s io.SegLens) bool { + return (currInfIdx == 0 && s.Seg2Len > 0) || + (currInfIdx == 1 && s.Seg2Len > 0 && s.Seg3Len > 0) ? + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + let inf := some(path.BytesToAbsInfoField(infoBytes, 0)) in + RightSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) == + RightSegWithInfo(hopBytes, currInfIdx, s, inf) : + RightSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) == + RightSegWithInfo(nil, currInfIdx, s, none[io.AbsInfoField]) +} + +// RightSegEquality ensures that the two definitions of abstract segments, RightSegWithInfo(..) +// and RightSeg(..), represent the same abstract segment. +// The right segment corresponds to different segments of the packet depending on the currInfIdx. +// To address this, we need to consider all possible cases of currInfIdx. This results in fairly +// complex preconditions and postconditions because, for every currInfIdx, we need an offset for +// its infofield and one for its hopfields. +ghost +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires -1 <= currInfIdx && currInfIdx < 2 +preserves acc(sl.Bytes(raw, 0, len(raw)), R49) +preserves (currInfIdx == 0 && s.Seg2Len > 0) || + (currInfIdx == 1 && s.Seg2Len > 0 && s.Seg3Len > 0) ==> + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && + acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) +ensures RightSegEqualitySpec(raw, currInfIdx, s) +decreases +func RightSegEquality(raw []byte, currInfIdx int, s io.SegLens) { + reveal RightSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) + if ((currInfIdx == 0 && s.Seg2Len > 0) || + (currInfIdx == 1 && s.Seg2Len > 0 && s.Seg3Len > 0)) { + infoBytes := InfofieldByteSlice(raw, currInfIdx) + hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) + inf := some(reveal path.BytesToAbsInfoField(infoBytes, 0)) + offset := HopfieldsStartIdx(currInfIdx, s) + segLen := currInfIdx == 0 ? s.Seg1Len : s.Seg2Len + reveal RightSegWithInfo(hopBytes, currInfIdx, s, inf) + CurrSegEquality(raw, offset, currInfIdx, segLen, segLen) + } else { + reveal RightSegWithInfo(nil, currInfIdx, s, none[io.AbsInfoField]) + } +} + +// MidSegEqualitySpec defines the conditions that must hold for MidSegWithInfo(..) +// and MidSeg(..) to represent the same abstract segment. +ghost +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires 2 <= currInfIdx && currInfIdx < 5 +requires acc(sl.Bytes(raw, 0, len(raw)), R49) +requires (s.Seg2Len > 0 && s.Seg3Len > 0 && + (currInfIdx == 2 || currInfIdx == 4)) ==> + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && + acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) +decreases +pure func MidSegEqualitySpec(raw []byte, currInfIdx int, s io.SegLens) bool { + return (s.Seg2Len > 0 && s.Seg3Len > 0 && + (currInfIdx == 2 || currInfIdx == 4)) ? + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + let inf := some(path.BytesToAbsInfoField(infoBytes, 0)) in + MidSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) == + MidSegWithInfo(hopBytes, currInfIdx, s, inf) : + MidSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) == + MidSegWithInfo(nil, currInfIdx, s, none[io.AbsInfoField]) +} + +// MidSegEquality ensures that the two definitions of abstract segments, MidSegWithInfo(..) +// and MidSeg(..), represent the same abstract segment. +// The mid segment corresponds to different segments of the packet depending on the currInfIdx. +// To address this, we need to consider all possible cases of currInfIdx. This results in fairly +// complex preconditions and postconditions because, for every currInfIdx, we need an offset for +// its infofield and one for its hopfields. +ghost +requires s.Valid() +requires pktLen(s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) <= len(raw) +requires 2 <= currInfIdx && currInfIdx < 5 +preserves acc(sl.Bytes(raw, 0, len(raw)), R49) +preserves (s.Seg2Len > 0 && s.Seg3Len > 0 && + (currInfIdx == 2 || currInfIdx == 4)) ==> + let infoBytes := InfofieldByteSlice(raw, currInfIdx) in + let hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) in + acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) && + acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49) +ensures MidSegEqualitySpec(raw, currInfIdx, s) +decreases +func MidSegEquality(raw []byte, currInfIdx int, s io.SegLens) { + reveal MidSeg(raw, currInfIdx, s.Seg1Len, s.Seg2Len, s.Seg3Len, MetaLen) + if (currInfIdx == 4 && s.Seg2Len > 0 && s.Seg3Len > 0) { + infoBytes := InfofieldByteSlice(raw, 0) + hopBytes := HopfieldsByteSlice(raw, 0, s) + inf := some(reveal path.BytesToAbsInfoField(infoBytes, 0)) + offset := HopfieldsStartIdx(currInfIdx, s) + reveal MidSegWithInfo(hopBytes, currInfIdx, s, inf) + CurrSegEquality(raw, offset, 0, s.Seg1Len, s.Seg1Len) + } else if (currInfIdx == 2 && s.Seg2Len > 0 && s.Seg3Len > 0) { + infoBytes := InfofieldByteSlice(raw, currInfIdx) + hopBytes := HopfieldsByteSlice(raw, currInfIdx, s) + inf := some(reveal path.BytesToAbsInfoField(infoBytes, 0)) + offset := HopfieldsStartIdx(currInfIdx, s) + reveal MidSegWithInfo(hopBytes, currInfIdx, s, inf) + CurrSegEquality(raw, offset, currInfIdx, 0, s.Seg3Len) + } else { + reveal MidSegWithInfo(nil, currInfIdx, s, none[io.AbsInfoField]) + } +} \ No newline at end of file diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go index c2ace96b6..8490963f4 100644 --- a/pkg/slayers/path/scion/raw.go +++ b/pkg/slayers/path/scion/raw.go @@ -252,7 +252,7 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) { //@ oldSeg3Len := int(s.PathMeta.SegLen[2]) //@ oldSegLen := LengthOfCurrSeg(oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len) //@ oldPrevSegLen := LengthOfPrevSeg(oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len) - //@ oldOffset := HopFieldOffset(s.Base.NumINF, 0, 0) + //@ oldOffset := HopFieldOffset(s.Base.NumINF, oldPrevSegLen, 0) //@ fold acc(s.Base.Mem(), R56) if err := s.Base.IncPath(); err != nil { //@ fold s.NonInitMem() @@ -264,14 +264,13 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) { //@ sl.Reslice_Bytes(ubuf, MetaLen, len(ubuf), HalfPerm) //@ tail := ubuf[MetaLen:] //@ unfold acc(sl.Bytes(tail, 0, len(tail)), R50) - //@ oldoffsetWithHops := oldOffset + path.HopLen * oldPrevSegLen //@ oldHfIdxSeg := oldCurrHfIdx-oldPrevSegLen - //@ WidenCurrSeg(ubuf, oldoffsetWithHops + MetaLen, oldCurrInfIdx, oldHfIdxSeg, + //@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg, //@ oldSegLen, MetaLen, MetaLen, len(ubuf)) //@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf)) //@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf)) //@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf)) - //@ LenCurrSeg(tail, oldoffsetWithHops, oldCurrInfIdx, oldHfIdxSeg, oldSegLen) + //@ LenCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen) //@ oldAbsPkt := reveal s.absPkt(ubuf) //@ sl.SplitRange_Bytes(ubuf, 0, MetaLen, HalfPerm) //@ unfold acc(s.Base.Mem(), R2) @@ -295,8 +294,8 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) { //@ assert currHfIdx == oldCurrHfIdx + 1 //@ ghost if(currInfIdx == oldCurrInfIdx) { - //@ IncCurrSeg(tail, oldoffsetWithHops, oldCurrInfIdx, oldHfIdxSeg, oldSegLen) - //@ WidenCurrSeg(ubuf, oldoffsetWithHops + MetaLen, oldCurrInfIdx, oldHfIdxSeg + 1, + //@ IncCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen) + //@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg + 1, //@ oldSegLen, MetaLen, MetaLen, len(ubuf)) //@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf)) //@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf)) @@ -305,7 +304,7 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) { //@ } else { //@ segLen := LengthOfCurrSeg(currHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len) //@ prevSegLen := LengthOfPrevSeg(currHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len) - //@ offsetWithHops := oldOffset + path.HopLen * prevSegLen + MetaLen + //@ offsetWithHops := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen) //@ hfIdxSeg := currHfIdx-prevSegLen //@ XoverSegNotNone(tail, oldCurrInfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len) //@ XoverCurrSeg(tail, oldCurrInfIdx + 1, oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len) @@ -355,8 +354,10 @@ func (s *Raw) GetInfoField(idx int /*@, ghost ubuf []byte @*/) (ifield path.Info //@ sl.CombineRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, R21) //@ unfold acc(sl.Bytes(ubuf, 0, len(ubuf)), R56) //@ unfold acc(sl.Bytes(ubuf[infOffset : infOffset+path.InfoLen], 0, path.InfoLen), R56) - //@ assert info.ToIntermediateAbsInfoField() == - //@ path.BytesToIntermediateAbsInfoField(ubuf, 0, infOffset, len(ubuf)) + //@ assert reveal path.BytesToAbsInfoField(ubuf, infOffset) == + //@ reveal path.BytesToAbsInfoField(ubuf[infOffset : infOffset+path.InfoLen], 0) + //@ assert info.ToAbsInfoField() == + //@ reveal path.BytesToAbsInfoField(ubuf, infOffset) //@ fold acc(sl.Bytes(ubuf, 0, len(ubuf)), R56) //@ fold acc(sl.Bytes(ubuf[infOffset : infOffset+path.InfoLen], 0, path.InfoLen), R56) //@ sl.CombineRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, R21) @@ -397,18 +398,29 @@ func (s *Raw) GetCurrentInfoField( /*@ ghost ubuf []byte @*/ ) (res path.InfoFie // @ ensures sl.Bytes(ubuf, 0, len(ubuf)) // @ ensures r != nil ==> r.ErrorMem() // posts for IO: -// @ ensures r == nil && idx == int(old(s.GetCurrINF(ubuf))) ==> +// @ ensures r == nil ==> // @ validPktMetaHdr(ubuf) && s.EqAbsHeader(ubuf) // @ ensures r == nil && idx == int(old(s.GetCurrINF(ubuf))) ==> // @ let oldPkt := old(s.absPkt(ubuf)) in -// @ let newPkt := AbsSetInfoField(oldPkt, info.ToIntermediateAbsInfoField()) in +// @ let newPkt := oldPkt.UpdateInfoField(info.ToAbsInfoField()) in // @ s.absPkt(ubuf) == newPkt // @ decreases +// @ #backend[exhaleMode(1)] func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @*/) (r error) { //@ share info - //@ ghost oldCurrINF := int(old(s.GetCurrINF(ubuf))) + //@ reveal validPktMetaHdr(ubuf) //@ unfold acc(s.Mem(ubuf), R50) //@ unfold acc(s.Base.Mem(), R50) + //@ currInfIdx := int(s.PathMeta.CurrINF) + //@ currHfIdx := int(s.PathMeta.CurrHF) + //@ seg1Len := int(s.PathMeta.SegLen[0]) + //@ seg2Len := int(s.PathMeta.SegLen[1]) + //@ seg3Len := int(s.PathMeta.SegLen[2]) + //@ segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) + //@ prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) + //@ offset := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen) + //@ hopfieldOffset := MetaLen + s.NumINF*path.InfoLen + //@ segLens := io.CombineSegLens(seg1Len, seg2Len, seg3Len) if idx >= s.NumINF { err := serrors.New("InfoField index out of bounds", "max", s.NumINF-1, "actual", idx) //@ fold acc(s.Base.Mem(), R50) @@ -416,35 +428,41 @@ func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @ return err } infOffset := MetaLen + idx*path.InfoLen - //@ assert idx == oldCurrINF ==> reveal validPktMetaHdr(ubuf) - //@ assert idx == oldCurrINF ==> s.EqAbsHeader(ubuf) - - //@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm) - //@ ValidPktMetaHdrSublice(ubuf, len(s.Raw)) - //@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm) - //@ assert idx == oldCurrINF ==> RawBytesToBase(ubuf[:len(s.Raw)]).ValidCurrIdxsSpec() - //@ assert sl.Bytes(s.Raw, 0, len(s.Raw)) - //@ sl.SplitRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm) - //@ assert acc(sl.Bytes(s.Raw, 0, infOffset), HalfPerm) - //@ sl.Reslice_Bytes(s.Raw, 0, infOffset, HalfPerm/2) - //@ ValidPktMetaHdrSublice(s.Raw, infOffset) - //@ sl.SplitRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm) - //@ assert idx == oldCurrINF ==> RawBytesToBase(s.Raw[:infOffset]).ValidCurrIdxsSpec() + //@ SliceBytesIntoInfoFields(ubuf, s.NumINF, segLens, HalfPerm) + //@ SliceBytesIntoSegments(ubuf, segLens, R40) + //@ ValidPktMetaHdrSublice(ubuf, MetaLen) + //@ oldInfo := path.BytesToAbsInfoField(ubuf[infOffset : infOffset+path.InfoLen], 0) + //@ newInfo := info.ToAbsInfoField() + //@ hfIdxSeg := currHfIdx-prevSegLen + //@ hopfields := ubuf[offset:offset + segLen*path.HopLen] + //@ ghost if idx == currInfIdx { + //@ CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen) + //@ LeftSegEquality(ubuf, currInfIdx+1, segLens) + //@ MidSegEquality(ubuf, currInfIdx+2, segLens) + //@ RightSegEquality(ubuf, currInfIdx-1, segLens) + //@ } + //@ reveal s.absPkt(ubuf) + //@ sl.SplitRange_Bytes(ubuf[:hopfieldOffset], infOffset, infOffset+path.InfoLen, R40) + //@ sl.SplitRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, HalfPerm-R40) ret := info.SerializeTo(s.Raw[infOffset : infOffset+path.InfoLen]) - //@ sl.CombineRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm) - //@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm) - //@ ValidPktMetaHdrSublice(ubuf, infOffset) - - //@ sl.Unslice_Bytes(s.Raw, 0, infOffset, HalfPerm/2) - //@ sl.CombineRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, HalfPerm) - //@ assert idx == oldCurrINF ==> RawBytesToBase(ubuf).ValidCurrIdxsSpec() - //@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), HalfPerm) + //@ sl.CombineRange_Bytes(ubuf[:hopfieldOffset], infOffset, infOffset+path.InfoLen, R40) + //@ sl.CombineRange_Bytes(ubuf, infOffset, infOffset+path.InfoLen, HalfPerm-R40) + //@ ValidPktMetaHdrSublice(ubuf, MetaLen) + //@ assert reveal validPktMetaHdr(ubuf) + //@ ghost if idx == currInfIdx { + //@ CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen) + //@ UpdateCurrSegInfo(hopfields, hfIdxSeg, segLen, oldInfo, newInfo) + //@ LeftSegEquality(ubuf, currInfIdx+1, segLens) + //@ MidSegEquality(ubuf, currInfIdx+2, segLens) + //@ RightSegEquality(ubuf, currInfIdx-1, segLens) + //@ reveal s.absPkt(ubuf) + //@ } + //@ CombineBytesFromSegments(ubuf, segLens, R40) + //@ CombineBytesFromInfoFields(ubuf, s.NumINF, segLens, HalfPerm) //@ fold acc(s.Base.Mem(), R50) //@ fold acc(s.Mem(ubuf), R50) - //@ assert idx == oldCurrINF ==> reveal validPktMetaHdr(ubuf) - //@ TemporaryAssumeForIO(idx == oldCurrINF ==> s.absPkt(ubuf) == AbsSetInfoField(old(s.absPkt(ubuf)), info.ToIntermediateAbsInfoField())) return ret } diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra index c17c5eb61..53914f8b5 100644 --- a/pkg/slayers/path/scion/raw_spec.gobra +++ b/pkg/slayers/path/scion/raw_spec.gobra @@ -452,7 +452,7 @@ pure func MidSeg( seg3Len int, headerOffset int) option[io.IO_seg3] { return let offset := HopFieldOffset(NumInfoFields(seg1Len, seg2Len, seg3Len), 0, headerOffset) in - (currInfIdx == 4 && seg2Len > 0) ? + (currInfIdx == 4 && seg2Len > 0 && seg3Len > 0) ? some(CurrSeg(raw, offset, 0, seg1Len, seg1Len, headerOffset)) : ((currInfIdx == 2 && seg2Len > 0 && seg3Len > 0) ? some(CurrSeg(raw, offset + path.HopLen * (seg1Len + seg2Len), currInfIdx, 0, seg3Len, headerOffset)) : @@ -475,17 +475,15 @@ pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) { let segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) in let prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) in let numINF := NumInfoFields(seg1Len, seg2Len, seg3Len) in - let offset := HopFieldOffset(numINF, 0, MetaLen) in + let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in io.IO_Packet2 { - CurrSeg : CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen), + CurrSeg : CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen), LeftSeg : LeftSeg(raw, currInfIdx + 1, seg1Len, seg2Len , seg3Len, MetaLen), MidSeg : MidSeg(raw, currInfIdx + 2, seg1Len, seg2Len , seg3Len, MetaLen), RightSeg : RightSeg(raw, currInfIdx - 1, seg1Len, seg2Len , seg3Len, MetaLen), } } -// In the future, this should probably use AbsMetaHdr as -// the return type. ghost requires MetaLen <= len(raw) requires acc(sl.Bytes(raw, 0, len(raw)), R56) @@ -496,8 +494,6 @@ pure func RawBytesToMetaHdr(raw []byte) MetaHdr { DecodedFrom(hdr) } -// In the future, this should probably use AbsBase as -// the return type. ghost requires MetaLen <= len(raw) requires acc(sl.Bytes(raw, 0, len(raw)), R56) @@ -575,20 +571,6 @@ func (s *Raw) EstablishValidPktMetaHdr(ghost ub []byte) { fold acc(s.Mem(ub), R55) } -ghost -decreases -pure func AbsSetInfoField(oldPkt io.IO_pkt2, info path.IntermediateAbsInfoField) (newPkt io.IO_pkt2) { - return let newCurrSeg := io.IO_seg3_ { - info.AInfo, - info.UInfo, - info.ConsDir, - info.Peer, - oldPkt.CurrSeg.Past, - oldPkt.CurrSeg.Future, - oldPkt.CurrSeg.History} in - io.IO_Packet2{newCurrSeg, oldPkt.LeftSeg, oldPkt.MidSeg, oldPkt.RightSeg} -} - ghost requires oldPkt.LeftSeg != none[io.IO_seg2] requires len(oldPkt.CurrSeg.Future) > 0 @@ -649,8 +631,8 @@ pure func (s *Raw) CorrectlyDecodedInfWithIdx(ub []byte, idx int, info path.Info unfolding acc(s.Base.Mem(), _) in let infOffset := MetaLen + idx*path.InfoLen in infOffset+path.InfoLen <= len(ub) && - info.ToIntermediateAbsInfoField() == - path.BytesToIntermediateAbsInfoField(ub, 0, infOffset, len(ub)) + info.ToAbsInfoField() == + reveal path.BytesToAbsInfoField(ub, infOffset) } ghost @@ -664,8 +646,8 @@ pure func (s *Raw) CorrectlyDecodedInf(ub []byte, info path.InfoField) bool { unfolding acc(s.Base.Mem(), _) in let infOffset := MetaLen + int(s.Base.PathMeta.CurrINF)*path.InfoLen in infOffset+path.InfoLen <= len(ub) && - info.ToIntermediateAbsInfoField() == - path.BytesToIntermediateAbsInfoField(ub, 0, infOffset, len(ub)) + info.ToAbsInfoField() == + reveal path.BytesToAbsInfoField(ub, infOffset) } ghost @@ -716,9 +698,9 @@ func (s *Raw) LastHopLemma(ubuf []byte) { segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := HopFieldOffset(numINF, 0, MetaLen) + offset := HopFieldOffset(numINF, prevSegLen, MetaLen) pkt := reveal s.absPkt(ubuf) - assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen) + assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen) assert len(pkt.CurrSeg.Future) == 1 } @@ -742,9 +724,9 @@ func (s *Raw) XoverLemma(ubuf []byte) { segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := HopFieldOffset(numINF, 0, MetaLen) + offset := HopFieldOffset(numINF, prevSegLen, MetaLen) pkt := reveal s.absPkt(ubuf) - assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen) + assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen) assert pkt.LeftSeg == reveal LeftSeg(ubuf, currInfIdx + 1, seg1Len, seg2Len , seg3Len, MetaLen) assert len(pkt.CurrSeg.Future) == 1 assert pkt.LeftSeg != none[io.IO_seg2] @@ -762,7 +744,7 @@ pure func (s *Raw) EqAbsHopField(pkt io.IO_pkt2, hop io.IO_HF) bool { ghost opaque decreases -pure func (s *Raw) EqAbsInfoField(pkt io.IO_pkt2, info path.IntermediateAbsInfoField) bool { +pure func (s *Raw) EqAbsInfoField(pkt io.IO_pkt2, info io.AbsInfoField) bool { return let currseg := pkt.CurrSeg in info.AInfo == currseg.AInfo && info.UInfo == currseg.UInfo && @@ -780,7 +762,7 @@ preserves s.ValidCurrINF(ubuf) preserves s.ValidCurrHF(ubuf) preserves s.CorrectlyDecodedInf(ubuf, info) preserves s.CorrectlyDecodedHf(ubuf, hop) -ensures s.EqAbsInfoField(s.absPkt(ubuf), info.ToIntermediateAbsInfoField()) +ensures s.EqAbsInfoField(s.absPkt(ubuf), info.ToAbsInfoField()) ensures s.EqAbsHopField(s.absPkt(ubuf), hop.ToIO_HF()) decreases func (s *Raw) DecodingLemma(ubuf []byte, info path.InfoField, hop path.HopField) { @@ -794,19 +776,20 @@ func (s *Raw) DecodingLemma(ubuf []byte, info path.InfoField, hop path.HopField) segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := HopFieldOffset(numINF, 0, MetaLen) + offset := HopFieldOffset(numINF, prevSegLen, MetaLen) + hfIdxSeg := currHfIdx-prevSegLen reveal s.CorrectlyDecodedInf(ubuf, info) reveal s.CorrectlyDecodedHf(ubuf, hop) pkt := reveal s.absPkt(ubuf) - currseg := reveal CurrSeg(ubuf, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen) - hopFields := hopFields(ubuf, offset + path.HopLen * prevSegLen, 0, segLen) - hopFieldsBytePositionsLemma(ubuf, offset + path.HopLen * prevSegLen, 0, segLen, R54) - reveal hopFieldsBytePositions(ubuf, offset + path.HopLen * prevSegLen, 0, segLen, hopFields) - assert currseg.Future[0] == hopFields[currHfIdx-prevSegLen] - assert hopFields[currHfIdx-prevSegLen] == - path.BytesToIO_HF(ubuf, 0, offset + path.HopLen * currHfIdx, len(ubuf)) - assert currseg.Future[0] == path.BytesToIO_HF(ubuf, 0, offset + path.HopLen * currHfIdx, len(ubuf)) - assert reveal s.EqAbsInfoField(s.absPkt(ubuf), info.ToIntermediateAbsInfoField()) + currseg := reveal CurrSeg(ubuf, offset, currInfIdx, hfIdxSeg, segLen, MetaLen) + hopFields := hopFields(ubuf, offset, 0, segLen) + hopFieldsBytePositionsLemma(ubuf, offset, 0, segLen, R54) + reveal hopFieldsBytePositions(ubuf, offset, 0, segLen, hopFields) + assert currseg.Future[0] == hopFields[hfIdxSeg] + assert hopFields[hfIdxSeg] == + path.BytesToIO_HF(ubuf, 0, offset + path.HopLen * hfIdxSeg, len(ubuf)) + assert currseg.Future[0] == path.BytesToIO_HF(ubuf, 0, offset + path.HopLen * hfIdxSeg, len(ubuf)) + assert reveal s.EqAbsInfoField(s.absPkt(ubuf), info.ToAbsInfoField()) assert reveal s.EqAbsHopField(s.absPkt(ubuf), hop.ToIO_HF()) } @@ -878,23 +861,23 @@ ensures let prevSegLen := LengthOfPrevSeg(currHfIdx+1, seg1Len, seg2Len, seg3Len) in let segLen := LengthOfCurrSeg(currHfIdx+1, seg1Len, seg2Len, seg3Len) in let numInf := NumInfoFields(seg1Len, seg2Len, seg3Len) in - let offset := HopFieldOffset(numInf, 0, 0) in - CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen+1, segLen, 0) == + let offset := HopFieldOffset(numInf, prevSegLen, 0) in + CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen+1, segLen, 0) == get(LeftSeg(raw, currInfIdx, seg1Len, seg2Len, seg3Len, 0)) decreases func XoverCurrSeg(raw []byte, currInfIdx int, currHfIdx int, seg1Len int, seg2Len int, seg3Len int) { prevSegLen := LengthOfPrevSeg(currHfIdx+1, seg1Len, seg2Len, seg3Len) segLen := LengthOfCurrSeg(currHfIdx+1, seg1Len, seg2Len, seg3Len) numInf := NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := HopFieldOffset(numInf, 0, 0) - currseg := reveal CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, 0, segLen, 0) + offset := HopFieldOffset(numInf, prevSegLen, 0) + currseg := reveal CurrSeg(raw, offset, currInfIdx, 0, segLen, 0) leftseg := reveal LeftSeg(raw, currInfIdx, seg1Len, seg2Len, seg3Len, 0) assert currseg == get(leftseg) } ghost requires 0 < seg1Len -requires 0 <= seg2Len +requires 0 < seg2Len requires 0 <= seg3Len requires pktLen(seg1Len, seg2Len, seg3Len, 0) <= len(raw) requires 2 <= currInfIdx && currInfIdx < 4 @@ -910,10 +893,11 @@ func XoverLeftSeg(raw []byte, currInfIdx int, seg1Len int, seg2Len int, seg3Len ghost requires 0 < seg1Len -requires 0 <= seg2Len +requires 0 < seg2Len requires 0 <= seg3Len requires pktLen(seg1Len, seg2Len, seg3Len, 0) <= len(raw) requires -1 <= currInfIdx && currInfIdx < 1 +requires 0 == currInfIdx ==> 0 < seg3Len preserves acc(sl.Bytes(raw, 0, len(raw)), R56) ensures MidSeg(raw, currInfIdx+4, seg1Len, seg2Len, seg3Len, 0) == RightSeg(raw, currInfIdx, seg1Len, seg2Len, seg3Len, 0) @@ -939,8 +923,8 @@ ensures let prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) in let segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) in let numInf := NumInfoFields(seg1Len, seg2Len, seg3Len) in - let offset := HopFieldOffset(numInf, 0, 0) in - let currseg := CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, 0) in + let offset := HopFieldOffset(numInf, prevSegLen, 0) in + let currseg := CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, 0) in len(currseg.Future) > 0 && get(RightSeg(raw, currInfIdx, seg1Len, seg2Len, seg3Len, 0)) == absIncPathSeg(currseg) @@ -949,11 +933,11 @@ func XoverRightSeg(raw []byte, currInfIdx int, currHfIdx int, seg1Len int, seg2L prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numInf := NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := HopFieldOffset(numInf, 0, 0) - LenCurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, segLen - 1, segLen) - IncCurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, segLen - 1, segLen) - currseg := CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, segLen - 1, segLen, 0) - nextseg := CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, segLen, segLen, 0) + offset := HopFieldOffset(numInf, prevSegLen, 0) + LenCurrSeg(raw, offset, currInfIdx, segLen - 1, segLen) + IncCurrSeg(raw, offset, currInfIdx, segLen - 1, segLen) + currseg := CurrSeg(raw, offset, currInfIdx, segLen - 1, segLen, 0) + nextseg := CurrSeg(raw, offset, currInfIdx, segLen, segLen, 0) rightseg := reveal RightSeg(raw, currInfIdx, seg1Len, seg2Len, seg3Len, 0) assert absIncPathSeg(currseg) == nextseg assert nextseg == get(rightseg) diff --git a/router/dataplane.go b/router/dataplane.go index da01b5d9f..bab621d04 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1981,7 +1981,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce // @ absPktFutureLemma(ub) // @ p.path.DecodingLemma(ubPath, p.infoField, p.hopField) // @ assert reveal p.path.EqAbsInfoField(p.path.absPkt(ubPath), - // @ p.infoField.ToIntermediateAbsInfoField()) + // @ p.infoField.ToAbsInfoField()) // @ assert reveal p.path.EqAbsHopField(p.path.absPkt(ubPath), // @ p.hopField.ToIO_HF()) // @ assert reveal p.EqAbsHopField(absPkt(ub)) @@ -2527,7 +2527,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost oldPkt io.IO_pkt2, gh // @ reveal p.EqAbsInfoField(oldPkt) // @ reveal p.EqAbsHopField(oldPkt) // (VerifiedSCION) Assumptions for Cryptography: - // @ absInf := p.infoField.ToIntermediateAbsInfoField() + // @ absInf := p.infoField.ToAbsInfoField() // @ absHF := p.hopField.ToIO_HF() // @ AssumeForIO(dp.hf_valid(absInf.ConsDir, absInf.AInfo, absInf.UInfo, absHF)) // @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp) diff --git a/router/io-spec-lemmas.gobra b/router/io-spec-lemmas.gobra index 60daa8c8c..01377e461 100644 --- a/router/io-spec-lemmas.gobra +++ b/router/io-spec-lemmas.gobra @@ -66,9 +66,9 @@ func absPktFutureLemma(raw []byte) { segLen := scion.LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := scion.LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := scion.NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := scion.HopFieldOffset(numINF, 0, headerOffsetWithMetaLen) + offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) pkt := reveal absPkt(raw) - assert pkt.CurrSeg == reveal scion.CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen) + assert pkt.CurrSeg == reveal scion.CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen) assert len(pkt.CurrSeg.Future) > 0 } @@ -294,9 +294,9 @@ func (p* scionPacketProcessor) AbsPktToSubSliceAbsPkt(ub []byte, start int, end segLen := scion.LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := scion.LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := scion.NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := scion.HopFieldOffset(numINF, 0, headerOffsetWithMetaLen) + offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) - scion.WidenCurrSeg(ub, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen, start, end) + scion.WidenCurrSeg(ub, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen, start, end) scion.WidenLeftSeg(ub, currInfIdx + 1, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, start, end) scion.WidenMidSeg(ub, currInfIdx + 2, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, start, end) scion.WidenRightSeg(ub, currInfIdx - 1, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, start, end) @@ -355,9 +355,9 @@ func (p* scionPacketProcessor) SubSliceAbsPktToAbsPkt(ub []byte, start int, end segLen := scion.LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := scion.LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := scion.NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := scion.HopFieldOffset(numINF, 0, headerOffsetWithMetaLen) + offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) - scion.WidenCurrSeg(ub, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen, start, end) + scion.WidenCurrSeg(ub, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen, start, end) scion.WidenLeftSeg(ub, currInfIdx + 1, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, start, end) scion.WidenMidSeg(ub, currInfIdx + 2, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, start, end) scion.WidenRightSeg(ub, currInfIdx - 1, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, start, end) @@ -380,7 +380,7 @@ opaque requires acc(&p.infoField, R55) decreases pure func (p* scionPacketProcessor) EqAbsInfoField(pkt io.IO_pkt2) bool { - return let absInf := p.infoField.ToIntermediateAbsInfoField() in + return let absInf := p.infoField.ToAbsInfoField() in let currseg := pkt.CurrSeg in absInf.AInfo == currseg.AInfo && absInf.UInfo == currseg.UInfo && diff --git a/router/io-spec.gobra b/router/io-spec.gobra index fb37adf58..c891e8f2f 100644 --- a/router/io-spec.gobra +++ b/router/io-spec.gobra @@ -50,9 +50,9 @@ pure func absPkt(raw []byte) (res io.IO_pkt2) { let segLen := scion.LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) in let prevSegLen := scion.LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) in let numINF := scion.NumInfoFields(seg1Len, seg2Len, seg3Len) in - let offset := scion.HopFieldOffset(numINF, 0, headerOffsetWithMetaLen) in + let offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) in io.IO_Packet2 { - CurrSeg : scion.CurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen), + CurrSeg : scion.CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen), LeftSeg : scion.LeftSeg(raw, currInfIdx + 1, seg1Len, seg2Len , seg3Len, headerOffsetWithMetaLen), MidSeg : scion.MidSeg(raw, currInfIdx + 2, seg1Len, seg2Len , seg3Len, headerOffsetWithMetaLen), RightSeg : scion.RightSeg(raw, currInfIdx - 1, seg1Len, seg2Len , seg3Len, headerOffsetWithMetaLen), diff --git a/router/widen-lemma.gobra b/router/widen-lemma.gobra index 06ed67245..4abb48e83 100644 --- a/router/widen-lemma.gobra +++ b/router/widen-lemma.gobra @@ -139,9 +139,9 @@ func absPktWidenLemma(raw []byte, length int) { segLen := scion.LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len) prevSegLen := scion.LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len) numINF := scion.NumInfoFields(seg1Len, seg2Len, seg3Len) - offset := scion.HopFieldOffset(numINF, 0, headerOffsetWithMetaLen) + offset := scion.HopFieldOffset(numINF, prevSegLen, headerOffsetWithMetaLen) - scion.WidenCurrSeg(raw, offset + path.HopLen * prevSegLen, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen, 0, length) + scion.WidenCurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, headerOffsetWithMetaLen, 0, length) scion.WidenLeftSeg(raw, currInfIdx + 1, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, 0, length) scion.WidenMidSeg(raw, currInfIdx + 2, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, 0, length) scion.WidenRightSeg(raw, currInfIdx - 1, seg1Len, seg2Len, seg3Len, headerOffsetWithMetaLen, 0, length) diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra index de71c2e17..c7e98c92d 100644 --- a/verification/io/io-spec.gobra +++ b/verification/io/io-spec.gobra @@ -51,46 +51,6 @@ requires CBio_IN_bio3s_enter(t, v) decreases pure func CBio_IN_bio3s_enter_T(t Place, v IO_val) Place -/*** Helper functions, not in Isabelle ***/ -// Establishes the traversed segment for packets which are not incremented (internal). -ghost -requires len(currseg.Future) > 0 -decreases -pure func establishGuardTraversedseg(currseg IO_seg3, direction bool) IO_seg3 { - return let uinfo := direction ? - upd_uinfo(currseg.UInfo, currseg.Future[0]) : - currseg.UInfo in - IO_seg3_ { - AInfo: currseg.AInfo, - UInfo: uinfo, - ConsDir: currseg.ConsDir, - Peer: currseg.Peer, - Past: currseg.Past, - Future: currseg.Future, - History: currseg.History, - } -} - -// Establishes the traversed segment for packets that are incremented (external). -ghost -requires len(currseg.Future) > 0 -decreases -pure func establishGuardTraversedsegInc(currseg IO_seg3, direction bool) IO_seg3 { - return let uinfo := direction ? - upd_uinfo(currseg.UInfo, currseg.Future[0]) : - currseg.UInfo in - IO_seg3_ { - AInfo: currseg.AInfo, - UInfo: uinfo, - ConsDir: currseg.ConsDir, - Peer: currseg.Peer, - Past: seq[IO_HF]{currseg.Future[0]} ++ currseg.Past, - Future: currseg.Future[1:], - History: seq[IO_ahi]{currseg.Future[0].Toab()} ++ currseg.History, - } -} -/*** End of helper functions, not in Isabelle ***/ - // This corresponds to the condition of the if statement in the io-spec case for enter ghost requires v.isIO_Internal_val1 diff --git a/verification/io/io_spec_definitions.gobra b/verification/io/io_spec_definitions.gobra new file mode 100644 index 000000000..71eb1b5ed --- /dev/null +++ b/verification/io/io_spec_definitions.gobra @@ -0,0 +1,127 @@ +// Copyright 2024 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package io + +/*** This file contains helpful definitions that do not have a counterpart in the Isabelle formalization. ***/ + +// Establishes the traversed segment for packets which are not incremented (internal). +ghost +requires len(currseg.Future) > 0 +decreases +pure func establishGuardTraversedseg(currseg IO_seg3, direction bool) IO_seg3 { + return let uinfo := direction ? + upd_uinfo(currseg.UInfo, currseg.Future[0]) : + currseg.UInfo in + IO_seg3_ { + AInfo: currseg.AInfo, + UInfo: uinfo, + ConsDir: currseg.ConsDir, + Peer: currseg.Peer, + Past: currseg.Past, + Future: currseg.Future, + History: currseg.History, + } +} + +// Establishes the traversed segment for packets that are incremented (external). +ghost +requires len(currseg.Future) > 0 +decreases +pure func establishGuardTraversedsegInc(currseg IO_seg3, direction bool) IO_seg3 { + return let uinfo := direction ? + upd_uinfo(currseg.UInfo, currseg.Future[0]) : + currseg.UInfo in + IO_seg3_ { + AInfo: currseg.AInfo, + UInfo: uinfo, + ConsDir: currseg.ConsDir, + Peer: currseg.Peer, + Past: seq[IO_HF]{currseg.Future[0]} ++ currseg.Past, + Future: currseg.Future[1:], + History: seq[IO_ahi]{currseg.Future[0].Toab()} ++ currseg.History, + } +} + +ghost +decreases +pure func (seg IO_seg3) UpdateCurrSeg( info AbsInfoField) IO_seg3 { + return IO_seg3_ { + info.AInfo, + info.UInfo, + info.ConsDir, + info.Peer, + seg.Past, + seg.Future, + seg.History, + } +} + +ghost +decreases +pure func (pkt IO_pkt2) UpdateInfoField(info AbsInfoField) IO_pkt2 { + return let newCurrSeg := pkt.CurrSeg.UpdateCurrSeg(info) in + IO_Packet2{newCurrSeg, pkt.LeftSeg, pkt.MidSeg, pkt.RightSeg} +} + +// This type simplifies the infoField, making it easier +// to use than the IO_seg3 from the IO-spec. +type AbsInfoField adt { + AbsInfoField_ { + AInfo IO_ainfo + UInfo set[IO_msgterm] + ConsDir bool + Peer bool + } +} + +// The segment lengths of a packet are frequently used together. +// This type combines them into a single structure to simplify +// their specification. +type SegLens adt { + SegLens_ { + Seg1Len int + Seg2Len int + Seg3Len int + } +} + +ghost +decreases +pure func (s SegLens) Valid() bool { + return s.Seg1Len > 0 && + s.Seg2Len >= 0 && + s.Seg3Len >= 0 +} + +ghost +requires seg1Len > 0 +requires seg2Len >= 0 +requires seg3Len >= 0 +decreases +pure func CombineSegLens(seg1Len int, seg2Len int, seg3Len int) SegLens { + return SegLens_ { + seg1Len, + seg2Len, + seg3Len, + } +} + +ghost +decreases +pure func (s SegLens) NumInfoFields() int { + return s.Seg3Len > 0 ? 3 : (s.Seg2Len > 0 ? 2 : (s.Seg1Len > 0 ? 1 : 0)) +} \ No newline at end of file