diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra index c4141b936..8bdbbde15 100644 --- a/pkg/slayers/path/epic/epic_spec.gobra +++ b/pkg/slayers/path/epic/epic_spec.gobra @@ -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), _) @@ -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 \ No newline at end of file diff --git a/pkg/slayers/path/hopfield.go b/pkg/slayers/path/hopfield.go index b0d99f91c..89ceaab80 100644 --- a/pkg/slayers/path/hopfield.go +++ b/pkg/slayers/path/hopfield.go @@ -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. @@ -74,23 +74,23 @@ 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] @@ -98,19 +98,19 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) { 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 @@ -118,11 +118,11 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) { // 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)) @@ -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 } diff --git a/pkg/slayers/path/infofield.go b/pkg/slayers/path/infofield.go index cf3759a2e..0e1a9442c 100644 --- a/pkg/slayers/path/infofield.go +++ b/pkg/slayers/path/infofield.go @@ -60,14 +60,14 @@ 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] @@ -75,7 +75,7 @@ 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.AbsSlice_Bytes(raw, 0, InfoLen), R11) + //@ fold acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R50) return nil } diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go index 431623074..7b03e90e8 100644 --- a/pkg/slayers/path/path.go +++ b/pkg/slayers/path/path.go @@ -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 diff --git a/pkg/slayers/path/scion/base.go b/pkg/slayers/path/scion/base.go index bb89a26aa..f8960fd72 100644 --- a/pkg/slayers/path/scion/base.go +++ b/pkg/slayers/path/scion/base.go @@ -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. @@ -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) { @@ -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 { @@ -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() @@ -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) } @@ -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 @@ -205,9 +240,20 @@ 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) { @@ -215,25 +261,35 @@ func (m *MetaHdr) DecodeFromBytes(raw []byte) (e error) { // (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 { @@ -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 } diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 3d4037ebb..04c3031ab 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -16,6 +16,11 @@ package scion +import ( + "encoding/binary" + sl "github.com/scionproto/scion/verification/utils/slices" +) + pred (b *Base) NonInitMem() { acc(b) } @@ -32,19 +37,92 @@ pred (b *Base) Mem() { acc(&b.PathMeta.SegLen[0]) && acc(&b.PathMeta.SegLen[1]) && acc(&b.PathMeta.SegLen[2]) && - // 3 is the value of MaxINFs and 64 is the number of MaxHops. 0 <= b.NumINF && b.NumINF <= MaxINFs && - // the Code defines 64 as the maximum number of hops, + // the program defines 64 as the maximum number of hops, // but this does not seem to be enforced anywhere. - 0 <= b.NumHops && // && b.NumHops <= MaxHops && + 0 <= b.NumHops && // b.NumHops <= MaxHops && (0 < b.NumINF ==> 0 < b.NumHops) } +ghost +decreases +pure func (b Base) ValidCurrInfSpec() bool { + return 0 <= b.PathMeta.CurrINF && b.PathMeta.CurrINF < b.NumINF +} + +ghost +decreases +pure func (b Base) ValidCurrHfSpec() bool { + return 0 <= b.PathMeta.CurrHF && b.PathMeta.CurrHF < b.NumHops +} + +ghost +decreases +pure func (b Base) ValidCurrIdxsSpec() bool { + return 0 <= b.NumINF && b.NumINF <= MaxINFs && + 0 <= b.NumHops && b.NumHops <= MaxHops && + b.ValidCurrHfSpec() && + b.ValidCurrInfSpec() && + 0 <= b.PathMeta.SegLen[0] && b.PathMeta.SegLen[0] < MaxHops && + 0 <= b.PathMeta.SegLen[1] && b.PathMeta.SegLen[1] < MaxHops && + 0 <= b.PathMeta.SegLen[2] && b.PathMeta.SegLen[2] < MaxHops && + (b.NumINF == 1 ==> b.NumHops == int(b.PathMeta.SegLen[0])) && + (b.NumINF == 2 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1])) && + (b.NumINF == 3 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1] + b.PathMeta.SegLen[2])) && + (forall i int :: { b.PathMeta.SegLen[i] } 0 <= i && i < b.NumINF ==> + b.PathMeta.SegLen[i] != 0) && + (forall i int :: { b.PathMeta.SegLen[i] } b.NumINF <= i && i < MaxINFs ==> + b.PathMeta.SegLen[i] == 0) + // Surprisingly, the following does not seem to be needed + // b.PathMeta.CurrINF == b.InfForHfSpec(b.PathMeta.CurrHF) +} + +ghost +decreases +pure func (b Base) InfsMatchHfsSpec() bool { + return 0 <= b.NumINF && b.NumINF <= 3 && + (b.NumINF == 1 ==> b.NumHops == int(b.PathMeta.SegLen[0])) && + (b.NumINF == 2 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1])) && + (b.NumINF == 3 ==> b.NumHops == int(b.PathMeta.SegLen[0] + b.PathMeta.SegLen[1] + b.PathMeta.SegLen[2])) && + (forall i int :: { b.PathMeta.SegLen[i] } 0 <= i && i < b.NumINF ==> + b.PathMeta.SegLen[i] != 0) && + (forall i int :: { b.PathMeta.SegLen[i] } b.NumINF <= i && i < MaxINFs ==> + b.PathMeta.SegLen[i] == 0) +} + +ghost +requires acc(b.Mem(), _) +decreases +pure func (b *Base) ValidCurrINF() bool { + return unfolding acc(b.Mem(), _) in (*b).ValidCurrInfSpec() +} + +ghost +requires acc(b.Mem(), _) +decreases +pure func (b *Base) ValidCurrHF() bool { + return unfolding acc(b.Mem(), _) in (*b).ValidCurrHfSpec() +} + +ghost +requires acc(b.Mem(), _) +decreases +pure func (b *Base) ValidCurrIdxs() bool { + return unfolding acc(b.Mem(), _) in (*b).ValidCurrIdxsSpec() +} + +ghost +requires acc(b.Mem(), _) +decreases +pure func (b *Base) InfsMatchHfs() bool { + return unfolding acc(b.Mem(), _) in (*b).InfsMatchHfsSpec() +} + ghost requires acc(b.Mem(), _) ensures 0 <= res && res <= 3 decreases -pure func (b *Base) getNumINF() (res int) { +pure func (b *Base) GetNumINF() (res int) { return unfolding acc(b.Mem(), _) in b.NumINF } @@ -52,10 +130,55 @@ ghost requires acc(b.Mem(), _) ensures 0 <= res decreases -pure func (b *Base) getNumHops() (res int) { +pure func (b *Base) GetNumHops() (res int) { return unfolding acc(b.Mem(), _) in b.NumHops } +ghost +requires acc(s.Mem(), _) +decreases +pure func (s *Base) GetMetaHdr() MetaHdr { + return unfolding acc(s.Mem(), _) in s.PathMeta +} + +ghost +requires acc(s.Mem(), _) +decreases +pure func (s *Base) GetCurrHF() uint8 { + return s.GetMetaHdr().CurrHF +} + +ghost +ensures 0 <= r && r < 3 +decreases +pure func (s Base) InfForHfSpec(hf uint8) (r uint8) { + return hf < s.PathMeta.SegLen[0] ? + 0 : + (hf < s.PathMeta.SegLen[0] + s.PathMeta.SegLen[1] ? 1 : 2) +} + +ghost +requires acc(s.Mem(), _) +decreases +pure func (s *Base) IsXoverSpec() bool { + return unfolding acc(s.Mem(), _) in ( + s.PathMeta.CurrHF+1 < uint8(s.NumHops) && + s.PathMeta.CurrINF != s.InfForHfSpec(s.PathMeta.CurrHF+1)) +} + +ghost +requires s.NumINF != 0 +requires int(s.PathMeta.CurrHF) < s.NumHops-1 +ensures s.ValidCurrIdxsSpec() ==> res.ValidCurrIdxsSpec() +decreases +pure func (s Base) IncPathSpec() (res Base) { + return Base{ + PathMeta: MetaHdr{s.InfForHfSpec(s.PathMeta.CurrHF+1), s.PathMeta.CurrHF+1, s.PathMeta.SegLen}, + NumINF: s.NumINF, + NumHops: s.NumHops, + } +} + ghost requires b.Mem() ensures b.NonInitMem() @@ -63,4 +186,51 @@ decreases func (b *Base) DowngradePerm() { unfold b.Mem() fold b.NonInitMem() -} \ No newline at end of file +} + +ghost +decreases +pure func DecodedFrom(line uint32) MetaHdr { + return MetaHdr { + CurrINF: uint8(line >> 30), + CurrHF: uint8(line>>24) & 0x3F, + SegLen: [3]uint8{uint8(line>>12) & 0x3F, uint8(line>>6) & 0x3F, uint8(line) & 0x3F}, + } +} + +ghost +decreases +pure func (m MetaHdr) SegsInBounds() bool { + return 0 <= m.SegLen[0] && m.SegLen[0] <= 63 && + 0 <= m.SegLen[1] && m.SegLen[1] <= 63 && + 0 <= m.SegLen[2] && m.SegLen[2] <= 63 +} + +ghost +decreases +pure func (m MetaHdr) SerializedToLine() uint32 { + return uint32(m.CurrINF)<<30 | + uint32(m.CurrHF&0x3F)<<24 | + uint32(m.SegLen[0]&0x3F) << 12 | + uint32(m.SegLen[1]&0x3F) << 6 | + uint32(m.SegLen[2] & 0x3F) +} + +ghost +decreases +pure func (m MetaHdr) InBounds() bool { + return 0 <= m.CurrINF && m.CurrINF <= 3 && + 0 <= m.CurrHF && m.CurrHF <= 63 && + 0 <= m.SegLen[0] && m.SegLen[0] <= 63 && + 0 <= m.SegLen[1] && m.SegLen[1] <= 63 && + 0 <= m.SegLen[2] && m.SegLen[2] <= 63 +} + +/** Lemma proven in /VerifiedSCION/verification/utils/bitwise/proofs.dfy **/ +ghost +requires m.InBounds() +ensures let line1 := m.SerializedToLine() in + binary.BigEndian.PutUint32Spec(b0, b1, b2, b3, line1) ==> + let line2 := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in DecodedFrom(line2) == m +decreases +func (m MetaHdr) SerializeAndDeserializeLemma(b0, b1, b2, b3 byte) \ No newline at end of file diff --git a/pkg/slayers/path/scion/decoded.go b/pkg/slayers/path/scion/decoded.go index 9faeaa60b..6af13f001 100644 --- a/pkg/slayers/path/scion/decoded.go +++ b/pkg/slayers/path/scion/decoded.go @@ -17,10 +17,11 @@ package scion import ( + //@ "encoding/binary" "github.com/scionproto/scion/pkg/private/serrors" "github.com/scionproto/scion/pkg/slayers/path" //@ . "github.com/scionproto/scion/verification/utils/definitions" - //@ "github.com/scionproto/scion/verification/utils/slices" + //@ sl "github.com/scionproto/scion/verification/utils/slices" ) const ( @@ -43,8 +44,19 @@ type Decoded struct { // DecodeFromBytes fully decodes the SCION path into the corresponding fields. // @ requires s.NonInitMem() -// @ preserves slices.AbsSlice_Bytes(data, 0, len(data)) -// @ ensures r == nil ==> s.Mem(data) +// @ preserves acc(sl.AbsSlice_Bytes(data, 0, len(data)), R40) +// @ ensures r == nil ==> ( +// @ s.Mem(data) && +// @ 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(data) && +// @ s.InfsMatchHfs(data)) // @ ensures r != nil ==> (r.ErrorMem() && s.NonInitMem()) // @ decreases func (s *Decoded) DecodeFromBytes(data []byte) (r error) { @@ -62,58 +74,58 @@ func (s *Decoded) DecodeFromBytes(data []byte) (r error) { } offset := MetaLen s.InfoFields = make([]path.InfoField, ( /*@ unfolding s.Base.Mem() in @*/ s.NumINF)) - //@ assert len(data) >= MetaLen + s.Base.getNumINF() * path.InfoLen + s.Base.getNumHops() * path.HopLen - //@ slices.SplitByIndex_Bytes(data, 0, len(data), offset, R1) + //@ assert len(data) >= MetaLen + s.Base.GetNumINF() * path.InfoLen + s.Base.GetNumHops() * path.HopLen + //@ sl.SplitByIndex_Bytes(data, 0, len(data), offset, R41) //@ invariant acc(&s.InfoFields) //@ invariant acc(s.Base.Mem(), R1) - //@ invariant len(s.InfoFields) == s.Base.getNumINF() - //@ invariant 0 <= i && i <= s.Base.getNumINF() - //@ invariant len(data) >= MetaLen + s.Base.getNumINF() * path.InfoLen + s.Base.getNumHops() * path.HopLen + //@ invariant len(s.InfoFields) == s.Base.GetNumINF() + //@ invariant 0 <= i && i <= s.Base.GetNumINF() + //@ invariant len(data) >= MetaLen + s.Base.GetNumINF() * path.InfoLen + s.Base.GetNumHops() * path.HopLen //@ invariant offset == MetaLen + i * path.InfoLen - //@ invariant forall j int :: { &s.InfoFields[j] } 0 <= j && j < s.Base.getNumINF() ==> acc(&s.InfoFields[j]) - //@ invariant acc(slices.AbsSlice_Bytes(data, 0, offset), R1) - //@ invariant acc(slices.AbsSlice_Bytes(data, offset, len(data)), R1) - //@ decreases s.Base.getNumINF() - i + //@ invariant forall j int :: { &s.InfoFields[j] } 0 <= j && j < s.Base.GetNumINF() ==> acc(&s.InfoFields[j]) + //@ invariant acc(sl.AbsSlice_Bytes(data, 0, offset), R41) + //@ invariant acc(sl.AbsSlice_Bytes(data, offset, len(data)), R41) + //@ decreases s.Base.GetNumINF() - i for i := 0; i < /*@ unfolding acc(s.Base.Mem(), _) in @*/ s.NumINF; i++ { - //@ slices.SplitByIndex_Bytes(data, offset, len(data), offset + path.InfoLen, R1) - //@ slices.Reslice_Bytes(data, offset, offset + path.InfoLen, R1) + //@ sl.SplitByIndex_Bytes(data, offset, len(data), offset + path.InfoLen, R41) + //@ sl.Reslice_Bytes(data, offset, offset + path.InfoLen, R41) if err := s.InfoFields[i].DecodeFromBytes(data[offset : offset+path.InfoLen]); err != nil { // (VerifiedSCION) infofield.DecodeFromBytes guarantees that err == nil. // Thus, this branch is not reachable. return err } //@ assert len(data[offset:offset+path.InfoLen]) == path.InfoLen - //@ slices.Unslice_Bytes(data, offset, offset + path.InfoLen, R1) - //@ slices.CombineAtIndex_Bytes(data, 0, offset + path.InfoLen, offset, R1) + //@ sl.Unslice_Bytes(data, offset, offset + path.InfoLen, R41) + //@ sl.CombineAtIndex_Bytes(data, 0, offset + path.InfoLen, offset, R41) offset += path.InfoLen } s.HopFields = make([]path.HopField, ( /*@ unfolding s.Base.Mem() in @*/ s.NumHops)) //@ invariant acc(&s.HopFields) //@ invariant acc(s.Base.Mem(), R1) - //@ invariant len(s.HopFields) == s.Base.getNumHops() - //@ invariant 0 <= i && i <= s.Base.getNumHops() - //@ invariant forall j int :: { &s.HopFields[j] } i <= j && j < s.Base.getNumHops() ==> acc(&s.HopFields[j]) + //@ invariant len(s.HopFields) == s.Base.GetNumHops() + //@ invariant 0 <= i && i <= s.Base.GetNumHops() + //@ invariant forall j int :: { &s.HopFields[j] } i <= j && j < s.Base.GetNumHops() ==> acc(&s.HopFields[j]) //@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < i ==> s.HopFields[j].Mem() - //@ invariant len(data) >= MetaLen + s.Base.getNumINF() * path.InfoLen + s.Base.getNumHops() * path.HopLen - //@ invariant offset == MetaLen + s.Base.getNumINF() * path.InfoLen + i * path.HopLen - //@ invariant acc(slices.AbsSlice_Bytes(data, 0, offset), R1) - //@ invariant acc(slices.AbsSlice_Bytes(data, offset, len(data)), R1) - //@ decreases s.Base.getNumHops() - i + //@ invariant len(data) >= MetaLen + s.Base.GetNumINF() * path.InfoLen + s.Base.GetNumHops() * path.HopLen + //@ invariant offset == MetaLen + s.Base.GetNumINF() * path.InfoLen + i * path.HopLen + //@ invariant acc(sl.AbsSlice_Bytes(data, 0, offset), R41) + //@ invariant acc(sl.AbsSlice_Bytes(data, offset, len(data)), R41) + //@ decreases s.Base.GetNumHops() - i for i := 0; i < /*@ unfolding acc(s.Base.Mem(), R2) in @*/ s.NumHops; i++ { - //@ slices.SplitByIndex_Bytes(data, offset, len(data), offset + path.HopLen, R1) - //@ slices.Reslice_Bytes(data, offset, offset + path.HopLen, R1) + //@ sl.SplitByIndex_Bytes(data, offset, len(data), offset + path.HopLen, R41) + //@ sl.Reslice_Bytes(data, offset, offset + path.HopLen, R41) if err := s.HopFields[i].DecodeFromBytes(data[offset : offset+path.HopLen]); err != nil { // (VerifiedSCION) infofield.DecodeFromBytes guarantees that err == nil. // Thus, this branch should not be reachable. return err } //@ assert len(data[offset:offset+path.HopLen]) == path.HopLen - //@ slices.Unslice_Bytes(data, offset, offset + path.HopLen, R1) - //@ slices.CombineAtIndex_Bytes(data, 0, offset + path.HopLen, offset, R1) + //@ sl.Unslice_Bytes(data, offset, offset + path.HopLen, R41) + //@ sl.CombineAtIndex_Bytes(data, 0, offset + path.HopLen, offset, R41) offset += path.HopLen } - //@ slices.CombineAtIndex_Bytes(data, 0, len(data), offset, R1) + //@ sl.CombineAtIndex_Bytes(data, 0, len(data), offset, R41) //@ fold s.Mem(data) return nil } @@ -121,8 +133,8 @@ func (s *Decoded) DecodeFromBytes(data []byte) (r error) { // SerializeTo writePerms the path to a slice. The slice must be big enough to hold the entire data, // otherwise an error is returned. // @ preserves acc(s.Mem(ubuf), R1) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) -// @ preserves b !== ubuf ==> slices.AbsSlice_Bytes(b, 0, len(b)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves b !== ubuf ==> sl.AbsSlice_Bytes(b, 0, len(b)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { @@ -131,23 +143,23 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { "actual", len(b)) } //@ unfold acc(s.Mem(ubuf), R1) - //@ assert slices.AbsSlice_Bytes(b, 0, len(b)) - //@ slices.SplitByIndex_Bytes(b, 0, len(b), MetaLen, writePerm) - //@ slices.Reslice_Bytes(b, 0, MetaLen, writePerm) + //@ assert sl.AbsSlice_Bytes(b, 0, len(b)) + //@ sl.SplitByIndex_Bytes(b, 0, len(b), MetaLen, writePerm) + //@ sl.Reslice_Bytes(b, 0, MetaLen, writePerm) //@ unfold acc(s.Base.Mem(), R1) if err := s.PathMeta.SerializeTo(b[:MetaLen]); err != nil { // @ Unreachable() return err } //@ fold acc(s.Base.Mem(), R1) - //@ slices.Unslice_Bytes(b, 0, MetaLen, writePerm) - //@ slices.CombineAtIndex_Bytes(b, 0, len(b), MetaLen, writePerm) + //@ sl.Unslice_Bytes(b, 0, MetaLen, writePerm) + //@ sl.CombineAtIndex_Bytes(b, 0, len(b), MetaLen, writePerm) //@ fold acc(s.Mem(ubuf), R1) offset := MetaLen //@ invariant acc(s.Mem(ubuf), R1) - //@ invariant slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) - //@ invariant b !== ubuf ==> slices.AbsSlice_Bytes(b, 0, len(b)) + //@ invariant sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) + //@ invariant b !== ubuf ==> sl.AbsSlice_Bytes(b, 0, len(b)) //@ invariant s.Len(ubuf) <= len(b) //@ invariant 0 <= i && i <= s.getLenInfoFields(ubuf) //@ invariant offset == MetaLen + i * path.InfoLen @@ -158,23 +170,23 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { for i := 0; i < /*@ unfolding acc(s.Mem(ubuf), _) in @*/ len(s.InfoFields); i++ { //@ unfold acc(s.Mem(ubuf), R1) info := &s.InfoFields[i] - //@ slices.SplitByIndex_Bytes(b, 0, len(b), offset, writePerm) - //@ slices.SplitByIndex_Bytes(b, offset, len(b), offset + path.InfoLen, writePerm) - //@ slices.Reslice_Bytes(b, offset, offset + path.InfoLen, writePerm) - //@ assert slices.AbsSlice_Bytes(b[offset:offset+path.InfoLen], 0, path.InfoLen) + //@ sl.SplitByIndex_Bytes(b, 0, len(b), offset, writePerm) + //@ sl.SplitByIndex_Bytes(b, offset, len(b), offset + path.InfoLen, writePerm) + //@ sl.Reslice_Bytes(b, offset, offset + path.InfoLen, writePerm) + //@ assert sl.AbsSlice_Bytes(b[offset:offset+path.InfoLen], 0, path.InfoLen) if err := info.SerializeTo(b[offset : offset+path.InfoLen]); err != nil { //@ Unreachable() return err } - //@ slices.Unslice_Bytes(b, offset, offset + path.InfoLen, writePerm) - //@ slices.CombineAtIndex_Bytes(b, offset, len(b), offset + path.InfoLen, writePerm) - //@ slices.CombineAtIndex_Bytes(b, 0, len(b), offset, writePerm) + //@ sl.Unslice_Bytes(b, offset, offset + path.InfoLen, writePerm) + //@ sl.CombineAtIndex_Bytes(b, offset, len(b), offset + path.InfoLen, writePerm) + //@ sl.CombineAtIndex_Bytes(b, 0, len(b), offset, writePerm) //@ fold acc(s.Mem(ubuf), R1) offset += path.InfoLen } //@ invariant acc(s.Mem(ubuf), R1) - //@ invariant slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) - //@ invariant b !== ubuf ==> slices.AbsSlice_Bytes(b, 0, len(b)) + //@ invariant sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) + //@ invariant b !== ubuf ==> sl.AbsSlice_Bytes(b, 0, len(b)) //@ invariant s.Len(ubuf) <= len(b) //@ invariant 0 <= i && i <= s.getLenHopFields(ubuf) //@ invariant offset == MetaLen + s.getLenInfoFields(ubuf) * path.InfoLen + i * path.HopLen @@ -185,16 +197,16 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { for i := 0; i < /*@ unfolding acc(s.Mem(ubuf), _) in @*/ len(s.HopFields); i++ { //@ unfold acc(s.Mem(ubuf), R1) hop := &s.HopFields[i] - //@ slices.SplitByIndex_Bytes(b, 0, len(b), offset, writePerm) - //@ slices.SplitByIndex_Bytes(b, offset, len(b), offset + path.HopLen, writePerm) - //@ slices.Reslice_Bytes(b, offset, offset + path.HopLen, writePerm) + //@ sl.SplitByIndex_Bytes(b, 0, len(b), offset, writePerm) + //@ sl.SplitByIndex_Bytes(b, offset, len(b), offset + path.HopLen, writePerm) + //@ sl.Reslice_Bytes(b, offset, offset + path.HopLen, writePerm) if err := hop.SerializeTo(b[offset : offset+path.HopLen]); err != nil { //@ Unreachable() return err } - //@ slices.Unslice_Bytes(b, offset, offset + path.HopLen, writePerm) - //@ slices.CombineAtIndex_Bytes(b, offset, len(b), offset + path.HopLen, writePerm) - //@ slices.CombineAtIndex_Bytes(b, 0, len(b), offset, writePerm) + //@ sl.Unslice_Bytes(b, offset, offset + path.HopLen, writePerm) + //@ sl.CombineAtIndex_Bytes(b, offset, len(b), offset + path.HopLen, writePerm) + //@ sl.CombineAtIndex_Bytes(b, 0, len(b), offset, writePerm) //@ fold acc(s.Mem(ubuf), R1) offset += path.HopLen } @@ -203,13 +215,16 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { // Reverse reverses a SCION path. // @ requires s.Mem(ubuf) -// @ ensures r == nil ==> p != nil -// @ ensures r == nil ==> p.Mem(ubuf) -// @ ensures r == nil ==> p == s -// @ ensures r == nil ==> typeOf(p) == type[*Decoded] +// @ ensures r == nil ==> ( +// @ p != nil && +// @ p.Mem(ubuf) && +// @ p == s && +// @ typeOf(p) == type[*Decoded] && +// @ (old(s.ValidCurrIdxs(ubuf)) ==> s.ValidCurrIdxs(ubuf))) // @ ensures r != nil ==> r.ErrorMem() && s.Mem(ubuf) // @ decreases func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { + //@ ghost isValid := s.ValidCurrIdxs(ubuf) //@ unfold s.Mem(ubuf) //@ unfold s.Base.Mem() if s.NumINF == 0 { @@ -219,37 +234,33 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { } //@ fold s.Base.Mem() //@ fold s.Mem(ubuf) + //@ ghost base := s.GetBase(ubuf) + // Reverse order of InfoFields and SegLens //@ invariant s.Mem(ubuf) - //@ invariant 0 <= i && i < unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in s.NumINF) - //@ invariant 0 <= j && j < unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in s.NumINF) + //@ invariant isValid ==> s.ValidCurrIdxs(ubuf) + //@ invariant 0 <= i && i < s.GetNumINF(ubuf) + //@ invariant 0 <= j && j < s.GetNumINF(ubuf) //@ decreases j-i for i, j := 0, ( /*@ unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in @*/ s.NumINF - 1 /*@) @*/); i < j; i, j = i+1, j-1 { //@ unfold s.Mem(ubuf) s.InfoFields[i], s.InfoFields[j] = s.InfoFields[j], s.InfoFields[i] - //@ requires s.Base.Mem() - //@ requires 0 <= i && i < unfolding s.Base.Mem() in s.NumINF - //@ requires 0 <= j && j < unfolding s.Base.Mem() in s.NumINF - //@ ensures s.Base.Mem() - //@ ensures s.Base.getNumINF() == before(s.Base.getNumINF()) - //@ ensures s.Base.getNumHops() == before(s.Base.getNumHops()) - //@ decreases - //@ outline ( //@ unfold s.Base.Mem() s.PathMeta.SegLen[i], s.PathMeta.SegLen[j] = s.PathMeta.SegLen[j], s.PathMeta.SegLen[i] //@ fold s.Base.Mem() - //@ ) //@ fold s.Mem(ubuf) } //@ preserves s.Mem(ubuf) + //@ preserves isValid ==> s.ValidCurrIdxs(ubuf) //@ decreases //@ outline( //@ unfold s.Mem(ubuf) //@ invariant acc(s.Base.Mem(), R10) - //@ invariant 0 <= i && i <= s.getNumINF() + //@ invariant 0 <= i && i <= s.Base.GetNumINF() //@ invariant acc(&s.InfoFields, R10) - //@ invariant len(s.InfoFields) == s.getNumINF() + //@ invariant len(s.InfoFields) == s.Base.GetNumINF() //@ invariant forall i int :: { &s.InfoFields[i] } 0 <= i && i < len(s.InfoFields) ==> (acc(&s.InfoFields[i].ConsDir)) + //@ invariant isValid ==> s.Base.ValidCurrIdxs() //@ decreases MaxINFs-i // Reverse cons dir flags for i := 0; i < ( /*@ unfolding acc(s.Base.Mem(), R11) in @*/ s.NumINF); i++ { @@ -259,13 +270,11 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { //@ fold s.Mem(ubuf) //@ ) - //@ preserves s.Mem(ubuf) - //@ decreases - //@ outline( // Reverse order of hop fields //@ invariant s.Mem(ubuf) - //@ invariant 0 <= i && i <= unfolding s.Mem(ubuf) in s.getNumHops() - //@ invariant -1 <= j && j < unfolding s.Mem(ubuf) in s.getNumHops() + //@ invariant 0 <= i && i <= s.GetNumHops(ubuf) + //@ invariant -1 <= j && j < s.GetNumHops(ubuf) + //@ invariant isValid ==> s.ValidCurrIdxs(ubuf) //@ decreases j-i for i, j := 0, ( /*@ unfolding s.Mem(ubuf) in (unfolding s.Base.Mem() in @*/ s.NumHops - 1 /*@ ) @*/); i < j; i, j = i+1, j-1 { //@ unfold s.Mem(ubuf) @@ -279,9 +288,9 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { //@ fold s.HopFields[j].Mem() //@ fold s.Mem(ubuf) } - //@ ) // Update CurrINF and CurrHF and SegLens //@ preserves s.Mem(ubuf) + //@ preserves isValid ==> s.ValidCurrIdxs(ubuf) //@ decreases //@ outline( //@ unfold s.Mem(ubuf) @@ -296,7 +305,7 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { // ToRaw tranforms scion.Decoded into scion.Raw. // @ preserves s.Mem(ubuf1) -// @ preserves slices.AbsSlice_Bytes(ubuf1, 0, len(ubuf1)) +// @ preserves sl.AbsSlice_Bytes(ubuf1, 0, len(ubuf1)) // @ ensures err == nil ==> r.Mem(ubuf2) // @ ensures err != nil ==> err.ErrorMem() // @ decreases @@ -305,7 +314,7 @@ func (s *Decoded) ToRaw( /*@ ghost ubuf1 []byte @*/ ) (r *Raw, err error /*@, gh // make cannot contain ghost subexpressions tmp := s.Len( /*@ ubuf1 @*/ ) b := make([]byte, tmp) - //@ fold slices.AbsSlice_Bytes(b, 0, len(b)) + //@ fold sl.AbsSlice_Bytes(b, 0, len(b)) if err := s.SerializeTo(b /*@, ubuf1 @*/); err != nil { return nil, err /*@, b @*/ } diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index af5042296..fda3419f3 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -18,6 +18,7 @@ package scion import ( "github.com/scionproto/scion/pkg/slayers/path" + . "github.com/scionproto/scion/verification/utils/definitions" "github.com/scionproto/scion/verification/utils/slices" ) @@ -32,11 +33,11 @@ pred (d *Decoded) NonInitMem() { pred (d *Decoded) Mem(ubuf []byte) { d.Base.Mem() && acc(&d.InfoFields) && - d.Base.getNumINF() <= MaxINFs && - len(d.InfoFields) == d.Base.getNumINF() && + d.Base.GetNumINF() <= MaxINFs && + len(d.InfoFields) == d.Base.GetNumINF() && (forall i int :: { &d.InfoFields[i] } 0 <= i && i < len(d.InfoFields) ==> acc(&d.InfoFields[i])) && acc(&d.HopFields) && - len(d.HopFields) == d.Base.getNumHops() && + len(d.HopFields) == d.Base.GetNumHops() && (forall i int :: { &d.HopFields[i] } 0 <= i && i < len(d.HopFields) ==> d.HopFields[i].Mem()) } @@ -50,6 +51,7 @@ pred (d *Decoded) Mem(ubuf []byte) { * Unfortunately, Gobra does not fully support them yet, so we * introduced this method which acts as a wrapper. */ + // TODO: can this spec be simplified (by removing the access to d.Mem(...))? pure requires acc(d.Mem(ubuf), _) ensures unfolding acc(d.Mem(ubuf), _) in l == d.Base.Len() @@ -73,6 +75,20 @@ func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) { return unfolding acc(d.Mem(ubuf), _) in d.Base.Type() } +/** + * This method is not part of the original SCION codebase. + * Instead, `IsXover` was defined in `*Decoded` via embedded structs. + * Unfortunately, Gobra does not fully support them yet, so we + * introduced this method which acts as a wrapper. + */ +preserves acc(d.Mem(ubuf), R19) +decreases +func (d *Decoded) IsXover(ghost ubuf []byte) bool { + unfold acc(d.Mem(ubuf), R19) + defer fold acc(d.Mem(ubuf), R19) + return d.Base.IsXover() +} + /** * This method is not part of the original SCION codebase. * This method creates an override of `IncPath` for `Decoded` which @@ -81,10 +97,11 @@ func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) { * which can be extremely cumbersome. */ requires d.Mem(ubuf) -ensures e == nil ==> d.Mem(ubuf) -ensures e == nil ==> d.Len(ubuf) == old(d.Len(ubuf)) -ensures e != nil ==> d.NonInitMem() -ensures e != nil ==> e.ErrorMem() +ensures e == nil ==> ( + d.Mem(ubuf) && + d.Len(ubuf) == old(d.Len(ubuf)) && + (old(d.ValidCurrIdxs(ubuf)) ==> d.ValidCurrIdxs(ubuf))) +ensures e != nil ==> d.NonInitMem() && e.ErrorMem() decreases func (d *Decoded) IncPath(ghost ubuf []byte) (e error) { unfold d.Mem(ubuf) @@ -97,6 +114,55 @@ func (d *Decoded) IncPath(ghost ubuf []byte) (e error) { return e } +ghost +requires acc(d.Mem(ub), _) +decreases +pure func (d *Decoded) ValidCurrINF(ub []byte) bool { + return unfolding acc(d.Mem(ub), _) in d.Base.ValidCurrINF() +} + +ghost +requires acc(d.Mem(ub), _) +decreases +pure func (d *Decoded) ValidCurrHF(ub []byte) bool { + return unfolding acc(d.Mem(ub), _) in d.Base.ValidCurrHF() +} + +ghost +requires acc(d.Mem(ub), _) +decreases +pure func (d *Decoded) ValidCurrIdxs(ub []byte) bool { + return unfolding acc(d.Mem(ub), _) in d.Base.ValidCurrIdxs() +} + +ghost +requires acc(d.Mem(ub), _) +decreases +pure func (d *Decoded) GetNumINF(ub []byte) (res int) { + return unfolding acc(d.Mem(ub), _) in d.Base.GetNumINF() +} + +ghost +requires acc(d.Mem(ub), _) +decreases +pure func (d *Decoded) GetNumHops(ub []byte) (res int) { + return unfolding acc(d.Mem(ub), _) in d.Base.GetNumHops() +} + +ghost +requires acc(s.Mem(ub), _) +decreases +pure func (s *Decoded) GetMetaHdr(ub []byte) MetaHdr { + return unfolding acc(s.Mem(ub), _) in s.Base.GetMetaHdr() +} + +ghost +requires acc(d.Mem(ub), _) +decreases +pure func (d *Decoded) InfsMatchHfs(ub []byte) bool { + return unfolding acc(d.Mem(ub), _) in d.Base.InfsMatchHfs() +} + /**** End of Stubs ****/ /**** Auxiliary Functions ****/ @@ -113,6 +179,14 @@ pure func (d *Decoded) getLenHopFields(ubuf []byte) int { return unfolding acc(d.Mem(ubuf), _) in len(d.HopFields) } +ghost +requires acc(d.Mem(ubuf), _) +decreases +pure func (d *Decoded) GetBase(ubuf []byte) Base { + return unfolding acc(d.Mem(ubuf), _) in + (unfolding acc(d.Base.Mem(), _) in d.Base) +} + /**** End of Auxiliary Functions ****/ /**** Lemmas ****/ diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go index c636233de..68dd61154 100644 --- a/pkg/slayers/path/scion/raw.go +++ b/pkg/slayers/path/scion/raw.go @@ -17,10 +17,11 @@ package scion import ( + // @ "encoding/binary" "github.com/scionproto/scion/pkg/private/serrors" "github.com/scionproto/scion/pkg/slayers/path" //@ . "github.com/scionproto/scion/verification/utils/definitions" - //@ "github.com/scionproto/scion/verification/utils/slices" + //@ sl "github.com/scionproto/scion/verification/utils/slices" ) // Raw is a raw representation of the SCION (data-plane) path type. It is designed to parse as @@ -33,7 +34,7 @@ type Raw struct { // DecodeFromBytes only decodes the PathMetaHeader. Otherwise the nothing is decoded and simply kept // as raw bytes. // @ requires s.NonInitMem() -// @ preserves slices.AbsSlice_Bytes(data, 0, len(data)) +// @ preserves sl.AbsSlice_Bytes(data, 0, len(data)) // @ ensures res == nil ==> s.Mem(data) // @ ensures res != nil ==> (s.NonInitMem() && res.ErrorMem()) // @ decreases @@ -59,8 +60,8 @@ func (s *Raw) DecodeFromBytes(data []byte) (res error) { // SerializeTo writes the path to a slice. The slice must be big enough to hold the entire data, // otherwise an error is returned. // @ preserves acc(s.Mem(ubuf), R1) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) -// @ preserves slices.AbsSlice_Bytes(b, 0, len(b)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves sl.AbsSlice_Bytes(b, 0, len(b)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases func (s *Raw) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { @@ -74,28 +75,28 @@ func (s *Raw) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { // XXX(roosd): This modifies the underlying buffer. Consider writing to data // directly. //@ unfold acc(s.Base.Mem(), R1) - //@ slices.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) - //@ assert slices.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)) - //@ slices.SplitRange_Bytes(s.Raw, 0, MetaLen, writePerm) + //@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ assert sl.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)) + //@ sl.SplitRange_Bytes(s.Raw, 0, MetaLen, writePerm) if err := s.PathMeta.SerializeTo(s.Raw[:MetaLen]); err != nil { // @ Unreachable() return err } //@ fold acc(s.Base.Mem(), R1) - //@ slices.CombineRange_Bytes(s.Raw, 0, MetaLen, writePerm) - //@ unfold acc(slices.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)), R2) - //@ unfold slices.AbsSlice_Bytes(b, 0, len(b)) + //@ sl.CombineRange_Bytes(s.Raw, 0, MetaLen, writePerm) + //@ unfold acc(sl.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)), R2) + //@ unfold sl.AbsSlice_Bytes(b, 0, len(b)) copy(b, s.Raw /*@ , R2 @*/) - //@ fold slices.AbsSlice_Bytes(b, 0, len(b)) - //@ fold acc(slices.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)), R2) - //@ slices.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ fold sl.AbsSlice_Bytes(b, 0, len(b)) + //@ fold acc(sl.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)), R2) + //@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) //@ fold acc(s.Mem(ubuf), R1) return nil } // Reverse reverses the path such that it can be used in the reverse direction. // @ requires s.Mem(ubuf) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) // @ ensures err == nil ==> typeOf(p) == type[*Raw] // @ ensures err == nil ==> p != nil && p != (*Raw)(nil) // @ ensures err == nil ==> p.Mem(ubuf) @@ -114,57 +115,109 @@ func (s *Raw) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) { return nil, err } //@ unfold s.Mem(ubuf) - //@ slices.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) if err := reversed. /*@ (*Decoded). @*/ SerializeTo(s.Raw /*@, s.Raw @*/); err != nil { - //@ slices.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) return nil, err } //@ ghost sraw := s.Raw //@ fold s.Mem(ubuf) //@ s.DowngradePerm(ubuf) err = s.DecodeFromBytes( /*@ unfolding s.NonInitMem() in @*/ s.Raw) - //@ slices.CombineRange_Bytes(ubuf, 0, len(sraw), writePerm) + //@ sl.CombineRange_Bytes(ubuf, 0, len(sraw), writePerm) //@ ghost if err == nil { s.Widen(sraw, ubuf) } return s, err } // ToDecoded transforms a scion.Raw to a scion.Decoded. -// @ preserves s.Mem(ubuf) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) -// @ ensures err == nil ==> d.Mem(unfolding acc(s.Mem(ubuf), _) in s.Raw) +// @ preserves acc(s.Mem(ubuf), R5) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ ensures err == nil ==> ( +// @ let newUb := s.RawBufferMem(ubuf) in +// @ d.Mem(newUb) && +// @ (old(s.ValidCurrIdxs(ubuf)) ==> d.ValidCurrIdxs(newUb))) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) { - //@ s.RawIdxPerm(ubuf, MetaLen, writePerm) - //@ unfold acc(s.Base.Mem(), R1) + //@ unfold acc(s.Mem(ubuf), R6) + //@ unfold acc(s.Base.Mem(), R6) + //@ ghost var base Base = s.Base + //@ ghost var pathMeta MetaHdr = s.Base.PathMeta + //@ ghost validIdxs := s.ValidCurrIdxs(ubuf) + //@ assert validIdxs ==> s.Base.PathMeta.InBounds() + //@ assert validIdxs ==> base.ValidCurrIdxsSpec() + //@ assert s.Raw[:MetaLen] === ubuf[:MetaLen] + + // (VerifiedSCION) In this method, many slice operations are done in two + // steps to preserve framming information. + //@ sl.SplitRange_Bytes(ubuf, 0, MetaLen, HalfPerm) + //@ sl.SplitRange_Bytes(ubuf, 0, MetaLen, HalfPerm) // Serialize PathMeta to ensure potential changes are reflected Raw. if err := s.PathMeta.SerializeTo(s.Raw[:MetaLen]); err != nil { // @ Unreachable() return nil, err } - //@ fold acc(s.Base.Mem(), R1) - //@ s.UndoRawIdxPerm(ubuf, MetaLen, writePerm) + //@ ghost b0 := (unfolding acc(sl.AbsSlice_Bytes(s.Raw[:MetaLen], 0, MetaLen), _) in s.Raw[0]) + //@ ghost b1 := (unfolding acc(sl.AbsSlice_Bytes(s.Raw[:MetaLen], 0, MetaLen), _) in s.Raw[1]) + //@ ghost b2 := (unfolding acc(sl.AbsSlice_Bytes(s.Raw[:MetaLen], 0, MetaLen), _) in s.Raw[2]) + //@ ghost b3 := (unfolding acc(sl.AbsSlice_Bytes(s.Raw[:MetaLen], 0, MetaLen), _) in s.Raw[3]) + //@ assert let line := s.PathMeta.SerializedToLine() in binary.BigEndian.PutUint32Spec(b0, b1, b2, b3, line) + //@ sl.CombineRange_Bytes(ubuf, 0, MetaLen, HalfPerm) + //@ assert &ubuf[0] == &s.Raw[:MetaLen][0] + //@ assert &ubuf[1] == &s.Raw[:MetaLen][1] + //@ assert &ubuf[2] == &s.Raw[:MetaLen][2] + //@ assert &ubuf[3] == &s.Raw[:MetaLen][3] + //@ assert b0 == (unfolding acc(sl.AbsSlice_Bytes(s.Raw[:MetaLen], 0, MetaLen), _) in ubuf[0]) + // (VerifiedSCION): for some reason, silicon requires the following line to be able to prove + // bX == ubuf[X]. + //@ assert unfolding acc(sl.AbsSlice_Bytes(s.Raw[:MetaLen], 0, MetaLen), _) in + //@ (ubuf[0] == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), _) in ubuf[0])) + //@ sl.CombineRange_Bytes(ubuf, 0, MetaLen, HalfPerm) decoded := &Decoded{} //@ fold decoded.Base.NonInitMem() //@ fold decoded.NonInitMem() - //@ unfold s.Mem(ubuf) - //@ slices.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), writePerm) - //@ slices.Reslice_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ sl.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), HalfPerm) + //@ assert unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), _) in + //@ (ubuf[0] == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(s.Raw)), _) in ubuf[0])) + //@ sl.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), HalfPerm) + //@ sl.Reslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm) + //@ assert &ubuf[0] == &ubuf[:len(s.Raw)][0] + //@ assert &ubuf[1] == &ubuf[:len(s.Raw)][1] + //@ assert &ubuf[2] == &ubuf[:len(s.Raw)][2] + //@ assert &ubuf[3] == &ubuf[:len(s.Raw)][3] + //@ assert unfolding acc(sl.AbsSlice_Bytes(ubuf[:len(s.Raw)], 0, len(s.Raw)), _) in + //@ (ubuf[0] == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(s.Raw)), _) in ubuf[0])) + //@ assert b0 == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(s.Raw)), _) in ubuf[0]) + //@ assert b1 == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(s.Raw)), _) in ubuf[1]) + //@ assert b2 == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(s.Raw)), _) in ubuf[2]) + //@ assert b3 == (unfolding acc(sl.AbsSlice_Bytes(ubuf, 0, len(s.Raw)), _) in ubuf[3]) + //@ sl.Reslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm) if err := decoded.DecodeFromBytes(s.Raw); err != nil { - //@ slices.Unslice_Bytes(ubuf, 0, len(s.Raw), writePerm) - //@ slices.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), writePerm) - //@ fold s.Mem(ubuf) + //@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ sl.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), writePerm) + //@ fold acc(s.Base.Mem(), R6) + //@ fold acc(s.Mem(ubuf), R6) return nil, err } - //@ slices.Unslice_Bytes(ubuf, 0, len(s.Raw), writePerm) - //@ slices.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), writePerm) - //@ fold s.Mem(ubuf) + //@ ghost lenR := len(s.Raw) // TODO: move to the top and rewrite body + //@ ghost if validIdxs { + //@ s.PathMeta.SerializeAndDeserializeLemma(b0, b1, b2, b3) + //@ assert pathMeta == decoded.GetMetaHdr(s.Raw) + //@ assert decoded.GetBase(s.Raw).ValidCurrIdxsSpec() + //@ assert decoded.ValidCurrIdxs(s.Raw) + //@ } + //@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm) + //@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm) + //@ sl.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), HalfPerm) + //@ sl.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(s.Raw), HalfPerm) + //@ fold acc(s.Base.Mem(), R6) + //@ fold acc(s.Mem(ubuf), R6) return decoded, nil } // IncPath increments the path and writes it to the buffer. // @ requires s.Mem(ubuf) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) // @ ensures old(unfolding s.Mem(ubuf) in unfolding // @ s.Base.Mem() in (s.NumINF <= 0 || int(s.PathMeta.CurrHF) >= s.NumHops-1)) ==> r != nil // @ ensures r == nil ==> s.Mem(ubuf) @@ -189,7 +242,7 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) { // GetInfoField returns the InfoField at a given index. // @ requires acc(s.Mem(ubuf), R10) // @ requires 0 <= idx -// @ preserves acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R10) +// @ preserves acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R10) // @ ensures acc(s.Mem(ubuf), R10) // @ ensures (idx < old(s.GetNumINF(ubuf))) == (err == nil) // @ ensures err != nil ==> err.ErrorMem() @@ -219,7 +272,7 @@ func (s *Raw) GetInfoField(idx int /*@, ghost ubuf []byte @*/) (ifield path.Info // GetCurrentInfoField is a convenience method that returns the current hop field pointed to by the // CurrINF index in the path meta header. // @ preserves acc(s.Mem(ubuf), R8) -// @ preserves acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R1) +// @ preserves acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R1) // @ ensures (r == nil) == (s.GetCurrINF(ubuf) < s.GetNumINF(ubuf)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases @@ -238,7 +291,7 @@ func (s *Raw) GetCurrentInfoField( /*@ ghost ubuf []byte @*/ ) (res path.InfoFie // SetInfoField updates the InfoField at a given index. // @ requires 0 <= idx // @ preserves acc(s.Mem(ubuf), R20) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @*/) (r error) { @@ -252,12 +305,12 @@ func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @ return err } infOffset := MetaLen + idx*path.InfoLen - //@ slices.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) - //@ assert slices.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)) - //@ slices.SplitRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, writePerm) + //@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ assert sl.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)) + //@ sl.SplitRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, writePerm) ret := info.SerializeTo(s.Raw[infOffset : infOffset+path.InfoLen]) - //@ slices.CombineRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, writePerm) - //@ slices.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ sl.CombineRange_Bytes(s.Raw, infOffset, infOffset+path.InfoLen, writePerm) + //@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) //@ fold acc(s.Base.Mem(), R20) //@ fold acc(s.Mem(ubuf), R20) return ret @@ -266,7 +319,7 @@ func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @ // GetHopField returns the HopField at a given index. // @ requires 0 <= idx // @ preserves acc(s.Mem(ubuf), R10) -// @ preserves acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R10) +// @ preserves acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R10) // @ ensures (idx < old(s.GetNumHops(ubuf))) == (r == nil) // @ ensures r != nil ==> r.ErrorMem() // @ decreases @@ -296,7 +349,7 @@ func (s *Raw) GetHopField(idx int /*@, ghost ubuf []byte @*/) (res path.HopField // GetCurrentHopField is a convenience method that returns the current hop field pointed to by the // CurrHF index in the path meta header. // @ preserves acc(s.Mem(ubuf), R8) -// @ preserves acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R1) +// @ preserves acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R1) // @ ensures (r == nil) == (s.GetCurrHF(ubuf) < s.GetNumHops(ubuf)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases @@ -315,7 +368,7 @@ func (s *Raw) GetCurrentHopField( /*@ ghost ubuf []byte @*/ ) (res path.HopField // SetHopField updates the HopField at a given index. // @ requires 0 <= idx // @ preserves acc(s.Mem(ubuf), R20) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/) (r error) { @@ -334,12 +387,12 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/) return err } hopOffset := MetaLen + s.NumINF*path.InfoLen + idx*path.HopLen - //@ slices.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) - //@ assert slices.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)) - //@ slices.SplitRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm) + //@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ assert sl.AbsSlice_Bytes(s.Raw, 0, len(s.Raw)) + //@ sl.SplitRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm) ret := hop.SerializeTo(s.Raw[hopOffset : hopOffset+path.HopLen]) - //@ slices.CombineRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm) - //@ slices.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) + //@ sl.CombineRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm) + //@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm) //@ fold acc(s.Base.Mem(), R20) //@ fold acc(s.Mem(ubuf), R20) return ret diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra index a929fe2c7..da1a0d05a 100644 --- a/pkg/slayers/path/scion/raw_spec.gobra +++ b/pkg/slayers/path/scion/raw_spec.gobra @@ -19,7 +19,7 @@ package scion import ( "github.com/scionproto/scion/pkg/slayers/path" . "github.com/scionproto/scion/verification/utils/definitions" - "github.com/scionproto/scion/verification/utils/slices" + sl "github.com/scionproto/scion/verification/utils/slices" ) /**** Predicates ****/ @@ -97,6 +97,31 @@ func (s *Raw) IsXover(ghost ub []byte) bool { defer fold acc(s.Mem(ub), R9) return s.Base.IsXover() } + +ghost +requires acc(s.Mem(ub), _) +decreases +pure func (s *Raw) ValidCurrINF(ghost ub []byte) bool { + return unfolding acc(s.Mem(ub), _) in + s.Base.ValidCurrINF() +} + +ghost +requires acc(s.Mem(ub), _) +decreases +pure func (s *Raw) ValidCurrHF(ghost ub []byte) bool { + return unfolding acc(s.Mem(ub), _) in + s.Base.ValidCurrHF() +} + +ghost +requires acc(s.Mem(ub), _) +decreases +pure func (s *Raw) ValidCurrIdxs(ghost ub []byte) bool { + return unfolding acc(s.Mem(ub), _) in + s.Base.ValidCurrIdxs() +} + /**** End of Stubs ****/ /**** Lemmas ****/ @@ -120,38 +145,38 @@ pred (r *Raw) RawPermRemainder(ubuf []byte, p perm) { acc(&r.Raw, p/2) && len(r.Raw) <= len(ubuf) && r.Raw === ubuf[:len(r.Raw)] && - acc(slices.AbsSlice_Bytes(ubuf, len(r.Raw), len(ubuf)), p) && + acc(sl.AbsSlice_Bytes(ubuf, len(r.Raw), len(ubuf)), p) && len(r.Raw) == r.Base.Len() } ghost requires 0 < p -requires acc(&r.Raw, p/2) && acc(slices.AbsSlice_Bytes(r.Raw, 0, len(r.Raw)), p) && acc(r.Base.Mem(), p/2) +requires acc(&r.Raw, p/2) && acc(sl.AbsSlice_Bytes(r.Raw, 0, len(r.Raw)), p) && acc(r.Base.Mem(), p/2) requires r.RawPermRemainder(ubuf, p) ensures acc(r.Mem(ubuf), p) -ensures acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) +ensures acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) decreases func (r *Raw) UndoRawPerm(ubuf []byte, p perm) { unfold r.RawPermRemainder(ubuf, p) - slices.Unslice_Bytes(ubuf, 0, len(r.Raw), p) - slices.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(r.Raw), p) + sl.Unslice_Bytes(ubuf, 0, len(r.Raw), p) + sl.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), len(r.Raw), p) fold acc(r.Mem(ubuf), p) } ghost requires 0 < p requires acc(r.Mem(ubuf), p) -requires acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) +requires acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) ensures acc(&r.Raw, p/2) -ensures acc(slices.AbsSlice_Bytes(r.Raw, 0, len(r.Raw)), p) +ensures acc(sl.AbsSlice_Bytes(r.Raw, 0, len(r.Raw)), p) ensures acc(r.Base.Mem(), p/2) ensures r.RawPermRemainder(ubuf, p) ensures r.Raw === old(unfolding acc(r.Mem(ubuf), p) in r.Raw) decreases func (r *Raw) RawPerm(ubuf []byte, p perm) { unfold acc(r.Mem(ubuf), p) - slices.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(r.Raw), p) - slices.Reslice_Bytes(ubuf, 0, len(r.Raw), p) + sl.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(r.Raw), p) + sl.Reslice_Bytes(ubuf, 0, len(r.Raw), p) fold r.RawPermRemainder(ubuf, p) } /******** End of Lemma: RawPerm ********/ @@ -163,7 +188,7 @@ pred (r *Raw) RawIdxPermRemainder(ubuf []byte, idx int, p perm) { acc(&r.Raw, p/2) && len(r.Raw) <= len(ubuf) && r.Raw === ubuf[:len(r.Raw)] && - acc(slices.AbsSlice_Bytes(ubuf, idx, len(ubuf)), p) && + acc(sl.AbsSlice_Bytes(ubuf, idx, len(ubuf)), p) && len(r.Raw) == r.Base.Len() && idx <= len(r.Raw) } @@ -172,32 +197,32 @@ ghost requires 0 < p requires acc(&r.Raw, p/2) requires 0 <= idx && idx <= len(r.Raw) -requires acc(slices.AbsSlice_Bytes(r.Raw[:idx], 0, idx), p) && acc(r.Base.Mem(), p/2) +requires acc(sl.AbsSlice_Bytes(r.Raw[:idx], 0, idx), p) && acc(r.Base.Mem(), p/2) requires r.RawIdxPermRemainder(ubuf, idx, p) ensures acc(r.Mem(ubuf), p) -ensures acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) +ensures acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) decreases func (r *Raw) UndoRawIdxPerm(ubuf []byte, idx int, p perm) { unfold r.RawIdxPermRemainder(ubuf, idx, p) - slices.Unslice_Bytes(ubuf, 0, idx, p) - slices.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), idx, p) + sl.Unslice_Bytes(ubuf, 0, idx, p) + sl.CombineAtIndex_Bytes(ubuf, 0, len(ubuf), idx, p) fold acc(r.Mem(ubuf), p) } ghost requires 0 < p requires acc(r.Mem(ubuf), p) -requires acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) +requires acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) requires 0 <= idx && idx <= unfolding acc(r.Mem(ubuf), p) in len(r.Raw) ensures acc(&r.Raw, p/2) ensures r.Raw === old(unfolding acc(r.Mem(ubuf), p) in r.Raw) -ensures acc(slices.AbsSlice_Bytes(r.Raw[:idx], 0, idx), p) && acc(r.Base.Mem(), p/2) +ensures acc(sl.AbsSlice_Bytes(r.Raw[:idx], 0, idx), p) && acc(r.Base.Mem(), p/2) ensures r.RawIdxPermRemainder(ubuf, idx, p) decreases func (r *Raw) RawIdxPerm(ubuf []byte, idx int, p perm) { unfold acc(r.Mem(ubuf), p) - slices.SplitByIndex_Bytes(ubuf, 0, len(ubuf), idx, p) - slices.Reslice_Bytes(ubuf, 0, idx, p) + sl.SplitByIndex_Bytes(ubuf, 0, len(ubuf), idx, p) + sl.Reslice_Bytes(ubuf, 0, idx, p) fold r.RawIdxPermRemainder(ubuf, idx, p) } /******** End of Lemma: RawIdxPerm ********/ @@ -210,9 +235,9 @@ pred (r *Raw) RawRangePermRemainder(ubuf []byte, start, end int, p perm) { 0 <= start && start <= end && end <= len(r.Raw) && len(r.Raw) <= len(ubuf) && r.Raw === ubuf[:len(r.Raw)] && - acc(slices.AbsSlice_Bytes(r.Raw, 0, start), p) && - acc(slices.AbsSlice_Bytes(r.Raw, end, len(r.Raw)), p) && - acc(slices.AbsSlice_Bytes(ubuf, len(r.Raw), len(ubuf)), p) && + acc(sl.AbsSlice_Bytes(r.Raw, 0, start), p) && + acc(sl.AbsSlice_Bytes(r.Raw, end, len(r.Raw)), p) && + acc(sl.AbsSlice_Bytes(ubuf, len(r.Raw), len(ubuf)), p) && len(r.Raw) == r.Base.Len() } @@ -220,16 +245,16 @@ ghost requires 0 < p requires acc(&r.Raw, p/2) requires 0 <= start && start <= end && end <= len(r.Raw) -requires acc(slices.AbsSlice_Bytes(r.Raw[start:end], 0, end-start), p) +requires acc(sl.AbsSlice_Bytes(r.Raw[start:end], 0, end-start), p) requires r.RawRangePermRemainder(ubuf, start, end, p) ensures acc(r.Mem(ubuf), p) -ensures acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) +ensures acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) decreases func (r *Raw) UndoRawRangePerm(ubuf []byte, start, end int, p perm) { unfold r.RawRangePermRemainder(ubuf, start, end, p) - slices.Unslice_Bytes(r.Raw, start, end, p) - slices.CombineAtIndex_Bytes(r.Raw, 0, end, start, p) - slices.CombineAtIndex_Bytes(r.Raw, 0, len(r.Raw), end, p) + sl.Unslice_Bytes(r.Raw, start, end, p) + sl.CombineAtIndex_Bytes(r.Raw, 0, end, start, p) + sl.CombineAtIndex_Bytes(r.Raw, 0, len(r.Raw), end, p) fold r.RawPermRemainder(ubuf, p) r.UndoRawPerm(ubuf, p) } @@ -238,20 +263,20 @@ func (r *Raw) UndoRawRangePerm(ubuf []byte, start, end int, p perm) { ghost requires 0 < p requires acc(r.Mem(ubuf), p) -requires acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) +requires acc(sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)), p) requires 0 <= start && start <= end && end <= unfolding acc(r.Mem(ubuf), p) in len(r.Raw) ensures acc(&r.Raw, p/2) ensures r.Raw === old(unfolding acc(r.Mem(ubuf), p) in r.Raw) -ensures acc(slices.AbsSlice_Bytes(r.Raw[start:end], 0, end-start), p) +ensures acc(sl.AbsSlice_Bytes(r.Raw[start:end], 0, end-start), p) ensures r.RawRangePermRemainder(ubuf, start, end, p) decreases func (r *Raw) RawRangePerm(ubuf []byte, start, end int, p perm) { unfold acc(r.Mem(ubuf), p) - slices.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(r.Raw), p) - slices.Reslice_Bytes(ubuf, 0, len(r.Raw), p) - slices.SplitByIndex_Bytes(r.Raw, 0, len(r.Raw), start, p) - slices.SplitByIndex_Bytes(r.Raw, start, len(r.Raw), end, p) - slices.Reslice_Bytes(r.Raw, start, end, p) + sl.SplitByIndex_Bytes(ubuf, 0, len(ubuf), len(r.Raw), p) + sl.Reslice_Bytes(ubuf, 0, len(r.Raw), p) + sl.SplitByIndex_Bytes(r.Raw, 0, len(r.Raw), start, p) + sl.SplitByIndex_Bytes(r.Raw, start, len(r.Raw), end, p) + sl.Reslice_Bytes(r.Raw, start, end, p) fold r.RawRangePermRemainder(ubuf, start, end, p) } /******** End of Lemma: RawRangePerm ********/ diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra index 3c1af49bf..f464b6951 100644 --- a/pkg/slayers/scion_spec.gobra +++ b/pkg/slayers/scion_spec.gobra @@ -180,6 +180,18 @@ pred (s *SCION) Mem(ubuf []byte) { (typeOf(s.Path) == type[*onehop.Path] ==> CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.Len(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]) <= len(ubuf)) } +ghost +requires acc(s.Mem(ub), _) +decreases +pure func (s *SCION) ValidPathMetaData(ghost ub []byte) bool { + return unfolding acc(s.Mem(ub), _) in + let ubPath := s.UBPath(ub) in + (typeOf(s.Path) == type[*scion.Raw] ==> + s.Path.(*scion.Raw).ValidCurrIdxs(ubPath)) && + (typeOf(s.Path) == type[*epic.Path] ==> + s.Path.(*epic.Path).ValidCurrIdxs(ubPath)) +} + // TODO: simplify the body of the predicate when let expressions // support predicates pred (s *SCION) HeaderMem(ubuf []byte) { @@ -285,6 +297,18 @@ func (s *SCION) PathEndIdx(ub []byte) int { return unfolding acc(s.Mem(ub), _) in int(s.HdrLen*LineLen) } +ghost +requires 0 < p +preserves acc(s.Mem(ub), p) +ensures let start := s.PathStartIdx(ub) in + let end := s.PathEndIdx(ub) in + 0 <= start && start <= end && end <= len(ub) +decreases +func LemmaPathIdxStartEnd(s *SCION, ub []byte, p perm) { + unfold acc(s.Mem(ub), p) + fold acc(s.Mem(ub), p) +} + ghost pure requires acc(s.Mem(ub), _) diff --git a/router/dataplane.go b/router/dataplane.go index cd71061a6..92701013c 100644 --- a/router/dataplane.go +++ b/router/dataplane.go @@ -1347,7 +1347,7 @@ func (p *scionPacketProcessor) packSCMP( } } - rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause) + rawSCMP, err := p.prepareSCMP(typ, code, scmpP, cause /*@ , nil @*/) // (VerifiedSCION) replace nil by sth else return processResult{OutPkt: rawSCMP}, err } @@ -2674,73 +2674,179 @@ func (b *bfdSend) Send(bfd *layers.BFD) error { return err } -// @ trusted -// @ requires false +// @ requires acc(&p.d, _) && acc(MutexInvariant!(), _) +// @ requires acc(p.scionLayer.Mem(ub), R4) +// @ requires p.scionLayer.ValidPathMetaData(ub) +// @ requires sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ requires acc(&p.ingressID, R15) +// @ ensures acc(p.scionLayer.Mem(ub), R4) +// @ ensures sl.AbsSlice_Bytes(ub, 0, len(ub)) +// @ ensures acc(&p.ingressID, R15) +// @ decreases func (p *scionPacketProcessor) prepareSCMP( typ slayers.SCMPType, code slayers.SCMPCode, scmpP gopacket.SerializableLayer, cause error, + // @ ghost ub []byte, ) ([]byte, error) { // *copy* and reverse path -- the original path should not be modified as this writes directly // back to rawPkt (quote). var path *scion.Raw - pathType := p.scionLayer.Path.Type() + // @ ghost startP := p.scionLayer.PathStartIdx(ub) + // @ ghost endP := p.scionLayer.PathEndIdx(ub) + // @ slayers.LemmaPathIdxStartEnd(&p.scionLayer, ub, R20) + // @ ghost ubPath := ub[startP:endP] + // @ unfold acc(p.scionLayer.Mem(ub), R4) + pathType := p.scionLayer.Path.Type( /*@ ubPath @*/ ) + // @ establishCannotRoute() + // @ ghost pathFromEpic := false + // @ ghost var epicPathUb []byte = nil switch pathType { case scion.PathType: var ok bool path, ok = p.scionLayer.Path.(*scion.Raw) if !ok { + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.WithCtx(cannotRoute, "details", "unsupported path type", "path type", pathType) } case epic.PathType: epicPath, ok := p.scionLayer.Path.(*epic.Path) if !ok { + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.WithCtx(cannotRoute, "details", "unsupported path type", "path type", pathType) } + /*@ + scionBuf := epicPath.GetUnderlyingScionPathBuf(ubPath) + unfold acc(epicPath.Mem(ubPath), R4) + assert ubPath[epic.MetadataLen:] === scionBuf + epicPathUb = ubPath + ubPath = scionBuf + startP += epic.MetadataLen + assert ubPath === ub[startP:endP] + @*/ path = epicPath.ScionPath + // @ pathFromEpic = true default: + // @ fold acc(p.scionLayer.Mem(ub), R4) return nil, serrors.WithCtx(cannotRoute, "details", "unsupported path type", "path type", pathType) } - decPath, err := path.ToDecoded() + /*@ + assert pathType == scion.PathType || pathType == epic.PathType + assert typeOf(p.scionLayer.Path) == type[*scion.Raw] || typeOf(p.scionLayer.Path) == type[*epic.Path] + assert !pathFromEpic ==> typeOf(p.scionLayer.Path) == type[*scion.Raw] + assert pathFromEpic ==> typeOf(p.scionLayer.Path) == type[*epic.Path] + sl.SplitRange_Bytes(ub, startP, endP, writePerm) + @*/ + decPath, err := path.ToDecoded( /*@ ubPath @*/ ) if err != nil { + /*@ + sl.CombineRange_Bytes(ub, startP, endP, writePerm) + ghost if pathFromEpic { + epicPath := p.scionLayer.Path.(*epic.Path) + assert acc(path.Mem(ubPath), R4) + fold acc(epicPath.Mem(epicPathUb), R4) + } else { + rawPath := p.scionLayer.Path.(*scion.Raw) + assert acc(path.Mem(ubPath), R4) + assert acc(rawPath.Mem(ubPath), R4) + } + fold acc(p.scionLayer.Mem(ub), R4) + @*/ return nil, serrors.Wrap(cannotRoute, err, "details", "decoding raw path") } - revPathTmp, err := decPath.Reverse() + // @ ghost rawPath := path.RawBufferMem(ubPath) + revPathTmp, err := decPath.Reverse( /*@ rawPath @*/ ) if err != nil { + /*@ + sl.CombineRange_Bytes(ub, startP, endP, writePerm) + ghost if pathFromEpic { + epicPath := p.scionLayer.Path.(*epic.Path) + assert acc(path.Mem(ubPath), R4) + fold acc(epicPath.Mem(epicPathUb), R4) + } else { + rawPath := p.scionLayer.Path.(*scion.Raw) + assert acc(path.Mem(ubPath), R4) + assert acc(rawPath.Mem(ubPath), R4) + } + fold acc(p.scionLayer.Mem(ub), R4) + @*/ return nil, serrors.Wrap(cannotRoute, err, "details", "reversing path for SCMP") } + // @ assert revPathTmp.Mem(rawPath) revPath := revPathTmp.(*scion.Decoded) + // @ assert revPath.Mem(rawPath) // Revert potential path segment switches that were done during processing. - if revPath.IsXover() { - if err := revPath.IncPath(); err != nil { + if revPath.IsXover( /*@ rawPath @*/ ) { + if err := revPath.IncPath( /*@ rawPath @*/ ); err != nil { + /*@ + sl.CombineRange_Bytes(ub, startP, endP, writePerm) + ghost if pathFromEpic { + epicPath := p.scionLayer.Path.(*epic.Path) + assert acc(path.Mem(ubPath), R4) + fold acc(epicPath.Mem(epicPathUb), R4) + } else { + rawPath := p.scionLayer.Path.(*scion.Raw) + assert acc(path.Mem(ubPath), R4) + assert acc(rawPath.Mem(ubPath), R4) + } + fold acc(p.scionLayer.Mem(ub), R4) + @*/ return nil, serrors.Wrap(cannotRoute, err, "details", "reverting cross over for SCMP") } } // If the packet is sent to an external router, we need to increment the // path to prepare it for the next hop. + // @ p.d.getExternalMem() + // @ if p.d.external != nil { unfold acc(AccBatchConn(p.d.external), _) } _, external := p.d.external[p.ingressID] if external { + // @ requires revPath.Mem(rawPath) + // @ requires revPath.ValidCurrIdxs(rawPath) + // @ ensures revPath.Mem(rawPath) + // @ decreases + // @ outline( + // @ unfold revPath.Mem(rawPath) + // @ unfold revPath.Base.Mem() infoField := &revPath.InfoFields[revPath.PathMeta.CurrINF] if infoField.ConsDir { - hopField := revPath.HopFields[revPath.PathMeta.CurrHF] + hopField := /*@ unfolding acc(revPath.HopFields[revPath.PathMeta.CurrHF].Mem(), _) in @*/ + revPath.HopFields[revPath.PathMeta.CurrHF] infoField.UpdateSegID(hopField.Mac) } - if err := revPath.IncPath(); err != nil { + // @ fold revPath.Base.Mem() + // @ fold revPath.Mem(rawPath) + // @ ) + if err := revPath.IncPath( /*@ rawPath @*/ ); err != nil { + /*@ + sl.CombineRange_Bytes(ub, startP, endP, writePerm) + ghost if pathFromEpic { + epicPath := p.scionLayer.Path.(*epic.Path) + assert acc(path.Mem(ubPath), R4) + fold acc(epicPath.Mem(epicPathUb), R4) + } else { + rawPath := p.scionLayer.Path.(*scion.Raw) + assert acc(path.Mem(ubPath), R4) + assert acc(rawPath.Mem(ubPath), R4) + } + fold acc(p.scionLayer.Mem(ub), R4) + @*/ return nil, serrors.Wrap(cannotRoute, err, "details", "incrementing path for SCMP") } } + // @ TODO() // create new SCION header for reply. - var scionL slayers.SCION + var scionL /*@@@*/ slayers.SCION + // (VerifiedSCION) TODO: adapt *SCION.Mem(...) scionL.FlowID = p.scionLayer.FlowID scionL.TrafficClass = p.scionLayer.TrafficClass - scionL.PathType = revPath.Type() + scionL.PathType = revPath.Type( /*@ nil @*/ ) scionL.Path = revPath scionL.DstIA = p.scionLayer.SrcIA scionL.SrcIA = p.d.localIA @@ -2748,16 +2854,16 @@ func (p *scionPacketProcessor) prepareSCMP( if err != nil { return nil, serrors.Wrap(cannotRoute, err, "details", "extracting src addr") } - if err := scionL.SetDstAddr(srcA); err != nil { + if err := scionL.SetDstAddr(srcA /*@ , false @*/); err != nil { return nil, serrors.Wrap(cannotRoute, err, "details", "setting dest addr") } - if err := scionL.SetSrcAddr(&net.IPAddr{IP: p.d.internalIP}); err != nil { + if err := scionL.SetSrcAddr(&net.IPAddr{IP: p.d.internalIP} /*@ , false @*/); err != nil { return nil, serrors.Wrap(cannotRoute, err, "details", "setting src addr") } scionL.NextHdr = slayers.L4SCMP typeCode := slayers.CreateSCMPTypeCode(typ, code) - scmpH := slayers.SCMP{TypeCode: typeCode} + scmpH /*@@@*/ := slayers.SCMP{TypeCode: typeCode} scmpH.SetNetworkLayerForChecksum(&scionL) if err := p.buffer.Clear(); err != nil { @@ -2771,7 +2877,7 @@ func (p *scionPacketProcessor) prepareSCMP( scmpLayers := []gopacket.SerializableLayer{&scionL, &scmpH, scmpP} if cause != nil { // add quote for errors. - hdrLen := slayers.CmnHdrLen + scionL.AddrHdrLen() + scionL.Path.Len() + hdrLen := slayers.CmnHdrLen + scionL.AddrHdrLen( /*@ nil, false @*/ ) + scionL.Path.Len( /*@ nil @*/ ) switch scmpH.TypeCode.Type() { case slayers.SCMPTypeExternalInterfaceDown: hdrLen += 20 @@ -2785,10 +2891,10 @@ func (p *scionPacketProcessor) prepareSCMP( if len(quote) > maxQuoteLen { quote = quote[:maxQuoteLen] } - scmpLayers = append(scmpLayers, gopacket.Payload(quote)) + scmpLayers = append( /*@ noPerm, @*/ scmpLayers, gopacket.Payload(quote)) } // XXX(matzf) could we use iovec gather to avoid copying quote? - err = gopacket.SerializeLayers(p.buffer, sopts, scmpLayers...) + err = gopacket.SerializeLayers(p.buffer, sopts /*@ , nil @*/, scmpLayers...) if err != nil { return nil, serrors.Wrap(cannotRoute, err, "details", "serializing SCMP message") } diff --git a/verification/dependencies/encoding/binary/binary.gobra b/verification/dependencies/encoding/binary/binary.gobra index e0cb3d902..8861e78b8 100644 --- a/verification/dependencies/encoding/binary/binary.gobra +++ b/verification/dependencies/encoding/binary/binary.gobra @@ -59,7 +59,7 @@ type bigEndian int (littleEndian) implements ByteOrder -(bigEndian) implements ByteOrder +(bigEndian) implements ByteOrder trusted // related to https://github.com/viperproject/gobra/issues/192 requires acc(&b[0], _) && acc(&b[1], _) @@ -78,7 +78,8 @@ func (e littleEndian) PutUint16(b []byte, v uint16) { trusted // related to https://github.com/viperproject/gobra/issues/192 requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _) -ensures res >= 0 +ensures 0 <= res +ensures res == uint32(b[0]) | uint32(b[1])<<8 | uint32(b[2])<<16 | uint32(b[3])<<24 decreases pure func (e littleEndian) Uint32(b []byte) (res uint32) { return uint32(b[0]) | uint32(b[1])<<8 | uint32(b[2])<<16 | uint32(b[3])<<24 @@ -140,15 +141,30 @@ func (e bigEndian) PutUint16(b []byte, v uint16) { b[1] = byte(v) } +decreases +pure func (e bigEndian) Uint32Spec(b0, b1, b2, b3 byte) (res uint32) { + return uint32(b3) | uint32(b2)<<8 | uint32(b1)<<16 | uint32(b0)<<24 +} + trusted // related to https://github.com/viperproject/gobra/issues/192 requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _) -ensures res >= 0 +ensures 0 <= res +ensures res == BigEndian.Uint32Spec(b[0], b[1], b[2], b[3]) decreases pure func (e bigEndian) Uint32(b []byte) (res uint32) { return uint32(b[3]) | uint32(b[2])<<8 | uint32(b[1])<<16 | uint32(b[0])<<24 } +decreases +pure func (e bigEndian) PutUint32Spec(b0, b1, b2, b3 byte, v uint32) bool { + return b0 == byte(v >> 24) && + b1 == byte(v >> 16) && + b2 == byte(v >> 8) && + b3 == byte(v) +} + preserves acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3]) +ensures BigEndian.PutUint32Spec(b[0], b[1], b[2], b[3], v) decreases func (e bigEndian) PutUint32(b []byte, v uint32) { b[0] = byte(v >> 24) diff --git a/verification/utils/bitwise/bitwise-eqs.gobra b/verification/utils/bitwise/bitwise-eqs.gobra index d703fec6e..605e754b5 100644 --- a/verification/utils/bitwise/bitwise-eqs.gobra +++ b/verification/utils/bitwise/bitwise-eqs.gobra @@ -40,4 +40,16 @@ pure ensures 0 <= b & 0x7 && b & 0x7 <= 7 ensures res == b & 0x7 decreases -func BitAnd7(b int) (res int) \ No newline at end of file +func BitAnd7(b int) (res int) + +ghost +ensures res == b >> 30 +ensures 0 <= res && res <= 3 +decreases +pure func Shift30LessThan4(b uint32) (res uint32) + +ghost +ensures res == b & 0x3F +ensures 0 <= res && res < 64 +decreases +pure func And3fAtMost64(b uint8) (res uint8) \ No newline at end of file diff --git a/verification/utils/bitwise/proofs.dfy b/verification/utils/bitwise/proofs.dfy index bed87c8ed..d788a165f 100644 --- a/verification/utils/bitwise/proofs.dfy +++ b/verification/utils/bitwise/proofs.dfy @@ -9,31 +9,95 @@ // and for when it has 64bit. lemma ByteValue(b: bv8) - ensures 0 <= (b as int) && (b as int) < 256 + ensures 0 <= (b as int) && (b as int) < 256 {} lemma BitAnd3_32bit(b: bv32) - ensures var res := b & 0x3; - 0 <= res && res <= 3 && - (b == 0 ==> res == 0) && - (b == 3 ==> res == 3) && - (b == 4 ==> res == 0) + ensures var res := b & 0x3; + 0 <= res && res <= 3 && + (b == 0 ==> res == 0) && + (b == 3 ==> res == 3) && + (b == 4 ==> res == 0) {} lemma BitAnd3_64bit(b: bv64) - ensures var res := b & 0x3; - 0 <= res <= 3 && - (b == 0 ==> res == 0) && - (b == 3 ==> res == 3) && - (b == 4 ==> res == 0) + ensures var res := b & 0x3; + 0 <= res <= 3 && + (b == 0 ==> res == 0) && + (b == 3 ==> res == 3) && + (b == 4 ==> res == 0) {} lemma BitAnd7_32bit(b: bv32) - ensures var res := b & 0x7; - 0 <= res <= 7 + ensures var res := b & 0x7; + 0 <= res <= 7 {} lemma BitAnd7_64bit(b: bv64) - ensures var res := b & 0x7; - 0 <= res <= 7 -{} \ No newline at end of file + ensures var res := b & 0x7; + 0 <= res <= 7 +{} + +lemma Shift30LessThan4(b: bv32) + ensures var res := b >> 30; + 0 <= res <= 3 +{} + +lemma And3fAtMost64(b: bv8) + ensures var res := b & 0x3F; + 0 <= res < 64 +{} + +datatype MetaHdr = MetaHdr( + CurrINF: bv8, + CurrHF: bv8, + SegLen0: bv8, + SegLen1: bv8, + SegLen2: bv8 +) + +function InBounds(m: MetaHdr): bool { + // each of the following conditions is essential for + // proving SerializeAndDeserializeLemma + 0 <= m.CurrINF <= 3 && + 0 <= m.CurrHF <= 63 && + 0 <= m.SegLen0 <= 63 && + 0 <= m.SegLen1 <= 63 && + 0 <= m.SegLen2 <= 63 +} + +function Uint32Spec(b0: bv8, b1: bv8, b2: bv8, b3: bv8): bv32 { + (b3 as bv32) | ((b2 as bv32)<<8) | ((b1 as bv32)<<16) | ((b0 as bv32)<<24) +} + +function PutUint32Spec(b0: bv8, b1: bv8, b2: bv8, b3: bv8, v: bv32): bool { + var mask: bv32 := 0x000000FF; + && b0 == ((v >> 24) & mask) as bv8 + && b1 == ((v >> 16) & mask) as bv8 + && b2 == ((v >> 8) & mask) as bv8 + && b3 == (v & mask) as bv8 +} + +function DecodedFrom(line: bv32): MetaHdr { + MetaHdr( + (line >> 30) as bv8, + ((line>>24) & 0x3F) as bv8, + ((line>>12) & 0x3F) as bv8, + ((line>>6) & 0x3F) as bv8, + (line & 0x3F) as bv8 + ) +} + +function SerializedToLine(m: MetaHdr): bv32 { + ((m.CurrINF as bv32) << 30) | + (((m.CurrHF & 0x3F) as bv32)<<24) | + (((m.SegLen0 & 0x3F) as bv32) << 12) | + (((m.SegLen1 & 0x3F) as bv32) << 6) | + ((m.SegLen2 & 0x3F) as bv32) +} + +lemma SerializeAndDeserializeLemma(m: MetaHdr, b0: bv8, b1: bv8, b2: bv8, b3: bv8) + requires InBounds(m) + ensures var line := SerializedToLine(m); + PutUint32Spec(b0, b1, b2, b3, line) ==> (DecodedFrom(Uint32Spec(b0, b1, b2, b3)) == m) +{} diff --git a/verification/utils/slices/slices.gobra b/verification/utils/slices/slices.gobra index ecac51a60..b1ba04332 100644 --- a/verification/utils/slices/slices.gobra +++ b/verification/utils/slices/slices.gobra @@ -32,6 +32,14 @@ pred AbsSlice_Bytes(s []byte, start int, end int) { forall i int :: { &s[i] } start <= i && i < end ==> acc(&s[i]) } +pure +requires acc(AbsSlice_Bytes(s, start, end), _) +requires start <= i && i < end +decreases +func GetByte(s []byte, start int, end int, i int) byte { + return unfolding acc(AbsSlice_Bytes(s, start, end), _) in s[i] +} + ghost requires 0 < p requires acc(AbsSliceC_Bytes(s, 0, len(s), contents), p)