Address PR feedback

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{})
 }

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)
     }
 
 }