Move ownership of underlying slice of SerializableBuffer to outside…

… of `Mem()` (#374)

* fix missing precondition for packSCMP

* progress scmp

* further progress

* further scmp fixes

* fix syntax error and strengthen spec of erros.Is function

* fix verification error

* fix verification errors in process()

* drop last scmp assumption

* fix verification errors in process()

* add missing postconditions to resolveInbound

* fix p.d permissions

* save

* remove wrong precondition from validateEgressUp()

* clean up

* feedback

* change dependencies to new buffer approach

* remove buffWithFullPerm flag from scionPacketProcessor

* fix verification errors

* fix permission mistake

* Apply suggestions from code review

Co-authored-by: João Pereira <[email protected]>

* pass underlying buffer slice to prepareSCMP

* remove deep ownership of buffer slice in message

* fix verification error in run

* fix injectivity issue in run() and verification error in newPacketProcessor

* different trigger

* proves injectivity for message buffer directly without sets

* test: remove unnecessary invariants in run()

* improvements to injectivity lemma for messages

* introduce new lemma PermsImplyIneq()

* fixed missing preconditions

* minor fixes and feedback

* fix verification error

* fmt

---------

Co-authored-by: João Pereira <[email protected]>

pkg/slayers/scion.go

@@ -218,9 +218,11 @@ func (s *SCION) NetworkFlow() (res gopacket.Flow) {
 // @ requires b != nil && b.Mem()
 // @ requires acc(s.Mem(ubuf), R0)
 // @ requires sl.Bytes(ubuf, 0, len(ubuf))
+// @ requires sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
 // @ ensures b.Mem()
 // @ ensures acc(s.Mem(ubuf), R0)
 // @ ensures sl.Bytes(ubuf, 0, len(ubuf))
+// @ ensures sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
 // TODO: hide internal spec details
 // @ ensures e == nil && s.HasOneHopPath(ubuf) ==>
 // @ len(b.UBuf()) == old(len(b.UBuf())) + unfolding acc(s.Mem(ubuf), R55) in
@@ -257,7 +259,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
  }
  // @ ghost uSerBufN := b.UBuf()
  // @ assert buf === uSerBufN[:scnLen]
- // @ b.ExchangePred()
 
  // @ unfold acc(sl.Bytes(uSerBufN, 0, len(uSerBufN)), writePerm)
  // Serialize common header.
@@ -287,7 +288,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
  // @ sl.Unslice_Bytes(uSerBufN, 0, CmnHdrLen, R54)
  // @ sl.CombineRange_Bytes(uSerBufN, CmnHdrLen, scnLen, writePerm)
  // @ sl.CombineRange_Bytes(ubuf, CmnHdrLen, len(ubuf), R10)
- // @ b.RestoreMem(uSerBufN)
  return err
  }
  offset := CmnHdrLen + s.AddrHdrLen( /*@ nil, true @*/ )
@@ -320,7 +320,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO
  // @ sl.CombineRange_Bytes(uSerBufN, offset, scnLen, HalfPerm)
  // @ sl.CombineRange_Bytes(ubuf, startP, endP, HalfPerm)
  // @ reveal IsSupportedPkt(uSerBufN)
- // @ b.RestoreMem(uSerBufN)
  // @ reveal IsSupportedRawPkt(b.View())
  return tmp
 }

pkg/slayers/scmp.go

@@ -111,6 +111,7 @@ func (s *SCMP) NextLayerType( /*@ ghost ub []byte @*/ ) gopacket.LayerType {
 // @ requires b != nil
 // @ requires s.Mem(ubufMem)
 // @ preserves b.Mem()
+// @ preserves sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
 // @ ensures err == nil ==> s.Mem(ubufMem)
 // @ ensures err != nil ==> err.ErrorMem()
 // @ decreases
@@ -121,15 +122,6 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp
  return err
  }
  // @ unfold s.Mem(ubufMem)
-
- // @ requires len(underlyingBufRes) >= 4
- // @ requires bytes === underlyingBufRes[:4]
- // @ requires b != nil
- // @ preserves acc(&s.TypeCode)
- // @ preserves b.Mem() && b.UBuf() === underlyingBufRes
- // @ decreases
- // @ outline (
- // @ b.ExchangePred()
  // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm)
  // @ unfold sl.Bytes(underlyingBufRes, 0, 2)
  // @ assert forall i int :: { &bytes[i] } 0 <= i && i < 2 ==> &bytes[i] == &underlyingBufRes[i]
@@ -138,59 +130,37 @@ func (s *SCMP) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOp
  // @ unfold sl.Bytes(bytes, 0, 2)
  // @ fold sl.Bytes(underlyingBufRes, 0, 2)
  // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 2, writePerm)
- // @ b.RestoreMem(underlyingBufRes)
- // @ )
 
  if opts.ComputeChecksums {
  if s.scn == nil {
  // @ fold s.Mem(ubufMem)
  return serrors.New("can not calculate checksum without SCION header")
  }
  // zero out checksum bytes
- // @ requires len(underlyingBufRes) >= 4
- // @ requires bytes === underlyingBufRes[:4]
- // @ requires b != nil
- // @ preserves b.Mem() && b.UBuf() === underlyingBufRes
- // @ decreases
- // @ outline (
- // @ b.ExchangePred()
  // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
  // @ unfold sl.Bytes(underlyingBufRes, 0, 4)
  // @ assert forall i int :: { &bytes[i] } 0 <= i && i < 4 ==> &bytes[i] == &underlyingBufRes[i]
  bytes[2] = 0
  bytes[3] = 0
  // @ fold sl.Bytes(underlyingBufRes, 0, 4)
  // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
- // @ b.RestoreMem(underlyingBufRes)
- // @ )
  verScionTmp := b.Bytes()
  // @ unfold s.scn.ChecksumMem()
  s.Checksum, err = s.scn.computeChecksum(verScionTmp, uint8(L4SCMP))
  // @ fold s.scn.ChecksumMem()
- // @ b.RestoreMem(verScionTmp)
  if err != nil {
  // @ fold s.Mem(ubufMem)
  return err
  }
 
  }
- // @ requires len(underlyingBufRes) >= 4
- // @ requires bytes === underlyingBufRes[:4]
- // @ requires b != nil
- // @ preserves acc(&s.Checksum)
- // @ preserves b.Mem() && b.UBuf() === underlyingBufRes
- // @ decreases
- // @ outline (
- // @ b.ExchangePred()
  // @ sl.SplitByIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
  // @ unfold sl.Bytes(underlyingBufRes, 0, 4)
  // @ assert forall i int :: { &bytes[i] } 0 <= i && i < 4 ==> &bytes[i] == &underlyingBufRes[i]
  // @ assert forall i int :: { &bytes[2:][i] } 0 <= i && i < 2 ==> &bytes[2:][i] == &bytes[i + 2]
  binary.BigEndian.PutUint16(bytes[2:], s.Checksum)
  // @ fold sl.Bytes(underlyingBufRes, 0, 4)
  // @ sl.CombineAtIndex_Bytes(underlyingBufRes, 0, len(underlyingBufRes), 4, writePerm)
- // @ b.RestoreMem(underlyingBufRes)
- // @ )
  // @ fold s.Mem(ubufMem)
  return nil
 }