diff --git a/verification/scratch/mwe1/mwe1.gobra b/verification/scratch/mwe1/mwe1.gobra index 4b8e49984..97d747383 100644 --- a/verification/scratch/mwe1/mwe1.gobra +++ b/verification/scratch/mwe1/mwe1.gobra @@ -3,7 +3,7 @@ // 1. We receive a message M over the network. // 2. We compute a "MAC tag" of M using K. // 3. We send the computed tag over the network. -package mwe1 +package mwe ////////////////////////////// I/O Actions ////////////////////////////// // cf. running-example/policy/actions.gobra @@ -96,27 +96,43 @@ pure func Low(v int) Observation { // this allows us to assume that the sensitivity postconditions are satisfied. ghost decreases -requires acc(History(), 1/2) && low(Pre(sig,*History())) -ensures acc(History(), 1/2) && low(Post(sig,*History())) +requires sig != nil && acc(History(), 1/2) && low(Pre(sig,*History())) +ensures acc(History(), 1/2) && low(Post(sig,*History())) func LowPost(sig ClassificationSpec) -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 +ghost +decreases +pure func pre_(spec Specification) Observation { + return match spec { + case Spec{?p, _}: p + } +} +ghost +decreases +pure func post_(spec Specification) Observation { + return match spec { + case Spec{_, ?q}: q + } +} - // 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) +ghost +decreases len(trace) +requires sig != nil +pure func Pre(sig ClassificationSpec, trace Trace) ObservationTrace { + return match trace { + case Empty{}: EmptyObs{} + case Snoc{?t, ?e}: SnocObs{Pre(sig, t), pre_(sig.Classification(e))} } +} - 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))}) +ghost +decreases len(trace) +requires sig != nil +pure func Post(sig ClassificationSpec, trace Trace) ObservationTrace { + return match trace { + case Empty{}: EmptyObs{} + case Snoc{?t, ?e}: SnocObs{Post(sig, t), post_(sig.Classification(e))} } } @@ -147,17 +163,13 @@ type IODSpec interface { pure Update(state, Action) state } +// NOTE: We don't need IsTrace but it is not clear how to translate Reaches. type Restriction domain { - func IsTrace(IODSpec, Trace) bool 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)) } - - axiom { - forall r IODSpec, t Trace, s state :: {Reaches(r, t, s)} Reaches(r, t, s) ==> IsTrace(r,t) - } } // Our I/O spec. The state is the private key and the most recently received message. @@ -175,7 +187,7 @@ ghost decreases pure func (MWE1) Guard(s state, a Action) bool { return match a { - // NOTE: This makess our IOD spec well-formed, as what is allowed to be + // NOTE: This makes our IOD spec well-formed, as what is allowed to be // declassified is now deterministic in the previous I/O actions. case DeclassifyIO{?t}: t == MAC(s.key, s.lastMsg) case _: true @@ -231,6 +243,12 @@ pure func MAC(int, int) int // In the original example, I think this is done via the shared invariant. preserves acc(History()) && acc(s) && low(Pre(DefaultClassification{}, *History())) && Reaches(MWE1{}, *History(), *s) func authenticate(ghost s *state) { + // NOTE: forgetting the calls to either of `Declassify` and `LowPost` + // would result in a verification error *in the postcondition* (and not in + // the call to send), as here, compliance to the classification spec is + // not checked on every I/O call, but instead on the trace at the end of + // the function call. + m := Recv() LowPost(DefaultClassification{}) ghost s.lastMsg = m @@ -240,5 +258,8 @@ func authenticate(ghost s *state) { /* ghost */ Declassify(t) /* ghost */ LowPost(DefaultClassification{}) Send(t) + // The following call to `LowPost` is the only one not needed (here), + // as we don't need the postcondition of the last I/O call to verify + // the remainder of the function. /* ghost */ LowPost(DefaultClassification{}) } \ No newline at end of file diff --git a/verification/scratch/mwe2/mwe2.gobra b/verification/scratch/mwe2/mwe2.gobra index 8f1a1297f..477bdf79f 100644 --- a/verification/scratch/mwe2/mwe2.gobra +++ b/verification/scratch/mwe2/mwe2.gobra @@ -1,5 +1,5 @@ // Minimal working example 2. -package mwe2 +package mwe // Used to track position in protocol. type Place int @@ -10,13 +10,11 @@ pred RecvPerm(ghost p Place) // Returns the next place after calling `Recv` from `p`. // Avoids using an existential quantifier. ghost -requires RecvPerm(p) decreases pure func Recv_T(ghost p Place) Place // Used to refer to the received message. ghost -requires RecvPerm(p) decreases pure func Recv_R(ghost p Place) int @@ -27,51 +25,47 @@ pure func Recv_S(s state, m int) state { } requires token(p) && RecvPerm(p) -ensures token(old(Recv_T(p))) -ensures m == old(Recv_R(p)) +ensures token(next_p) && next_p == Recv_T(p) +ensures m == Recv_R(p) ensures low(m) -func Recv(ghost p Place) (m int) +func Recv(ghost p Place) (ghost next_p Place, m int) pred SendPerm(ghost p Place, t int) ghost -requires SendPerm(p, t) decreases pure func Send_T(ghost p Place, t int) Place requires token(p) && SendPerm(p, t) requires low(t) -ensures token(old(Send_T(p, t))) -func Send(ghost p Place, t int) +ensures token(next_p) && next_p == Send_T(p, t) +func Send(ghost p Place, t int) (ghost next_p Place) pred DeclassifyPerm(ghost p Place, tag int, t int) ghost -requires DeclassifyPerm(p, tag, t) decreases pure func Declassify_T(ghost p Place, tag int, t int) Place -// In order to make permitted declassifications deterministic in low data, -// we add low parameter `p` to "tag" declassifications. -// (Necessary as otherwise IOD spec Protocol2 would not be well-formed.) ghost requires token(p) && DeclassifyPerm(p, tag, t) requires low(tag) -ensures token(old(Declassify_T(p, tag, t))) +ensures token(next_p) && next_p == Declassify_T(p, tag, t) ensures low(t) decreases -func Declassify(ghost p Place, tag int, t int) +func Declassify(ghost p Place, tag int, t int) (ghost next_p Place) // "Linear" protocol. -pred Protocol1(ghost p Place, key int) { +pred Protocol1(ghost p0 Place, key int) { // 1. Receive a message. - RecvPerm(p) && + RecvPerm(p0) && let p1, m := Recv_T(p0), Recv_R(p0) in // 2. Compute MAC tag and declassify it. - DeclassifyPerm(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))) && + let tag := MAC(key, m) in + DeclassifyPerm(p1, m, tag) && let p2 := Declassify_T(p1, m, tag) in // 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))) && + SendPerm(p2, tag) && let p3 := Send_T(p2, tag) in // 4. Restart. - Protocol1(Send_T(Declassify_T(Recv_T(p), Recv_R(p), MAC(key, Recv_R(p))), MAC(key, Recv_R(p))), key) + Protocol1(p3, key) } type state struct { @@ -81,15 +75,26 @@ type state struct { lastMsg3 int // 3rd } -pred Protocol2(ghost p Place, s state) { +pred Protocol2(ghost p0 Place, s0 state) { // Receive a message at any time. - RecvPerm(p) && Protocol2(Recv_T(p), Recv_S(s, Recv_R(p))) && + RecvPerm(p0) && + let p1, s1 := Recv_T(p0), Recv_S(s0, Recv_R(p0)) in Protocol2(p1, s1) && // 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) + // Declassify and send either the MAC tag of the most or the 2nd most + // recently received message. + let tag1, tag2 := MAC(s0.key, s0.lastMsg1), MAC(s0.key, s0.lastMsg2) in + + DeclassifyPerm(p0, s0.lastMsg1, tag1) && + let p1 := Declassify_T(p0, s0.lastMsg1, tag1) in Protocol2(p1, s0) && + + DeclassifyPerm(p0, s0.lastMsg2, tag2) && + let p1 := Declassify_T(p0, s0.lastMsg2, tag2) in Protocol2(p1, s0) && + + SendPerm(p0, tag1) && + let p1 := Send_T(p0, tag1) in Protocol2(p1, s0) && + + SendPerm(p0, tag2) && + let p1 := Send_T(p0, tag2) in Protocol2(p1, s0) } // Abstract function representing the computation of a MAC. @@ -103,30 +108,30 @@ func authenticate(ghost p0 Place, s state) { invariant token(p0) && Protocol2(p0, s) for { unfold Protocol2(p0, s) - ghost p1 := Recv_T(p0) - m1 := Recv(p0) + // ghost p1 := Recv_T(p0) + p1, m1 := Recv(p0) s = Recv_S(s, m1) unfold Protocol2(p1, s) - ghost p2 := Recv_T(p1) - m2 := Recv(p1) + // ghost p2 := Recv_T(p1) + p2, m2 := Recv(p1) s = Recv_S(s, m2) unfold Protocol2(p2, s) - ghost p3 := Recv_T(p2) - m3 := Recv(p2) + // ghost p3 := Recv_T(p2) + p3, m3 := Recv(p2) s = Recv_S(s, m3) // We can use m2, m3 here. m1 won't work. t := MAC(s.key, m3) unfold Protocol2(p3, s) - ghost p4 := Declassify_T(p3, m3, t) - Declassify(p3, m3, t) + // ghost p4 := Declassify_T(p3, m3, t) + ghost p4 := Declassify(p3, m3, t) unfold Protocol2(p4, s) - ghost p0 = Send_T(p4, t) - Send(p4, t) + // ghost p0 = Send_T(p4, t) + p0 = Send(p4, t) } } \ No newline at end of file