diff --git a/apps/system/components/kata-os-common/src/capdl/mod.rs b/apps/system/components/kata-os-common/src/capdl/mod.rs
index 38e0bec..662693b 100644
--- a/apps/system/components/kata-os-common/src/capdl/mod.rs
+++ b/apps/system/components/kata-os-common/src/capdl/mod.rs
@@ -131,24 +131,6 @@ pub const CDL_TCB_TemporalFaultEP_Slot: seL4_Word = CDL_TCB_SC_Slot + 1;
 // CONFIG_ARM_HYPERVISOR_SUPPORT || CONFIG_VTX
 pub const CDL_TCB_VCPU_Slot: seL4_Word = CDL_TCB_TemporalFaultEP_Slot + 1;
 
-#[derive(Debug, PartialEq, Eq)]
-pub enum kobject_t {
-    KOBJECT_PAGE_DIRECTORY,
-    KOBJECT_PAGE_TABLE,
-    KOBJECT_FRAME,
-    KOBJECT_ARCH_NUM_TYPES,
-
-    KOBJECT_TCB,
-    KOBJECT_CNODE,
-    KOBJECT_CSLOT,
-    KOBJECT_UNTYPED,
-    KOBJECT_ENDPOINT,
-    KOBJECT_NOTIFICATION,
-    KOBJECT_REPLY,
-    KOBJECT_SCHED_CONTEXT,
-    NUM_KOBJECT_TYPES,
-}
-
 pub type CDL_ObjID = seL4_Word;
 // NB: some object id's are written in the spec as -1
 pub fn is_objid_valid(val: CDL_ObjID) -> bool {
@@ -201,7 +183,19 @@ pub enum CDL_CapType {
     CDL_PGDCap,
     CDL_ASIDControlCap,
     CDL_ASIDPoolCap,
-    // TODO(sleffler): missing arch-specific caps
+
+    #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
+    CDL_IOPortsCap,
+    #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
+    CDL_IOSpaceCap,
+
+    #[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
+    CDL_ARMIOSpaceCap,
+    #[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
+    CDL_SIDCap,
+    #[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
+    CDL_CBCap,
+
     CDL_SCCap,
     CDL_SchedControlCap,
     CDL_RTReplyCap,
@@ -366,13 +360,13 @@ impl CDL_Cap {
     #[inline]
     pub fn rights(&self) -> CDL_CapRights {
         unsafe {
-            ::core::mem::transmute::<u32, CDL_CapRights>(self._bitfield.get(4, 4) as u32)
+            ::core::mem::transmute::<usize, CDL_CapRights>(self._bitfield.get(4, 4) as usize)
         }
     }
     #[inline]
     pub fn set_rights(&mut self, val: CDL_CapRights) {
         unsafe {
-            let val: u32 = ::core::mem::transmute(val);
+            let val: usize = ::core::mem::transmute(val);
             self._bitfield.set(4, 4, val as u64)
         }
     }
@@ -415,29 +409,45 @@ impl<'a> CDL_CapMap {
     }
 }
 
-// TODO(sleffler): values depend on config & arch, this works for riscv
-//   might be better to ditch the enum or move to arch
+// Object tyype as found in the capdl input stream. This is partly defined
+// in terms of the seL4_ObjectType and otherwise using seL4_LastObjectCount.
+// The result is a mess and for zero gain (relative to just never reusing
+// an enum member value).
 #[repr(C)]
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum CDL_ObjectType {
-    CDL_Untyped = 0,
-    CDL_TCB,
-    CDL_Endpoint,
-    CDL_Notification,
-    CDL_CNode,
+    CDL_Endpoint        = sel4_sys::seL4_EndpointObject as isize,
+    CDL_Notification    = sel4_sys::seL4_NotificationObject as isize,
+    CDL_TCB             = sel4_sys::seL4_TCBObject as isize,
+    CDL_CNode           = sel4_sys::seL4_CapTableObject as isize,
+    CDL_Untyped         = sel4_sys::seL4_UntypedObject as isize,
 
     #[cfg(feature = "CONFIG_KERNEL_MCS")]
-    CDL_SchedContext,
+    CDL_SchedContext    = sel4_sys::seL4_SchedContextObject as isize,
     #[cfg(feature = "CONFIG_KERNEL_MCS")]
-    CDL_RTReply,
+    CDL_RTReply         = sel4_sys::seL4_ReplyObject as isize,
 
-    // XXX these work for CONFIG_ARCH_RISCV
-    CDL_Frame,
-    CDL_Mega_Frame,
-    CDL_PT,
+    CDL_Frame           = sel4_sys::seL4_SmallPageObject as isize,
+    CDL_PT              = sel4_sys::seL4_PageTableObject as isize,
+    #[cfg(any(target_arch = "arm", target_arch = "aarch64", target_arch = "x86"))]
+    CDL_PD              = sel4_sys::seL4_PageDirectoryObject as isize,
 
-    // NB: remainder are numbered relative to seL4_ObjectTypeCount
-    CDL_ASIDPool = seL4_ObjectTypeCount + 1,
+    #[cfg(target_arch = "aarch64")]
+    CDL_PUD             = sel4_sys::seL4_PageUpperDirectoryObject as isize,
+    #[cfg(target_arch = "aarch64")]
+    CDL_PGD             = sel4_sys::seL4_PageGlobalDirectoryObject as isize,
+
+    #[cfg(any(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT", feature = "CONFIG_VTX"))]
+    CDL_VCPU            = sel4_sys::seL4_VCPUObject as isize,
+
+    #[cfg(target_arch = "x86_64")]
+    CDL_PML4             = sel4_sys::seL4_PML4Object as isize,
+    #[cfg(target_arch = "x86_64")]
+    CDL_PDPT             = sel4_sys::seL4_PDPTObject as isize,
+
+    // NB: the following are numbered relative to seL4_ObjectTypeCount,
+    //   do not re-order!
+    CDL_ASIDPool        = seL4_ObjectTypeCount + 1,
     CDL_Interrupt,
     CDL_IOPorts,        // CONFIG_ARCH_X86
     CDL_IODevice,       // CONFIG_ARCH_X86
@@ -458,6 +468,7 @@ pub enum CDL_ObjectType {
 }
 impl From<CDL_ObjectType> for seL4_ObjectType {
     fn from(type_: CDL_ObjectType) -> seL4_ObjectType {
+        // TODO(sleffler): maybe assert type_ < seL4_ObjectTypeCount
         unsafe { ::core::mem::transmute(type_) }
     }
 }
diff --git a/apps/system/components/kata-os-common/src/model/Cargo.toml b/apps/system/components/kata-os-common/src/model/Cargo.toml
index 5e5a5fc..88bd469 100644
--- a/apps/system/components/kata-os-common/src/model/Cargo.toml
+++ b/apps/system/components/kata-os-common/src/model/Cargo.toml
@@ -8,6 +8,8 @@ build = "build.rs"
 
 [build-dependencies]
 sel4-config = { path = "../sel4-config" }
+serde = { version = "1.0", features = ["derive"] }
+serde_yaml = "0.8"
 
 [build-env]
 SEL4_OUT_DIR = "${ROOTDIR}out/kata/kernel"
diff --git a/apps/system/components/kata-os-common/src/model/arch/aarch32.rs b/apps/system/components/kata-os-common/src/model/arch/aarch32.rs
new file mode 100644
index 0000000..2d6f703
--- /dev/null
+++ b/apps/system/components/kata-os-common/src/model/arch/aarch32.rs
@@ -0,0 +1,178 @@
+// ARM aarch32 target support.
+
+#![allow(non_camel_case_types)]
+
+use static_assertions::assert_cfg;
+assert_cfg!(all(target_arch = "arm", target_pointer_width = "32"));
+
+mod arm;
+pub use arm::*;
+
+use capdl::*;
+use capdl::CDL_CapType::*;
+use capdl::CDL_ObjectType::*;
+use crate::KataOsModel;
+
+use sel4_sys::seL4_CapInitThreadCNode;
+use sel4_sys::seL4_CapIRQControl;
+use sel4_sys::seL4_CPtr;
+use sel4_sys::seL4_Error;
+use sel4_sys::seL4_IRQControl_GetTrigger;
+use sel4_sys::seL4_LargePageBits;
+use sel4_sys::seL4_ObjectType::*;
+use sel4_sys::seL4_ObjectType;
+use sel4_sys::seL4_PageBits;
+use sel4_sys::seL4_PageTableIndexBits;
+use sel4_sys::seL4_Result;
+use sel4_sys::seL4_UserContext;
+use sel4_sys::seL4_Word;
+use sel4_sys::seL4_WordBits;
+
+const CDL_PT_NUM_LEVELS: usize = 2;
+// TOOD(sleffler): levels really should be 0 & 1, the names are vestiges of 64-bit support
+const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
+
+fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
+
+pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
+    match object_size {
+        seL4_PageBits => seL4_ARM_SmallPageObject,
+        seL4_LargePageBits => seL4_ARM_LargePageObject,
+        _ => panic!("Unexpected frame size {}", object_size),
+    }
+}
+
+pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Result {
+    assert_eq!(obj.r#type(), CDL_ARMInterrupt);
+    // XXX seL4_IRQControl_GetTriggerCore for NUM_NODES > 1
+    unsafe {
+        seL4_IRQControl_GetTrigger(
+            seL4_CapIRQControl,
+            irq,
+            obj.armirq_trigger(),
+            /*root=*/ seL4_CapInitThreadCNode as usize,
+            /*index=*/ free_slot,
+            /*depth=*/ seL4_WordBits as u8,
+        )
+    }
+}
+
+pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_UserContext {
+    #[rustfmt::skip]
+    static mut regs: seL4_UserContext = seL4_UserContext {
+        pc: 0, sp: 0, cpsr: 0,
+        r0:  0, r1:  0, r8:  0, r9:  0, r10: 0, r11: 0, r12: 0,
+        r2:  0, r3:  0, r4:  0, r5:  0, r6:  0, r7:  0, r14: 0,
+        tpidrurw: 0, tpidruro: 0,
+    };
+
+    assert_eq!(cdl_tcb.r#type(), CDL_TCB);
+
+    unsafe {
+        regs.pc = cdl_tcb.tcb_pc();
+        regs.sp = sp; // NB: may be adjusted from cdl_tcb.tcb_sp()
+
+        let argv = core::slice::from_raw_parts(cdl_tcb.tcb_init(), cdl_tcb.tcb_init_sz());
+        regs.r0 = if argv.len() > 0 { argv[0] } else { 0 };
+        regs.r1 = if argv.len() > 1 { argv[1] } else { 0 };
+        regs.r2 = if argv.len() > 2 { argv[2] } else { 0 };
+        regs.r3 = if argv.len() > 3 { argv[3] } else { 0 };
+
+        //        trace!("Start {} with pc {:#x} sp {:#x} argv {:?}", cdl_tcb.name(),
+        //               regs.pc, regs.sp, argv);
+
+        &regs as *const seL4_UserContext
+    }
+}
+
+impl<'a> KataOsModel<'a> {
+    pub fn create_arch_object(
+        &mut self,
+        _obj: &CDL_Object,
+        _id: CDL_ObjID,
+        _free_slot: usize,
+    ) -> Option<seL4_Error> {
+        // CDL_SID objects with CONFIG_ARM_SMU?
+        None
+    }
+
+    // TODO(sleffler): BLINDLY COPIED FROM RISCV, CONVERT
+
+    pub fn init_vspace(&mut self, obj_id: CDL_ObjID) -> seL4_Result {
+        self.init_level_2(obj_id, 0, obj_id)
+    }
+
+    fn init_level_3(
+        &mut self,
+        level_3_obj: CDL_ObjID,
+        level_0_obj: CDL_ObjID,
+        level_3_base: usize,
+    ) -> seL4_Result {
+        for slot in self.get_object(level_3_obj).slots_slice() {
+            let frame_cap = &slot.cap;
+            self.map_page_frame(
+                frame_cap,
+                level_0_obj,
+                frame_cap.cap_rights().into(),
+                level_3_base + (slot.slot << seL4_PageBits),
+            )?;
+        }
+        Ok(())
+    }
+
+    fn init_level_2(
+        &mut self,
+        level_0_obj: CDL_ObjID,
+        level_2_base: usize,
+        level_2_obj: CDL_ObjID,
+    ) -> seL4_Result {
+        for slot in self.get_object(level_2_obj).slots_slice() {
+            let base = level_2_base + (slot.slot << (CDL_PT_LEVEL_3_IndexBits + seL4_PageBits));
+            let level_3_cap = &slot.cap;
+            if level_3_cap.r#type() == CDL_FrameCap {
+                self.map_page_frame(
+                    level_3_cap,
+                    level_0_obj,
+                    level_3_cap.cap_rights().into(),
+                    base,
+                )?;
+            } else {
+                let level_3_obj = level_3_cap.obj_id;
+                self.map_page_table(level_3_cap, level_0_obj, base)?;
+                self.init_level_3(level_3_obj, level_0_obj, base)?;
+            }
+        }
+        Ok(())
+    }
+
+    pub fn get_cdl_frame_pt(&self, pd: CDL_ObjID, vaddr: usize) -> Option<&'a CDL_Cap> {
+        self.get_cdl_frame_pt_recurse(pd, vaddr, 2)
+    }
+
+    /**
+     * Do a recursive traversal from the top to bottom of a page table structure to
+     * get the cap for a particular page table object for a certain vaddr at a certain
+     * level. The level variable treats level==CDL_PT_NUM_LEVELS as the root page table
+     * object, and level 0 as the bottom level 4k frames.
+     */
+    fn get_cdl_frame_pt_recurse(
+        &self,
+        root: CDL_ObjID,
+        vaddr: usize,
+        level: usize,
+    ) -> Option<&'a CDL_Cap> {
+        fn PT_LEVEL_SLOT(vaddr: usize, level: usize) -> usize {
+            (vaddr >> ((seL4_PageTableIndexBits * (level - 1)) + seL4_PageBits))
+                & MASK(seL4_PageTableIndexBits)
+        }
+
+        let obj_id = if level < CDL_PT_NUM_LEVELS {
+            self.get_cdl_frame_pt_recurse(root, vaddr, level + 1)?
+                .obj_id
+        } else {
+            root
+        };
+        self.get_object(obj_id)
+            .get_cap_at(PT_LEVEL_SLOT(vaddr, level))
+    }
+}
diff --git a/apps/system/components/kata-os-common/src/model/arch/aarch64.rs b/apps/system/components/kata-os-common/src/model/arch/aarch64.rs
index b020c0f..c976fa1 100644
--- a/apps/system/components/kata-os-common/src/model/arch/aarch64.rs
+++ b/apps/system/components/kata-os-common/src/model/arch/aarch64.rs
@@ -8,30 +8,32 @@ assert_cfg!(target_arch = "aarch64");
 mod arm;
 pub use arm::*;
 
-use crate::KataOsModel;
-use capdl::kobject_t::*;
+use capdl::*;
 use capdl::CDL_CapType::*;
 use capdl::CDL_ObjectType::*;
-use capdl::*;
-use log::{error, trace};
+use crate::KataOsModel;
 
+use sel4_sys::seL4_ARM_PageDirectory_Map;
+use sel4_sys::seL4_ARM_PageUpperDirectory_Map;
 use sel4_sys::seL4_CapInitThreadCNode;
 use sel4_sys::seL4_CapIRQControl;
 use sel4_sys::seL4_CPtr;
 use sel4_sys::seL4_Error;
-use sel4_sys::seL4_IRQControl_Get;
+use sel4_sys::seL4_HugePageBits;
+use sel4_sys::seL4_IRQControl_GetTrigger;
+use sel4_sys::seL4_LargePageBits;
 use sel4_sys::seL4_ObjectType::*;
+use sel4_sys::seL4_ObjectType;
 use sel4_sys::seL4_PageBits;
 use sel4_sys::seL4_PageDirIndexBits;
 use sel4_sys::seL4_PageTableIndexBits;
+use sel4_sys::seL4_PGDIndexBits;
 use sel4_sys::seL4_PUDIndexBits;
 use sel4_sys::seL4_Result;
 use sel4_sys::seL4_UserContext;
+use sel4_sys::seL4_VMAttributes;
 use sel4_sys::seL4_Word;
-
-pub use arm::PAGE_SIZE;
-pub const STACK_ALIGNMENT_BYTES: usize = 16;
-pub const REG_ARGS: seL4_Word = 4; // Number of regs for passing thread args
+use sel4_sys::seL4_WordBits;
 
 pub const CDL_PT_LEVEL_1_IndexBits: usize = seL4_PUDIndexBits;
 pub const CDL_PT_LEVEL_2_IndexBits: usize = seL4_PageDirIndexBits;
@@ -39,17 +41,21 @@ pub const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
 
 fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
 
-pub fn PD_SLOT(vaddr: usize) -> usize {
-    (vaddr >> (seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PageDirIndexBits)
+pub fn PGD_SLOT(vaddr: usize) -> usize {
+    (vaddr >> (seL4_PUDIndexBits + seL4_PageDirIndexBits + seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PGDIndexBits)
+}
+pub fn PUD_SLOT(vaddr: usize) -> usize {
+    (vaddr >> (seL4_PageDirIndexBits + seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PUDIndexBits)
 }
-// NB: used for tcb_args::maybe_spill_tcb_args
-pub fn PT_SLOT(vaddr: usize) -> usize { (vaddr >> seL4_PageBits) & MASK(seL4_PageTableIndexBits) }
 
-// Identifies IRQ objects that potentially need special processing.
-pub fn is_irq(type_: CDL_ObjectType) -> bool { type_ == CDL_ARMInterrupt || type_ == CDL_Interrupt }
-
-// Identifies objects that need to be instantiated.
-pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
+pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
+    match object_size {
+        seL4_PageBits => seL4_ARM_SmallPageObject,
+        seL4_LargePageBits => seL4_ARM_LargePageObject,
+        seL4_HugePageBits => seL4_ARM_HugePageObject,
+        _ => panic!("Unexpected frame size {}", object_size),
+    }
+}
 
 pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Result {
     assert_eq!(obj.r#type(), CDL_ARMInterrupt);
@@ -96,40 +102,6 @@ pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_User
     }
 }
 
-pub fn kobject_get_size(t: kobject_t, object_size: seL4_Word) -> seL4_Word {
-    if t == KOBJECT_FRAME && object_size == seL4_HugePageBits {
-        return object_size;
-    }
-    if t == KOBJECT_PAGE_UPPER_DIRECTORY {
-        return seL4_PUDBits;
-    }
-    #[cfg(feature = "CONFIG_KERNEL_MCS")]
-    if t == KOBJECT_SCHED_CONTEXT {
-        return core::cmp::max(object_size, sel4_sys::seL4_MinSchedContextBits);
-    }
-    error!("Unexpected object: type {:?} size {}", t, object_size);
-    0
-}
-pub fn kobject_get_type(t: kobject_t, object_size: seL4_Word) -> seL4_ObjectType {
-    match t {
-        KOBJECT_PAGE_GLOBAL_DIRECTORY => {
-            return seL4_ARM_PageGlobalDirectoryObject;
-        }
-        KOBJECT_PAGE_UPPER_DIRECTORY => {
-            return seL4_ARM_PageUpperDirectoryObject;
-        }
-        KOBJECT_FRAME => {
-            if object_size == seL4_HugePageBits {
-                return seL4_ARM_HugePageObject;
-            }
-            error!("Unexpected frame size {}", object_size);
-        }
-        _ => {}
-    }
-    error!("Unexpected object: type {:?} size {}", t, object_size);
-    seL4_InvalidObjectType
-}
-
 impl<'a> KataOsModel<'a> {
     pub fn create_arch_object(
         &mut self,
@@ -214,11 +186,11 @@ impl<'a> KataOsModel<'a> {
                     base,
                 )?;
             } else {
-                let level_3_obj = level_3_cap.obj_id;
                 self.map_page_dir(level_2_cap, level_0_obj, base)?;
-                self.init_level_2(level_0_obj, base, level_2_obj.obj_id)?;
+                self.init_level_2(level_0_obj, base, level_2_cap.obj_id)?;
             }
         }
+        Ok(())
     }
 
     fn map_page_dir(&self, page_cap: &CDL_Cap, pd_id: CDL_ObjID, vaddr: seL4_Word) -> seL4_Result {
@@ -240,19 +212,19 @@ impl<'a> KataOsModel<'a> {
         &mut self,
         level_0_obj: CDL_ObjID,
         level_0_base: usize,
-        level_0_obj: CDL_ObjID,
-    ) -> Result<(), seL4_Error> {
+        _level_0_obj: CDL_ObjID,
+    ) -> seL4_Result {
         for slot in self.get_object(level_0_obj).slots_slice() {
-            let base = level_0_base
-                + (slot.slot
+            let base = (level_0_base + slot.slot)
                     << (CDL_PT_LEVEL_1_IndexBits
                         + CDL_PT_LEVEL_2_IndexBits
                         + CDL_PT_LEVEL_3_IndexBits
-                        + seL4_PageBits));
+                        + seL4_PageBits);
             let level_1_cap = &slot.cap;
             self.map_page_upper_dir(level_1_cap, level_0_obj, base)?;
             self.init_level_1(level_0_obj, base, level_1_cap.obj_id)?;
         }
+        Ok(())
     }
 
     fn map_page_upper_dir(
@@ -277,7 +249,7 @@ impl<'a> KataOsModel<'a> {
 
     pub fn get_cdl_frame_pt(&self, pd: CDL_ObjID, vaddr: usize) -> Option<&'a CDL_Cap> {
         let pd_cap = self.get_cdl_frame_pd(pd, vaddr)?;
-        self.get_spec_object(pd_cap.obj_id)
+        self.get_object(pd_cap.obj_id)
             .get_cap_at(PD_SLOT(vaddr))
     }
 
@@ -286,15 +258,15 @@ impl<'a> KataOsModel<'a> {
             feature = "CONFIG_ARM_HYPERVISOR_SUPPORT",
             feature = "CONFIG_ARM_PA_SIZE_BITS_40"
         )) {
-            self.get_spec_object(root).get_cap_at(PUD_SLOT(vaddr))
+            self.get_object(root).get_cap_at(PUD_SLOT(vaddr))
         } else {
             let pud_cap = self.get_cdl_frame_pud(root, vaddr)?;
-            self.get_spec_object(pud_cap.obj_id)
+            self.get_object(pud_cap.obj_id)
                 .get_cap_at(PUD_SLOT(vaddr))
         }
     }
 
     fn get_cdl_frame_pud(&self, root: CDL_ObjID, vaddr: usize) -> Option<&'a CDL_Cap> {
-        self.get_spec_object(root).get_cap_at(PGD_SLOT(vaddr))
+        self.get_object(root).get_cap_at(PGD_SLOT(vaddr))
     }
 }
diff --git a/apps/system/components/kata-os-common/src/model/arch/arm.rs b/apps/system/components/kata-os-common/src/model/arch/arm.rs
index 032b738..cbd39fb 100644
--- a/apps/system/components/kata-os-common/src/model/arch/arm.rs
+++ b/apps/system/components/kata-os-common/src/model/arch/arm.rs
@@ -1,84 +1,71 @@
-// ARM 32-bit target support.
+// ARM common target support.
 
 #![allow(non_camel_case_types)]
 
 use static_assertions::assert_cfg;
-assert_cfg!(all(target_arch = "arm", target_pointer_width = "32"));
+assert_cfg!(any(target_arch = "arm", target_arch = "aarch64"));
 
-use crate::KataOsModel;
-use capdl::kobject_t::*;
-use capdl::CDL_CapType::*;
 use capdl::CDL_ObjectType::*;
 use capdl::*;
-use log::{error, trace};
 
 use sel4_sys::seL4_ARM_Page_CleanInvalidate_Data;
-use sel4_sys::seL4_ARM_Page_Map;
+use sel4_sys::seL4_ARM_Page_GetAddress;
 use sel4_sys::seL4_ARM_Page_Unify_Instruction;
-
-use sel4_sys::seL4_CapInitThreadCNode;
-use sel4_sys::seL4_CapIRQControl;
-use sel4_sys::seL4_CPtr;
-use sel4_sys::seL4_Error;
-use sel4_sys::seL4_IRQControl_Get;
-use sel4_sys::seL4_ObjectType::*;
+use sel4_sys::seL4_CapRights;
+use sel4_sys::seL4_ObjectType;
+use sel4_sys::seL4_Page;
 use sel4_sys::seL4_PageBits;
 use sel4_sys::seL4_PageDirIndexBits;
 use sel4_sys::seL4_PageTableIndexBits;
-use sel4_sys::seL4_PUDIndexBits;
 use sel4_sys::seL4_Result;
-use sel4_sys::seL4_UserContext;
+use sel4_sys::seL4_VMAttributes;
 use sel4_sys::seL4_Word;
 
 pub const PAGE_SIZE: usize = 4096;
 pub const STACK_ALIGNMENT_BYTES: usize = 16;
 pub const REG_ARGS: seL4_Word = 4; // Number of regs for passing thread args
 
-pub const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
+include!(concat!(env!("OUT_DIR"), "/platform_gen.rs"));
 
-// NB: this overrides what sel4_sys provides
-pub fn seL4_Page_Map(
-    sel4_page: seL4_ARM_Page,
-    sel4_pd: seL4_ARM_PageTable,
-    vaddr: seL4_Word,
+// When seL4 creates a new frame object it zeroes the associated memory
+// through a cached kernel mapping. If we are configuring a cached
+// mapping for the target, standard coherence protocols ensure
+// everything works as expected. However, if we are configuring an
+// uncached mapping for the target, the dirty zero data cached from the
+// kernel's mapping is likely flushed to memory at some time in the
+// future causing an unpleasant surprise for the target whose own
+// uncached writes are mysteriously overwritten. To prevent this, we
+// unify the mapping here, flushing the cached data from the kernel's
+// mapping.
+pub unsafe fn seL4_Page_Map_Flush(
+    page_type: seL4_ObjectType,
+    sel4_page: seL4_Page,
     rights: seL4_CapRights,
-    vm_attribs: seL4_ARM_VMAttributes,
+    vm_attribs: seL4_VMAttributes,
 ) -> seL4_Result {
-    if !rights.get_capAllowGrant() {
-        vm_attribs |= seL4_ARM_ExecuteNever;
-    }
-    seL4_ARM_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs)?;
-
-    // XXX lookup frame_size_bits & page
-    /* When seL4 creates a new frame object it zeroes the associated memory
-     * through a cached kernel mapping. If we are configuring a cached
-     * mapping for the target, standard coherence protocols ensure
-     * everything works as expected. However, if we are configuring an
-     * uncached mapping for the target, the dirty zero data cached from the
-     * kernel's mapping is likely flushed to memory at some time in the
-     * future causing an unpleasant surprise for the target whose own
-     * uncached writes are mysteriously overwritten. To prevent this, we
-     * unify the mapping here, flushing the cached data from the kernel's
-     * mapping.
-     */
-    const CHAR_BIT: usize = 8; // XXX
-    assert!(frame_size_bits <= size_of::<usize>() * CHAR_BIT - 1, "illegal object size");
-
     let addr = seL4_ARM_Page_GetAddress(sel4_page);
-    if addr.paddr >= memory_region[0].start && addr.paddr <= memory_region[0].end {
-        if !(vm_attribs & seL4_ARM_PageCacheable) && spec.objects[page].paddr() == 0 {
+    if MEMORY_REGIONS[0].start <= addr.paddr && addr.paddr <= MEMORY_REGIONS[0].end {
+        let frame_size_bits = page_type.size_bits().unwrap();
+        assert!(frame_size_bits <= (usize::BITS - 1) as usize,
+                "{:?}: illegal object size", page_type);
+
+        // NB: could minimize invalidations by checking page's paddr, but
+        //   given the cost already incurred to lookup the page's paddr
+        //   just always do it
+        if ((vm_attribs as u32) & sel4_sys::seL4_ARM_VMAttributes::PageCacheable as u32) == 0 {
             seL4_ARM_Page_CleanInvalidate_Data(sel4_page, 0, BIT(frame_size_bits))?;
         }
-        if rights.get_capAllowGrant() {
+        if rights.get_capAllowGrant() != 0 {
             seL4_ARM_Page_Unify_Instruction(sel4_page, 0, BIT(frame_size_bits))?;
         }
     }
-
     Ok(())
 }
 
-fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
+fn BIT(bit_num: usize) -> usize { 1 << bit_num }
+fn MASK(pow2_bits: usize) -> usize { BIT(pow2_bits) - 1 }
 
+#[allow(dead_code)]
 pub fn PD_SLOT(vaddr: usize) -> usize {
     (vaddr >> (seL4_PageTableIndexBits + seL4_PageBits)) & MASK(seL4_PageDirIndexBits)
 }
@@ -90,198 +77,3 @@ pub fn is_irq(type_: CDL_ObjectType) -> bool { type_ == CDL_ARMInterrupt || type
 
 // Identifies objects that need to be instantiated.
 pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
-
-pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Error {
-    let root = seL4_CapInitThreadCNode;
-    let index = free_slot;
-    let depth = seL4_WordBits as u8;
-    match obj.r#type() {
-        // XXX seL4_IRQControl_GetTriggerCore for NUM_NODES > 1
-        #[cfg(feature = "CONFIG_SMP_SUPPORT")]
-        CDL_ARMInterrupt => {
-            seL4_IRQControl_GetTriggerCore(
-                seL4_CapIRQControl,
-                irq,
-                obj.armirq_trigger(),
-                root,
-                index,
-                depth,
-                obj.armirq_target(),
-            )
-        }
-        #[cfg(not(feature = "CONFIG_SMP_SUPPORT"))]
-        CDL_ARMInterrupt => {
-            seL4_IRQControl_GetTrigger(
-                seL4_CapIRQControl,
-                irq,
-                obj.armirq_trigger(),
-                root,
-                index,
-                depth,
-            )
-        }
-        _ => seL4_IRQControl_Get(seL4_CapIRQControl, irq, root, index, depth),
-    }
-}
-
-pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_UserContext {
-    #[rustfmt::skip]
-    static mut regs: seL4_UserContext = seL4_UserContext {
-        pc: 0, sp: 0, spsr: 0,
-        x0:  0, x1:  0, x2:  0, x3:  0, x4:  0, x5:  0, x6:  0, x7:  0,
-        x8:  0, x9:  0, x10: 0, x11: 0, x12: 0, x13: 0, x14: 0, x15: 0,
-        x16: 0, x17: 0, x18: 0, x19: 0, x20: 0, x21: 0, x22: 0, x23: 0,
-        x24: 0, x25: 0, x26: 0, x27: 0, x28: 0, x29: 0, x30: 0,
-        tpidr_el0: 0, tpidrro_el0: 0,
-    };
-
-    assert_eq!(cdl_tcb.r#type(), CDL_TCB);
-
-    unsafe {
-        regs.pc = cdl_tcb.tcb_pc();
-        regs.sp = sp; // NB: may be adjusted from cdl_tcb.tcb_sp()
-
-        let argv = core::slice::from_raw_parts(cdl_tcb.tcb_init(), cdl_tcb.tcb_init_sz());
-        regs.x0 = if argv.len() > 0 { argv[0] } else { 0 };
-        regs.x1 = if argv.len() > 1 { argv[1] } else { 0 };
-        regs.x2 = if argv.len() > 2 { argv[2] } else { 0 };
-        regs.x3 = if argv.len() > 3 { argv[3] } else { 0 };
-
-        //        trace!("Start {} with pc {:#x} sp {:#x} argv {:?}", cdl_tcb.name(),
-        //               regs.pc, regs.sp, argv);
-
-        &regs as *const seL4_UserContext
-    }
-}
-
-pub fn kobject_get_size(t: kobject_t, object_size: seL4_Word) -> seL4_Word {
-    if t == KOBJECT_FRAME && object_size == seL4_HugePageBits {
-        return object_size;
-    }
-    if t == KOBJECT_PAGE_UPPER_DIRECTORY {
-        return seL4_PUDBits;
-    }
-    #[cfg(feature = "CONFIG_KERNEL_MCS")]
-    if t == KOBJECT_SCHED_CONTEXT {
-        return core::cmp::max(object_size, sel4_sys::seL4_MinSchedContextBits);
-    }
-    error!("Unexpected object: type {:?} size {}", t, object_size);
-    0
-}
-pub fn kobject_get_type(t: kobject_t, object_size: seL4_Word) -> seL4_ObjectType {
-    match t {
-        KOBJECT_PAGE_GLOBAL_DIRECTORY => {
-            return seL4_ARM_PageGlobalDirectoryObject;
-        }
-        KOBJECT_PAGE_UPPER_DIRECTORY => {
-            return seL4_ARM_PageUpperDirectoryObject;
-        }
-        KOBJECT_FRAME => {
-            if object_size == seL4_HugePageBits {
-                return seL4_ARM_HugePageObject;
-            }
-            error!("Unexpected frame size {}", object_size);
-        }
-        _ => {}
-    }
-    error!("Unexpected object: type {:?} size {}", t, object_size);
-    seL4_InvalidObjectType
-}
-
-impl<'a> KataOsModel<'a> {
-    pub fn create_arch_object(
-        &mut self,
-        obj: &CDL_Object,
-        _id: CDL_ObjID,
-        free_slot: usize,
-    ) -> Option<seL4_Error> {
-        match obj.r#type() {
-            #[cfg(feature = "CONFIG_ARM_SMMU")]
-            CDL_SID => {
-                /* There can be multiple sids per context bank, currently only 1
-                 * sid per cb is implemented for the vms. When this gets extended
-                 * we need to decide to add sid number -> cb number map into the
-                 * haskell / python tool or generate the capdl spec so that the
-                 * order remains correct here e.g a list a stream ids followed by
-                 * the cb they are mapped to, the cb condition here (1***) will the
-                 * reset the stream id number back to 0 for the next context bank.
-                 */
-                assert!(sid_number <= MAX_STREAM_IDS);
-                // XXX handle error
-                seL4_ARM_SIDControl_GetSID(
-                    seL4_CapSMMUSIDControl,
-                    self.sid_number,
-                    seL4_CapInitThreadCNode,
-                    free_slot,
-                    seL4_WordBits as u8,
-                );
-                self.sid_number += 1;
-                Some(seL4_NoError)
-            }
-            #[cfg(feature = "CONFIG_ARM_SMMU")]
-            CDL_CB => {
-                self.sid_number = 0; //(1***)
-                Some(seL4_ARM_CBControl_GetCB(
-                    seL4_CapSMMUCBControl,
-                    obj.cb_bank(),
-                    seL4_CapInitThreadCNode,
-                    free_slot,
-                    seL4_WordBits as u8,
-                ))
-            }
-            _ => None,
-        }
-    }
-
-    pub fn init_vspace(&mut self, obj_id: CDL_ObjID) -> seL4_Result {
-        assert_eq!(self.get_object(obj_id).r#type(), CDL_PD);
-        // XXX C code does all PD's before PT's, not sure if this works
-        self.map_page_directory(obj_id)?;
-        self.map_page_directory_page_tables(obj_id)?;
-        Ok(())
-    }
-
-    fn map_page_directory(&self, pd_id: CDL_ObjID) {
-        fn map_page_directory_slot(pd_id: CDL_ObjID, pd_slot: &CDL_CapSlot) {
-            let page_cap = &pd_slot.cap;
-            let page_vaddr = pd_slot.slot << (seL4_PageTableIndexBits + seL4_PageBits);
-            self.map_page(page_cap, pd_id, page_cap.cap_rights(), page_vaddr);
-        }
-
-        for slot in self.spec.get_object(pd_id).slots_slice() {
-            map_page_directory_slot(pd_id, &slot);
-        }
-    }
-
-    fn map_page_directory_page_tables(&self, pd: CDL_ObjID) {
-        fn map_page_table_slots(pd: CDL_ObjID, pd_slot: &CDL_CapSlot) {
-            fn map_page_table_slot(
-                pd: CDL_ObjID,
-                pt: CDL_ObjID,
-                pt_vaddr: seL4_Word,
-                pt_slot: &CDL_CapSlot,
-            ) {
-                let page_cap = &pt_slot.cap;
-                let page_vaddr = pt_vaddr + (pt_slot.slot << seL4_PageBits);
-                self.map_page(page_cap, pd, page_cap.cap_rights(), page_vaddr);
-            }
-
-            let page_cap = &pd_slot.cap;
-            if (page_cap.r#type() == CDL_PTCap) {
-                let page = page_cap.obj_id;
-                let page_vaddr = pd_slot.slot << (seL4_PageTableIndexBits + seL4_PageBits);
-                for slot in self.spec.get_object(page).slots_slice() {
-                    self.map_page_table_slot(pd, page, page_vaddr, &slot);
-                }
-            }
-        }
-
-        for slot in self.spec.get_object(pd).slots_slice() {
-            self.map_page_table_slots(pd, &slot);
-        }
-    }
-
-    pub fn get_cdl_frame_pt(&mut self, pd: CDL_ObjID, vaddr: usize) -> Option<&'a mut CDL_Cap> {
-        self.get_spec_object(pd).get_cap_at(PD_SLOT(vaddr))
-    }
-}
diff --git a/apps/system/components/kata-os-common/src/model/arch/riscv.rs b/apps/system/components/kata-os-common/src/model/arch/riscv.rs
index 43a9af5..af73e03 100644
--- a/apps/system/components/kata-os-common/src/model/arch/riscv.rs
+++ b/apps/system/components/kata-os-common/src/model/arch/riscv.rs
@@ -9,9 +9,14 @@ assert_cfg!(any(target_arch = "riscv32", target_arch = "riscv64"));
 use capdl::CDL_ObjectType::*;
 use capdl::*;
 
+use sel4_sys::seL4_CapRights;
+use sel4_sys::seL4_ObjectType;
+use sel4_sys::seL4_Page;
 use sel4_sys::seL4_PageBits;
 use sel4_sys::seL4_PageDirIndexBits;
 use sel4_sys::seL4_PageTableIndexBits;
+use sel4_sys::seL4_Result;
+use sel4_sys::seL4_VMAttributes;
 use sel4_sys::seL4_Word;
 
 pub const PAGE_SIZE: usize = 4096; // Base page size
@@ -34,3 +39,10 @@ pub fn is_irq(type_: CDL_ObjectType) -> bool { type_ == CDL_Interrupt }
 // by architectures that have device objects that are not backed by
 // untyped memory (i.e. that need creation).
 pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
+
+pub unsafe fn seL4_Page_Map_Flush(
+    _page_type: seL4_ObjectType,
+    _sel4_page: seL4_Page,
+    _rights: seL4_CapRights,
+    _vm_attribs: seL4_VMAttributes,
+) -> seL4_Result { Ok(()) }
diff --git a/apps/system/components/kata-os-common/src/model/arch/riscv32.rs b/apps/system/components/kata-os-common/src/model/arch/riscv32.rs
index 81a9091..103abe2 100644
--- a/apps/system/components/kata-os-common/src/model/arch/riscv32.rs
+++ b/apps/system/components/kata-os-common/src/model/arch/riscv32.rs
@@ -8,12 +8,10 @@ assert_cfg!(target_arch = "riscv32");
 mod riscv;
 pub use riscv::*;
 
-use crate::KataOsModel;
-use capdl::kobject_t::*;
+use capdl::*;
 use capdl::CDL_CapType::*;
 use capdl::CDL_ObjectType::*;
-use capdl::*;
-use log::error;
+use crate::KataOsModel;
 
 use sel4_sys::seL4_CapInitThreadCNode;
 use sel4_sys::seL4_CapIRQControl;
@@ -21,13 +19,12 @@ use sel4_sys::seL4_CPtr;
 use sel4_sys::seL4_Error;
 use sel4_sys::seL4_IRQControl_Get;
 use sel4_sys::seL4_LargePageBits;
-use sel4_sys::seL4_MinSchedContextBits;
 use sel4_sys::seL4_ObjectType;
-use sel4_sys::seL4_ObjectType::*;
 use sel4_sys::seL4_PageBits;
-use sel4_sys::seL4_PageTableBits;
 use sel4_sys::seL4_PageTableIndexBits;
 use sel4_sys::seL4_Result;
+use sel4_sys::seL4_RISCV_4K_Page;
+use sel4_sys::seL4_RISCV_Mega_Page;
 use sel4_sys::seL4_UserContext;
 use sel4_sys::seL4_Word;
 use sel4_sys::seL4_WordBits;
@@ -36,6 +33,14 @@ const CDL_PT_NUM_LEVELS: usize = 2;
 // TOOD(sleffler): levels really should be 0 & 1, the names are vestiges of 64-bit support
 const CDL_PT_LEVEL_3_IndexBits: usize = seL4_PageTableIndexBits;
 
+pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
+    match object_size {
+        seL4_PageBits => seL4_RISCV_4K_Page,
+        seL4_LargePageBits => seL4_RISCV_Mega_Page,
+        _ => panic!("Unexpected frame size {}", object_size),
+    }
+}
+
 fn MASK(pow2_bits: usize) -> usize { (1 << pow2_bits) - 1 }
 
 pub fn create_irq_cap(irq: CDL_IRQ, _obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Result {
@@ -79,46 +84,6 @@ pub fn get_user_context(cdl_tcb: &CDL_Object, sp: seL4_Word) -> *const seL4_User
     }
 }
 
-pub fn kobject_get_size(t: kobject_t, object_size: seL4_Word) -> seL4_Word {
-    match t {
-        KOBJECT_FRAME => {
-            if object_size == seL4_PageBits || object_size == seL4_LargePageBits {
-                return object_size;
-            }
-        }
-        KOBJECT_PAGE_TABLE  => {
-            return seL4_PageTableBits;
-        }
-        KOBJECT_SCHED_CONTEXT => {
-            return core::cmp::max(object_size, seL4_MinSchedContextBits);
-        }
-        _ => {}
-    }
-    error!("Unexpected object: type {:?} size {}", t, object_size);
-    object_size
-}
-pub fn kobject_get_type(t: kobject_t, object_size: seL4_Word) -> seL4_ObjectType {
-    match t {
-        KOBJECT_PAGE_DIRECTORY => {
-            return seL4_RISCV_PageTableObject;
-        }
-        KOBJECT_PAGE_TABLE => {
-            return seL4_RISCV_PageTableObject;
-        }
-        KOBJECT_FRAME => {
-            if object_size == seL4_PageBits {
-                return seL4_RISCV_4K_Page;
-            }
-            if object_size == seL4_LargePageBits {
-                return seL4_RISCV_Mega_Page;
-            }
-        }
-        _ => {}
-    }
-    error!("Unexpected object: type {:?} size {}", t, object_size);
-    seL4_LastObjectType // XXX not right
-}
-
 impl<'a> KataOsModel<'a> {
     pub fn create_arch_object(
         &mut self,
diff --git a/apps/system/components/kata-os-common/src/model/arch/x86.rs b/apps/system/components/kata-os-common/src/model/arch/x86.rs
index 2f34d39..39d1dfd 100644
--- a/apps/system/components/kata-os-common/src/model/arch/x86.rs
+++ b/apps/system/components/kata-os-common/src/model/arch/x86.rs
@@ -4,6 +4,7 @@ use static_assertions::assert_cfg;
 assert_cfg!(target_arch = "x86");
 
 use log::{debug, error, info, trace, warn};
+use sel4_sys::seL4_Result;
 
 pub const PAGE_SIZE: usize = 4096;
 pub const STACK_ALIGNMENT_BYTES: usize = 16;
@@ -24,6 +25,21 @@ pub fn is_irq(type_: CDL_ObjectType) -> bool {
 // Identifies objects that need to be instantiated.
 pub fn requires_creation(type_: CDL_ObjectType) -> bool { !is_irq(type_) }
 
+pub unsafe fn seL4_Page_Map_Flush(
+    _page_type: seL4_ObjectType,
+    _sel4_page: seL4_Page,
+    _rights: seL4_CapRights,
+    _vm_attribs: seL4_VMAttributes,
+) -> seL4_Result { Ok(()) }
+
+pub fn get_frame_type(object_size: seL4_Word) -> seL4_ObjectType {
+    match object_size {
+        seL4_PageBits => seL4_X86_4K,
+        seL4_LargePageBits => seL4_X86_LargePageObject,
+        _ => panic!("Unexpected frame size {}", object_size),
+    }
+}
+
 pub fn create_irq_cap(irq: CDL_IRQ, obj: &CDL_Object, free_slot: seL4_CPtr) -> seL4_Error {
     let root = seL4_CapInitThreadCNode;
     let index = free_slot;
diff --git a/apps/system/components/kata-os-common/src/model/build.rs b/apps/system/components/kata-os-common/src/model/build.rs
index 95474c6..94002c9 100644
--- a/apps/system/components/kata-os-common/src/model/build.rs
+++ b/apps/system/components/kata-os-common/src/model/build.rs
@@ -1,5 +1,18 @@
 extern crate sel4_config;
 use std::env;
+use std::fs;
+use std::io::Write;
+
+#[derive(serde::Deserialize)]
+struct PlatformInfo {
+    memory: Vec<MemoryRange>,
+}
+
+#[derive(serde::Deserialize)]
+struct MemoryRange {
+    start: u64,
+    end: u64,
+}
 
 fn main() {
     // If SEL4_OUT_DIR is not set we expect the kernel build at a fixed
@@ -18,4 +31,24 @@ fn main() {
     for feature in features {
         println!("cargo:rustc-cfg=feature=\"{}\"", feature);
     }
+
+    // Some architectures need informations from platform_yaml.
+    let platform_yaml_path = format!("{}/gen_headers/plat/machine/platform_gen.yaml", sel4_out_dir);
+    if let Ok(platform_yaml) = fs::File::open(&platform_yaml_path) {
+        let platform_info: PlatformInfo = serde_yaml::from_reader(platform_yaml).expect("invalid yaml file");
+        let out_dir = env::var("OUT_DIR").unwrap();
+        let out_path = std::path::Path::new(&out_dir).join("platform_gen.rs");
+        let mut out_file = fs::File::create(&out_path).unwrap();
+
+        writeln!(&mut out_file,
+            "struct MemoryRegion {{
+                 start: usize,
+                 end: usize,
+            }}").unwrap();
+        writeln!(&mut out_file, "const MEMORY_REGIONS: [MemoryRegion; {}] = [", platform_info.memory.len()).unwrap();
+        for range in platform_info.memory {
+            writeln!(&mut out_file, "    MemoryRegion {{ start: 0x{:X}, end: 0x{:X} }},", range.start, range.end).ok();
+        }
+        writeln!(&mut out_file, "];").ok();
+    }
 }
diff --git a/apps/system/components/kata-os-common/src/model/feature/dynamic_alloc.rs b/apps/system/components/kata-os-common/src/model/feature/dynamic_alloc.rs
index de36272..d3fea46 100644
--- a/apps/system/components/kata-os-common/src/model/feature/dynamic_alloc.rs
+++ b/apps/system/components/kata-os-common/src/model/feature/dynamic_alloc.rs
@@ -1,11 +1,10 @@
 // Dynamic Object Allocation.
 
-use crate::KataOsModel;
-use capdl::kobject_t::KOBJECT_FRAME;
-use capdl::CDL_FrameFillType_t::*;
-use capdl::CDL_FrameFill_BootInfoEnum_t::*;
-use capdl::CDL_ObjectType::*;
 use capdl::*;
+use capdl::CDL_FrameFill_BootInfoEnum_t::*;
+use capdl::CDL_FrameFillType_t::*;
+use capdl::CDL_ObjectType::*;
+use crate::KataOsModel;
 use log::{debug, info, trace};
 use smallvec::SmallVec;
 
@@ -29,8 +28,7 @@ use sel4_sys::seL4_Untyped_Retype;
 use sel4_sys::seL4_Word;
 use sel4_sys::seL4_WordBits;
 
-use crate::arch::kobject_get_type;
-use crate::arch::requires_creation;
+use crate::arch;
 
 use static_assertions::assert_cfg;
 assert_cfg!(not(feature = "CONFIG_CAPDL_LOADER_STATIC_ALLOC"));
@@ -70,7 +68,7 @@ impl<'a> KataOsModel<'a> {
         let mut free_slot_index = 0;
         for (obj_id, obj) in self.spec.obj_slice().iter()
             .enumerate()
-            .filter(|(_, obj)| requires_creation(obj.r#type()))
+            .filter(|(_, obj)| arch::requires_creation(obj.r#type()))
         {
             let free_slot = self.free_slot_start + free_slot_index;
 
@@ -304,7 +302,7 @@ impl<'a> KataOsModel<'a> {
                 unsafe {
                     seL4_Untyped_Retype(
                         ut_slot,
-                        kobject_get_type(KOBJECT_FRAME, seL4_PageBits).into(),
+                        arch::get_frame_type(seL4_PageBits).into(),
                         seL4_PageBits,
                         seL4_CapInitThreadCNode,
                         0,
diff --git a/apps/system/components/kata-os-common/src/model/feature/spill_tcb_args.rs b/apps/system/components/kata-os-common/src/model/feature/spill_tcb_args.rs
index 6c5b7dd..2b3ecd0 100644
--- a/apps/system/components/kata-os-common/src/model/feature/spill_tcb_args.rs
+++ b/apps/system/components/kata-os-common/src/model/feature/spill_tcb_args.rs
@@ -13,6 +13,9 @@ use capdl::*;
 use core::mem::size_of;
 use core::ptr;
 
+#[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
+use sel4_sys::seL4_ARM_Page_Unify_Instruction;
+
 use sel4_sys::seL4_CapInitThreadVSpace;
 use sel4_sys::seL4_CapRights;
 use sel4_sys::seL4_CPtr;
@@ -109,7 +112,7 @@ impl<'a> KataOsModel<'a> {
             };
         }
 
-        #[cfg(target_arch = "arm")]
+        #[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
         unsafe { seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE) }?;
 
         unsafe { seL4_Page_Unmap(frame) }?;
diff --git a/apps/system/components/kata-os-common/src/model/feature/static_alloc.rs b/apps/system/components/kata-os-common/src/model/feature/static_alloc.rs
index 262e9f1..d2d0c0b 100644
--- a/apps/system/components/kata-os-common/src/model/feature/static_alloc.rs
+++ b/apps/system/components/kata-os-common/src/model/feature/static_alloc.rs
@@ -1,14 +1,14 @@
 // Static Object Allocation.
 // Expect a statically-allocated capDL spec.
 
-use crate::KataOsModel;
-use capdl::CDL_ObjectType::*;
 use capdl::*;
+use capdl::CDL_ObjectType::*;
+use crate::arch;
+use crate::KataOsModel;
 use log::debug;
 use smallvec::SmallVec;
 
-use crate::arch::seL4_ASIDControl_MakePool;
-
+use sel4_sys::seL4_ASIDControl_MakePool;
 use sel4_sys::seL4_CapASIDControl;
 use sel4_sys::seL4_CapInitThreadCNode;
 use sel4_sys::seL4_CPtr;
@@ -94,7 +94,7 @@ impl<'a> KataOsModel<'a> {
                 let untyped_cptr = self.state.get_untyped_cptr(ut_index);
 
                 assert!(
-                    !capdl_obj_type.requires_creation(),
+                    !arch::requires_creation(capdl_obj_type),
                     "Object {} requires dynamic allocation",
                     obj.name()
                 );
diff --git a/apps/system/components/kata-os-common/src/model/mod.rs b/apps/system/components/kata-os-common/src/model/mod.rs
index 73fc491..1dc4a3a 100644
--- a/apps/system/components/kata-os-common/src/model/mod.rs
+++ b/apps/system/components/kata-os-common/src/model/mod.rs
@@ -7,7 +7,6 @@
 #![allow(non_upper_case_globals)]
 #![allow(non_snake_case)]
 
-use capdl::kobject_t::*;
 use capdl::CDL_CapType::*;
 use capdl::CDL_FrameFillType_t::*;
 use capdl::CDL_FrameFill_BootInfoEnum_t::*;
@@ -31,7 +30,7 @@ use static_assertions::*;
 #[cfg_attr(target_arch = "aarch64", path = "arch/aarch64.rs")]
 #[cfg_attr(
     all(target_arch = "arm", target_pointer_width = "32"),
-    path = "arch/arm.rs"
+    path = "arch/aarch32.rs"
 )]
 #[cfg_attr(target_arch = "riscv32", path = "arch/riscv32.rs")]
 #[cfg_attr(target_arch = "x86", path = "arch/x86.rs")]
@@ -40,6 +39,7 @@ mod arch;
 
 use arch::is_irq;
 use arch::PAGE_SIZE; // Base  page size, typically 4KB
+use arch::seL4_Page_Map_Flush; // XXX temp until moved to sel4_sys
 
 // Allocation-specific support
 #[cfg_attr(
@@ -361,14 +361,14 @@ impl<'a> KataOsModel<'a> {
         let arch_type: seL4_ObjectType = match obj.r#type() {
             CDL_Frame => {
                 // Calculate the frame-size-specific cap.
-                arch::kobject_get_type(KOBJECT_FRAME, obj_size)
+                arch::get_frame_type(obj_size)
             }
             CDL_ASIDPool => {
                 obj_size = seL4_ASIDPoolBits;
                 seL4_UntypedObject
             }
             CDL_SchedContext => {
-                obj_size = arch::kobject_get_size(KOBJECT_SCHED_CONTEXT, obj_size);
+                obj_size = core::cmp::max(obj_size, seL4_MinSchedContextBits);
                 CDL_SchedContext.into()
             }
             obj_type => obj_type.into(),
@@ -736,9 +736,13 @@ impl<'a> KataOsModel<'a> {
             page_cap.vm_attribs());
 
         // FIXME: Add support for super-pages.
-        // NB: arch::seL4_Page_Map handles arch-specific work like
-        //     marking the NX bit and invalidating/flushing caches.
-        let mut result = unsafe { seL4_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs) };
+        // NB: seL4_Page_Map handles marking the NX bit, we explicitly
+        //   call seL4_Page_Map_Flush to invalidate and/or flush caches.
+        let mut result = unsafe {
+            seL4_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs).and_then(|_|
+                seL4_Page_Map_Flush(self.get_object(page).r#type().into(), sel4_page, rights, vm_attribs)
+            )
+        };
         #[cfg(feature = "CONFIG_CAPDL_SHARED_FRAMES")]
         if result == Err(seL4_InvalidCapability) {
             // Page is shared (and already mapped); clone a copy of the page
@@ -963,7 +967,8 @@ impl<'a> KataOsModel<'a> {
         let target_cap_rights = target_cap.cap_rights();
 
         // For endpoint this is the badge, for cnodes, this is the (encoded) guard.
-        let target_cap_data = target_cap.cap_data();
+        #[allow(unused_mut)]
+        let mut target_cap_data = target_cap.cap_data();
 
         /* To support moving original caps, we need a spec with a CDT (most don't).
          * This shoud probably become a separate configuration option for when to
@@ -986,13 +991,13 @@ impl<'a> KataOsModel<'a> {
         // Use an original cap to reference the object to copy.
         let src_root = seL4_CapInitThreadCNode;
         let (move_cap, src_index) = match target_cap_type {
-            #[cfg(target_arch = "x86")]
+            #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
             CDL_IOSpaceCap => (false, seL4_CapIOSpace),
 
-            #[cfg(target_arch = "arm")]
+            #[cfg(any(target_arch = "arm", target_arch = "aarch64"))]
             CDL_ARMIOSpaceCap => {
                 target_cap_data = 0;
-                (false, first_arm_iospace + target_cap_data)
+                (false, self.first_arm_iospace + target_cap_data)
             }
 
             CDL_IRQHandlerCap => (false, self.get_irq_cap(target_cap_irq)),
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml b/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml
index e926c21..d92ae49 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml
+++ b/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml
@@ -62,5 +62,6 @@ CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE = []
 path = "lib.rs"
 
 [dependencies]
+cfg-if = "1.0"
 static_assertions = "1.1"
 serde = { version = "1.0", default-features = false, features = ["derive"] }
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch32.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch32.rs
index ca3a8cd..ffc336e 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch32.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch32.rs
@@ -9,10 +9,21 @@
  * @TAG(NICTA_BSD)
  */
 
+use static_assertions::assert_cfg;
+assert_cfg!(all(target_arch = "arm", target_pointer_width = "32"));
+
+use cfg_if::cfg_if;
+
 pub const seL4_WordBits: usize = 32;
 pub const seL4_PageBits: usize = 12;
 pub const seL4_SlotBits: usize = 4;
 
+pub const seL4_ASIDPoolBits: usize = 12;
+pub const seL4_EndpointBits: usize = 4;
+pub const seL4_IOPageTableBits: usize = 12;
+pub const seL4_LargePageBits: usize = 16;
+pub const seL4_PageDirBits: usize = 14;
+
 #[cfg(all(
     feature = "CONFIG_HAVE_FPU",
     any(
@@ -43,15 +54,33 @@ pub const seL4_TCBBits: usize = 10;
 )))]
 pub const seL4_TCBBits: usize = 9;
 
-pub const seL4_EndpointBits: usize = 4;
+cfg_if! {
+    if #[cfg(feature = "CONFIG_KERNEL_MCS")] {
+        pub const seL4_NotificationBits: usize = 5;
+    } else {
+        pub const seL4_NotificationBits: usize = 4;
+    }
+}
 
-#[cfg(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT")]
-pub const seL4_PageTableBits: usize = 12;
-#[cfg(not(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT"))]
-pub const seL4_PageTableBits: usize = 10;
-
-pub const seL4_PageDirBits: usize = 14;
-pub const seL4_ASIDPoolBits: usize = 12;
+cfg_if! {
+    if #[cfg(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT")] {
+        pub const seL4_PageTableBits: usize = 12;
+        pub const seL4_PageTableEntryBits: usize = 3;
+        pub const seL4_PageTableIndexBits: usize = 9;
+        pub const seL4_SectionBits: usize = 21;
+        pub const seL4_SuperSectionBits: usize = 25;
+        pub const seL4_PageDirEntryBits: usize = 3;
+        pub const seL4_PageDirIndexBits: usize = 11;
+    } else {
+        pub const seL4_PageTableBits: usize = 10;
+        pub const seL4_PageTableEntryBits: usize = 2;
+        pub const seL4_PageTableIndexBits: usize = 8;
+        pub const seL4_SectionBits: usize = 20;
+        pub const seL4_SuperSectionBits: usize = 24;
+        pub const seL4_PageDirEntryBits: usize = 2;
+        pub const seL4_PageDirIndexBits: usize = 12;
+    }
+}
 
 pub const seL4_Frame_Args: usize = 4;
 pub const seL4_Frame_MRs: usize = 7;
@@ -101,7 +130,7 @@ pub enum seL4_ARM_VMAttributes {
     ExecuteNever = 4,
 }
 impl From<u32> for seL4_ARM_VMAttributes {
-    fn from(val: u32) -> seL4_RISCV_VMAttributes {
+    fn from(val: u32) -> seL4_ARM_VMAttributes {
         unsafe { ::core::mem::transmute(val & 7) }
     }
 }
@@ -109,7 +138,7 @@ pub const seL4_ARM_Default_VMAttributes: seL4_ARM_VMAttributes =
     seL4_ARM_VMAttributes::Default;
 
 #[repr(C)]
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
 pub enum seL4_ObjectType {
     seL4_UntypedObject = 0,
     seL4_TCBObject,
@@ -137,15 +166,42 @@ pub enum seL4_ObjectType {
 
     seL4_LastObjectType,
 }
+impl seL4_ObjectType {
+    // Returns the log2 size of fixed-size objects; typically for use
+    // with seL4_Retype_Untyped. seL4_UntypedObject has no fixed-size,
+    // callers must specify a size. seL4_CapTableObject has a per-slot
+    // fixed-size that callers must scale by the #slots.
+    // seL4_SchedContextObject size must be in the range
+    // [seL4_MinSchedContextBits..seL4_MaxSchedContextBits].
+    pub fn size_bits(&self) -> Option<usize> {
+        match self {
+            seL4_TCBObject => Some(seL4_TCBBits),
+            seL4_EndpointObject => Some(seL4_EndpointBits),
+            seL4_NotificationObject =>  Some(seL4_NotificationBits),
+            #[cfg(feature = "CONFIG_KERNEL_MCS")]
+            seL4_ReplyObject => Some(seL4_ReplyBits),
+            #[cfg(feature = "CONFIG_KERNEL_MCS")]
+            seL4_SchedContextObject => Some(seL4_MinSchedContextBits), // XXX maybe None?
+            // NB: caller must scale by #slots
+            seL4_CapTableObject => Some(seL4_SlotBits),
+
+            seL4_ARM_SmallPageObject => Some(seL4_PageBits),
+            seL4_ARM_LargePageObject => Some(seL4_LargePageBits),
+            seL4_ARM_SectionObject => Some(seL4_SectionBits),
+            seL4_ARM_SuperSectionObject => Some(seL4_SuperSectionBits),
+            seL4_ARM_PageTableObject => Some(seL4_PageTableBits),
+            seL4_ARM_PageDirectoryObject => Some(seL4_PageDirBits),
+
+            _ => None,
+        }
+    }
+}
 impl From<seL4_ObjectType> for seL4_Word {
     fn from(type_: seL4_ObjectType) -> seL4_Word {
         type_ as seL4_Word
     }
 }
 
-// NB: capDL is defined using this (sigh)
-pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
-
 #[inline(always)]
 pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
     // Use magic external symbol setup by runtime once TLS is primed
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
index 18b827d..dc9bda7 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/aarch64.rs
@@ -9,23 +9,48 @@
  * @TAG(NICTA_BSD)
  */
 
-pub const seL4_WordBits: usize = 32;
+use static_assertions::assert_cfg;
+assert_cfg!(target_arch = "aarch64");
+
+use cfg_if::cfg_if;
+
+pub const seL4_WordBits: usize = 64;
 pub const seL4_PageBits: usize = 12;
 pub const seL4_SlotBits: usize = 5;
 
-pub const seL4_TCBBits: usize = 11;
-#[cfg(feature = "CONFIG_KERNEL_MCS")]
-pub const seL4_NotificationBits: usize = 6;
-#[cfg(feature = "CONFIG_KERNEL_MCS")]
-pub const seL4_ReplyBits: usize = 5;
-
-#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
-pub const seL4_NotificationBits: usize = 5;
-
-pub const seL4_EndpointBits: usize = 4;
-pub const seL4_PageTableBits: usize = 12;
-pub const seL4_PageDirBits: usize = 12;
 pub const seL4_ASIDPoolBits: usize = 12;
+pub const seL4_EndpointBits: usize = 4;
+pub const seL4_IOPageTableBits: usize = 12;
+pub const seL4_HugePageBits: usize = 30;
+pub const seL4_LargePageBits: usize = 21;
+pub const seL4_PageDirBits: usize = 12;
+pub const seL4_PageDirIndexBits: usize = 9;
+pub const seL4_PageTableBits: usize = 12;
+pub const seL4_PageTableIndexBits: usize = 9;
+pub const seL4_ReplyBits: usize = 5;
+pub const seL4_TCBBits: usize = 11;
+
+cfg_if! {
+    if #[cfg(feature = "CONFIG_KERNEL_MCS")] {
+        pub const seL4_NotificationBits: usize = 6;
+    } else {
+        pub const seL4_NotificationBits: usize = 5;
+    }
+}
+
+cfg_if! {
+    if #[cfg(all(feature = "CONFIG_ARM_HYPERVISOR_SUPPORT", feature = "CONFIG_ARM_PA_SIZE_BITS_40"))] {
+        pub const seL4_PUDIndexBits: usize = 10;
+        pub const seL4_PUDBits: usize = 13;
+        pub const seL4_PGDIndexBits: usize = 0;
+        pub const seL4_PGDBits: usize = 0;
+    } else {
+        pub const seL4_PUDIndexBits: usize = 9;
+        pub const seL4_PUDBits: usize = 12;
+        pub const seL4_PGDIndexBits: usize = 9;
+        pub const seL4_PGDBits: usize = 13;
+    }
+}
 
 pub const seL4_Frame_Args: usize = 4;
 pub const seL4_Frame_MRs: usize = 7;
@@ -42,6 +67,9 @@ pub type seL4_ARM_VSpace = seL4_CPtr;
 #[cfg(feature = "arch_generic")]
 include!("arm_generic.rs");
 
+pub use seL4_ARM_PageUpperDirectoryObject as seL4_PageUpperDirectoryObject;
+pub use seL4_ARM_PageGlobalDirectoryObject as seL4_PageGlobalDirectoryObject;
+
 error_types!(u64);
 
 #[repr(C)]
@@ -94,7 +122,7 @@ pub enum seL4_ARM_VMAttributes {
     ExecuteNever = 4,
 }
 impl From<u32> for seL4_ARM_VMAttributes {
-    fn from(val: u32) -> seL4_RISCV_VMAttributes {
+    fn from(val: u32) -> seL4_ARM_VMAttributes {
         unsafe { ::core::mem::transmute(val & 7) }
     }
 }
@@ -102,7 +130,7 @@ pub const seL4_ARM_Default_VMAttributes: seL4_ARM_VMAttributes =
     seL4_ARM_VMAttributes::Default;
 
 #[repr(C)]
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
 pub enum seL4_ObjectType {
     seL4_UntypedObject = 0,
     seL4_TCBObject,
@@ -115,6 +143,10 @@ pub enum seL4_ObjectType {
     #[cfg(feature = "CONFIG_KERNEL_MCS")]
     seL4_ReplyObject,
 
+    seL4_ARM_HugePageObject,
+    seL4_ARM_PageUpperDirectoryObject,
+    seL4_ARM_PageGlobalDirectoryObject,
+
     seL4_ARM_SmallPageObject,
     seL4_ARM_LargePageObject,
     seL4_ARM_PageTableObject,
@@ -125,6 +157,40 @@ pub enum seL4_ObjectType {
 
     #[cfg(feature = "CONFIG_TK1_SMMU")]
     seL4_ARM_IOPageTableObject,
+
+    seL4_LastObjectType,
+}
+impl seL4_ObjectType {
+    // Returns the log2 size of fixed-size objects; typically for use
+    // with seL4_Retype_Untyped. seL4_UntypedObject has no fixed-size,
+    // callers must specify a size. seL4_CapTableObject has a per-slot
+    // fixed-size that callers must scale by the #slots.
+    // seL4_SchedContextObject size must be in the range
+    // [seL4_MinSchedContextBits..seL4_MaxSchedContextBits].
+    pub fn size_bits(&self) -> Option<usize> {
+        match self {
+            seL4_TCBObject => Some(seL4_TCBBits),
+            seL4_EndpointObject => Some(seL4_EndpointBits),
+            seL4_NotificationObject =>  Some(seL4_EndpointBits),
+            #[cfg(feature = "CONFIG_KERNEL_MCS")]
+            seL4_ReplyObject => Some(seL4_ReplyBits),
+            #[cfg(feature = "CONFIG_KERNEL_MCS")]
+            seL4_SchedContextObject => Some(seL4_MinSchedContextBits), // XXX maybe None?
+            // NB: caller must scale by #slots
+            seL4_CapTableObject => Some(seL4_SlotBits),
+
+            seL4_ARM_HugePageObject => Some(seL4_HugePageBits),
+            seL4_ARM_PageUpperDirectoryObject => Some(seL4_PUDBits),
+            seL4_ARM_PageGlobalDirectoryObject => Some(seL4_PGDBits),
+
+            seL4_ARM_SmallPageObject => Some(seL4_PageBits),
+            seL4_ARM_LargePageObject => Some(seL4_LargePageBits),
+            seL4_ARM_PageTableObject => Some(seL4_PageTableBits),
+            seL4_ARM_PageDirectoryObject => Some(seL4_PageDirBits),
+
+            _ => None,
+        }
+    }
 }
 impl From<seL4_ObjectType> for seL4_Word {
     fn from(type_: seL4_ObjectType) -> seL4_Word {
@@ -132,9 +198,6 @@ impl From<seL4_ObjectType> for seL4_Word {
     }
 }
 
-// NB: capDL is defined using this (sigh)
-// pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
-
 #[inline(always)]
 pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
     // Use magic external symbol setup by runtime once TLS is primed
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/arm_generic.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/arm_generic.rs
index 290f42c..8408461 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/arm_generic.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/arm_generic.rs
@@ -17,5 +17,21 @@ pub use seL4_ARM_ASIDControl_MakePool as seL4_ASIDControl_MakePool;
 pub use seL4_ARM_ASIDPool_Assign as seL4_ASIDPool_Assign;
 pub use seL4_ARM_PageTable_Map as seL4_PageTable_Map;
 pub use seL4_ARM_Page_GetAddress as seL4_Page_GetAddress;
-pub use seL4_ARM_Page_Map as seL4_Page_Map;
+// NB: seL4_Page_Map impl found below
 pub use seL4_ARM_Page_Unmap as seL4_Page_Unmap;
+
+pub unsafe fn seL4_Page_Map(
+    sel4_page: seL4_CPtr,
+    sel4_pd: seL4_CPtr,
+    vaddr: seL4_Word,
+    rights: seL4_CapRights,
+    vm_attribs: seL4_VMAttributes,
+) -> seL4_Result {
+    if rights.get_capAllowGrant() != 0 {
+        // NB: executable
+        seL4_ARM_Page_Map(sel4_page, sel4_pd, vaddr, rights, vm_attribs)
+    } else {
+        seL4_ARM_Page_Map(sel4_page, sel4_pd, vaddr, rights,
+                          seL4_ARM_VMAttributes::ExecuteNever)
+    }
+}
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/riscv32.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/riscv32.rs
index d4bd30b..8d377c0 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/riscv32.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/riscv32.rs
@@ -130,7 +130,9 @@ impl seL4_ObjectType {
             seL4_TCBObject => Some(seL4_TCBBits),
             seL4_EndpointObject => Some(seL4_EndpointBits),
             seL4_NotificationObject =>  Some(seL4_EndpointBits),
+            #[cfg(feature = "CONFIG_KERNEL_MCS")]
             seL4_ReplyObject => Some(seL4_ReplyBits),
+            #[cfg(feature = "CONFIG_KERNEL_MCS")]
             seL4_SchedContextObject => Some(seL4_MinSchedContextBits), // XXX maybe None?
             // NB: caller must scale by #slots
             seL4_CapTableObject => Some(seL4_SlotBits),
@@ -152,9 +154,6 @@ impl From<seL4_ObjectType> for seL4_Word {
     }
 }
 
-// NB: capDL is defined using this (sigh)
-pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
-
 #[inline(always)]
 pub unsafe fn seL4_GetIPCBuffer() -> *mut seL4_IPCBuffer {
     // Use magic external symbol setup by runtime once TLS is primed
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/x86.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/x86.rs
index 5e4f7e3..087199a 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/x86.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/x86.rs
@@ -51,7 +51,7 @@ include!("x86_generic.rs");
 error_types!(u32);
 
 #[repr(C)]
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
 pub enum seL4_ObjectType {
     seL4_UntypedObject = 0,
     seL4_TCBObject,
@@ -91,9 +91,6 @@ impl From<seL4_ObjectType> for seL4_Word {
     }
 }
 
-// NB: capDL is defined using this (sigh)
-pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
-
 #[repr(u32)]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum seL4_X86_VMAttributes {
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs b/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
index e6bdd1a..0aba694 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/arch/x86_64.rs
@@ -53,7 +53,7 @@ include!("x86_generic.rs");
 error_types!(u64);
 
 #[repr(C)]
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
 pub enum seL4_ObjectType {
     seL4_UntypedObject = 0,
     seL4_TCBObject,
@@ -98,9 +98,6 @@ impl From<seL4_ObjectType> for seL4_Word {
     }
 }
 
-// NB: capDL is defined using this (sigh)
-pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
-
 #[repr(u32)]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum seL4_X86_VMAttributes {
diff --git a/apps/system/components/kata-os-common/src/sel4-sys/lib.rs b/apps/system/components/kata-os-common/src/sel4-sys/lib.rs
index 99ec2b4..b6ff9a0 100644
--- a/apps/system/components/kata-os-common/src/sel4-sys/lib.rs
+++ b/apps/system/components/kata-os-common/src/sel4-sys/lib.rs
@@ -161,6 +161,9 @@ pub type seL4_Untyped = seL4_CPtr;
 // TODO(sleffler): seL4 uses seL4_Uint64 but it's not defined for us
 pub type seL4_Time = u64;
 
+// NB: capDL CDL_ObjectType is defined using this (sigh)
+pub const seL4_ObjectTypeCount: isize = seL4_ObjectType::seL4_LastObjectType as isize;
+
 pub const seL4_MsgLengthBits: usize = 7;
 pub const seL4_MsgMaxLength: usize = 120;
 pub const seL4_MsgExtraCapBits: usize = 2;