Conversation
verification/scratch/mwe1/mwe1.gobra
Outdated
| type Collect domain { | ||
| func Post(ClassificationSpec, Trace) ObservationTrace | ||
| func Pre(ClassificationSpec, Trace) ObservationTrace | ||
| func pre_(Specification) Observation | ||
| func post_(Specification) Observation | ||
|
|
||
| // NOTE: these are the low projections mentioned in the paper | ||
| axiom { | ||
| (forall p,q Observation :: {pre_(Spec{p,q})} pre_(Spec{p,q}) == p) && | ||
| (forall p,q Observation :: {post_(Spec{p,q})} post_(Spec{p,q}) == q) | ||
| } | ||
|
|
||
| axiom { | ||
| (forall sig ClassificationSpec :: {Post(sig,Empty{})} Post(sig,Empty{}) == EmptyObs{}) && | ||
| (forall sig ClassificationSpec :: {Pre(sig,Empty{})} Pre(sig,Empty{}) == EmptyObs{}) && | ||
| (forall sig ClassificationSpec, t Trace, e Action :: {Post(sig,Snoc{t,e})} Post(sig,Snoc{t,e}) == SnocObs{Post(sig,t), post_(sig.Classification(e))}) && | ||
| (forall sig ClassificationSpec, t Trace, e Action :: {Pre(sig,Snoc{t,e})} Pre(sig,Snoc{t,e}) == SnocObs{Pre(sig,t), pre_(sig.Classification(e))}) | ||
| } | ||
| } |
There was a problem hiding this comment.
the type Collect introduced here does not seem to be used anywhere. As such, I think we should define these operations not through a domain, but with pure functions instead. Please check if this applies to other domains you introduced as well
verification/scratch/mwe1/mwe1.gobra
Outdated
| func Reaches(IODSpec, Trace, state) bool | ||
|
|
||
| axiom { | ||
| forall r IODSpec, t Trace, s state, a Action :: { Snoc{t, a}, Reaches(r, t, s) } Reaches(r, t, s) && r.Guard(s, a) ==> Reaches(r, Snoc{t, a}, r.Update(s, a)) |
There was a problem hiding this comment.
Doesn't this produce a verification error? I would have expected that the call r.Guard(s, a) can only succeed if r is not nil
There was a problem hiding this comment.
This does not produce a verification error as is. Only when moving the call r.Guard(s, a) to a pure function (while trying to extract the Restriction domain / Reaches), Gobra complains
verification/scratch/mwe1/mwe1.gobra
Outdated
| /* ghost */ Declassify(t) | ||
| /* ghost */ LowPost(DefaultClassification{}) | ||
| Send(t) | ||
| /* ghost */ LowPost(DefaultClassification{}) |
There was a problem hiding this comment.
We should have a comment here about what would happen if we, for example, forgot to call LowPost(DefaultClassification{}) or Declassify in any of the three places where we currently do. The interesting point is that we would get a verification error in the postcondition instead of in the the call to Send
verification/scratch/mwe2/mwe2.gobra
Outdated
| ensures token(old(Recv_T(p))) | ||
| ensures m == old(Recv_R(p)) | ||
| ensures low(m) | ||
| func Recv(ghost p Place) (m int) |
There was a problem hiding this comment.
I would return the new place here as a ghost return value
verification/scratch/mwe2/mwe2.gobra
Outdated
| requires token(p) && SendPerm(p, t) | ||
| requires low(t) | ||
| ensures token(old(Send_T(p, t))) | ||
| func Send(ghost p Place, t int) |
There was a problem hiding this comment.
Same here and in declassify
verification/scratch/mwe2/mwe2.gobra
Outdated
| // 1. Receive a message. | ||
| RecvPerm(p) && | ||
| // 2. Compute MAC tag and declassify it. | ||
| DeclassifyPerm(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))) && | ||
| // 3. Send MAC tag over network. | ||
| SendPerm(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))) && | ||
| // 4. Restart. | ||
| Protocol1(Send_T(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))), key) |
There was a problem hiding this comment.
you might want to simplify this with let bindings to introduce intermediate variables for the places and for the mac
verification/scratch/mwe2/mwe2.gobra
Outdated
| lastMsg2 int // 2nd | ||
| lastMsg3 int // 3rd |
There was a problem hiding this comment.
why did we introduce lastMsg2 and lastMsg3 here?
There was a problem hiding this comment.
See comment below. Protocol2 allows sending the MAC tag of either the most or second most recently received message, and to ensure this, we need to keep track of these in our state. lastMsg3 is actually not needed, however, and I removed it. I put it in initially to make it more explicit which messages' tags can be sent and which can't.
verification/scratch/mwe2/mwe2.gobra
Outdated
| pred Protocol2(ghost p Place, s state) { | ||
| // Receive a message at any time. | ||
| RecvPerm(p) && Protocol2(Recv_T(p), Recv_S(s, Recv_R(p))) && | ||
| // NOTE: at the moment we can declassify things before receiving anything | ||
| // Declassify and send either the most or the 2nd most recently received message. | ||
| DeclassifyPerm(p, s.lastMsg1, MAC(s.key, s.lastMsg1)) && Protocol2(Declassify_T(p, s.lastMsg1, MAC(s.key, s.lastMsg1)), s) && | ||
| DeclassifyPerm(p, s.lastMsg2, MAC(s.key, s.lastMsg2)) && Protocol2(Declassify_T(p, s.lastMsg2, MAC(s.key, s.lastMsg2)), s) && | ||
| SendPerm(p, MAC(s.key, s.lastMsg1)) && Protocol2(Send_T(p, MAC(s.key, s.lastMsg1)), s) && | ||
| SendPerm(p, MAC(s.key, s.lastMsg2)) && Protocol2(Send_T(p, MAC(s.key, s.lastMsg2)), s) | ||
| } |
There was a problem hiding this comment.
does this protocol show sth that the other did not?
There was a problem hiding this comment.
I constructed Protocol2 to show a protocol ...
- ... which allows declassifying different values at any point, and thus needs the additional parameter
pfor declassification (to make the IOD spec deterministic and the low data, which includesp). - ... where one is allowed by the IOD spec to send something before declassifying, which is only "caught" (in case it was high data) by the classification spec / pre- and postconditions of the I/O functions (in the other protocol, one had to declassify before sending just to conform to the IOD spec). This is supposed to exemplify that SIF goes beyond simply following the IOD spec.
- ... which contains more complex, mutable state, and how to work with it.
|
It may be worth to move these examples to the test cases of viperproject/gobra#802 |
2 participants
Not supposed to be merged. (Very) minimal working example of how to verify secure information flow for the router