mkm: add state machine to client_event spec

GaloisInc · Dec 21, 2024 · 093dd29 · 093dd29
1 parent c7f87d3
commit 093dd29
Showing 1 changed file with 15 additions and 2 deletions.
diff --git a/components/mission_key_management/client.c b/components/mission_key_management/client.c
@@ -22,8 +22,9 @@
 #endif 
 
 /* TODO list: 
+ - Fix some of the TODOs
+ - Run the test generator on the code 
  - make the key access table into a global?? 
- - Start to impose state machine properties on the protocol 
 */
 
 /*$ predicate (map<u64,u8>) KeyPred (pointer p) 
@@ -50,9 +51,19 @@ predicate (struct client) ClientPred (pointer p)
 {
     take C = Owned<struct client>(p); 
     assert ( ValidState(C.state) ) ; 
-    take K = KeyPred(C.key); // Discard the key, for now 
+    take K = KeyPred(C.key); // Discard the key
     return C; 
 }
+
+function (boolean) ValidTransition (u32 pre, u32 post) {
+   (
+       ( pre == post ) 
+    || ( (pre == (u32) CS_RECV_KEY_ID)    && (post == (u32) CS_SEND_CHALLENGE) ) 
+    || ( (pre == (u32) CS_SEND_CHALLENGE) && (post == (u32) CS_RECV_RESPONSE)  ) 
+    || ( (pre == (u32) CS_RECV_RESPONSE)  && (post == (u32) CS_SEND_KEY)       ) 
+    || ( ValidState(pre)                  && (post == (u32) CS_DONE)           ) 
+   )
+}
 $*/
 
 
@@ -303,6 +314,7 @@ requires
     ! is_null(Client_in.key); 
 ensures 
     take Client_out = ClientPred(c); 
+    Client_out.state == Client_in.state; 
 $*/
 {
     const uint8_t* buf = client_write_buffer(c);
@@ -373,6 +385,7 @@ requires
     ! is_null(Client_in.key); // TODO: should depend on state machine state 
  ensures 
     take Client_out = ClientPred(c); 
+    ValidTransition(Client_in.state, Client_out.state); 
 $*/
 {
     if (events & EPOLLIN) {