Prove simple malicious server example

etc/update-goose.py

@@ -314,6 +314,9 @@ def run_goose_test_gen(src_path, output):
         pkgs = [
             "chat4",
             "full",
+            "full2/shared",
+            "full2/fc_ffi_shim",
+            "full2",
         ]
 
         for pkg in pkgs:

external/Goose/github_com/mit_pdos/secure_chat/full2.v

@@ -0,0 +1,145 @@
+(* autogenerated from github.com/mit-pdos/secure-chat/full2 *)
+From Perennial.goose_lang Require Import prelude.
+From Goose Require github_com.mit_pdos.gokv.urpc.
+From Goose Require github_com.mit_pdos.secure_chat.full2.fc_ffi_shim.
+From Goose Require github_com.mit_pdos.secure_chat.full2.shared.
+
+From Perennial.goose_lang Require Import ffi.grove_prelude.
+
+(* app.go *)
+
+Definition Alice := struct.decl [
+  "ck" :: ptrT;
+  "a_msg" :: ptrT;
+  "b_msg" :: ptrT
+].
+
+(* Clerk from clerk.go *)
+
+(* Clerk only supports sequential calls to its methods. *)
+Definition Clerk := struct.decl [
+  "cli" :: ptrT;
+  "log" :: slice.T ptrT;
+  "myNum" :: uint64T;
+  "signer" :: ptrT;
+  "verifiers" :: slice.T ptrT
+].
+
+Definition Clerk__Put: val :=
+  rec: "Clerk__Put" "c" "m" :=
+    let: "m2" := shared.MsgT__Copy "m" in
+    let: "log" := NewSlice ptrT (slice.len (struct.loadF Clerk "log" "c")) in
+    SliceCopy ptrT "log" (struct.loadF Clerk "log" "c");;
+    let: "log2" := SliceAppend ptrT "log" "m2" in
+    let: "log2B" := shared.EncodeMsgTSlice "log2" in
+    let: ("sig", "err1") := fc_ffi_shim.SignerT__Sign (struct.loadF Clerk "signer" "c") "log2B" in
+    control.impl.Assume ("err1" = shared.ErrNone);;
+    let: "pa" := shared.NewPutArg (struct.loadF Clerk "myNum" "c") "sig" "log2B" in
+    let: "argB" := shared.PutArg__Encode "pa" in
+    let: "r" := NewSlice byteT #0 in
+    let: "err2" := urpc.Client__Call (struct.loadF Clerk "cli" "c") shared.RpcPut "argB" "r" #100 in
+    control.impl.Assume ("err2" = urpc.ErrNone);;
+    #().
+
+Definition Alice__One: val :=
+  rec: "Alice__One" "a" :=
+    Clerk__Put (struct.loadF Alice "ck" "a") (struct.loadF Alice "a_msg" "a");;
+    #().
+
+Definition Clerk__Get: val :=
+  rec: "Clerk__Get" "c" :=
+    let: "nilRet" := NewSlice ptrT #0 in
+    let: "r" := NewSlice byteT #0 in
+    let: "err1" := urpc.Client__Call (struct.loadF Clerk "cli" "c") shared.RpcGet (NewSlice byteT #0) "r" #100 in
+    (if: "err1" ≠ urpc.ErrNone
+    then ("nilRet", shared.ErrSome)
+    else
+      let: ("arg", "err2") := shared.DecodePutArg "r" in
+      (if: "err2" ≠ shared.ErrNone
+      then ("nilRet", shared.ErrSome)
+      else
+        let: "pk" := SliceGet ptrT (struct.loadF Clerk "verifiers" "c") (struct.loadF shared.PutArg "Sender" "arg") in
+        let: "err3" := fc_ffi_shim.VerifierT__Verify "pk" (struct.loadF shared.PutArg "Sig" "arg") (struct.loadF shared.PutArg "LogB" "arg") in
+        (if: "err3" ≠ shared.ErrNone
+        then ("nilRet", shared.ErrSome)
+        else
+          let: ("log", <>) := shared.DecodeMsgTSlice (struct.loadF shared.PutArg "LogB" "arg") in
+          (if: (~ (shared.IsMsgTSlicePrefix (struct.loadF Clerk "log" "c") "log"))
+          then ("nilRet", shared.ErrSome)
+          else
+            struct.storeF Clerk "log" "c" (shared.CopyMsgTSlice "log");;
+            ("log", shared.ErrNone))))).
+
+Definition Alice__Two: val :=
+  rec: "Alice__Two" "a" :=
+    let: ("g", "err") := Clerk__Get (struct.loadF Alice "ck" "a") in
+    control.impl.Assume ("err" = shared.ErrNone);;
+    (if: #2 ≤ (slice.len "g")
+    then
+      control.impl.Assert ((struct.loadF shared.MsgT "Body" (SliceGet ptrT "g" #0)) = (struct.loadF shared.MsgT "Body" (struct.loadF Alice "a_msg" "a")));;
+      control.impl.Assert ((struct.loadF shared.MsgT "Body" (SliceGet ptrT "g" #1)) = (struct.loadF shared.MsgT "Body" (struct.loadF Alice "b_msg" "a")));;
+      control.impl.Assert ((slice.len "g") = #2);;
+      let: ("g2", "err") := Clerk__Get (struct.loadF Alice "ck" "a") in
+      control.impl.Assume ("err" = shared.ErrNone);;
+      control.impl.Assert ((struct.loadF shared.MsgT "Body" (SliceGet ptrT "g2" #0)) = (struct.loadF shared.MsgT "Body" (struct.loadF Alice "a_msg" "a")));;
+      control.impl.Assert ((struct.loadF shared.MsgT "Body" (SliceGet ptrT "g2" #1)) = (struct.loadF shared.MsgT "Body" (struct.loadF Alice "b_msg" "a")));;
+      control.impl.Assert ((slice.len "g2") = #2);;
+      SliceGet ptrT "g" #0
+    else slice.nil).
+
+Definition MakeClerk: val :=
+  rec: "MakeClerk" "host" "myNum" "signer" "verifiers" :=
+    let: "c" := struct.new Clerk [
+    ] in
+    struct.storeF Clerk "cli" "c" (urpc.MakeClient "host");;
+    struct.storeF Clerk "log" "c" (NewSlice ptrT #0);;
+    struct.storeF Clerk "myNum" "c" "myNum";;
+    struct.storeF Clerk "signer" "c" "signer";;
+    struct.storeF Clerk "verifiers" "c" "verifiers";;
+    "c".
+
+Definition MakeAlice: val :=
+  rec: "MakeAlice" "host" "signer" "verifiers" :=
+    let: "a" := struct.new Alice [
+    ] in
+    struct.storeF Alice "ck" "a" (MakeClerk "host" shared.AliceNum "signer" "verifiers");;
+    struct.storeF Alice "a_msg" "a" (struct.new shared.MsgT [
+      "Body" ::= shared.AliceMsg
+    ]);;
+    struct.storeF Alice "b_msg" "a" (struct.new shared.MsgT [
+      "Body" ::= shared.BobMsg
+    ]);;
+    "a".
+
+Definition Bob := struct.decl [
+  "ck" :: ptrT;
+  "a_msg" :: ptrT;
+  "b_msg" :: ptrT
+].
+
+Definition Bob__One: val :=
+  rec: "Bob__One" "b" :=
+    let: ("g", "err") := Clerk__Get (struct.loadF Bob "ck" "b") in
+    control.impl.Assume ("err" = shared.ErrNone);;
+    (if: #1 ≤ (slice.len "g")
+    then
+      control.impl.Assert ((struct.loadF shared.MsgT "Body" (SliceGet ptrT "g" #0)) = (struct.loadF shared.MsgT "Body" (struct.loadF Bob "a_msg" "b")));;
+      control.impl.Assert ((slice.len "g") = #1);;
+      Clerk__Put (struct.loadF Bob "ck" "b") (struct.loadF Bob "b_msg" "b");;
+      SliceGet ptrT "g" #0
+    else slice.nil).
+
+Definition MakeBob: val :=
+  rec: "MakeBob" "host" "signer" "verifiers" :=
+    let: "b" := struct.new Bob [
+    ] in
+    struct.storeF Bob "ck" "b" (MakeClerk "host" shared.BobNum "signer" "verifiers");;
+    struct.storeF Bob "a_msg" "b" (struct.new shared.MsgT [
+      "Body" ::= shared.AliceMsg
+    ]);;
+    struct.storeF Bob "b_msg" "b" (struct.new shared.MsgT [
+      "Body" ::= shared.BobMsg
+    ]);;
+    "b".
+
+(* clerk.go *)

external/Goose/github_com/mit_pdos/secure_chat/full2/fc_ffi_shim.v

@@ -0,0 +1,38 @@
+(* autogenerated from github.com/mit-pdos/secure-chat/full2/fc_ffi_shim *)
+From Perennial.goose_lang Require Import prelude.
+From Goose Require github_com.mit_pdos.secure_chat.full2.shared.
+
+Section code.
+Context `{ext_ty: ext_types}.
+Local Coercion Var' s: expr := Var s.
+
+Definition CryptoT := struct.decl [
+].
+
+Definition Init: val :=
+  rec: "Init" <> :=
+    Panic "ffi";;
+    #().
+
+Definition SignerT := struct.decl [
+].
+
+Definition VerifierT := struct.decl [
+].
+
+Definition CryptoT__MakeKeys: val :=
+  rec: "CryptoT__MakeKeys" "c" :=
+    Panic "ffi";;
+    #().
+
+Definition SignerT__Sign: val :=
+  rec: "SignerT__Sign" "s" "data" :=
+    Panic "ffi";;
+    #().
+
+Definition VerifierT__Verify: val :=
+  rec: "VerifierT__Verify" "v" "signature" "data" :=
+    Panic "ffi";;
+    #().
+
+End code.

external/Goose/github_com/mit_pdos/secure_chat/full2/shared.v

@@ -0,0 +1,141 @@
+(* autogenerated from github.com/mit-pdos/secure-chat/full2/shared *)
+From Perennial.goose_lang Require Import prelude.
+From Goose Require github_com.tchajed.marshal.
+
+Section code.
+Context `{ext_ty: ext_types}.
+Local Coercion Var' s: expr := Var s.
+
+Definition ErrorT: ty := uint64T.
+
+Definition ErrNone : expr := #0.
+
+Definition ErrSome : expr := #1.
+
+Definition RpcGet : expr := #1.
+
+Definition RpcPut : expr := #2.
+
+Definition AliceNum : expr := #0.
+
+Definition BobNum : expr := #1.
+
+Definition MaxSenders : expr := #2.
+
+Definition AliceMsg : expr := #10.
+
+Definition BobMsg : expr := #11.
+
+Definition SigLen : expr := #69.
+
+Definition MsgT := struct.decl [
+  "Body" :: uint64T
+].
+
+Definition NewMsgT: val :=
+  rec: "NewMsgT" "body" :=
+    struct.new MsgT [
+      "Body" ::= "body"
+    ].
+
+Definition MsgT__Equals: val :=
+  rec: "MsgT__Equals" "m" "o" :=
+    (struct.loadF MsgT "Body" "m") = (struct.loadF MsgT "Body" "o").
+
+Definition MsgT__Copy: val :=
+  rec: "MsgT__Copy" "m" :=
+    struct.new MsgT [
+      "Body" ::= struct.loadF MsgT "Body" "m"
+    ].
+
+Definition MsgT__Encode: val :=
+  rec: "MsgT__Encode" "m" :=
+    let: "b" := ref_to (slice.T byteT) (NewSlice byteT #0) in
+    "b" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "b") (struct.loadF MsgT "Body" "m"));;
+    ![slice.T byteT] "b".
+
+Definition DecodeMsgT: val :=
+  rec: "DecodeMsgT" "b" :=
+    let: ("body", "b2") := marshal.ReadInt "b" in
+    (NewMsgT "body", "b2").
+
+Definition CopyMsgTSlice: val :=
+  rec: "CopyMsgTSlice" "sl" :=
+    let: "sl2" := ref_to (slice.T ptrT) (NewSlice ptrT (slice.len "sl")) in
+    ForSlice ptrT "i" "v" "sl"
+      (SliceSet ptrT (![slice.T ptrT] "sl2") "i" (MsgT__Copy "v"));;
+    ![slice.T ptrT] "sl2".
+
+Definition IsMsgTSlicePrefix: val :=
+  rec: "IsMsgTSlicePrefix" "short" "long" :=
+    (if: (slice.len "long") < (slice.len "short")
+    then #false
+    else
+      let: "ret" := ref_to boolT #true in
+      ForSlice ptrT "i" "m" "short"
+        ((if: (~ (MsgT__Equals "m" (SliceGet ptrT "long" "i")))
+        then "ret" <-[boolT] #false
+        else #()));;
+      ![boolT] "ret").
+
+Definition EncodeMsgTSlice: val :=
+  rec: "EncodeMsgTSlice" "sl" :=
+    let: "b" := ref_to (slice.T byteT) (NewSlice byteT #0) in
+    "b" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "b") (slice.len "sl"));;
+    ForSlice ptrT <> "v" "sl"
+      ("b" <-[slice.T byteT] (marshal.WriteBytes (![slice.T byteT] "b") (MsgT__Encode "v")));;
+    ![slice.T byteT] "b".
+
+Definition DecodeMsgTSlice: val :=
+  rec: "DecodeMsgTSlice" "b" :=
+    let: "b2" := ref_to (slice.T byteT) "b" in
+    let: ("l", "b2") := marshal.ReadInt (![slice.T byteT] "b2") in
+    let: "sl" := NewSlice ptrT "l" in
+    let: "i" := ref_to uint64T #0 in
+    (for: (λ: <>, (![uint64T] "i") < "l"); (λ: <>, "i" <-[uint64T] ((![uint64T] "i") + #1)) := λ: <>,
+      let: ("0_ret", "1_ret") := DecodeMsgT (![slice.T byteT] "b2") in
+      SliceSet ptrT "sl" (![uint64T] "i") "0_ret";;
+      "b2" <-[slice.T byteT] "1_ret";;
+      Continue);;
+    ("sl", ![slice.T byteT] "b2").
+
+Definition PutArg := struct.decl [
+  "Sender" :: uint64T;
+  "Sig" :: slice.T byteT;
+  "LogB" :: slice.T byteT
+].
+
+Definition NewPutArg: val :=
+  rec: "NewPutArg" "sender" "sig" "logB" :=
+    struct.new PutArg [
+      "Sender" ::= "sender";
+      "Sig" ::= "sig";
+      "LogB" ::= "logB"
+    ].
+
+Definition PutArg__Encode: val :=
+  rec: "PutArg__Encode" "pa" :=
+    control.impl.Assume ((slice.len (struct.loadF PutArg "Sig" "pa")) = SigLen);;
+    let: "b" := ref_to (slice.T byteT) (NewSlice byteT #0) in
+    "b" <-[slice.T byteT] (marshal.WriteInt (![slice.T byteT] "b") (struct.loadF PutArg "Sender" "pa"));;
+    "b" <-[slice.T byteT] (marshal.WriteBytes (![slice.T byteT] "b") (struct.loadF PutArg "Sig" "pa"));;
+    "b" <-[slice.T byteT] (marshal.WriteBytes (![slice.T byteT] "b") (struct.loadF PutArg "LogB" "pa"));;
+    ![slice.T byteT] "b".
+
+(* Input comes from adv RPC, so need to validate it. *)
+Definition DecodePutArg: val :=
+  rec: "DecodePutArg" "b" :=
+    (if: (slice.len "b") < #8
+    then (slice.nil, ErrSome)
+    else
+      let: ("sender", "r2") := marshal.ReadInt "b" in
+      (if: (~ ((#0 ≤ "sender") && ("sender" < MaxSenders)))
+      then (slice.nil, ErrSome)
+      else
+        (if: (slice.len "r2") < SigLen
+        then (slice.nil, ErrSome)
+        else
+          let: ("sig", "logB") := marshal.ReadBytes "r2" SigLen in
+          (NewPutArg "sender" "sig" "logB", ErrNone)))).
+
+End code.