Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Decode layers; extract permissions to the underlying buffer from memory predicates #166

Merged
merged 16 commits into from
Feb 7, 2023
Merged

Decode layers; extract permissions to the underlying buffer from memory predicates #166

Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
b16e746
backup
jcp19 Feb 5, 2023
2602dc3
backup
jcp19 Feb 6, 2023
2e74180
backup
jcp19 Feb 6, 2023
f67cc53
onehop
jcp19 Feb 6, 2023
0a56521
epic
jcp19 Feb 6, 2023
fd7534c
simplify slices
jcp19 Feb 6, 2023
2c763b4
adapt and clean-up stuff
jcp19 Feb 6, 2023
f9a91de
save current state
jcp19 Feb 6, 2023
238b1c3
continue slayers
jcp19 Feb 6, 2023
9b64e6c
backup
jcp19 Feb 7, 2023
fdc08a1
Merge branch 'master' into joao-extract-ubuf-perm-from-pred
jcp19 Feb 7, 2023
e89e824
Backup
jcp19 Feb 7, 2023
9a6adaf
Clean up
jcp19 Feb 7, 2023
59f1df4
backup
jcp19 Feb 7, 2023
c9b4bb9
Finish early version of decodeLayers
jcp19 Feb 7, 2023
d3a7916
fix assumptions
jcp19 Feb 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
105 changes: 41 additions & 64 deletions pkg/slayers/extn.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,11 +239,10 @@ func (e *extnBase) serializeToWithTLVOptions(b gopacket.SerializeBuffer,
return nil
}

// @ requires sl.AbsSlice_Bytes(data, 0, len(data))
// @ requires df != nil
// @ preserves df.Mem()
// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ ensures resErr != nil ==> resErr.ErrorMem()
// @ ensures sl.AbsSlice_Bytes(data, 0, len(data))
// The following poscondition is more a lot more complicated than it would be if the return type
// was *extnBase instead of extnBase
// @ ensures resErr == nil ==> (
Expand All @@ -260,10 +259,10 @@ func decodeExtnBase(data []byte, df gopacket.DecodeFeedback) (res extnBase, resE
len(data)))
}

// @ unfold sl.AbsSlice_Bytes(data, 0, len(data))
// @ unfold acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
e.NextHdr = L4ProtocolType(data[0])
e.ExtLen = data[1]
// @ fold sl.AbsSlice_Bytes(data, 0, len(data))
// @ fold acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
e.ActualLen = (int(e.ExtLen) + 1) * LineLen
if len(data) < e.ActualLen {
return extnBase{}, serrors.New(fmt.Sprintf("invalid extension header. "+
Expand Down Expand Up @@ -304,22 +303,23 @@ func (h *HopByHopExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer
return scionNextLayerTypeAfterHBH( /*@ unfolding acc(h.Mem(ubuf), def.ReadL20) in (unfolding acc(h.extnBase.Mem(ubuf), def.ReadL20) in @*/ h.NextHdr /*@ ) @*/)
}

// @ requires h.Mem(ub)
// @ ensures sl.AbsSlice_Bytes(res, 0, len(res))
// @ ensures sl.AbsSlice_Bytes(res, 0, len(res)) --* h.Mem(ub)
// @ preserves acc(h.Mem(ub), def.ReadL20)
// @ ensures 0 <= start && start <= end && end <= len(ub)
// @ ensures len(res) == end - start
// @ ensures res === ub[start:end]
// @ decreases
func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte) {
// @ unfold h.Mem(ub)
// @ unfold h.extnBase.Mem(ub)
func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) {
// @ unfold acc(h.Mem(ub), def.ReadL20)
// @ unfold acc(h.extnBase.Mem(ub), def.ReadL20)
// @ ghost base := &h.extnBase.BaseLayer
// @ unfold base.Mem(ub)
// @ unfold acc(base.Mem(ub, h.ActualLen), def.ReadL20)
tmp := h.Payload
// @ package sl.AbsSlice_Bytes(tmp, 0, len(tmp)) --* h.Mem(ub) {
// @ fold base.Mem(ub)
// @ fold h.extnBase.Mem(ub)
// @ fold h.Mem(ub)
// @ }
return tmp
// @ start = h.ActualLen
// @ end = len(ub)
// @ fold acc(base.Mem(ub, h.ActualLen), def.ReadL20)
// @ fold acc(h.extnBase.Mem(ub), def.ReadL20)
// @ fold acc(h.Mem(ub), def.ReadL20)
return tmp /*@ , start, end @*/
}

// SerializeTo implementation according to gopacket.SerializableLayer.
Expand All @@ -340,13 +340,12 @@ func (h *HopByHopExtn) SerializeTo(b gopacket.SerializeBuffer,
}

// DecodeFromBytes implementation according to gopacket.DecodingLayer.
// @ requires sl.AbsSlice_Bytes(data, 0, len(data))
// @ requires h.NonInitMem()
// @ requires df != nil
// @ preserves df.Mem()
// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ ensures res == nil ==> h.Mem(data)
// @ ensures res != nil ==> (h.NonInitMem() && res.ErrorMem())
// @ ensures res != nil ==> sl.AbsSlice_Bytes(data, 0, len(data))
// @ decreases
func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res error) {
var err error
Expand All @@ -371,8 +370,7 @@ func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ invariant len(h.Options) == lenOptions
// @ invariant forall i int :: { &h.Options[i] } 0 <= i && i < lenOptions ==>
// @ (acc(&h.Options[i]) && h.Options[i].Mem(i))
// @ invariant sl.AbsSlice_Bytes(data, 0, len(data))
// framing:
// @ invariant acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ invariant h.BaseLayer.Contents === data[:h.ActualLen]
// @ invariant h.BaseLayer.Payload === data[h.ActualLen:]
// @ decreases h.ActualLen - offset
Expand All @@ -391,10 +389,7 @@ func (h *HopByHopExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ fold tmp.Mem(lenOptions)
// @ lenOptions += 1
}
// @ sl.SplitByIndex_Bytes(data, 0, len(data), h.ActualLen, writePerm)
// @ sl.Reslice_Bytes(data, 0, h.ActualLen, writePerm)
// @ sl.Reslice_Bytes(data, h.ActualLen, len(data), writePerm)
// @ fold h.extnBase.BaseLayer.Mem(data)
// @ fold h.extnBase.BaseLayer.Mem(data, h.extnBase.ActualLen)
// @ fold h.extnBase.Mem(data)
// @ fold h.Mem(data)
return nil
Expand Down Expand Up @@ -456,32 +451,32 @@ func (e *EndToEndExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer
return scionNextLayerTypeAfterE2E( /*@ unfolding acc(e.Mem(ubuf), def.ReadL20) in (unfolding acc(e.extnBase.Mem(ubuf), def.ReadL20) in @*/ e.NextHdr /*@ ) @*/)
}

// @ requires e.Mem(ub)
// @ ensures sl.AbsSlice_Bytes(res, 0, len(res))
// @ ensures sl.AbsSlice_Bytes(res, 0, len(res)) --* e.Mem(ub)
// @ preserves acc(e.Mem(ub), def.ReadL20)
// @ ensures 0 <= start && start <= end && end <= len(ub)
// @ ensures len(res) == end - start
// @ ensures res === ub[start:end]
// @ decreases
func (e *EndToEndExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte) {
// @ unfold e.Mem(ub)
// @ unfold e.extnBase.Mem(ub)
func (e *EndToEndExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) {
// @ unfold acc(e.Mem(ub), def.ReadL20)
// @ unfold acc(e.extnBase.Mem(ub), def.ReadL20)
// @ ghost base := &e.extnBase.BaseLayer
// @ unfold base.Mem(ub)
// @ unfold acc(base.Mem(ub, e.ActualLen), def.ReadL20)
tmp := e.Payload
// @ package sl.AbsSlice_Bytes(tmp, 0, len(tmp)) --* e.Mem(ub) {
// @ fold base.Mem(ub)
// @ fold e.extnBase.Mem(ub)
// @ fold e.Mem(ub)
// @ }
return tmp
// @ start = e.ActualLen
// @ end = len(ub)
// @ fold acc(base.Mem(ub, e.ActualLen), def.ReadL20)
// @ fold acc(e.extnBase.Mem(ub), def.ReadL20)
// @ fold acc(e.Mem(ub), def.ReadL20)
return tmp /*@ , start, end @*/
}

// DecodeFromBytes implementation according to gopacket.DecodingLayer.
// @ requires sl.AbsSlice_Bytes(data, 0, len(data))
// @ requires e.NonInitMem()
// @ requires df != nil
// @ preserves df.Mem()
// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ ensures res == nil ==> e.Mem(data)
// @ ensures res != nil ==> (e.NonInitMem() && res.ErrorMem())
// @ ensures res != nil ==> sl.AbsSlice_Bytes(data, 0, len(data))
// @ decreases
func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res error) {
var err error
Expand All @@ -506,8 +501,7 @@ func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ invariant len(e.Options) == lenOptions
// @ invariant forall i int :: { &e.Options[i] } 0 <= i && i < lenOptions ==>
// @ (acc(&e.Options[i]) && e.Options[i].Mem(i))
// @ invariant sl.AbsSlice_Bytes(data, 0, len(data))
// framing:
// @ invariant acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ invariant e.BaseLayer.Contents === data[:e.ActualLen]
// @ invariant e.BaseLayer.Payload === data[e.ActualLen:]
// @ decreases e.ActualLen - offset
Expand All @@ -526,10 +520,7 @@ func (e *EndToEndExtn) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback)
// @ fold tmp.Mem(lenOptions)
// @ lenOptions += 1
}
// @ sl.SplitByIndex_Bytes(data, 0, len(data), e.ActualLen, writePerm)
// @ sl.Reslice_Bytes(data, 0, e.ActualLen, writePerm)
// @ sl.Reslice_Bytes(data, e.ActualLen, len(data), writePerm)
// @ fold e.extnBase.BaseLayer.Mem(data)
// @ fold e.extnBase.BaseLayer.Mem(data, e.ActualLen)
// @ fold e.extnBase.Mem(data)
// @ fold e.Mem(data)
return nil
Expand Down Expand Up @@ -599,13 +590,12 @@ type HopByHopExtnSkipper struct {
}

// DecodeFromBytes implementation according to gopacket.DecodingLayer
// @ requires sl.AbsSlice_Bytes(data, 0, len(data))
// @ requires s.NonInitMem()
// @ requires df != nil
// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ preserves df.Mem()
// @ ensures res == nil ==> s.Mem(data)
// @ ensures res != nil ==> (s.NonInitMem() && res.ErrorMem())
// @ ensures res != nil ==> sl.AbsSlice_Bytes(data, 0, len(data))
// @ decreases
func (s *HopByHopExtnSkipper) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res error) {
var err error
Expand All @@ -620,13 +610,7 @@ func (s *HopByHopExtnSkipper) DecodeFromBytes(data []byte, df gopacket.DecodeFee
return err
}
// @ ghost contentsLen := s.extnBase.ActualLen
// @ sl.SplitByIndex_Bytes(data, 0, len(data), contentsLen, writePerm)
// @ sl.Reslice_Bytes(data, 0, contentsLen, writePerm)
// @ sl.Reslice_Bytes(data, contentsLen, len(data), writePerm)
// @ assert sl.AbsSlice_Bytes(s.extnBase.Contents, 0, len(s.extnBase.Contents))
// @ assert sl.AbsSlice_Bytes(s.extnBase.Payload, 0, len(s.extnBase.Payload))
// @ assert acc(&s.extnBase)
// @ fold s.extnBase.BaseLayer.Mem(data)
// @ fold s.extnBase.BaseLayer.Mem(data, s.ActualLen)
// @ fold s.extnBase.Mem(data)
// @ fold s.Mem(data)
return nil
Expand Down Expand Up @@ -658,13 +642,12 @@ type EndToEndExtnSkipper struct {
}

// DecodeFromBytes implementation according to gopacket.DecodingLayer
// @ requires sl.AbsSlice_Bytes(data, 0, len(data))
// @ requires s.NonInitMem()
// @ requires df != nil
// @ preserves df.Mem()
// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), def.ReadL20)
// @ ensures res == nil ==> s.Mem(data)
// @ ensures res != nil ==> (s.NonInitMem() && res.ErrorMem())
// @ ensures res != nil ==> sl.AbsSlice_Bytes(data, 0, len(data))
// @ decreases
func (s *EndToEndExtnSkipper) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (res error) {
var err error
Expand All @@ -679,13 +662,7 @@ func (s *EndToEndExtnSkipper) DecodeFromBytes(data []byte, df gopacket.DecodeFee
return err
}
// @ ghost contentsLen := s.extnBase.ActualLen
// @ sl.SplitByIndex_Bytes(data, 0, len(data), contentsLen, writePerm)
// @ sl.Reslice_Bytes(data, 0, contentsLen, writePerm)
// @ sl.Reslice_Bytes(data, contentsLen, len(data), writePerm)
// @ assert sl.AbsSlice_Bytes(s.extnBase.Contents, 0, len(s.extnBase.Contents))
// @ assert sl.AbsSlice_Bytes(s.extnBase.Payload, 0, len(s.extnBase.Payload))
// @ assert acc(&s.extnBase)
// @ fold s.extnBase.BaseLayer.Mem(data)
// @ fold s.extnBase.BaseLayer.Mem(data, s.ActualLen)
// @ fold s.extnBase.Mem(data)
// @ fold s.Mem(data)
return nil
Expand Down
77 changes: 28 additions & 49 deletions pkg/slayers/extn_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,10 @@ pred (e *extnBase) NonInitMem() {
}

pred (e *extnBase) Mem(ubuf []byte) {
e.BaseLayer.Mem(ubuf) &&
acc(&e.NextHdr) &&
acc(&e.ExtLen) &&
acc(&e.ActualLen)
acc(&e.ActualLen) &&
e.BaseLayer.Mem(ubuf, e.ActualLen)
}

/** end of extnBase **/
Expand Down Expand Up @@ -82,21 +82,21 @@ func (h *HopByHopExtnSkipper) LayerContents() (res []byte) {

// Gobra is not able to infer that HopByHopExtnSkipper is "inheriting"
// the implementation of LayerPayload from extnBase.
requires h.Mem(ub)
ensures slices.AbsSlice_Bytes(res, 0, len(res))
ensures slices.AbsSlice_Bytes(res, 0, len(res)) --* h.Mem(ub)
preserves acc(h.Mem(ub), def.ReadL20)
ensures 0 <= start && start <= end && end <= len(ub)
ensures len(res) == end - start
ensures res === ub[start:end]
decreases
func (h *HopByHopExtnSkipper) LayerPayload(ghost ub []byte) (res []byte) {
unfold h.Mem(ub)
unfold h.extnBase.Mem(ub)
func (h *HopByHopExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
unfold acc(h.Mem(ub), def.ReadL20)
unfold acc(h.extnBase.Mem(ub), def.ReadL20)
ghost base := &h.extnBase.BaseLayer
r := base.LayerPayload(ub)
package slices.AbsSlice_Bytes(r, 0, len(r)) --* h.Mem(ub) {
apply slices.AbsSlice_Bytes(r, 0, len(r)) --* base.Mem(ub)
fold h.extnBase.Mem(ub)
fold h.Mem(ub)
}
return r
res = base.LayerPayload(ub, h.ActualLen)
start = h.ActualLen
end = len(ub)
fold acc(h.extnBase.Mem(ub), def.ReadL20)
fold acc(h.Mem(ub), def.ReadL20)
return res, start, end
}

(*HopByHopExtnSkipper) implements gopacket.Layer
Expand Down Expand Up @@ -150,21 +150,21 @@ func (e *EndToEndExtnSkipper) LayerContents() (res []byte) {

// Gobra is not able to infer that EndToEndExtnSkipper is "inheriting"
// the implementation of LayerPayload from extnBase.
requires e.Mem(ub)
ensures slices.AbsSlice_Bytes(res, 0, len(res))
ensures slices.AbsSlice_Bytes(res, 0, len(res)) --* e.Mem(ub)
preserves acc(e.Mem(ub), def.ReadL20)
ensures 0 <= start && start <= end && end <= len(ub)
ensures len(res) == end - start
ensures res === ub[start:end]
decreases
func (e *EndToEndExtnSkipper) LayerPayload(ghost ub []byte) (res []byte) {
unfold e.Mem(ub)
unfold e.extnBase.Mem(ub)
func (e *EndToEndExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
unfold acc(e.Mem(ub), def.ReadL20)
unfold acc(e.extnBase.Mem(ub), def.ReadL20)
ghost base := &e.extnBase.BaseLayer
r := base.LayerPayload(ub)
package slices.AbsSlice_Bytes(r, 0, len(r)) --* e.Mem(ub) {
apply slices.AbsSlice_Bytes(r, 0, len(r)) --* base.Mem(ub)
fold e.extnBase.Mem(ub)
fold e.Mem(ub)
}
return r
res = base.LayerPayload(ub, e.ActualLen)
start = e.ActualLen
end = len(ub)
fold acc(e.extnBase.Mem(ub), def.ReadL20)
fold acc(e.Mem(ub), def.ReadL20)
return res, start, end
}

(*EndToEndExtnSkipper) implements gopacket.Layer
Expand All @@ -173,27 +173,6 @@ func (e *EndToEndExtnSkipper) LayerPayload(ghost ub []byte) (res []byte) {
/** end of EndToEndExtnSkipper **/

/** Definitions required for serializeTLVOptions **/
ghost
requires acc(&o.OptType, _) && acc(&o.OptData, _) && acc(&o.OptDataLen, _)
// may need: ensures 0 <= res
decreases
pure func (o *tlvOption) lengthGhost(fixLengths bool) (res int) {
return o.OptType == OptTypePad1? 1 : (fixLengths? len(o.OptData) + 2 : int(o.OptDataLen) + 2)
}

// The following computes the sum of elements from right to left, makes it trivial to prove
// computeLen(options, start, end-1) + options[end].lengthGhost(false) == computeLen(options, start, end)
// when start, end, and end-1 are valid indexes in options.
ghost
requires 0 <= start && start <= end && end < len(options)
requires forall i int :: { &options[i] } start <= i && i <= end ==> acc(&options[i], _)
requires forall i int :: { &options[i] } start <= i && i <= end ==>
(acc(&options[i].OptType, _) && acc(&options[i].OptData, _) && acc(&options[i].OptDataLen, _))
// decreases end
pure func computeLen(options []*tlvOption, start, end int) (res int) {
return start < end? options[end].lengthGhost(false) + computeLen(options, start, end-1) : /* start==end */ options[start].lengthGhost(false)
}

/** End of definitions required for serializeTLVOptions **/

/** start of options **/
Expand Down
28 changes: 0 additions & 28 deletions pkg/slayers/extn_spec_test.gobra
View file
Open in desktop

This file was deleted.

16 changes: 0 additions & 16 deletions pkg/slayers/path/empty/empty_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,26 +28,10 @@ pred (e Path) NonInitMem() { true }
ghost
requires e.Mem(buf)
ensures e.NonInitMem()
ensures slices.AbsSlice_Bytes(buf, 0, len(buf))
decreases
func (e Path) DowngradePerm(buf []byte) {
unfold e.Mem(buf)
fold slices.AbsSlice_Bytes(buf, 0, len(buf))
fold e.NonInitMem()
}

ghost
requires 0 < p
requires acc(e.Mem(ub), p)
ensures acc(slices.AbsSlice_Bytes(ub, 0, len(ub)), p)
ensures acc(slices.AbsSlice_Bytes(ub, 0, len(ub)), p) --* acc(e.Mem(ub), p)
decreases
func (e Path) AccUnderlyingBuf(ghost ub []byte, ghost p perm) {
unfold acc(e.Mem(ub), p)
fold acc(slices.AbsSlice_Bytes(ub, 0, len(ub)), p)
package acc(slices.AbsSlice_Bytes(ub, 0, len(ub)), p) --* acc(e.Mem(ub), p) {
fold acc(e.Mem(ub), p)
}
}

Path implements path.Path
Loading