diff --git a/apps/system/components/ProcessManager/kata-proc-manager/src/sel4bundle/mod.rs b/apps/system/components/ProcessManager/kata-proc-manager/src/sel4bundle/mod.rs
index 8ae2e48..e3f3085 100644
--- a/apps/system/components/ProcessManager/kata-proc-manager/src/sel4bundle/mod.rs
+++ b/apps/system/components/ProcessManager/kata-proc-manager/src/sel4bundle/mod.rs
@@ -18,6 +18,7 @@ use kata_memory_interface::ObjDesc;
 use kata_memory_interface::ObjDescBundle;
 use kata_os_common::copyregion::CopyRegion;
 use kata_os_common::cspace_slot::CSpaceSlot;
+use kata_os_common::scheduling::Domain;
 use kata_os_common::sel4_sys;
 use kata_proc_interface::Bundle;
 use kata_proc_interface::BundleImage;
@@ -174,7 +175,7 @@ pub struct seL4BundleImpl {
     cap_tcb: CSpaceSlot,
 
     affinity: seL4_Word, // CPU affinity
-    domain: seL4_Word,   // Scheduling domain
+    domain: Domain,      // Scheduling domain
 
     tcb_name: String,
     tcb_max_priority: seL4_Word,
@@ -292,7 +293,7 @@ impl seL4BundleImpl {
             first_page: first_vaddr / PAGE_SIZE,
 
             affinity: 0, // CPU 0
-            domain: 0,   // XXX share scheduling domain with system services for now
+            domain: Domain::AppSandbox,
 
             tcb_name: bundle.app_id.clone(),
             tcb_max_priority: 254, // TODO(sleffler): guess
diff --git a/apps/system/components/kata-os-common/Cargo.toml b/apps/system/components/kata-os-common/Cargo.toml
index b30b381..b4d6ca6 100644
--- a/apps/system/components/kata-os-common/Cargo.toml
+++ b/apps/system/components/kata-os-common/Cargo.toml
@@ -16,5 +16,6 @@ cspace-slot = { path = "src/cspace-slot" }
 logger = { path = "src/logger" }
 model = { path = "src/model" }
 panic = { path = "src/panic" }
+scheduling = { path = "src/scheduling" }
 sel4-sys = { path = "src/sel4-sys" }
 slot-allocator = { path = "src/slot-allocator" }
diff --git a/apps/system/components/kata-os-common/src/lib.rs b/apps/system/components/kata-os-common/src/lib.rs
index be1f716..0379efe 100644
--- a/apps/system/components/kata-os-common/src/lib.rs
+++ b/apps/system/components/kata-os-common/src/lib.rs
@@ -11,5 +11,6 @@ pub extern crate cspace_slot;
 pub extern crate logger;
 pub extern crate model;
 pub extern crate panic;
+pub extern crate scheduling;
 pub extern crate sel4_sys;
 pub extern crate slot_allocator;
diff --git a/apps/system/components/kata-os-common/src/scheduling/Cargo.toml b/apps/system/components/kata-os-common/src/scheduling/Cargo.toml
new file mode 100644
index 0000000..750b90b
--- /dev/null
+++ b/apps/system/components/kata-os-common/src/scheduling/Cargo.toml
@@ -0,0 +1,3 @@
+[package]
+name = "scheduling"
+version = "0.1.0"
diff --git a/apps/system/components/kata-os-common/src/scheduling/src/lib.rs b/apps/system/components/kata-os-common/src/scheduling/src/lib.rs
new file mode 100644
index 0000000..ece2599
--- /dev/null
+++ b/apps/system/components/kata-os-common/src/scheduling/src/lib.rs
@@ -0,0 +1,14 @@
+//! Kata OS seL4 scheduling primitives
+
+#![no_std]
+
+/// Scheduling domains configured for seL4 TCBs.
+///
+/// Currently we have this setup as a pair of domains, one for the system
+/// components and another for the third party application sandbox.
+///
+#[derive(Debug, Eq, PartialEq, Copy, Clone)]
+pub enum Domain {
+    System = 0,
+    AppSandbox,
+}
diff --git a/easy-settings.cmake b/easy-settings.cmake
index 6191fad..0e160d8 100644
--- a/easy-settings.cmake
+++ b/easy-settings.cmake
@@ -13,3 +13,6 @@ set(LibUtilsDefaultZfLogLevel 5 CACHE STRING "seL4 internal logging level (0-5).
 set(SIMULATION ON CACHE BOOL "Whether to build simulate script")
 set(RELEASE OFF CACHE BOOL "Performance optimized build")
 set(UseRiscVBBL OFF CACHE BOOL "Whether to use bbl")
+
+set(KernelNumDomains 2 CACHE STRING "How many scheduling domains to build for")
+set(KernelDomainSchedule "${CMAKE_CURRENT_LIST_DIR}/kernel/round_robin_domain.c" CACHE INTERNAL "Domain scheduler algorithm")
diff --git a/kernel/round_robin_domain.c b/kernel/round_robin_domain.c
new file mode 100644
index 0000000..a0d10a2
--- /dev/null
+++ b/kernel/round_robin_domain.c
@@ -0,0 +1,22 @@
+#include <model/statedata.h>
+#include <object/structures.h>
+
+/* Dual-domain schedule for Kata to isolate third party applications from system
+ * applications.
+ *
+ * Note that this doesn't actually implement the schedule -- that's hardwired in
+ * seL4's kernel source. See also kata/kernel/src/kernel/thread.c, in the
+ * nextDomain function around line 302 and the timerTick function around 630.
+ *
+ * Effectively this is a round-robin scheduler, so half of the CPU time is given
+ * to system applications, while third party applications are allocated the
+ * other half. Note that even if there's nothing to run in the third-party
+ * application domain, the scheduler will schedule an idle thread to ensure that
+ * domain gets it's allocated share of time.
+ */
+const dschedule_t ksDomSchedule[] = {
+    {.domain = 0, .length = 1},  // System domain
+    {.domain = 1, .length = 1},  // Third party application domain
+};
+
+const word_t ksDomScheduleLength = sizeof(ksDomSchedule) / sizeof(dschedule_t);