Start proving client serialization safety

Author: CharlesAverill

theories/Client.v

@@ -13,7 +13,7 @@ Open Scope sint63_scope.
 (**
     The internal loop of our client sending thread
 *)
-Definition client_send_thread (uname_sockfd : username * file_descr) : optionE unit :=
+Definition client_send_thread (uname_sockfd : username * file_descr) : result unit :=
     let '(uname, sockfd) := uname_sockfd in 
     repeat_until_timeout max_int (fun _ => 
         let* _ <= print_string ">>> " #;
@@ -46,18 +46,18 @@ Definition client_send_thread (uname_sockfd : username * file_descr) : optionE u
                 send_message sockfd (serialize_client_message 
                     (MESG msg))
         else
-            SomeE tt)) with
-        | SomeE _ => SomeE Recurse
-        | NoneE s => 
+            Ok tt)) with
+        | Ok _ => Ok Recurse
+        | Error s => 
             let* _ <= log Log_Error s #;
-            SomeE Recurse
+            Ok Recurse
         end
     ).
 
 (**
     The internal loop of our client receiving thread
 *)
-Definition client_recv_thread (sockfd : file_descr) : optionE unit :=
+Definition client_recv_thread (sockfd : file_descr) : result unit :=
     repeat_until_timeout max_int (fun _ => 
         server_msg <- recv_server_message sockfd ;;
         let* _ <= (match server_msg with
@@ -70,13 +70,13 @@ Definition client_recv_thread (sockfd : file_descr) : optionE unit :=
             print_string ">>> "
         | _ => tt
         end) #;
-        SomeE Recurse
+        Ok Recurse
     ).
 
 (**
     Wraps up all client logic: port binding, threading, etc.
 *)
-Definition client (host : string) (portno : port) : optionE unit :=
+Definition client (host : string) (portno : port) : result unit :=
     (* Obtain username from user *)
     let* _ <= print_endline "Please enter a username (length 1-32, no spaces)" #;
     username_string <- read_line tt ;;
@@ -101,9 +101,9 @@ Definition client (host : string) (portno : port) : optionE unit :=
     (* Display chatroom information to user output *)
     let* _ <= log Log_Info ("Total users: " ++ (string_of_int num_users)) #;
     (* Get user input *)
-    input_thread <- create (username *file_descr) (optionE unit) client_send_thread (uname, socket_fd) ;;
+    input_thread <- create (username *file_descr) (result unit) client_send_thread (uname, socket_fd) ;;
     (* Display server messages *)
-    recv_thread <- create file_descr (optionE unit) client_recv_thread socket_fd ;;
+    recv_thread <- create file_descr (result unit) client_recv_thread socket_fd ;;
     let* _ <= join input_thread #;
     (* let* _ <= join recv_thread #; *)
     let* _ <= log Log_Info "Closing connection to server" #;

theories/Messages.v

@@ -17,12 +17,12 @@ Open Scope Z_scope.
 Open Scope sint63_scope.
 Open Scope list_scope.
 Open Scope monad_scope.
-
 (** ** Usernames 
 
     Usernames have specific properties per the project requirements. This
     section implements a dependently-typed Record type for usernames and some
     automation to create them at will.
+
 *)
 
 (** 
@@ -34,6 +34,8 @@ Record username : Type := {
         (1 <= to_Z (int_len_string Uname) <= 32)%Z
     ; NoSpaces :
         ~ InString space Uname
+    ; NoNulls :
+        ~ InString (ascii_of_byte "000"%byte) Uname
 }.
 
 (**
@@ -49,7 +51,7 @@ Record username : Type := {
 *)
 Definition validate_username (name : string) : bool :=
     ((1 <=? int_len_string name) && (int_len_string name <=? 32))
-        && (no_spaces name).
+        && (no_spaces name) && (no_nulls name).
 
 (**
     Ensure that [validate_username] provides
@@ -60,45 +62,58 @@ Theorem validate_username_correct :
     forall (name : string)
     (VALID : validate_username name = true),
         (1 <= to_Z (int_len_string name) <= 32)%Z /\
-        ~ InString space name.
+        ~ InString space name /\ ~ InString (ascii_of_byte "000"%byte) name.
 Proof.
     intros. unfold validate_username in VALID.
-    apply andb_true_iff in VALID.
-    destruct VALID as [Length NoSpaces].
-    apply andb_true_iff in Length.
-    destruct Length as [NonEmpty Le32].
+    rewrite andb_true_iff in VALID.
+      destruct VALID as (VALID & NoNulls).
+    rewrite andb_true_iff in VALID.
+      destruct VALID as (VALID & NoSpaces).
+    rewrite andb_true_iff in VALID.
+      destruct VALID as (NonEmpty & Le32).
     apply leb_spec in NonEmpty, Le32.
     split.
-    - change 1%Z with (to_Z 1). now split. 
+      change 1%Z with (to_Z 1). now split.
+    split.
     - clear - NoSpaces. induction name as [| a name']. auto.
         simpl. simpl in NoSpaces. 
         destruct (ascii_dec a space) as [a_space|a_space].
         -- inversion NoSpaces.
         -- intro Contra. destruct Contra.
             + now apply a_space.
             + now apply IHname'.
+    - clear - NoNulls. induction name as [| a name']. auto.
+        simpl. simpl in NoNulls.
+        destruct (ascii_dec a (ascii_of_byte "000"%byte)) as [a_null|a_null].
+        -- inversion NoNulls.
+        -- intro Contra. destruct Contra.
+            + now apply a_null.
+            + now apply IHname'.
 Qed.
 
 (**
     Instantiate a username object if it
     passes [validate_username], or return
     [None]
 *)
-Definition new_username (s : string) : optionE username.
+Definition new_username (s : string) : result username.
     destruct (validate_username s) eqn:E.
     - apply validate_username_correct in E. 
-      destruct E.
-      exact (SomeE {|
+      destruct E, H0.
+      exact (Ok {|
         Uname := s;
         ValidLength := H;
-        NoSpaces := H0
+        NoSpaces := H0;
+        NoNulls := H1
       |}).
     - destruct (no_spaces s).
-        -- (* No Spaces *) 
-        exact (NoneE 
+        -- (* No Spaces *)
+        destruct (no_nulls s).
+          exact (Error ("Username cannot contain nulls")).
+        exact (Error 
             ("Username length must be in range [1..32]: '" ++ s ++ "'")).
         -- (* Spaces *)
-        exact (NoneE ("Username cannot contain spaces: '" ++ s ++ "'")).
+        exact (Error ("Username cannot contain spaces: '" ++ s ++ "'")).
 Defined.
 
 (** A placeholder username *)
@@ -107,7 +122,9 @@ Definition dummy_username : username.
         (split; unfold to_Z, Uint63.to_Z; simpl; lia).
     assert (~ InString space "X") by
         (intro; destruct H0; [discriminate | auto]).
-    exact {|Uname := "X"; ValidLength := H; NoSpaces := H0|}.
+    assert (~ InString (ascii_of_byte "000"%byte) "X") by
+        (intro; destruct H1; [discriminate | auto]).
+    exact {|Uname := "X"; ValidLength := H; NoSpaces := H0; NoNulls := H1|}.
 Defined.
 
 (** Username equality *)
@@ -183,7 +200,7 @@ Definition serialize_client_message (cm : client_message) : bytes :=
     end.
 
 (** Convert a list of [byte]s into a [client_message] *)
-Definition deserialize_client_message (b : bytes) : optionE client_message :=
+Definition deserialize_client_message (b : bytes) : result client_message :=
     match b with
     | x00 :: t => 
         uname <- new_username (trim_null t) ;;
@@ -197,9 +214,65 @@ Definition deserialize_client_message (b : bytes) : optionE client_message :=
     | x03 :: t => 
         uname <- new_username (trim_null t) ;;
         return (EXIT uname)
-    | _ => NoneE ("Client message code not recognized: " ++ (string_of_bytes b))
+    | _ => Error ("Client message code not recognized: " ++ (string_of_bytes b))
     end.
 
+Lemma create_null_list_forall : forall n,
+  Forall (fun b0 : byte => b0 = "000"%byte) (create_list_nat "000"%byte n).
+Proof.
+  induction n.
+    apply Forall_nil.
+  apply Forall_cons. reflexivity.
+  apply IHn.
+Qed.
+
+Lemma trim_null_app : forall n l,
+  trim_null (l ++ create_list_nat "000"%byte n) = trim_null l.
+Proof.
+  intros. pose proof (create_null_list_forall n).
+  remember (create_list_nat _ _).
+  clear Heql0.
+  induction l.
+Admitted.
+
+Lemma trim_null_pad_r : forall (s : string) (p : int),
+  trim_null (bytes_of_string (pad_string_r s "000" p)) = trim_null (bytes_of_string s).
+Proof.
+  intros. unfold pad_string_r. rewrite bytes_of_string_app, bytes_of_string_of_bytes.
+  unfold create_list. apply trim_null_app.
+Qed.
+
+Lemma not_instring_inv : forall c a s,
+  ~ InString c (String a s) -> c <> a /\ ~ InString c s.
+Proof.
+  intros. split.
+    intro. apply H. subst. unfold InString. now left.
+  intro. apply H. unfold InString. right. apply H0.
+Qed.
+
+Lemma trim_null_uname : forall uname,
+  trim_null (bytes_of_string (Uname uname)) = Uname uname.
+Proof.
+  intros. pose proof (NoNulls uname). induction (Uname uname).
+    reflexivity.
+  apply not_instring_inv in H. destruct H.
+Admitted.
+
+Lemma new_username_clean : forall (name : username),
+  new_username (trim_null (bytes_of_string (pad_string_r (Uname name) "000" 32))) = Ok name.
+Proof.
+  intros. rewrite trim_null_pad_r, trim_null_uname.
+  enough (validate_username (Uname name) = true).
+Admitted.
+
+Theorem serialize_client_message_safe :
+  forall (cm : client_message),
+    deserialize_client_message (serialize_client_message cm) = Ok cm.
+Proof.
+  intros. destruct cm.
+  - simpl. unfold serialize_username. now rewrite new_username_clean.
+Admitted.
+
 Theorem serialize_username_len : forall (u : username),
     int_len_list (serialize_username u) = 32.
 Proof.
@@ -308,7 +381,7 @@ Definition serialize_server_message (sm : server_message) : bytes :=
     end.
 
 (** Convert a list of [byte]s into a [server_message] *)
-Definition deserialize_server_message (b : bytes) : optionE server_message :=
+Definition deserialize_server_message (b : bytes) : result server_message :=
     match b with
     (** This case isn't helpful... why should we deserialize 
         something when we don't even know how many bytes to pull?
@@ -346,7 +419,7 @@ Function resend
         (sockfd : file_descr) (message : bytes)
         (len_msg : int)
         {measure (fun x => (Z.to_nat (to_Z x))) fuel}
-        : optionE unit :=
+        : result unit :=
     if sub1_no_underflow fuel then
         let send_result := n_sent + send sockfd message n_sent (len_msg - n_sent) [] in
         (* If uncommented, the extractor will call [send] twice, because it tries
@@ -355,45 +428,45 @@ Function resend
         if send_result <? len_msg then
             resend (fuel - 1) send_result sockfd message len_msg
         else
-            SomeE tt
+            Ok tt
     else
-        NoneE ("Timed out while sending message '" ++ (string_of_bytes message) ++ "'").
+        Error ("Timed out while sending message '" ++ (string_of_bytes message) ++ "'").
     prove_sub1.
 Defined.
 
 (** Wrapper for [resend] *)
-Definition send_message (sockfd : file_descr) (message : bytes) : optionE unit :=
+Definition send_message (sockfd : file_descr) (message : bytes) : result unit :=
     resend 100 0 sockfd message (int_len_list message).
 
 (** Receives a message from a socket *)
-Definition recv_message (sockfd : file_descr) (len : int) : optionE bytes :=
+Definition recv_message (sockfd : file_descr) (len : int) : result bytes :=
     match recv sockfd 0 len [] with
-    | (_, out) => SomeE out
+    | (_, out) => Ok out
     end.
 
 (** Receives a message from a socket and deserializes it as a client message *)
-(* Definition recv_client_message (sockfd : file_descr) : optionE client_message :=
+(* Definition recv_client_message (sockfd : file_descr) : result client_message :=
     msg_bytes <- recv_message sockfd max_message_len ;;
     deserialize_client_message msg_bytes. *)
 
 (** Receives an int from a socket *)
-Definition recv_int (sockfd : file_descr) : optionE int :=
+Definition recv_int (sockfd : file_descr) : result int :=
     n_bytes <- recv_message sockfd 8 ;;
     return bytes_to_int63 (n_bytes).
 
 (** Receives a string from a socket *)
-Definition recv_string (sockfd : file_descr) : optionE string :=
+Definition recv_string (sockfd : file_descr) : result string :=
     str_len <- recv_int sockfd ;;
     str_bytes <- recv_message sockfd str_len ;;
     return string_of_bytes (str_bytes).
 
-Definition recv_username (sockfd : file_descr) : optionE username :=
+Definition recv_username (sockfd : file_descr) : result username :=
     username_bytes <- recv_message sockfd 32 ;;
     uname <- new_username (string_of_bytes username_bytes) ;;
     return uname.
 
 (** Receives an ACK message *)
-Definition recv_server_ACK (sockfd : file_descr) : optionE server_message :=
+Definition recv_server_ACK (sockfd : file_descr) : result server_message :=
     (* Receive a serialized int63 detailing number of connected users *)
     num_users <- recv_int sockfd ;;
     usernames_bytes <- recv_message sockfd (num_users * 32) ;;
@@ -404,18 +477,18 @@ Definition recv_server_ACK (sockfd : file_descr) : optionE server_message :=
     return ACK num_users usernames.
 
 (** Receives a server MSG message *)
-Definition recv_server_MSG (sockfd : file_descr) : optionE server_message :=
+Definition recv_server_MSG (sockfd : file_descr) : result server_message :=
     username <- recv_username sockfd ;;
     msg <- recv_string sockfd ;;
     return MSG username msg.
 
-Definition recv_server_ERR (sockfd : file_descr) : optionE server_message :=
+Definition recv_server_ERR (sockfd : file_descr) : result server_message :=
     err_code <- recv_int sockfd ;;
     return ERR (error_of_int err_code).
 
 (** Consumes the message code and dispatches to specific receiver functions to
     deserialize and parse a server message*)
-Definition recv_server_message (sockfd : file_descr) : optionE server_message :=
+Definition recv_server_message (sockfd : file_descr) : result server_message :=
     code <- recv_message sockfd 1 ;;
     match code with
     | [x00] => recv_server_ACK sockfd
@@ -424,24 +497,24 @@ Definition recv_server_message (sockfd : file_descr) : optionE server_message :=
     | _ => fail ("Failed to receieve server message with opcode " ++ (string_of_bytes code))
     end.
 
-Definition recv_client_REG (sockfd : file_descr) : optionE client_message :=
+Definition recv_client_REG (sockfd : file_descr) : result client_message :=
     uname <- recv_username sockfd ;;
     return REG uname.
 
-Definition recv_client_MESG (sockfd : file_descr) : optionE client_message :=
+Definition recv_client_MESG (sockfd : file_descr) : result client_message :=
     msg <- recv_string sockfd ;;
     return MESG msg.
 
-Definition recv_client_PMSG (sockfd : file_descr) : optionE client_message :=
+Definition recv_client_PMSG (sockfd : file_descr) : result client_message :=
     uname <- recv_username sockfd ;;
     msg <- recv_string sockfd ;;
     return PMSG msg uname.
 
-Definition recv_client_EXIT (sockfd : file_descr) : optionE client_message :=
+Definition recv_client_EXIT (sockfd : file_descr) : result client_message :=
     uname <- recv_username sockfd ;;
     return EXIT uname.
 
-Definition recv_client_message (sockfd : file_descr) : optionE client_message :=
+Definition recv_client_message (sockfd : file_descr) : result client_message :=
     code <- recv_message sockfd 1 ;;
     match code with
     | [x00] => recv_client_REG sockfd