Skip to content

Commit

Permalink
Merge branch 'master' into markus-io-spec-setHopField-proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@jcp19
jcp19 authored Jul 23, 2024
2 parents 2adfbe3 + 3a6f9f4 commit c18c7c9
Show file tree
Hide file tree
Showing 6 changed files with 141 additions and 77 deletions.
81 changes: 47 additions & 34 deletions pkg/slayers/scion.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,13 +228,16 @@ func (s *SCION) NetworkFlow() (res gopacket.Flow) {
// @ ensures e == nil && s.HasOneHopPath(ubuf) ==>
// @ (unfolding acc(s.Mem(ubuf), R55) in CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen])) <= len(ubuf)
// @ ensures e != nil ==> e.ErrorMem()
// post for IO:
// @ ensures e == nil && old(s.EqPathType(ubuf)) ==>
// @ IsSupportedRawPkt(b.View()) == old(IsSupportedPkt(ubuf))
// @ decreases
func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions /* @ , ghost ubuf []byte @*/) (e error) {
// @ unfold acc(s.Mem(ubuf), R0)
// @ defer fold acc(s.Mem(ubuf), R0)
// @ sl.SplitRange_Bytes(ubuf, int(CmnHdrLen+s.AddrHdrLen(nil, true)), int(s.HdrLen*LineLen), writePerm)
// @ ghost defer sl.CombineRange_Bytes(ubuf, int(CmnHdrLen+s.AddrHdrLenSpecInternal()), int(s.HdrLen*LineLen), writePerm)
// @ unfold acc(s.Mem(ubuf), R1)
// @ defer fold acc(s.Mem(ubuf), R1)
// @ sl.SplitRange_Bytes(ubuf, int(CmnHdrLen+s.AddrHdrLen(nil, true)), int(s.HdrLen*LineLen), R10)
scnLen := CmnHdrLen + s.AddrHdrLen( /*@ nil, true @*/ ) + s.Path.Len( /*@ ubuf[CmnHdrLen+s.AddrHdrLen(nil, true) : s.HdrLen*LineLen] @*/ )
// @ sl.CombineRange_Bytes(ubuf, int(CmnHdrLen+s.AddrHdrLenSpecInternal()), int(s.HdrLen*LineLen), R10)
if scnLen > MaxHdrLen {
return serrors.New("header length exceeds maximum",
"max", MaxHdrLen, "actual", scnLen)
Expand All @@ -255,60 +258,70 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
// @ ghost uSerBufN := b.UBuf()
// @ assert buf === uSerBufN[:scnLen]
// @ b.ExchangePred()
// @ sl.SplitRange_Bytes(uSerBufN, 0, scnLen, writePerm)

// @ unfold acc(sl.Bytes(uSerBufN, 0, len(uSerBufN)), writePerm)
// Serialize common header.
firstLine := uint32(s.Version&0xF)<<28 | uint32(s.TrafficClass)<<20 | s.FlowID&0xFFFFF
// @ sl.SplitRange_Bytes(buf, 0, 4, writePerm)
// @ unfold acc(sl.Bytes(buf[:4], 0, 4), writePerm)
binary.BigEndian.PutUint32(buf[:4], firstLine)
// @ fold acc(sl.Bytes(buf[:4], 0, 4), writePerm)
// @ sl.CombineRange_Bytes(buf, 0, 4, writePerm)
// @ unfold acc(sl.Bytes(buf, 0, len(buf)), writePerm)
buf[4] = uint8(s.NextHdr)
buf[5] = s.HdrLen
// @ fold acc(sl.Bytes(buf, 0, len(buf)), writePerm)
// @ sl.SplitRange_Bytes(buf, 6, 8, writePerm)
// @ unfold acc(sl.Bytes(buf[6:8], 0, 2), writePerm)
// @ assert &buf[6:8][0] == &buf[6] && &buf[6:8][1] == &buf[7]
binary.BigEndian.PutUint16(buf[6:8], s.PayloadLen)
// @ fold acc(sl.Bytes(buf[6:8], 0, 2), writePerm)
// @ sl.CombineRange_Bytes(buf, 6, 8, writePerm)
// @ unfold acc(sl.Bytes(buf, 0, len(buf)), writePerm)
buf[8] = uint8(s.PathType)
buf[9] = uint8(s.DstAddrType&0x7)<<4 | uint8(s.SrcAddrType&0x7)
// @ fold acc(sl.Bytes(buf, 0, len(buf)), writePerm)
// @ sl.SplitRange_Bytes(buf, 10, 12, writePerm)
// @ unfold acc(sl.Bytes(buf[10:12], 0, 2), writePerm)
// @ assert &buf[10:12][0] == &buf[10] && &buf[10:12][1] == &buf[11]
binary.BigEndian.PutUint16(buf[10:12], 0)
// @ fold acc(sl.Bytes(buf[10:12], 0, 2), writePerm)
// @ sl.CombineRange_Bytes(buf, 10, 12, writePerm)

// @ ghost sPath := s.Path
// @ ghost pathSlice := ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]
// @ sl.CombineRange_Bytes(ubuf, CmnHdrLen+s.AddrHdrLenSpecInternal(), int(s.HdrLen*LineLen), R10)
// @ fold acc(sl.Bytes(uSerBufN, 0, len(uSerBufN)), writePerm)
// @ ghost if s.EqPathType(ubuf) {
// @ assert reveal s.EqPathTypeWithBuffer(ubuf, uSerBufN)
// @ s.IsSupportedPktLemma(ubuf, uSerBufN)
// @ }

// Serialize address header.
// @ sl.SplitRange_Bytes(buf, CmnHdrLen, len(buf), writePerm)
// @ sl.SplitRange_Bytes(uSerBufN, CmnHdrLen, scnLen, HalfPerm)
// @ sl.Reslice_Bytes(uSerBufN, 0, CmnHdrLen, R54)
// @ IsSupportedPktSubslice(uSerBufN, CmnHdrLen)
// @ sl.SplitRange_Bytes(uSerBufN, CmnHdrLen, scnLen, HalfPerm)
// @ sl.SplitRange_Bytes(ubuf, CmnHdrLen, len(ubuf), R10)
if err := s.SerializeAddrHdr(buf[CmnHdrLen:] /*@ , ubuf[CmnHdrLen:] @*/); err != nil {
// @ sl.CombineRange_Bytes(buf, CmnHdrLen, len(buf), writePerm)
// @ sl.Unslice_Bytes(uSerBufN, 0, CmnHdrLen, R54)
// @ sl.CombineRange_Bytes(uSerBufN, CmnHdrLen, scnLen, writePerm)
// @ sl.CombineRange_Bytes(ubuf, CmnHdrLen, len(ubuf), R10)
// @ sl.SplitRange_Bytes(ubuf, CmnHdrLen+s.AddrHdrLenSpecInternal(), int(s.HdrLen*LineLen), R10)
// @ sl.CombineRange_Bytes(uSerBufN, 0, scnLen, writePerm)
// @ b.RestoreMem(uSerBufN)
return err
}
offset := CmnHdrLen + s.AddrHdrLen( /*@ nil, true @*/ )

// @ sl.CombineRange_Bytes(buf, CmnHdrLen, len(buf), writePerm)
// @ sl.CombineRange_Bytes(uSerBufN, CmnHdrLen, scnLen, HalfPerm)
// @ sl.CombineRange_Bytes(ubuf, CmnHdrLen, len(ubuf), R10)
// @ sl.SplitRange_Bytes(ubuf, CmnHdrLen+s.AddrHdrLenSpecInternal(), int(s.HdrLen*LineLen), R10)
// @ IsSupportedPktSubslice(uSerBufN, CmnHdrLen)
// @ sl.Unslice_Bytes(uSerBufN, 0, CmnHdrLen, R54)
// @ sl.CombineRange_Bytes(uSerBufN, CmnHdrLen, scnLen, HalfPerm)

// Serialize path header.
// @ sl.SplitRange_Bytes(buf, offset, len(buf), writePerm)
// @ ghost startP := int(CmnHdrLen+s.AddrHdrLenSpecInternal())
// @ ghost endP := int(s.HdrLen*LineLen)
// @ ghost pathSlice := ubuf[startP : endP]
// @ sl.SplitRange_Bytes(uSerBufN, offset, scnLen, HalfPerm)
// @ sl.SplitRange_Bytes(ubuf, startP, endP, HalfPerm)
// @ sl.Reslice_Bytes(uSerBufN, 0, offset, R54)
// @ sl.Reslice_Bytes(ubuf, 0, startP, R54)
// @ IsSupportedPktSubslice(uSerBufN, offset)
// @ IsSupportedPktSubslice(ubuf, startP)
// @ sl.SplitRange_Bytes(uSerBufN, offset, scnLen, HalfPerm)
// @ sl.SplitRange_Bytes(ubuf, startP, endP, HalfPerm)
tmp := s.Path.SerializeTo(buf[offset:] /*@, pathSlice @*/)
// @ sl.CombineRange_Bytes(buf, offset, len(buf), writePerm)
// @ sl.CombineRange_Bytes(uSerBufN, 0, scnLen, writePerm)
// @ sl.CombineRange_Bytes(uSerBufN, offset, scnLen, HalfPerm)
// @ sl.CombineRange_Bytes(ubuf, startP, endP, HalfPerm)
// @ IsSupportedPktSubslice(uSerBufN, offset)
// @ IsSupportedPktSubslice(ubuf, startP)
// @ sl.Unslice_Bytes(uSerBufN, 0, offset, R54)
// @ sl.Unslice_Bytes(ubuf, 0, startP, R54)
// @ sl.CombineRange_Bytes(uSerBufN, offset, scnLen, HalfPerm)
// @ sl.CombineRange_Bytes(ubuf, startP, endP, HalfPerm)
// @ reveal IsSupportedPkt(uSerBufN)
// @ b.RestoreMem(uSerBufN)
// @ reveal IsSupportedRawPkt(b.View())
return tmp
}

Expand Down
41 changes: 39 additions & 2 deletions pkg/slayers/scion_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ import (
sl "verification/utils/slices"
"verification/io"
"encoding/binary"
"verification/utils/seqs"
)

pred PathPoolMem(pathPool []path.Path, pathPoolRaw path.Path) {
Expand Down Expand Up @@ -486,6 +487,17 @@ pure func IsSupportedPkt(raw []byte) bool {
nextHdr != L4SCMP
}

ghost
opaque
decreases
pure func IsSupportedRawPkt(raw seq[byte]) bool {
return CmnHdrLen <= len(raw) &&
let pathType := path.Type(raw[8]) in
let nextHdr := L4ProtocolType(raw[4]) in
pathType == scion.PathType &&
nextHdr != L4SCMP
}

ghost
requires CmnHdrLen <= idx && idx <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), R55)
Expand All @@ -501,6 +513,21 @@ func IsSupportedPktSubslice(raw []byte, idx int) {
fold acc(sl.Bytes(raw[:idx], 0, idx), R56)
}

ghost
preserves acc(s.Mem(ub), R55)
preserves acc(sl.Bytes(ub, 0, len(ub)), R55)
preserves acc(sl.Bytes(buffer, 0, len(buffer)), R55)
preserves s.EqPathType(ub)
preserves s.EqPathTypeWithBuffer(ub, buffer)
ensures IsSupportedPkt(ub) == IsSupportedPkt(buffer)
decreases
func (s *SCION) IsSupportedPktLemma(ub []byte, buffer []byte) {
reveal s.EqPathType(ub)
reveal s.EqPathTypeWithBuffer(ub, buffer)
reveal IsSupportedPkt(ub)
reveal IsSupportedPkt(buffer)
}

ghost
requires acc(sl.Bytes(ub, 0, len(ub)), _)
requires CmnHdrLen <= len(ub)
Expand Down Expand Up @@ -558,9 +585,19 @@ requires acc(s.Mem(ub), _)
requires acc(sl.Bytes(ub, 0, len(ub)), _)
decreases
pure func (s *SCION) EqPathType(ub []byte) bool {
return reveal s.EqPathTypeWithBuffer(ub, ub)
}

ghost
opaque
requires acc(s.Mem(ub), _)
requires acc(sl.Bytes(buffer, 0, len(buffer)), _)
decreases
pure func (s *SCION) EqPathTypeWithBuffer(ub []byte, buffer []byte) bool {
return unfolding acc(s.Mem(ub), _) in
path.Type(GetPathType(ub)) == s.PathType &&
L4ProtocolType(GetNextHdr(ub)) == s.NextHdr
CmnHdrLen <= len(buffer) &&
path.Type(GetPathType(buffer)) == s.PathType &&
L4ProtocolType(GetNextHdr(buffer)) == s.NextHdr
}

ghost
Expand Down
Loading

0 comments on commit c18c7c9

Please sign in to comment.