From 3847c393018e6950710a59c9154074d517731aff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 22 Nov 2021 15:17:05 +0100 Subject: [PATCH 1/4] Backup progress --- gobra/lib/slayers/scion.gobra | 94 +++++++++++++++++++++-------------- 1 file changed, 57 insertions(+), 37 deletions(-) diff --git a/gobra/lib/slayers/scion.gobra b/gobra/lib/slayers/scion.gobra index 198b30893..633493cfe 100644 --- a/gobra/lib/slayers/scion.gobra +++ b/gobra/lib/slayers/scion.gobra @@ -509,7 +509,7 @@ pure func (s *SCION) getPathLen() (ret int) /* { // (joao) Partially Verified requires s.Mem() && b.Mem() ensures retErr == nil ==> s.Mem() && b.Mem() -func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions) (retErr error) { +func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions) (retErr error) /*{ scnLen := CmnHdrLen + s.AddrHdrLen() + s.getPathLen() buf, err := b.PrependBytes(scnLen) if err != nil { @@ -571,6 +571,7 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO fold verifyutils.BytesAcc(buf) b.CombinePrependBytesMem(buf) } +*/ preserves s.Mem() preserves forall i int :: 0 <= i && i < len(buf) ==> acc(&buf[i]) @@ -591,19 +592,25 @@ requires acc(s) && df.Mem() requires forall i int :: 0 <= i && i < len(data) ==> acc(&data[i]) ensures df.Mem() ensures errRes == nil ==> s.Mem() -func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes error) /* { +func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes error) { // Decode common header. if len(data) < CmnHdrLen { df.SetTruncated() 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) @@ -612,10 +619,13 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes s.SrcAddrLen = AddrLen(data[9] & 0x3) // 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 } + assume false + /* addrHdrLen := s.AddrHdrLen() offset := CmnHdrLen + addrHdrLen @@ -668,12 +678,14 @@ func (s *SCION) DecodeFromBytes(data []byte, df gopacket.DecodeFeedback) (errRes s.Payload = data[hdrBytes:] return nil + */ } -*/ // (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 { @@ -681,7 +693,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()) } */ @@ -730,7 +744,7 @@ func (s *SCION) DstAddr() (resAddr net.Addr, resErr error) { unfold acc(s.Mem(), 1/200) // (joao) this call used to be part of the return statement res, err := parseAddr(s.DstAddrType, s.DstAddrLen, s.RawDstAddr) - assume err == nil ==> s.ReadDstAddr(res) + inhale err == nil ==> s.ReadDstAddr(res) return res, err } @@ -751,13 +765,14 @@ func (s *SCION) AddReadSrcAddr(addr net.Addr) // address. requires acc(s.Mem(), 1/200) ensures resErr == nil ==> acc(resAddr.Mem(), 1/200) && s.ReadSrcAddr(resAddr) -func (s *SCION) SrcAddr() (resAddr net.Addr, resErr error) { +func (s *SCION) SrcAddr() (resAddr net.Addr, resErr error) /*{ unfold acc(s.Mem(), 1/200) // (joao) this call used to be part of the return statement res, err := parseAddr(s.SrcAddrType, s.SrcAddrLen, s.RawSrcAddr) - assume err == nil ==> s.ReadSrcAddr(res) + inhale err == nil ==> s.ReadSrcAddr(res) return res, err } +*/ // (joao) Verified // SetDstAddr sets the destination address and updates the DstAddrLen/Type fields accordingly. @@ -765,7 +780,7 @@ func (s *SCION) SrcAddr() (resAddr net.Addr, resErr error) { // Changes to dst might leave the layer in an inconsistent state. requires s.Mem() && dst.Mem() ensures ret == nil ==> s.Mem() -func (s *SCION) SetDstAddr(dst net.Addr) (ret error) { +func (s *SCION) SetDstAddr(dst net.Addr) (ret error) /* { unfold s.Mem() var err error s.DstAddrLen, s.DstAddrType, s.RawDstAddr, err = packAddr(dst) @@ -778,6 +793,7 @@ func (s *SCION) SetDstAddr(dst net.Addr) (ret error) { } return err } +*/ // 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. @@ -785,7 +801,7 @@ func (s *SCION) SetDstAddr(dst net.Addr) (ret error) { // (joao) Verified requires s.Mem() && src.Mem() ensures ret == nil ==> s.Mem() -func (s *SCION) SetSrcAddr(src net.Addr) (ret error) { +func (s *SCION) SetSrcAddr(src net.Addr) (ret error) /* { var err error unfold s.Mem() s.SrcAddrLen, s.SrcAddrType, s.RawSrcAddr, err = packAddr(src) @@ -798,6 +814,7 @@ func (s *SCION) SetSrcAddr(src net.Addr) (ret error) { } return err } +*/ requires addrLen == AddrLen4 ==> len(raw) == 4 requires addrLen == AddrLen16 ==> len(raw) == 16 @@ -806,7 +823,7 @@ ensures addrLen != AddrLen4 && addrLen != AddrLen16 ==> resErr != nil ensures (addrLen == AddrLen4 && (addrType == T4Ip || addrType == T4Svc)) ==> resErr == nil ensures (addrLen == AddrLen16 && addrType == T16Ip) ==> resErr == nil ensures resErr == nil ==> acc(resAddr.Mem(), 1/200) -func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr, resErr error) { +func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr, resErr error) /*{ switch addrLen { case AddrLen4: switch addrType { @@ -840,7 +857,9 @@ func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr return nil, serrors.New("unsupported address type/length combination", "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 @@ -886,7 +905,7 @@ preserves acc(s.Mem(), 1/100) preserves forall i int :: 0 <= i && i < len(buf) ==> acc(&buf[i]) ensures len(buf) >= s.AddrHdrLen() ==> err == nil ensures len(buf) < s.AddrHdrLen() ==> err != nil -func (s *SCION) SerializeAddrHdr(buf []byte) (err error) { +func (s *SCION) SerializeAddrHdr(buf []byte) (err error) /*{ if len(buf) < s.AddrHdrLen() { return serrors.New("provided buffer is too small", "expected", s.AddrHdrLen(), "actual", len(buf)) @@ -924,13 +943,14 @@ func (s *SCION) SerializeAddrHdr(buf []byte) (err error) { copyRawSrcAddr(s, buf[offset:offset+srcAddrBytes]) 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]) 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) @@ -941,13 +961,11 @@ 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]) 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) @@ -956,16 +974,15 @@ 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)) +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 @@ -978,9 +995,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:]) @@ -992,14 +1007,14 @@ 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] + assume false + 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 } */ @@ -1011,7 +1026,7 @@ preserves forall j int :: 0 <= j && j < len(upperLayer) ==> acc(&upperLayer[j], ensures retErr != nil ==> ret == 0 ensures s == nil ==> retErr != nil ensures s != nil && s.getLenRawSrcAddr() > 0 && s.getLenRawDstAddr() > 0 ==> retErr == nil -func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (ret uint16, retErr error) { +func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (ret uint16, retErr error) /*{ if s == nil { return 0, serrors.New("SCION header missing") } @@ -1023,6 +1038,7 @@ func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (ret uint16, folded := s.foldChecksum(csum) return folded, nil } +*/ // (joao) Verified requires acc(s.Mem(), 1/100) @@ -1030,7 +1046,7 @@ ensures acc(s.Mem(), 1/100) ensures s.getLenRawSrcAddr() == 0 ==> resErr != nil ensures s.getLenRawDstAddr() == 0 ==> resErr != nil ensures s.getLenRawSrcAddr() > 0 && s.getLenRawDstAddr() > 0 ==> resErr == nil -func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (resUint uint32, resErr error) { +func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (resUint uint32, resErr error) /*{ // (joao) len(s.RawDstAddr) replaced by s.getLenRawDstAddr() to avoid unfoldings // if len(s.RawDstAddr) == 0 { if s.getLenRawDstAddr() == 0 { @@ -1107,6 +1123,7 @@ func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (resUint uint32 csum += uint32(protocol) return csum, nil } +*/ // (joao) Verified requires len(srcIA) == 8 && len(dstIA) == 8 @@ -1116,7 +1133,7 @@ requires forall i int :: 0 <= i && i < 8 ==> acc(&dstIA[i]) ensures acc(s.Mem(), 1/200) ensures forall i int :: 0 <= i && i < 8 ==> acc(&srcIA[i]) ensures forall i int :: 0 <= i && i < 8 ==> acc(&dstIA[i]) -func (s *SCION) pseudoHeaderChecksumOutlineBlock1(srcIA []byte, dstIA []byte) { +func (s *SCION) pseudoHeaderChecksumOutlineBlock1(srcIA []byte, dstIA []byte) /*{ // (joao) Original code, omitted to avoid unfolding // s.SrcIA.Write(srcIA) (s.getSrcIA()).Write(srcIA) @@ -1124,11 +1141,12 @@ func (s *SCION) pseudoHeaderChecksumOutlineBlock1(srcIA []byte, dstIA []byte) { // s.DstIA.Write(dstIA) (s.getDstIA()).Write(srcIA) } +*/ // (joao) Verified requires forall j int :: 0 <= j && j < len(upperLayer) ==> acc(&upperLayer[j], 1/10000) ensures forall j int :: 0 <= j && j < len(upperLayer) ==> acc(&upperLayer[j], 1/10000) -func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 { +func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 /*{ // Compute safe boundary to ensure we do not access out of bounds. // Odd lengths are handled at the end. safeBoundary := len(upperLayer) - 1 @@ -1144,11 +1162,13 @@ func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 { } return csum } +*/ // (joao) Verified -func (s *SCION) foldChecksum(csum uint32) uint16 { +func (s *SCION) foldChecksum(csum uint32) uint16 /*{ for csum > 0xffff { csum = (csum >> 16) + (csum & 0xffff) } return ^uint16(csum) -} \ No newline at end of file +} +*/ \ No newline at end of file From a7749da535c5ab0249b5a76ed46862edc52e151d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 23 Nov 2021 18:06:35 +0100 Subject: [PATCH 2/4] Uncomment verified methods --- gobra/lib/slayers/scion.gobra | 42 +++++++++++++---------------------- 1 file changed, 15 insertions(+), 27 deletions(-) diff --git a/gobra/lib/slayers/scion.gobra b/gobra/lib/slayers/scion.gobra index 633493cfe..4c28f5e6d 100644 --- a/gobra/lib/slayers/scion.gobra +++ b/gobra/lib/slayers/scion.gobra @@ -509,7 +509,7 @@ pure func (s *SCION) getPathLen() (ret int) /* { // (joao) Partially Verified requires s.Mem() && b.Mem() ensures retErr == nil ==> s.Mem() && b.Mem() -func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions) (retErr error) /*{ +func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeOptions) (retErr error) { scnLen := CmnHdrLen + s.AddrHdrLen() + s.getPathLen() buf, err := b.PrependBytes(scnLen) if err != nil { @@ -571,7 +571,6 @@ func (s *SCION) SerializeTo(b gopacket.SerializeBuffer, opts gopacket.SerializeO fold verifyutils.BytesAcc(buf) b.CombinePrependBytesMem(buf) } -*/ preserves s.Mem() preserves forall i int :: 0 <= i && i < len(buf) ==> acc(&buf[i]) @@ -618,13 +617,13 @@ 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 } - assume false /* addrHdrLen := s.AddrHdrLen() offset := CmnHdrLen + addrHdrLen @@ -765,14 +764,13 @@ func (s *SCION) AddReadSrcAddr(addr net.Addr) // address. requires acc(s.Mem(), 1/200) ensures resErr == nil ==> acc(resAddr.Mem(), 1/200) && s.ReadSrcAddr(resAddr) -func (s *SCION) SrcAddr() (resAddr net.Addr, resErr error) /*{ +func (s *SCION) SrcAddr() (resAddr net.Addr, resErr error) { unfold acc(s.Mem(), 1/200) // (joao) this call used to be part of the return statement res, err := parseAddr(s.SrcAddrType, s.SrcAddrLen, s.RawSrcAddr) inhale err == nil ==> s.ReadSrcAddr(res) return res, err } -*/ // (joao) Verified // SetDstAddr sets the destination address and updates the DstAddrLen/Type fields accordingly. @@ -780,7 +778,7 @@ func (s *SCION) SrcAddr() (resAddr net.Addr, resErr error) /*{ // Changes to dst might leave the layer in an inconsistent state. requires s.Mem() && dst.Mem() ensures ret == nil ==> s.Mem() -func (s *SCION) SetDstAddr(dst net.Addr) (ret error) /* { +func (s *SCION) SetDstAddr(dst net.Addr) (ret error) { unfold s.Mem() var err error s.DstAddrLen, s.DstAddrType, s.RawDstAddr, err = packAddr(dst) @@ -793,15 +791,14 @@ 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) /* { +func (s *SCION) SetSrcAddr(src net.Addr) (ret error) { var err error unfold s.Mem() s.SrcAddrLen, s.SrcAddrType, s.RawSrcAddr, err = packAddr(src) @@ -814,7 +811,6 @@ func (s *SCION) SetSrcAddr(src net.Addr) (ret error) /* { } return err } -*/ requires addrLen == AddrLen4 ==> len(raw) == 4 requires addrLen == AddrLen16 ==> len(raw) == 16 @@ -823,7 +819,7 @@ ensures addrLen != AddrLen4 && addrLen != AddrLen16 ==> resErr != nil ensures (addrLen == AddrLen4 && (addrType == T4Ip || addrType == T4Svc)) ==> resErr == nil ensures (addrLen == AddrLen16 && addrType == T16Ip) ==> resErr == nil ensures resErr == nil ==> acc(resAddr.Mem(), 1/200) -func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr, resErr error) /*{ +func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr, resErr error) { switch addrLen { case AddrLen4: switch addrType { @@ -857,7 +853,6 @@ func parseAddr(addrType AddrType, addrLen AddrLen, raw []byte) (resAddr net.Addr return nil, serrors.New("unsupported address type/length combination", "type", addrType, "len", addrLen) } -*/ // TODO: verify with assumption // (joao) Assumed @@ -905,7 +900,7 @@ preserves acc(s.Mem(), 1/100) preserves forall i int :: 0 <= i && i < len(buf) ==> acc(&buf[i]) ensures len(buf) >= s.AddrHdrLen() ==> err == nil ensures len(buf) < s.AddrHdrLen() ==> err != nil -func (s *SCION) SerializeAddrHdr(buf []byte) (err error) /*{ +func (s *SCION) SerializeAddrHdr(buf []byte) (err error) { if len(buf) < s.AddrHdrLen() { return serrors.New("provided buffer is too small", "expected", s.AddrHdrLen(), "actual", len(buf)) @@ -943,7 +938,6 @@ func (s *SCION) SerializeAddrHdr(buf []byte) (err error) /*{ copyRawSrcAddr(s, buf[offset:offset+srcAddrBytes]) return nil } -*/ // (joao) verification does not terminate // (joao) function introduced for verification purposes @@ -983,7 +977,7 @@ requires forall i int :: 0 <= i && i < len(data) ==> acc(&data[i]) ensures acc(s) && validAddrLen(s.SrcAddrLen) && validAddrLen(s.DstAddrLen) 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) /* { +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 @@ -1017,7 +1011,6 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) /* { fold verifyutils.BytesAcc(s.RawSrcAddr) return nil } -*/ // (joao) Verified // computeChecksum computes the checksum with the SCION pseudo header. @@ -1026,7 +1019,7 @@ preserves forall j int :: 0 <= j && j < len(upperLayer) ==> acc(&upperLayer[j], ensures retErr != nil ==> ret == 0 ensures s == nil ==> retErr != nil ensures s != nil && s.getLenRawSrcAddr() > 0 && s.getLenRawDstAddr() > 0 ==> retErr == nil -func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (ret uint16, retErr error) /*{ +func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (ret uint16, retErr error) { if s == nil { return 0, serrors.New("SCION header missing") } @@ -1038,7 +1031,6 @@ func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (ret uint16, folded := s.foldChecksum(csum) return folded, nil } -*/ // (joao) Verified requires acc(s.Mem(), 1/100) @@ -1046,7 +1038,7 @@ ensures acc(s.Mem(), 1/100) ensures s.getLenRawSrcAddr() == 0 ==> resErr != nil ensures s.getLenRawDstAddr() == 0 ==> resErr != nil ensures s.getLenRawSrcAddr() > 0 && s.getLenRawDstAddr() > 0 ==> resErr == nil -func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (resUint uint32, resErr error) /*{ +func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (resUint uint32, resErr error) { // (joao) len(s.RawDstAddr) replaced by s.getLenRawDstAddr() to avoid unfoldings // if len(s.RawDstAddr) == 0 { if s.getLenRawDstAddr() == 0 { @@ -1123,7 +1115,6 @@ func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (resUint uint32 csum += uint32(protocol) return csum, nil } -*/ // (joao) Verified requires len(srcIA) == 8 && len(dstIA) == 8 @@ -1133,7 +1124,7 @@ requires forall i int :: 0 <= i && i < 8 ==> acc(&dstIA[i]) ensures acc(s.Mem(), 1/200) ensures forall i int :: 0 <= i && i < 8 ==> acc(&srcIA[i]) ensures forall i int :: 0 <= i && i < 8 ==> acc(&dstIA[i]) -func (s *SCION) pseudoHeaderChecksumOutlineBlock1(srcIA []byte, dstIA []byte) /*{ +func (s *SCION) pseudoHeaderChecksumOutlineBlock1(srcIA []byte, dstIA []byte) { // (joao) Original code, omitted to avoid unfolding // s.SrcIA.Write(srcIA) (s.getSrcIA()).Write(srcIA) @@ -1141,12 +1132,11 @@ func (s *SCION) pseudoHeaderChecksumOutlineBlock1(srcIA []byte, dstIA []byte) /* // s.DstIA.Write(dstIA) (s.getDstIA()).Write(srcIA) } -*/ // (joao) Verified requires forall j int :: 0 <= j && j < len(upperLayer) ==> acc(&upperLayer[j], 1/10000) ensures forall j int :: 0 <= j && j < len(upperLayer) ==> acc(&upperLayer[j], 1/10000) -func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 /*{ +func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 { // Compute safe boundary to ensure we do not access out of bounds. // Odd lengths are handled at the end. safeBoundary := len(upperLayer) - 1 @@ -1162,13 +1152,11 @@ func (s *SCION) upperLayerChecksum(upperLayer []byte, csum uint32) uint32 /*{ } return csum } -*/ // (joao) Verified -func (s *SCION) foldChecksum(csum uint32) uint16 /*{ +func (s *SCION) foldChecksum(csum uint32) uint16 { for csum > 0xffff { csum = (csum >> 16) + (csum & 0xffff) } return ^uint16(csum) -} -*/ \ No newline at end of file +} \ No newline at end of file From d0f5fdfacfec5dfee9b8ed20055661db4bb37d97 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 23 Nov 2021 22:50:05 +0100 Subject: [PATCH 3/4] Remove assume false --- gobra/lib/slayers/scion.gobra | 1 - 1 file changed, 1 deletion(-) diff --git a/gobra/lib/slayers/scion.gobra b/gobra/lib/slayers/scion.gobra index a78f97517..304afd4bb 100644 --- a/gobra/lib/slayers/scion.gobra +++ b/gobra/lib/slayers/scion.gobra @@ -1092,7 +1092,6 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) { s.RawDstAddr = data[offset : offset+dstAddrBytes] fold verifyutils.BytesAcc(s.RawDstAddr) offset += dstAddrBytes - assume false 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) From 6ba7643e325c4212941c42ee1a95e5a3b140295d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 24 Nov 2021 11:39:32 +0100 Subject: [PATCH 4/4] Increase timeouts --- .github/workflows/test.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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