mc: Verify rmi realm destroy

This harness verifies RMI_REALM_DESTROY's behaviors using model checking. Usage) (in islet/model-checking) $ RMI_TARGET=rmi_realm_destroy make verify Signed-off-by: Changho Choi <ch754.choi@samsung.com>
islet-project · Oct 31, 2024 · 841cf2b · 841cf2b
1 parent 8170579
commit 841cf2b
Show file tree

Hide file tree

Showing 10 changed files with 167 additions and 4 deletions.
diff --git a/doc/getting-started/verification.md b/doc/getting-started/verification.md
@@ -16,6 +16,7 @@ rmi_features
 rmi_granule_delegate
 rmi_granule_undelegate
 rmi_realm_activate
+rmi_realm_destroy
 rmi_rec_aux_count
 rmi_rec_destroy
 rmi_version

diff --git a/model-checking/Cargo.toml b/model-checking/Cargo.toml
@@ -10,6 +10,7 @@ mc_rmi_features = ["islet_rmm/mc_rmi_features"]
 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_realm_destroy = ["islet_rmm/mc_rmi_realm_destroy"]
 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"]

diff --git a/model-checking/Makefile b/model-checking/Makefile
@@ -13,6 +13,7 @@ ALLOWED_RMI_TARGET = \
 	rmi_granule_delegate \
 	rmi_granule_undelegate \
 	rmi_realm_activate \
+	rmi_realm_destroy \
 	rmi_rec_aux_count \
 	rmi_rec_destroy \
 	rmi_version

diff --git a/model-checking/src/common.rs b/model-checking/src/common.rs
@@ -118,6 +118,28 @@ pub fn post_rd_state(addr: usize) -> State {
     rd.state()
 }
 
+pub fn post_rtt_state(addr: usize) -> u8 {
+    let valid_addr = pre_valid_addr(addr);
+    let rd = content::<Rd>(valid_addr);
+    // XXX: we currently check only the first entry to
+    //      reduce the overall verification time
+    let rtt_base = rd.rtt_base();
+    post_granule_state(rtt_base)
+}
+
+pub fn pre_realm_is_live(addr: usize) -> bool {
+    let res = get_granule!(addr).map(|guard| guard.num_children());
+    let rd_num_children = if let Ok(v) = res { v } else { kani::any() };
+    let valid_addr = pre_valid_addr(addr);
+    let rd = content::<Rd>(valid_addr);
+    // XXX: we currently check only the first entry to
+    //      reduce the overall verification time
+    let rtt_base = rd.rtt_base();
+    let rtt_res = get_granule!(rtt_base).map(|guard| guard.num_children());
+    let rtt_num_children = if let Ok(v) = rtt_res { v } else { kani::any() };
+    rd_num_children > 0 || rtt_num_children > 0
+}
+
 pub fn pre_rec_state(addr: usize) -> RecState {
     let valid_addr = pre_valid_addr(addr);
     let rec = content::<Rec>(valid_addr);

diff --git a/model-checking/src/lib.rs b/model-checking/src/lib.rs
@@ -7,6 +7,8 @@ mod rmi_granule_delegate;
 mod rmi_granule_undelegate;
 #[cfg(feature = "mc_rmi_realm_activate")]
 mod rmi_realm_activate;
+#[cfg(feature = "mc_rmi_realm_destroy")]
+mod rmi_realm_destroy;
 #[cfg(feature = "mc_rmi_rec_aux_count")]
 mod rmi_rec_aux_count;
 #[cfg(feature = "mc_rmi_rec_destroy")]

diff --git a/model-checking/src/rmi_realm_destroy.rs b/model-checking/src/rmi_realm_destroy.rs
@@ -0,0 +1,119 @@
+use crate::common::addr_is_granule_aligned;
+use crate::common::initialize;
+use crate::common::{post_granule_state, post_rtt_state, pre_granule_state, pre_realm_is_live};
+use islet_rmm::granule::validate_addr;
+use islet_rmm::granule::GranuleState;
+use islet_rmm::monitor::Monitor;
+use islet_rmm::rmi;
+use islet_rmm::rmi::error::Error;
+
+#[kani::proof]
+#[kani::unwind(7)]
+fn verify_realm_destroy() {
+    initialize();
+
+    // Initialize registers (symbolic input)
+    let regs: [usize; 8] = kani::any();
+    kani::assume(regs[0] == rmi::REALM_DESTROY);
+    // TODO: check the below again
+    let rd = regs[1];
+
+    // Pre-conditions
+    let failure_rd_align_pre = !addr_is_granule_aligned(rd);
+    let failure_rd_bound_pre = !validate_addr(rd);
+    let failure_rd_state_pre = pre_granule_state(rd) != GranuleState::RD;
+    let failure_realm_live_pre = pre_realm_is_live(rd);
+    let no_failures_pre = !failure_rd_align_pre
+        && !failure_rd_bound_pre
+        && !failure_rd_state_pre
+        && !failure_realm_live_pre;
+
+    // Execute command and read the result.
+    let out = Monitor::new().run(regs);
+    let result = out[0];
+
+    // Failure condition assertions
+    let prop_failure_rd_align_ante = failure_rd_align_pre;
+
+    kani::cover!();
+    if prop_failure_rd_align_ante {
+        let failure_rd_align_post = result == Error::RmiErrorInput.into();
+        let prop_failure_rd_align_cons = failure_rd_align_post;
+
+        kani::cover!();
+        assert!(prop_failure_rd_align_cons);
+    }
+
+    let prop_failure_rd_bound_ante = !failure_rd_align_pre && failure_rd_bound_pre;
+
+    kani::cover!();
+    if prop_failure_rd_bound_ante {
+        let failure_rd_bound_post = result == Error::RmiErrorInput.into();
+        let prop_failure_rd_bound_cons = failure_rd_bound_post;
+
+        kani::cover!();
+        assert!(prop_failure_rd_bound_cons);
+    }
+
+    let prop_failure_rd_state_ante =
+        !failure_rd_align_pre && !failure_rd_bound_pre && failure_rd_state_pre;
+
+    kani::cover!();
+    if prop_failure_rd_state_ante {
+        let failure_rd_state_post = result == Error::RmiErrorInput.into();
+        let prop_failure_rd_state_cons = failure_rd_state_post;
+
+        kani::cover!();
+        assert!(prop_failure_rd_state_cons);
+    }
+
+    let prop_failure_realm_live_ante = !failure_rd_align_pre
+        && !failure_rd_bound_pre
+        && !failure_rd_state_pre
+        && failure_realm_live_pre;
+
+    kani::cover!();
+    if prop_failure_realm_live_ante {
+        let failure_realm_live_post = result == Error::RmiErrorRealm(0).into();
+        let prop_failure_realm_live_cons = failure_realm_live_post;
+
+        kani::cover!();
+        assert!(prop_failure_realm_live_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_rtt_state_ante = no_failures_pre;
+
+    kani::cover!();
+    if prop_success_rtt_state_ante {
+        let success_rtt_state_post = post_rtt_state(rd) == GranuleState::Delegated;
+        let prop_success_rtt_state_cons = success_rtt_state_post && result == rmi::SUCCESS;
+
+        kani::cover!();
+        assert!(prop_success_rtt_state_cons);
+    }
+
+    let prop_success_rd_state_ante = no_failures_pre;
+
+    kani::cover!();
+    if prop_success_rd_state_ante {
+        let success_rd_state_post = post_granule_state(rd) == GranuleState::Delegated;
+        let prop_success_rd_state_cons = success_rd_state_post && result == rmi::SUCCESS;
+
+        kani::cover!();
+        assert!(prop_success_rd_state_cons);
+    }
+
+    // TODO: add prop_sucess_vmid_ante
+}
diff --git a/rmm/Cargo.toml b/rmm/Cargo.toml
@@ -43,6 +43,7 @@ mc_rmi_features = []
 mc_rmi_granule_delegate = []
 mc_rmi_granule_undelegate = []
 mc_rmi_realm_activate = []
+mc_rmi_realm_destroy = []
 mc_rmi_rec_aux_count = []
 mc_rmi_rec_destroy = []
 mc_rmi_version = []
diff --git a/rmm/src/event/mainloop.rs b/rmm/src/event/mainloop.rs
@@ -44,7 +44,11 @@ impl Mainloop {
             feature = "mc_rmi_granule_undelegate"
         ))]
         rmi::gpt::set_event_handler(self);
-        #[cfg(any(feature = "mc_rmi_realm_activate", feature = "mc_rmi_rec_aux_count"))]
+        #[cfg(any(
+            feature = "mc_rmi_realm_activate",
+            feature = "mc_rmi_realm_destroy",
+            feature = "mc_rmi_rec_aux_count"
+        ))]
         rmi::realm::set_event_handler(self);
         #[cfg(feature = "mc_rmi_rec_destroy")]
         rmi::rec::set_event_handler(self);

diff --git a/rmm/src/event/mod.rs b/rmm/src/event/mod.rs
@@ -107,6 +107,7 @@ impl Context {
                 feature = "mc_rmi_granule_delegate",
                 feature = "mc_rmi_granule_undelegate",
                 feature = "mc_rmi_realm_activate",
+                feature = "mc_rmi_realm_destroy",
                 feature = "mc_rmi_rec_destroy"
             ))]
             assert!(ret_len == 1);

diff --git a/rmm/src/rmi/realm/mod.rs b/rmm/src/rmi/realm/mod.rs
@@ -115,7 +115,7 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
         Ok(())
     });
 
-    #[cfg(not(kani))]
+    #[cfg(any(not(kani), feature = "mc_rmi_realm_destroy"))]
     listen!(mainloop, rmi::REALM_DESTROY, |arg, _ret, rmm| {
         // get the lock for Rd
         let mut rd_granule = get_granule_if!(arg[0], GranuleState::RD)?;
@@ -124,9 +124,13 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
         }
         let rd = rd_granule.content::<Rd>()?;
         let vmid = rd.id();
-
         let rtt_base = rd.rtt_base();
 
+        // XXX: we use the below assumption to reduce the overall
+        //      verification time
+        #[cfg(kani)]
+        kani::assume(rd.rtt_num_start() == 1);
+
         #[cfg(not(feature = "gst_page_table"))]
         {
             for i in 0..rd.rtt_num_start() {
@@ -145,7 +149,12 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
 
         for i in 0..rd.rtt_num_start() {
             let rtt = rtt_base + i * GRANULE_SIZE;
-            let mut rtt_granule = get_granule_if!(rtt, GranuleState::RTT)?;
+
+            // XXX: the below can be guaranteed by Rd's invariants instead
+            #[cfg(kani)]
+            kani::assume(crate::granule::validate_addr(rtt));
+
+            let mut rtt_granule = get_granule!(rtt)?;
             set_granule(&mut rtt_granule, GranuleState::Delegated)?;
         }
 
@@ -154,6 +163,8 @@ pub fn set_event_handler(mainloop: &mut Mainloop) {
         #[cfg(not(kani))]
         // `page_table` is currently not reachable in model checking harnesses
         rmm.page_table.unmap(arg[0]);
+        // TODO: remove the below after modeling `VmidIsFree()`
+        #[cfg(not(kani))]
         remove(vmid)?;
 
         Ok(())