Merge pull request #62 from ku-sldg/asp_lib_rework

ASP Lib Rework + Demo Phrase and Client

.github/workflows/main.yml

@@ -24,7 +24,9 @@ jobs:
 
     steps:
       - name: Setup pre-deps
-        run: sudo apt install libgtk-3-0 libgtk-3-dev libgtksourceview-3.0-common libgtksourceview-3.0-dev opam
+        run: |
+          sudo apt update
+          sudo apt install libgtk-3-0 libgtk-3-dev libgtksourceview-3.0-common libgtksourceview-3.0-dev opam
 
 ############### OPAM STEPS
       - name: Restore Opam Cache

src/AM_Helpers.v

@@ -96,22 +96,19 @@ Definition lib_omits_manifest (al:AM_Library) (am:Manifest) : Manifest :=
     let aspid_list := am.(asps) in 
     let uuid_plcs_list := am.(uuidPlcs) in 
     let pubkey_plcs_list := am.(pubKeyPlcs) in 
-    let appraisal_asps_list := am.(appraisal_asps) in  
 
         Build_Manifest 
             am.(my_abstract_plc)
             aspid_list
-            appraisal_asps_list
             (lib_omits_uuid_plcs uuid_plcs_list al)
             (lib_omits_pubkey_plcs pubkey_plcs_list al)    
             manifest_set_empty 
             empty_PolicyT.
 
 Definition manifest_none_omitted (m:Manifest) : bool := 
     match m with 
-    | Build_Manifest _ asps app_asps uuids pubkeys _ _ => 
+    | Build_Manifest _ asps uuids pubkeys _ _ => 
         (is_empty_manset asps) && 
-        (is_empty_manset app_asps) &&
         (is_empty_manset uuids) &&
         (is_empty_manset pubkeys)
     end.

src/AM_Monad.v

@@ -22,7 +22,7 @@ Definition fromSome{A E:Type} (default:A) (opt:ResultT A E): A :=
   | _ => default
   end.
 
-Definition run_am_app_comp_with_default{A:Type} (am_comp:AM A) (default_A:A) (b:bool): A :=
+(* Definition run_am_app_comp_with_default{A:Type} (am_comp:AM A) (default_A:A) (b:bool): A :=
   if (b) 
   then (
   let optRes := evalErr am_comp empty_amst in
@@ -38,7 +38,7 @@ Definition run_am_app_comp_with_default{A:Type} (am_comp:AM A) (default_A:A) (b:
   (fromSome default_A optRes)
   ) 
   else 
-  (default_A).
+  (default_A). *)
 
 Definition run_am_app_comp_init_with_default{A:Type} (am_comp:AM A) (st:AM_St) (default_A:A) (b:bool): A :=
   if (b) 

src/AM_St.v

@@ -13,10 +13,6 @@ Record AM_St : Type := mkAM_St
                            am_nonceId : N_ID; 
                            amConfig : AM_Config }.
 
-Definition empty_amst :=
-  mkAM_St map_empty 0 empty_am_config.
-
-
 Inductive AM_Error : Type := 
 | cvm_error : CVM_Error -> AM_Error
 | am_error : string -> AM_Error

src/Appraisal_Defs.v

@@ -1,15 +1,15 @@
 (* Appraisal primitive implementations:  evidence unbundling, nonce generation, appraisal ASP dispatch.  *)
 
-Require Import Term_Defs_Core Term_Defs Manifest AM_St EqClass.
+Require Import String Term_Defs_Core Term_Defs Manifest AM_St EqClass Maps.
 
-Require Import Appraisal_IO_Stubs ErrorStMonad_Coq AM_Monad AM_St Manifest_Admits ErrorStringConstants.
+Require Import Appraisal_IO_Stubs ErrorStMonad_Coq AM_Monad AM_St Manifest_Admits ErrorStringConstants Manifest.
 
 
 Axiom decrypt_prim_runtime : forall bs params pk e,
   decrypt_bs_to_rawev_prim bs params pk = errC e -> e = (Runtime errStr_decryption_prim).
 
 Definition check_et_size (et:Evidence) (ls:RawEv) : ResultT unit DispatcherErrors := 
-  match (eqb (et_size et) (length ls)) with 
+  match (eqb (et_size et) (List.length ls)) with 
   | true => resultC tt 
   | false => errC (Runtime errStr_et_size)
   end.
@@ -39,13 +39,18 @@ Definition checkNonce' (nid:nat) (nonceCandidate:BS) : AM BS :=
   ret (checkNonce nonceGolden nonceCandidate).
 
 Definition check_asp_EXTD (params:ASP_PARAMS) (ls:RawEv) (ac : AM_Config) : ResultT RawEv DispatcherErrors :=
-  ac.(app_aspCb) params ls.
+  ac.(aspCb) params ls.
 
 Definition check_asp_EXTD' (params:ASP_PARAMS) (p:Plc) (sig:RawEv) (ls:RawEv) : AM RawEv :=
+  let '(asp_paramsC att_id args targ targid) := params in
   ac <- get_AM_amConfig ;;
-  match (check_asp_EXTD params (app sig ls) ac) with
-  | resultC r => ret r
-  | errC e => am_failm (am_dispatch_error e) (* (Runtime errStr_amNonce))  am_failm (am_dispatch_error e)) *)
+  match (map_get (ASP_to_APPR_ASP_Map ac) att_id) with
+  | Some appr_asp => 
+    match (check_asp_EXTD (asp_paramsC appr_asp args targ targid) (app sig ls) ac) with
+    | resultC r => ret r
+    | errC e => am_failm (am_dispatch_error e) 
+    end
+  | None => am_failm (am_dispatch_error (Runtime "We made it to appraisal without a translation for our attestation ASP"%string)) 
   end.
 
 

src/Client_AM.v

@@ -20,7 +20,8 @@ Import ListNotations.
 Set Nested Proofs Allowed.
 *)
 
-Definition am_sendReq (req_plc : Plc) (t:Term) (uuid : UUID) (authTok:ReqAuthTok) (e:RawEv) : ResultT RawEv string :=
+Definition am_sendReq (req_plc : Plc) (t:Term) (uuid : UUID) (* (authTok:ReqAuthTok) *)
+   (e:RawEv) : ResultT RawEv string :=
   let req := mkPRReq t req_plc e in 
   let js := ProtocolRunRequest_to_JSON req in
   let resp_res := make_JSON_Network_Request uuid js in
@@ -64,7 +65,7 @@ Definition gen_authEvC_if_some (ot:option Term) (uuid : UUID) (myPlc:Plc) (init_
   match ot with
   | Some auth_phrase =>
     let '(evc init_rawev_auth init_et_auth) := init_evc in
-    match am_sendReq myPlc auth_phrase uuid mt_evc init_rawev_auth with
+    match am_sendReq myPlc auth_phrase uuid (* mt_evc *) init_rawev_auth with
     | errC msg => ret (evc [] mt)
     | resultC auth_rawev =>
       let auth_et := eval auth_phrase myPlc init_et_auth in
@@ -73,14 +74,25 @@ Definition gen_authEvC_if_some (ot:option Term) (uuid : UUID) (myPlc:Plc) (init_
   | None => ret (evc [] mt)
   end.
 
-Definition run_appraisal_client (t:Term) (p:Plc) (et:Evidence) (re:RawEv) (addr:UUID) : ResultT AppResultC string :=
+Definition run_appraisal_client (t:Term) (p:Plc) (et:Evidence) (re:RawEv) 
+  (addr:UUID) : ResultT AppResultC string :=
   let expected_et := eval t p et in 
   am_sendReq_app addr t p et re.
   (*
   let comp := gen_appraise_AM expected_et re in
   run_am_app_comp comp mtc_app.
   *)
 
+Definition run_demo_client_AM (t:Term) (top_plc:Plc) (att_plc:Plc) (et:Evidence) 
+  (re:RawEv) (attester_addr:UUID) (appraiser_addr:UUID) : ResultT AppResultC string :=
+    let att_result := am_sendReq top_plc t attester_addr re in 
+    match att_result with 
+    | errC msg => errC msg 
+    | resultC att_rawev => 
+        run_appraisal_client t att_plc et att_rawev appraiser_addr
+    end.
+
+
 Definition get_am_clone_uuid : AM UUID := 
   ac <- get_AM_amConfig ;; 
   ret ( am_clone_addr ac).

src/Extraction_Cvm_Cake.v

@@ -32,7 +32,9 @@ Extract Constant get_ev => "bind get (fn st => ret (st_ev st)) : cvm_st -> coq_E
 *)
 
 Separate Extraction 
-    flexible_mechanisms run_cvm manifest_compiler 
+    flexible_mechanisms flexible_mechanisms_evidence
+    run_cvm manifest_compiler 
     Jsonifiable_AM_Library Jsonifiable_Manifest
 		handle_AM_request end_to_end_mangen_final
+    run_demo_client_AM
     Jsonifiable_Evidence_Plc_list Jsonifiable_Term_Plc_list.

src/Flexible_Mechanisms.v

@@ -58,4 +58,19 @@ Definition layered_background_check : Term :=
       )
     ).
 
-Definition flexible_mechanisms := [certificate_style; background_check; parallel_mutual_1; parallel_mutual_2; layered_background_check].
+Definition filehash_auth_phrase : Term := 
+  att P1 
+    (lseq 
+      (asp (ASPC ALL (EXTD 1) (asp_paramsC hashfile_id [] P1 hashfile_targ)))
+      (asp SIG) 
+    ).
+
+Definition filehash_demo_evidence_type : Evidence := 
+  eval filehash_auth_phrase P0 (nn 0).
+
+Definition flexible_mechanisms := 
+  [certificate_style; background_check; 
+   parallel_mutual_1; parallel_mutual_2; layered_background_check; 
+   filehash_auth_phrase].
+
+Definition flexible_mechanisms_evidence := [filehash_demo_evidence_type].

src/Flexible_Mechanisms_Vars.v

@@ -14,10 +14,12 @@ Definition P4 : Plc := "P4".
 Definition attest_id : ASP_ID := "attest_id".
 Definition appraise_id : ASP_ID := "appraise_id".
 Definition certificate_id : ASP_ID := "certificate_id".
+Definition hashfile_id : ASP_ID := "hashfile_id".
 
 (* TARG IDs *)
 Definition sys_targ : TARG_ID := "sys_targ".
 Definition att_targ : TARG_ID := "att_targ".
 Definition it_targ : TARG_ID := "it_targ".
+Definition hashfile_targ : TARG_ID := "hashfile_targ".
 
 Close Scope string_scope.

src/IO_Stubs.v

@@ -18,7 +18,7 @@ Import ListNotations.
 
 Definition make_JSON_Network_Request (uuid : UUID) (js : JSON) : ResultT JSON string. Admitted.
 
-Definition make_JSON_FS_Location_Request (dir : FS_Location) (aspid : ASP_ID) (js : JSON) : ResultT JSON string. Admitted.
+Definition make_JSON_FS_Location_Request (dir : FS_Location) (aspid : Concrete_ASP_ID) (js : JSON) : ResultT JSON string. Admitted.
 
 (** * Stub to simulate evidence collected by a parallel CVM instance *)
 Definition parallel_vm_thread (l:Loc) (t:Core_Term) (p:Plc) (e:EvC) : EvC.  Admitted.