diff --git a/apps/system/CMakeLists.txt b/apps/system/CMakeLists.txt
index 01aa616..f4cc8b9 100644
--- a/apps/system/CMakeLists.txt
+++ b/apps/system/CMakeLists.txt
@@ -14,6 +14,8 @@ cmake_minimum_required(VERSION 3.7.2)
 
 project(system)
 
+CAmkESAddImportPath(interfaces)
+
 include(${CMAKE_CURRENT_LIST_DIR}/rust.cmake)
 
 RustAddLibrary(
@@ -31,4 +33,8 @@ DeclareCAmkESComponent(UartDriver
   SOURCES components/UartDriver/src/driver.c
 )
 
+DeclareCAmkESComponent(SeL4Debug
+  SOURCES components/SeL4Debug/src/wrappers.c
+)
+
 DeclareCAmkESRootserver(system.camkes)
diff --git a/apps/system/components/DebugConsole/DebugConsole.camkes b/apps/system/components/DebugConsole/DebugConsole.camkes
index 81aa874..594efb2 100644
--- a/apps/system/components/DebugConsole/DebugConsole.camkes
+++ b/apps/system/components/DebugConsole/DebugConsole.camkes
@@ -1,6 +1,10 @@
+import <SeL4DebugInterface.camkes>;
+
 component DebugConsole {
   control;
   uses uart_inf uart;
   dataport Buf tx_dataport;
   dataport Buf rx_dataport;
+
+  uses SeL4DebugInterface sel4debug;
 }
diff --git a/apps/system/components/DebugConsole/kata-shell/src/lib.rs b/apps/system/components/DebugConsole/kata-shell/src/lib.rs
index 08f3c70..767fab9 100644
--- a/apps/system/components/DebugConsole/kata-shell/src/lib.rs
+++ b/apps/system/components/DebugConsole/kata-shell/src/lib.rs
@@ -74,6 +74,7 @@ fn dispatch_command(cmdline: &str, output: &mut dyn io::Write) {
                 "echo" => echo_command(cmdline, output),
                 "add" => add_command(&mut args, output),
                 "clear" => clear_command(output),
+                "ps" => ps_command(),
                 _ => Err(CommandError::UnknownCommand),
             };
             if let Err(e) = result {
@@ -100,6 +101,13 @@ fn echo_command(cmdline: &str, output: &mut dyn io::Write) -> Result<(), Command
     }
 }
 
+/// Implements a "ps" command that dumps seL4 scheduler state to the console.
+fn ps_command() -> Result<(), CommandError> {
+    extern "C" { fn sel4debug_dump_scheduler(); }
+    unsafe { sel4debug_dump_scheduler(); }
+    Ok(())
+}
+
 /// Implements a binary float addition command.
 ///
 /// This is a toy to demonstrate that the CLI can operate on some very basic
diff --git a/apps/system/components/SeL4Debug/SeL4Debug.camkes b/apps/system/components/SeL4Debug/SeL4Debug.camkes
new file mode 100644
index 0000000..0e87e70
--- /dev/null
+++ b/apps/system/components/SeL4Debug/SeL4Debug.camkes
@@ -0,0 +1,5 @@
+import <SeL4DebugInterface.camkes>;
+
+component SeL4Debug {
+  provides SeL4DebugInterface sel4debug;
+}
diff --git a/apps/system/components/SeL4Debug/src/wrappers.c b/apps/system/components/SeL4Debug/src/wrappers.c
new file mode 100644
index 0000000..1a9d02c
--- /dev/null
+++ b/apps/system/components/SeL4Debug/src/wrappers.c
@@ -0,0 +1,14 @@
+#include <camkes.h>
+#include <sel4/syscalls.h>
+
+void sel4debug_put_string(const char* msg) {
+#ifdef CONFIG_PRINTING
+  seL4_DebugPutString((char*) msg);
+#endif
+}
+
+void sel4debug_dump_scheduler() {
+#ifdef CONFIG_PRINTING
+  seL4_DebugDumpScheduler();
+#endif
+}
diff --git a/apps/system/interfaces/SeL4DebugInterface.camkes b/apps/system/interfaces/SeL4DebugInterface.camkes
new file mode 100644
index 0000000..ffac913
--- /dev/null
+++ b/apps/system/interfaces/SeL4DebugInterface.camkes
@@ -0,0 +1,4 @@
+procedure SeL4DebugInterface {
+  void put_string(in string msg);
+  void dump_scheduler();
+}
diff --git a/apps/system/system.camkes b/apps/system/system.camkes
index 59cb788..4758574 100644
--- a/apps/system/system.camkes
+++ b/apps/system/system.camkes
@@ -15,6 +15,7 @@ import <std_connector.camkes>;
 import "interfaces/uart.idl4";
 import "components/UartDriver/UartDriver.camkes";
 import "components/DebugConsole/DebugConsole.camkes";
+import "components/SeL4Debug/SeL4Debug.camkes";
 
 component UART {
     hardware;
@@ -28,6 +29,7 @@ assembly {
         component UART uart;
         component UartDriver drv;
         component DebugConsole debug_console;
+        component SeL4Debug sel4debug;
 
         connection seL4HardwareMMIO uart_mem(from drv.mem, to uart.mem);
         // TODO(mattharvey): Make receives wait on interrupt.
@@ -35,6 +37,10 @@ assembly {
         //     from uart.interrupt, to drv.interrupt);
         connection seL4RPCCall uart_inf(from debug_console.uart, to drv.uart);
 
+        // Connect the SeL4Debug interface of each component that needs access.
+        connection seL4RPCCall SeL4DebugInterface(from debug_console.sel4debug,
+                                                  to sel4debug.sel4debug);
+
         connection seL4SharedData tx_channel(
             from debug_console.tx_dataport, to drv.tx_dataport);
         connection seL4SharedData rx_channel(