mc: Verify rmi rec destroy

This harness verifies RMI_REC_DESTROY's behaviors using
model checking.

Usage)

(in islet/model-checking)

$ RMI_TARGET=rmi_rec_destroy make verify

Signed-off-by: Changho Choi <[email protected]>

doc/getting-started/verification.md

@@ -17,6 +17,7 @@ rmi_granule_delegate
 rmi_granule_undelegate
 rmi_realm_activate
 rmi_rec_aux_count
+rmi_rec_destroy
 rmi_version
 ```
 

model-checking/Cargo.toml

@@ -11,6 +11,7 @@ mc_rmi_granule_delegate = ["islet_rmm/mc_rmi_granule_delegate"]
 mc_rmi_granule_undelegate = ["islet_rmm/mc_rmi_granule_undelegate"]
 mc_rmi_realm_activate = ["islet_rmm/mc_rmi_realm_activate"]
 mc_rmi_rec_aux_count = ["islet_rmm/mc_rmi_rec_aux_count"]
+mc_rmi_rec_destroy = ["islet_rmm/mc_rmi_rec_destroy"]
 mc_rmi_version = ["islet_rmm/mc_rmi_version"]
 
 [dependencies]

model-checking/Makefile

@@ -14,6 +14,7 @@ ALLOWED_RMI_TARGET = \
 	rmi_granule_undelegate \
 	rmi_realm_activate \
 	rmi_rec_aux_count \
+	rmi_rec_destroy \
 	rmi_version
 
 ifeq ("$(filter $(RMI_TARGET), $(ALLOWED_RMI_TARGET))", "")

model-checking/src/common.rs

@@ -3,6 +3,8 @@ use islet_rmm::granule::entry::GranuleGpt;
 use islet_rmm::granule::validate_addr;
 use islet_rmm::realm::rd::Rd;
 use islet_rmm::realm::rd::State; // tmp
+use islet_rmm::rec::Rec;
+use islet_rmm::rec::State as RecState;
 
 extern "C" {
     fn CPROVER_havoc_object(address: usize);
@@ -116,6 +118,21 @@ pub fn post_rd_state(addr: usize) -> State {
     rd.state()
 }
 
+pub fn pre_rec_state(addr: usize) -> RecState {
+    let valid_addr = pre_valid_addr(addr);
+    let rec = content::<Rec>(valid_addr);
+    rec.get_state()
+}
+
+pub fn post_rec_aux_state(addr: usize) -> u8 {
+    let valid_addr = pre_valid_addr(addr);
+    let rec = content::<Rec>(valid_addr);
+    // XXX: we currently check only the first entry to
+    //      reduce the overall verification time
+    let rec_aux = rec.aux(0) as usize;
+    post_granule_state(rec_aux)
+}
+
 pub fn initialize() {
     unsafe {
         CPROVER_havoc_object(GRANULE_REGION.as_ptr() as usize);

model-checking/src/lib.rs

@@ -9,5 +9,7 @@ mod rmi_granule_undelegate;
 mod rmi_realm_activate;
 #[cfg(feature = "mc_rmi_rec_aux_count")]
 mod rmi_rec_aux_count;
+#[cfg(feature = "mc_rmi_rec_destroy")]
+mod rmi_rec_destroy;
 #[cfg(feature = "mc_rmi_version")]
 mod rmi_version;

model-checking/src/rmi_rec_destroy.rs

@@ -0,0 +1,122 @@
+use crate::common::addr_is_granule_aligned;
+use crate::common::initialize;
+use crate::common::post_granule_state;
+use crate::common::post_rec_aux_state;
+use crate::common::pre_granule_state;
+use crate::common::pre_rec_state;
+use islet_rmm::granule::validate_addr;
+use islet_rmm::granule::GranuleState;
+use islet_rmm::monitor::Monitor;
+use islet_rmm::rec::State;
+use islet_rmm::rmi;
+use islet_rmm::rmi::error::Error;
+
+#[kani::proof]
+#[kani::unwind(7)]
+fn verify_rec_destroy() {
+    initialize();
+
+    // Initialize registers (symbolic input)
+    let regs: [usize; 8] = kani::any();
+    kani::assume(regs[0] == rmi::REC_DESTROY);
+    // TODO: check the below again
+    let rec = regs[1];
+
+    // Pre-conditions
+    let failure_rec_align_pre = !addr_is_granule_aligned(rec);
+    let failure_rec_bound_pre = !validate_addr(rec);
+    let failure_rec_gran_state_pre = pre_granule_state(rec) != GranuleState::Rec;
+    let failure_rec_state_pre = pre_rec_state(rec) == State::Running;
+    let no_failures_pre = !failure_rec_align_pre
+        && !failure_rec_bound_pre
+        && !failure_rec_gran_state_pre
+        && !failure_rec_state_pre;
+
+    // Execute command and read the result.
+    let out = Monitor::new().run(regs);
+    let result = out[0];
+
+    // Failure condition assertions
+    let prop_failure_rec_align_ante = failure_rec_align_pre;
+
+    kani::cover!();
+    if prop_failure_rec_align_ante {
+        let failure_rec_align_post = result == Error::RmiErrorInput.into();
+        let prop_failure_rec_align_cons = failure_rec_align_post;
+
+        kani::cover!();
+        assert!(prop_failure_rec_align_cons);
+    }
+
+    let prop_failure_rec_bound_ante = !failure_rec_align_pre && failure_rec_bound_pre;
+
+    kani::cover!();
+    if prop_failure_rec_bound_ante {
+        let failure_rec_bound_post = result == Error::RmiErrorInput.into();
+        let prop_failure_rec_bound_cons = failure_rec_bound_post;
+
+        kani::cover!();
+        assert!(prop_failure_rec_bound_cons);
+    }
+
+    let prop_failure_rec_gran_state_ante =
+        !failure_rec_align_pre && !failure_rec_bound_pre && failure_rec_gran_state_pre;
+
+    kani::cover!();
+    if prop_failure_rec_gran_state_ante {
+        let failure_rec_gran_state_post = result == Error::RmiErrorInput.into();
+        let prop_failure_rec_gran_state_cons = failure_rec_gran_state_post;
+
+        kani::cover!();
+        assert!(prop_failure_rec_gran_state_cons);
+    }
+
+    let prop_failure_rec_state_ante = !failure_rec_align_pre
+        && !failure_rec_bound_pre
+        && !failure_rec_gran_state_pre
+        && failure_rec_state_pre;
+
+    kani::cover!();
+    if prop_failure_rec_state_ante {
+        let failure_rec_state_post = result == Error::RmiErrorRec.into();
+        let prop_failure_rec_state_cons = failure_rec_state_post;
+
+        kani::cover!();
+        assert!(prop_failure_rec_state_cons);
+    }
+
+    // Result assertion
+    let prop_result_ante = no_failures_pre;
+
+    kani::cover!();
+    if prop_result_ante {
+        let prop_result_cons = result == rmi::SUCCESS;
+
+        kani::cover!();
+        assert!(prop_result_cons);
+    }
+
+    // Success condition assertions
+    let prop_success_rec_gran_state_ante = no_failures_pre;
+
+    kani::cover!();
+    if prop_success_rec_gran_state_ante {
+        let success_rec_gran_state_post = post_granule_state(rec) == GranuleState::Delegated;
+        let prop_success_rec_gran_state_cons =
+            success_rec_gran_state_post && result == rmi::SUCCESS;
+
+        kani::cover!();
+        assert!(prop_success_rec_gran_state_cons);
+    }
+
+    let prop_success_rec_aux_state_ante = no_failures_pre;
+
+    kani::cover!();
+    if prop_success_rec_aux_state_ante {
+        let success_rec_aux_state_post = post_rec_aux_state(rec) == GranuleState::Delegated;
+        let prop_success_rec_aux_state_cons = success_rec_aux_state_post && result == rmi::SUCCESS;
+
+        kani::cover!();
+        assert!(prop_success_rec_aux_state_cons);
+    }
+}

rmm/Cargo.toml

@@ -44,4 +44,5 @@ mc_rmi_granule_delegate = []
 mc_rmi_granule_undelegate = []
 mc_rmi_realm_activate = []
 mc_rmi_rec_aux_count = []
+mc_rmi_rec_destroy = []
 mc_rmi_version = []

rmm/src/event/mainloop.rs

@@ -46,6 +46,8 @@ impl Mainloop {
         rmi::gpt::set_event_handler(self);
         #[cfg(any(feature = "mc_rmi_realm_activate", feature = "mc_rmi_rec_aux_count"))]
         rmi::realm::set_event_handler(self);
+        #[cfg(feature = "mc_rmi_rec_destroy")]
+        rmi::rec::set_event_handler(self);
         #[cfg(feature = "mc_rmi_version")]
         rmi::version::set_event_handler(self);
     }

rmm/src/event/mod.rs

@@ -106,7 +106,8 @@ impl Context {
             #[cfg(any(
                 feature = "mc_rmi_granule_delegate",
                 feature = "mc_rmi_granule_undelegate",
-                feature = "mc_rmi_realm_activate"
+                feature = "mc_rmi_realm_activate",
+                feature = "mc_rmi_rec_destroy"
             ))]
             assert!(ret_len == 1);
             #[cfg(any(feature = "mc_rmi_rec_aux_count", feature = "mc_rmi_features"))]

rmm/src/rec.rs

@@ -18,7 +18,7 @@ pub enum RmmRecAttestState {
     NoAttestInProgress,
 }
 
-#[derive(Copy, Clone, Debug)]
+#[derive(Copy, Clone, Debug, PartialEq)]
 pub enum State {
     Ready = 1,
     Running = 2,

rmm/src/rmi/rec/handlers.rs

@@ -42,6 +42,7 @@ fn prepare_args(rd: &mut Rd, mpidr: u64) -> Result<(usize, u64, u64), Error> {
 }
 
 pub fn set_event_handler(mainloop: &mut Mainloop) {
+    #[cfg(not(kani))]
     listen!(mainloop, rmi::REC_CREATE, |arg, ret, rmm| {
         let rd = arg[0];
         let rec = arg[1];
@@ -106,6 +107,7 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
         return set_granule(&mut rec_granule, GranuleState::Rec);
     });
 
+    #[cfg(any(not(kani), feature = "mc_rmi_rec_destroy"))]
     listen!(mainloop, rmi::REC_DESTROY, |arg, _ret, rmm| {
         let mut rec_granule = get_granule_if!(arg[0], GranuleState::Rec)?;
 
@@ -121,6 +123,7 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
         Ok(())
     });
 
+    #[cfg(not(kani))]
     listen!(mainloop, rmi::REC_ENTER, |arg, ret, rmm| {
         let run_pa = arg[1];
 
@@ -217,6 +220,7 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
         host::copy_to_ptr::<Run>(&run, run_pa).ok_or(Error::RmiErrorInput)
     });
 
+    #[cfg(not(kani))]
     listen!(mainloop, rmi::PSCI_COMPLETE, |arg, _ret, _rmm| {
         let caller_pa = arg[0];
         let target_pa = arg[1];