diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index ea58acfea..16fa03626 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -22,6 +22,6 @@ jobs: with: imageVersion: verified-scion-preview-without-selective packageLocation: gobra - globalTimeout: 4h - packageTimeout: 2h + globalTimeout: 6h + packageTimeout: 4h diff --git a/gobra/lib/slayers/scion.gobra b/gobra/lib/slayers/scion.gobra index 02a60cee2..304afd4bb 100644 --- a/gobra/lib/slayers/scion.gobra +++ b/gobra/lib/slayers/scion.gobra @@ -677,12 +677,18 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes return serrors.New("packet is shorter than the common header length", "min", CmnHdrLen, "actual", len(data)) } - firstLine := binary.BigEndian.Uint32(data[:4]) + assert &data[0:4][0] == &data[0] + assert &data[0:4][1] == &data[1] + assert &data[0:4][2] == &data[2] + assert &data[0:4][3] == &data[3] + firstLine := binary.BigEndian.Uint32(data[0:4]) s.Version = uint8(firstLine >> 28) s.TrafficClass = uint8((firstLine >> 20) & 0xFF) s.FlowID = firstLine & 0xFFFFF s.NextHdr = common.L4ProtocolType(data[4]) s.HdrLen = data[5] + assert &data[6:8][0] == &data[6] + assert &data[6:8][1] == &data[7] s.PayloadLen = binary.BigEndian.Uint16(data[6:8]) s.PathType = PathType(data[8]) s.DstAddrType = AddrType(data[9] >> 6) @@ -690,11 +696,14 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes s.SrcAddrType = AddrType(data[9] >> 2 & 0x3) s.SrcAddrLen = AddrLen(data[9] & 0x3) + assume false // Decode address header. + assert forall i int :: 0 <= i && i < len(data[CmnHdrLen:]) ==> &data[CmnHdrLen:][i] == &data[CmnHdrLen+i] if err := s.DecodeAddrHdr(data[CmnHdrLen:]); err != nil { df.SetTruncated() return err } + /* addrHdrLen := s.AddrHdrLen() offset := CmnHdrLen + addrHdrLen @@ -753,9 +762,10 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes } */ - // (joao) ignored for now, not used in this file -/* func decodeSCION(data []byte, pb gopacket.PacketBuilder) error { +requires pb.Mem() +requires forall i int :: 0 <= i && i < len(data) ==> acc(&data[i]) +func decodeSCION(data []byte, pb gopacket.PacketBuilder) error /* { scn := &SCION{} err := scn.DecodeFromBytes(data, pb) if err != nil { @@ -763,7 +773,9 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes } pb.AddLayer(scn) pb.SetNetworkLayer(scn) - return pb.NextDecoder(scionNextLayerType(scn.NextHdr)) + // rewrote the following + // return pb.NextDecoder(scionNextLayerType(scn.NextHdr)) + return pb.NextDecoder(s.NextLayerType()) } */ @@ -861,10 +873,10 @@ func (s *SCION) SetDstAddr(dst net.Addr) (ret error) { return err } +// (joao) Verified // SetSrcAddr sets the source address and updates the DstAddrLen/Type fields accordingly. // SetSrcAddr takes ownership of src and callers should not write to it after calling SetSrcAddr. // Changes to src might leave the layer in an inconsistent state. -// (joao) Verified requires s.Mem() && src.Mem() ensures ret == nil ==> s.Mem() func (s *SCION) SetSrcAddr(src net.Addr) (ret error) { @@ -923,6 +935,7 @@ func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr "type", addrType, "len", addrLen) } +// TODO: verify with assumption // (joao) Assumed // (joao) Verify this next // (joao) requires implementation proof that IPAddr implements Addr to verify the body @@ -1009,14 +1022,14 @@ func (s *SCION) SerializeAddrHdr(buf []byte) (err error) { return nil } -// (joao) Assumed -// (joao) function not present in the original code +// (joao) verification does not terminate +// (joao) function introduced for verification purposes preserves acc(s.Mem(), 1/1000) preserves forall i int :: 0 <= i && i < len(b) ==> acc(&b[i]) ensures (old(s.getRawPkt()) == s.getRawPkt()) && (old(s.getRawScionPath()) == s.getRawScionPath()) decreases func copyRawDstAddr(s *SCION, b []byte) /* { - // (joao) without this assumption, verification does not terminate + // (joao) verification does not terminate assume false unfold acc(s.Mem(), 1/1000) unfold acc(verifyutils.BytesAcc(s.RawDstAddr), 1/10000) @@ -1027,15 +1040,13 @@ func copyRawDstAddr(s *SCION, b []byte) /* { } */ -// (joao) Assumed -// (joao) function not present in the original code +// (joao) verification does not terminate +// (joao) function introduced for verification purposes preserves acc(s.Mem(), 1/1000) preserves forall i int :: 0 <= i && i < len(b) ==> acc(&b[i]) ensures (old(s.getRawPkt()) == s.getRawPkt()) && (old(s.getRawScionPath()) == s.getRawScionPath()) decreases func copyRawSrcAddr(s *SCION, b []byte) /* { - // (joao) without this assumption, verification does not terminate - assume false unfold acc(s.Mem(), 1/1000) unfold acc(verifyutils.BytesAcc(s.RawSrcAddr), 1/10000) verifyutils.OutlineMemorySafeCopy(b, s.RawSrcAddr) @@ -1044,17 +1055,16 @@ func copyRawSrcAddr(s *SCION, b []byte) /* { } */ -// (joao) TODO: remake this spec -// (joao) Assumed for now +// (joao) Verification takes too long // DecodeAddrHdr decodes the destination and source ISD-AS-Host address triples from the provided // buffer. The caller must ensure that the correct address types and lengths are set in the SCION // layer, otherwise the results of this method are undefined. requires acc(s) && validAddrLen(s.SrcAddrLen) && validAddrLen(s.DstAddrLen) requires forall i int :: 0 <= i && i < len(data) ==> acc(&data[i]) ensures acc(s) && validAddrLen(s.SrcAddrLen) && validAddrLen(s.DstAddrLen) -// (joao) uncommenting the following post-condition increases verification time from ~4min to ~26 -// ensures res == nil ==> (verifyutils.BytesAcc(s.RawSrcAddr) && verifyutils.BytesAcc(s.RawDstAddr) && validSrcAddr(s) && validDstAddr(s)) -func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* { +ensures res == nil ==> verifyutils.BytesAcc(s.RawSrcAddr) && len(s.RawSrcAddr) == addrBytes(s.SrcAddrLen) +ensures res == nil ==> verifyutils.BytesAcc(s.RawDstAddr) && len(s.RawDstAddr) == addrBytes(s.DstAddrLen) +func (s *SCION) DecodeAddrHdr(data []byte) (res error) { assert addrBytes(s.DstAddrLen) >= 0 assert addrBytes(s.SrcAddrLen) >= 0 // (joao) inline calls to s.AddrHdrLen due to missing s.Mem() permission @@ -1066,9 +1076,7 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* { return serrors.New("provided buffer is too small", "expected", 2*addr.IABytes + addrBytes(s.DstAddrLen) + addrBytes(s.SrcAddrLen), "actual", len(data)) } - assume false offset := 0 - unfold s.Mem() assert len(data[offset:]) == len(data) assert forall i int :: 0 <= i && i < len(data[offset:]) ==> &(data[offset:])[i] == &data[offset + i] s.DstIA = addr.IAFromRaw(data[offset:]) @@ -1080,17 +1088,15 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* { dstAddrBytes := addrBytes(s.DstAddrLen) srcAddrBytes := addrBytes(s.SrcAddrLen) assert len(data) >= 2 * addr.IABytes + srcAddrBytes + dstAddrBytes - assume false - assert len(data[offset:]) == len(data) - offset - assert forall i int :: 0 <= i && i < len(data[offset:]) ==> &(data[offset:])[i] == &data[offset + i] + assert forall i int :: 0 <= i && i < len(data[offset:offset+dstAddrBytes]) ==> &(data[offset:offset+dstAddrBytes])[i] == &data[offset + i] s.RawDstAddr = data[offset : offset+dstAddrBytes] + fold verifyutils.BytesAcc(s.RawDstAddr) offset += dstAddrBytes - assert len(data[offset:]) == len(data) - offset - assert forall i int :: 0 <= i && i < len(data[offset:]) ==> &(data[offset:])[i] == &data[offset + i] + assert forall i int :: 0 <= i && i < len(data[offset:offset+srcAddrBytes]) ==> &(data[offset:offset+srcAddrBytes])[i] == &data[offset + i] s.RawSrcAddr = data[offset : offset+srcAddrBytes] + fold verifyutils.BytesAcc(s.RawSrcAddr) return nil } -*/ // (joao) Verified // computeChecksum computes the checksum with the SCION pseudo header.