Move ownership of underlying slice of SerializableBuffer to outside of Mem()
#374
Conversation
|
This PR also addresses the second TODO mentioned in PR #139 |
verification/dependencies/github.com/google/gopacket/writer.gobra
Outdated
Show resolved
Hide resolved
verification/dependencies/github.com/google/gopacket/writer.gobra
Outdated
Show resolved
Hide resolved
Co-authored-by: João Pereira <[email protected]>
jcp19
changed the title
PackSCMP with weaker buffer invariantSerializableBuffer to outside of Mem()
verification/dependencies/golang.org/x/net/internal/socket/socket.gobra
Outdated
Show resolved
Hide resolved
verification/dependencies/golang.org/x/net/internal/socket/socket.gobra
Outdated
Show resolved
Hide resolved
router/dataplane.go
Outdated
| @@ -121,6 +121,8 @@ type BatchConn interface { | |||
| // @ requires acc(Mem(), _) | |||
| // @ requires forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> | |||
| // @ msgs[i].Mem() | |||
| // @ requires forall j int :: { &msgs[j] } (0 <= j && j < len(msgs)) ==> | |||
There was a problem hiding this comment.
I will look at this file again when my comments are addressed
pkg/scrypto/scrypto_spec.gobra
Outdated
| @@ -28,12 +28,15 @@ import sl "github.com/scionproto/scion/verification/utils/slices" | |||
| // ghost function. | |||
| ghost | |||
| requires acc(sl.Bytes(key, 0, len(key)), _) | |||
| requires len(key) > 0 | |||
| decreases _ | |||
| pure func ValidKeyForHash(key []byte) bool | |||
There was a problem hiding this comment.
Why do we not specify any criteria on the length of key? I looked at the implementation of InitMac() and it seems that it will only return a new hash if the length of key is either 16, 24, or 32 bytes. Hence requiring len(key) > 0 cannot cause any problems?
There was a problem hiding this comment.
Well, while that it is true, this restriction is not documented anywhere; as such, this might be an implementation detail, which should not be leaked in the specification. Passing a key of size 0 sounds non-sensical, but that is only one of the criteria that one might think for this.
Why is adding this restriction here useful? If it is not, then I would drop the restriction, considering that this case is still correctly handled by the implementation, which returns a non-nil error in that case
There was a problem hiding this comment.
We need to ensure that either len(verScionTmp.UBuf) > 0 or len(d.key) > 0 in newPacketProcessor() (dataplane.go) holds. We know from NewSerializeBuffer() that len(verScionTmp.UBuf) == 0. This means the condition len(d.key) > 0 must hold, passed via dataplane.Mem() in run(). The minimal required change is to add len(d.key) > 0 to dataplane.Mem(). So adding it to ValidKeyForHash() is optional. I just thought it would make it clearer why we need it in dataplane.Mem(). If you think it is better to remove it let me know.
There was a problem hiding this comment.
Hmm, I see. Would this still be necessary if we changed the post of PermsImplyIneqWithWildcard from s1 !== s2 to len(s1) > 0 || len(s2) > 0 ==> s1 !== s2 and dropped the precondition that len(s1) > 0 || len(s2) > 0?
Would this new contract be sufficient to prove function newPacketProcessor?
There was a problem hiding this comment.
No, unfortunately this is still not strong enough. So far I don't see a way without requiring len(d.key) > 0 in dataplane.Mem().
| unfold Bytes(s1, 0, len(s1)) | ||
| unfold acc(Bytes(s2, 0, len(s2)), _) | ||
| if len(s1) > 0 && len(s2) > 0 { | ||
| assert &s1[0] != &s2[0] |
There was a problem hiding this comment.
Can you add a comment explaining that you have this here to trigger the qtfier bodies?
pkg/scrypto/scrypto_spec.gobra
Outdated
| @@ -28,12 +28,15 @@ import sl "github.com/scionproto/scion/verification/utils/slices" | |||
| // ghost function. | |||
| ghost | |||
| requires acc(sl.Bytes(key, 0, len(key)), _) | |||
| requires len(key) > 0 | |||
| decreases _ | |||
| pure func ValidKeyForHash(key []byte) bool | |||
There was a problem hiding this comment.
Well, while that it is true, this restriction is not documented anywhere; as such, this might be an implementation detail, which should not be leaked in the specification. Passing a key of size 0 sounds non-sensical, but that is only one of the criteria that one might think for this.
Why is adding this restriction here useful? If it is not, then I would drop the restriction, considering that this case is still correctly handled by the implementation, which returns a non-nil error in that case
pkg/scrypto/scrypto_spec.gobra
Outdated
| @@ -28,12 +28,15 @@ import sl "github.com/scionproto/scion/verification/utils/slices" | |||
| // ghost function. | |||
| ghost | |||
| requires acc(sl.Bytes(key, 0, len(key)), _) | |||
| requires len(key) > 0 | |||
| decreases _ | |||
| pure func ValidKeyForHash(key []byte) bool | |||
There was a problem hiding this comment.
Hmm, I see. Would this still be necessary if we changed the post of PermsImplyIneqWithWildcard from s1 !== s2 to len(s1) > 0 || len(s2) > 0 ==> s1 !== s2 and dropped the precondition that len(s1) > 0 || len(s2) > 0?
Would this new contract be sufficient to prove function newPacketProcessor?
|
(I have a few minor comments, after which it should be ok to merge this PR) |
* start * make type-check * backup * fix syntax errors * establish necessary precondition of DecodeFromBytes * remove TODOs * backup * move on with proof obligations * verify packSCMP; reinstate TODO()s for doing the proof step by step * backup * backup * fix parse and type errors * fix packscmp * backup * backup * kill branches for now * backup * backup * remove files pushed by mistake * del file * fix verification error * change comment format * backup * reset changes to scion_spec.gobra * continue making progress * backup * simplify spec * backup * non-termination again * backup * packSCMP Continued (#373) * 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 * remove wrong precondition from validateEgressUp() * clean up * feedback * Update router/dataplane.go --------- Co-authored-by: João Pereira <[email protected]> * 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]> --------- Co-authored-by: Markus Limbeck <[email protected]>
No description provided.