Skip to content

Commit

Permalink
Dataplane: verify most of prepareSCMP and necessary lemmas (#210)
Browse files Browse the repository at this point in the history 
* tiny simplificaiton

* backup

* continue packscmp

* continue packscmp

* continue packscmp

* fix type error, verification error still present

* continue packscmp

* fix error

* backup

* enable require triggers

* merge with master

* disable requireTriggers for now

* add import

* backup

* progress towards proof

* progress towards proof

* progress towards proof

* progress towards proof

* backup

* backup

* backup

* Fix verification failures

* discharge proof obligation

* Discharge another proof obligation

* cleanup

* One more proof goal finished

* Clean-up

* Progress towards proving safety of ToDecoded

* backup

* backup

* light at the end of the tunnel

* Finish!
  • Loading branch information
@jcp19
jcp19 authored Oct 18, 2023
1 parent e97425c commit 5d9c8d8
Show file tree
Hide file tree
Showing 16 changed files with 925 additions and 276 deletions.
33 changes: 33 additions & 0 deletions pkg/slayers/path/epic/epic_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,33 @@ func (p *Path) DowngradePerm(buf []byte) {
fold p.NonInitMem()
}

ghost
requires acc(p.Mem(ub), _)
decreases
pure func (p *Path) ValidCurrINF(ghost ub []byte) bool {
return unfolding acc(p.Mem(ub), _) in
let ubPath := ub[MetadataLen:] in
p.ScionPath.ValidCurrINF(ubPath)
}

ghost
requires acc(p.Mem(ub), _)
decreases
pure func (p *Path) ValidCurrHF(ghost ub []byte) bool {
return unfolding acc(p.Mem(ub), _) in
let ubPath := ub[MetadataLen:] in
p.ScionPath.ValidCurrHF(ubPath)
}

ghost
requires acc(p.Mem(ub), _)
decreases
pure func (p *Path) ValidCurrIdxs(ghost ub []byte) bool {
return unfolding acc(p.Mem(ub), _) in
let ubPath := ub[MetadataLen:] in
p.ScionPath.ValidCurrIdxs(ubPath)
}

ghost
pure
requires acc(p.Mem(buf), _)
Expand Down Expand Up @@ -71,4 +98,10 @@ func (p *Path) hasScionPath(buf []byte) (r bool) {
return unfolding acc(p.Mem(buf), _) in p.ScionPath != nil
}

ghost
requires acc(p.Mem(buf), _)
pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
return unfolding acc(p.Mem(buf), _) in buf[MetadataLen:]
}

(*Path) implements path.Path
56 changes: 28 additions & 28 deletions pkg/slayers/path/hopfield.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,16 +40,16 @@ const expTimeUnit = MaxTTL / 256 // ~5m38s
// HopField is the HopField used in the SCION and OneHop path types.
//
// The Hop Field has the following format:
// 0 1 2 3
// 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
// |r r r r r r I E| ExpTime | ConsIngress |
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
// | ConsEgress | |
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ +
// | MAC |
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
//
// 0 1 2 3
// 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
// |r r r r r r I E| ExpTime | ConsIngress |
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
// | ConsEgress | |
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ +
// | MAC |
// +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
type HopField struct {
// IngressRouterAlert flag. If the IngressRouterAlert is set, the ingress router (in
// construction direction) will process the L4 payload in the packet.
Expand All @@ -74,55 +74,55 @@ type HopField struct {

// DecodeFromBytes populates the fields from a raw buffer. The buffer must be of length >=
// path.HopLen.
//@ requires acc(h)
//@ requires len(raw) >= HopLen
//@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R10)
//@ ensures h.Mem()
//@ ensures err == nil
//@ decreases
// @ requires acc(h)
// @ requires len(raw) >= HopLen
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R45)
// @ ensures h.Mem()
// @ ensures err == nil
// @ decreases
func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
if len(raw) < HopLen {
return serrors.New("HopField raw too short", "expected", HopLen, "actual", len(raw))
}
//@ preserves acc(h)
//@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R11)
//@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
//@ ensures h.ConsIngress >= 0
//@ ensures h.ConsEgress >= 0
//@ decreases
//@ outline(
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R11)
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
h.EgressRouterAlert = raw[0]&0x1 == 0x1
h.IngressRouterAlert = raw[0]&0x2 == 0x2
h.ExpTime = raw[1]
//@ assert &raw[2:4][0] == &raw[2] && &raw[2:4][1] == &raw[3]
h.ConsIngress = binary.BigEndian.Uint16(raw[2:4])
//@ assert &raw[4:6][0] == &raw[4] && &raw[4:6][1] == &raw[5]
h.ConsEgress = binary.BigEndian.Uint16(raw[4:6])
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R11)
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
//@ )
//@ preserves acc(&h.Mac)
//@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R11)
//@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
//@ decreases
//@ outline(
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R11)
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
//@ assert forall i int :: { &h.Mac[:][i] } 0 <= i && i < len(h.Mac[:]) ==>
//@ &h.Mac[i] == &h.Mac[:][i]
//@ assert forall i int :: { &raw[6:6+MacLen][i] } 0 <= i && i < len(raw[6:6+MacLen]) ==>
//@ &raw[6:6+MacLen][i] == &raw[i+6]
copy(h.Mac[:], raw[6:6+MacLen] /*@ , R12 @*/)
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R11)
copy(h.Mac[:], raw[6:6+MacLen] /*@ , R47 @*/)
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
//@ )
//@ fold h.Mem()
return nil
}

// SerializeTo writes the fields into the provided buffer. The buffer must be of length >=
// path.HopLen.
//@ requires len(b) >= HopLen
//@ preserves acc(h.Mem(), R10)
//@ preserves slices.AbsSlice_Bytes(b, 0, HopLen)
//@ ensures err == nil
//@ decreases
// @ requires len(b) >= HopLen
// @ preserves acc(h.Mem(), R10)
// @ preserves slices.AbsSlice_Bytes(b, 0, HopLen)
// @ ensures err == nil
// @ decreases
func (h *HopField) SerializeTo(b []byte) (err error) {
if len(b) < HopLen {
return serrors.New("buffer for HopField too short", "expected", MacLen, "actual", len(b))
Expand Down Expand Up @@ -170,7 +170,7 @@ func (h *HopField) SerializeTo(b []byte) (err error) {

// ExpTimeToDuration calculates the relative expiration time in seconds.
// Note that for a 0 value ExpTime, the minimal duration is expTimeUnit.
//@ decreases
// @ decreases
func ExpTimeToDuration(expTime uint8) time.Duration {
return (time.Duration(expTime) + 1) * time.Duration(expTimeUnit) * time.Second
}
6 changes: 3 additions & 3 deletions pkg/slayers/path/infofield.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,22 +60,22 @@ type InfoField struct {
// path.InfoLen.
// @ requires len(raw) >= InfoLen
// @ preserves acc(inf)
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R10)
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R45)
// @ ensures err == nil
// @ 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.AbsSlice_Bytes(raw, 0, InfoLen), R11)
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), 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]
inf.SegID = binary.BigEndian.Uint16(raw[2:4])
//@ 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.AbsSlice_Bytes(raw, 0, InfoLen), R11)
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R50)
return nil
}

Expand Down
1 change: 0 additions & 1 deletion pkg/slayers/path/path.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,6 @@ type Path interface {
Len( /*@ ghost underlyingBuf []byte @*/ ) (l int)
// Type returns the type of a path.
//@ pure
//@ requires acc(sl.AbsSlice_Bytes(underlyingBuf, 0, len(underlyingBuf)), _)
//@ requires acc(Mem(underlyingBuf), _)
//@ decreases
Type( /*@ ghost underlyingBuf []byte @*/ ) Type
Expand Down
118 changes: 87 additions & 31 deletions pkg/slayers/path/scion/base.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,9 @@ import (

"github.com/scionproto/scion/pkg/private/serrors"
"github.com/scionproto/scion/pkg/slayers/path"
//@ bit "github.com/scionproto/scion/verification/utils/bitwise"
//@ . "github.com/scionproto/scion/verification/utils/definitions"
//@ "github.com/scionproto/scion/verification/utils/slices"
//@ sl "github.com/scionproto/scion/verification/utils/slices"
)

// MetaLen is the length of the PathMetaHeader.
Expand Down Expand Up @@ -71,9 +72,20 @@ type Base struct {
}

// @ requires s.NonInitMem()
// @ preserves acc(slices.AbsSlice_Bytes(data, 0, len(data)), R1)
// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), R50)
// @ ensures r != nil ==> (s.NonInitMem() && r.ErrorMem())
// @ ensures r == nil ==> s.Mem()
// @ ensures r == nil ==> (
// @ s.Mem() &&
// @ let lenD := len(data) in
// @ MetaLen <= lenD &&
// @ let b0 := sl.GetByte(data, 0, lenD, 0) in
// @ let b1 := sl.GetByte(data, 0, lenD, 1) in
// @ let b2 := sl.GetByte(data, 0, lenD, 2) in
// @ let b3 := sl.GetByte(data, 0, lenD, 3) in
// @ let line := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in
// @ let metaHdr := DecodedFrom(line) in
// @ metaHdr == s.GetMetaHdr() &&
// @ s.InfsMatchHfs())
// @ ensures len(data) < MetaLen ==> r != nil
// @ decreases
func (s *Base) DecodeFromBytes(data []byte) (r error) {
Expand All @@ -86,10 +98,34 @@ func (s *Base) DecodeFromBytes(data []byte) (r error) {
}
s.NumINF = 0
s.NumHops = 0

//@ ghost var metaHdrCpy MetaHdr = s.PathMeta

//@ invariant -1 <= i && i <= 2
//@ invariant acc(s)
//@ invariant 0 <= s.NumHops && 0 <= s.NumINF && s.NumINF <= 3
//@ invariant metaHdrCpy == s.PathMeta
//@ invariant 0 <= s.NumHops
//@ invariant 0 <= s.NumINF && s.NumINF <= 3
//@ invariant 0 < s.NumINF ==> 0 < s.NumHops
// Invariant provided as a list of all four possible iterations:
//@ invariant i == 2 ==> (s.NumINF == 0 && s.NumHops == 0)
//@ invariant (i == 1 && s.NumINF == 0) ==> s.NumHops == 0
//@ invariant (i == 1 && s.NumINF != 0) ==>
//@ (s.NumINF == 3 && s.NumHops == int(s.PathMeta.SegLen[2]))
//@ invariant (i == 0 && s.NumINF == 0) ==> s.NumHops == 0
//@ invariant (i == 0 && s.NumINF != 0) ==> (
//@ 2 <= s.NumINF && s.NumINF <= 3 &&
//@ (s.NumINF == 2 ==> s.NumHops == int(s.PathMeta.SegLen[1])) &&
//@ (s.NumINF == 3 ==> s.NumHops == int(s.PathMeta.SegLen[1] + s.PathMeta.SegLen[2])))
//@ invariant (i == -1 && s.NumINF == 0) ==> s.NumHops == 0
//@ invariant (i == -1 && s.NumINF != 0) ==> (
//@ (s.NumINF == 1 ==> s.NumHops == int(s.PathMeta.SegLen[0])) &&
//@ (s.NumINF == 2 ==> s.NumHops == int(s.PathMeta.SegLen[0] + s.PathMeta.SegLen[1])) &&
//@ (s.NumINF == 3 ==> s.NumHops == int(s.PathMeta.SegLen[0] + s.PathMeta.SegLen[1] + s.PathMeta.SegLen[2])))
//@ invariant forall j int :: { s.PathMeta.SegLen[j] } i < j && j < s.NumINF ==>
//@ s.PathMeta.SegLen[j] != 0
//@ invariant forall j int :: { s.PathMeta.SegLen[j] } (s.NumINF <= j && i < j && j < MaxINFs) ==>
//@ s.PathMeta.SegLen[j] == 0
//@ decreases i
for i := 2; i >= 0; i-- {
if s.PathMeta.SegLen[i] == 0 && s.NumINF > 0 {
Expand All @@ -112,13 +148,15 @@ func (s *Base) DecodeFromBytes(data []byte) (r error) {

// IncPath increases the currHF index and currINF index if appropriate.
// @ requires s.Mem()
// @ ensures old(unfolding s.Mem() in s.NumINF == 0) ==> e != nil
// @ ensures old(unfolding s.Mem() in int(s.PathMeta.CurrHF) >= s.NumHops-1) ==> e != nil
// @ ensures e == nil ==> s.Mem()
// @ ensures e == nil ==> s.Len() == old(s.Len())
// @ ensures e == nil ==> s.getNumINF() == old(s.getNumINF())
// @ ensures e != nil ==> s.NonInitMem()
// @ ensures e != nil ==> e.ErrorMem()
// @ ensures (e != nil) == (
// @ old(s.GetNumINF()) == 0 ||
// @ old(int(s.GetCurrHF()) >= s.GetNumHops()-1))
// @ ensures e == nil ==> (
// @ s.Mem() &&
// @ let oldBase := old(unfolding s.Mem() in *s) in
// @ let newBase := (unfolding s.Mem() in *s) in
// @ newBase == oldBase.IncPathSpec())
// @ ensures e != nil ==> (s.NonInitMem() && e.ErrorMem())
// @ decreases
func (s *Base) IncPath() (e error) {
//@ unfold s.Mem()
Expand All @@ -139,11 +177,12 @@ func (s *Base) IncPath() (e error) {
}

// IsXover returns whether we are at a crossover point.
// @ preserves acc(s.Mem(), R19)
// @ preserves acc(s.Mem(), R45)
// @ ensures r == s.IsXoverSpec()
// @ decreases
func (s *Base) IsXover() bool {
//@ unfold acc(s.Mem(), R19)
//@ defer fold acc(s.Mem(), R19)
func (s *Base) IsXover() (r bool) {
//@ unfold acc(s.Mem(), R45)
//@ defer fold acc(s.Mem(), R45)
return s.PathMeta.CurrHF+1 < uint8(s.NumHops) &&
s.PathMeta.CurrINF != s.infIndexForHF(s.PathMeta.CurrHF+1)
}
Expand All @@ -159,14 +198,10 @@ func (s *Base) IsFirstHopAfterXover() (res bool) {
s.PathMeta.CurrINF-1 == s.infIndexForHF(s.PathMeta.CurrHF-1)
}

// @ preserves acc(s, R20)
// @ preserves 0 <= s.NumINF && s.NumINF <= 3 && 0 <= s.NumHops
// @ ensures (0 <= r && r < 3)
// @ preserves acc(s, R50)
// @ ensures r == s.InfForHfSpec(hf)
// @ decreases
func (s *Base) infIndexForHF(hf uint8) (r uint8) {
// (VerifiedSCION) Gobra cannot prove the following propertie, even though it
// is ensured by the type system.
// @ assume 0 <= hf
switch {
case hf < s.PathMeta.SegLen[0]:
return 0
Expand Down Expand Up @@ -205,35 +240,56 @@ type MetaHdr struct {
// DecodeFromBytes populates the fields from a raw buffer. The buffer must be of length >=
// scion.MetaLen.
// @ preserves acc(m)
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R1)
// @ preserves acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R50)
// @ ensures (len(raw) >= MetaLen) == (e == nil)
// @ ensures e == nil ==> (m.CurrINF >= 0 && m.CurrHF >= 0)
// @ ensures e == nil ==> (
// @ MetaLen <= len(raw) &&
// @ 0 <= m.CurrINF && m.CurrINF <= 3 &&
// @ 0 <= m.CurrHF && m.CurrHF < 64 &&
// @ m.SegsInBounds() &&
// @ let lenR := len(raw) in
// @ let b0 := sl.GetByte(raw, 0, lenR, 0) in
// @ let b1 := sl.GetByte(raw, 0, lenR, 1) in
// @ let b2 := sl.GetByte(raw, 0, lenR, 2) in
// @ let b3 := sl.GetByte(raw, 0, lenR, 3) in
// @ let line := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in
// @ DecodedFrom(line) == *m)
// @ ensures e != nil ==> e.ErrorMem()
// @ decreases
func (m *MetaHdr) DecodeFromBytes(raw []byte) (e error) {
if len(raw) < MetaLen {
// (VerifiedSCION) added cast, otherwise Gobra cannot verify call
return serrors.New("MetaHdr raw too short", "expected", int(MetaLen), "actual", int(len(raw)))
}
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R1)
//@ unfold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R50)
line := binary.BigEndian.Uint32(raw)
m.CurrINF = uint8(line >> 30)
m.CurrHF = uint8(line>>24) & 0x3F
// (VerifiedSCION) The following assumption is guaranteed by Go but still not modeled in Gobra.
//@ assume m.CurrINF >= 0 && m.CurrHF >= 0
//@ bit.Shift30LessThan4(line)
//@ bit.And3fAtMost64(uint8(line>>24))
m.SegLen[0] = uint8(line>>12) & 0x3F
m.SegLen[1] = uint8(line>>6) & 0x3F
m.SegLen[2] = uint8(line) & 0x3F
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R1)
//@ bit.And3fAtMost64(uint8(line>>12))
//@ bit.And3fAtMost64(uint8(line>>6))
//@ bit.And3fAtMost64(uint8(line))
//@ fold acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R50)
return nil
}

// SerializeTo writes the fields into the provided buffer. The buffer must be of length >=
// scion.MetaLen.
// @ requires len(b) >= MetaLen
// @ preserves acc(m, R10)
// @ preserves slices.AbsSlice_Bytes(b, 0, len(b))
// @ preserves acc(m, R50)
// @ preserves sl.AbsSlice_Bytes(b, 0, len(b))
// @ ensures e == nil
// @ ensures let lenR := len(b) in
// @ let b0 := sl.GetByte(b, 0, lenR, 0) in
// @ let b1 := sl.GetByte(b, 0, lenR, 1) in
// @ let b2 := sl.GetByte(b, 0, lenR, 2) in
// @ let b3 := sl.GetByte(b, 0, lenR, 3) in
// @ let v := m.SerializedToLine() in
// @ binary.BigEndian.PutUint32Spec(b0, b1, b2, b3, v)
// @ decreases
func (m *MetaHdr) SerializeTo(b []byte) (e error) {
if len(b) < MetaLen {
Expand All @@ -243,9 +299,9 @@ func (m *MetaHdr) SerializeTo(b []byte) (e error) {
line |= uint32(m.SegLen[0]&0x3F) << 12
line |= uint32(m.SegLen[1]&0x3F) << 6
line |= uint32(m.SegLen[2] & 0x3F)
//@ unfold acc(slices.AbsSlice_Bytes(b, 0, len(b)))
//@ unfold acc(sl.AbsSlice_Bytes(b, 0, len(b)))
binary.BigEndian.PutUint32(b, line)
//@ fold acc(slices.AbsSlice_Bytes(b, 0, len(b)))
//@ fold acc(sl.AbsSlice_Bytes(b, 0, len(b)))
return nil
}

Expand Down
Loading

0 comments on commit 5d9c8d8

Please sign in to comment.