diff --git a/apps/rust/hello/Cargo.toml b/apps/rust/hello/Cargo.toml
new file mode 100644
index 0000000..cfaa5ee
--- /dev/null
+++ b/apps/rust/hello/Cargo.toml
@@ -0,0 +1,38 @@
+# Copyright 2022 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+# https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+[package]
+name = "hello"
+version = "0.1.0"
+edition = "2021"
+build = "build.rs"
+
+[build-dependencies]
+# build.rs depends on SEL4_OUT_DIR = "${ROOTDIR}/out/kata/kernel"
+sel4-config = { path = "../../system/components/kata-os-common/src/sel4-config" }
+
+[features]
+default = []
+# Used by sel4-config to extract kernel config
+CONFIG_PRINTING = []
+
+[lib]
+name = "hello"
+path = "hello.rs"
+crate-type = ["staticlib"]
+
+[dependencies]
+cstr_core = { version = "0.2.3", default-features = false }
+kata-os-common = { path = "../../system/components/kata-os-common", default-features = false }
+log = "0.4"
diff --git a/apps/rust/hello/Makefile b/apps/rust/hello/Makefile
new file mode 100644
index 0000000..8ce6e77
--- /dev/null
+++ b/apps/rust/hello/Makefile
@@ -0,0 +1,24 @@
+OUT_KATA ?= $(OUT)/kata/riscv32-unknown-elf/release
+OUT_HELLO ?= $(OUT_KATA)/apps/hello
+CARGO_OPTS ?= --release
+
+# hello app staticlib (location set w/ --out-dir below)
+LIB_HELLO := ${OUT_HELLO}/libhello.a
+# To satisfy Rust core deps with debug build
+LIB_LIBC := ${OUT_KATA}/musllibc/build-temp/stage/lib/libc.a
+
+LD_FLAGS := -march=rv32imac -mabi=ilp32 -static -nostdlib -ftls-model=local-exec
+#DBG:=-g
+
+# NB: let cargo handle incremental build steps
+${OUT_HELLO}/hello.elf: hello.rs | tmp_check
+ SEL4_OUT_DIR=${OUT_KATA}/kernel kcargo build ${CARGO_OPTS} --target-dir ${OUT_HELLO} --out-dir ${OUT_HELLO}
+ riscv32-unknown-elf-gcc ${LD_FLAGS} $(DBG) ${LIB_HELLO} ${LIB_LIBC} -o ${OUT_HELLO}/hello.elf
+
+tmp_check:
+ mkdir -p $(OUT_HELLO)
+
+clean:
+ rm -rf ${OUT_HELLO}
+
+PHONY: tmp_check
diff --git a/apps/rust/hello/build.rs b/apps/rust/hello/build.rs
new file mode 100644
index 0000000..69753b1
--- /dev/null
+++ b/apps/rust/hello/build.rs
@@ -0,0 +1,34 @@
+// Copyright 2022 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+extern crate sel4_config;
+use std::env;
+
+fn main() {
+ // If SEL4_OUT_DIR is not set we expect the kernel build at a fixed
+ // location relative to the ROOTDIR env variable.
+ println!("SEL4_OUT_DIR {:?}", env::var("SEL4_OUT_DIR"));
+ let sel4_out_dir = env::var("SEL4_OUT_DIR")
+ .unwrap_or_else(|_| format!("{}/out/kata/kernel", env::var("ROOTDIR").unwrap()));
+ println!("sel4_out_dir {}", sel4_out_dir);
+
+ // Dredge seL4 kernel config for settings we need as features to generate
+ // correct code: e.g. CONFIG_KERNEL_MCS enables MCS support which changes
+ // the system call numbering.
+ let features = sel4_config::get_sel4_features(&sel4_out_dir);
+ println!("features={:?}", features);
+ for feature in features {
+ println!("cargo:rustc-cfg=feature=\"{}\"", feature);
+ }
+}
diff --git a/apps/rust/hello/hello.rs b/apps/rust/hello/hello.rs
new file mode 100644
index 0000000..f168a26
--- /dev/null
+++ b/apps/rust/hello/hello.rs
@@ -0,0 +1,87 @@
+/*
+ * Copyright 2021, Google LLC
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+#![no_std]
+#![no_main]
+#![feature(asm)]
+#![feature(thread_local)]
+
+// TODO(sleffler): plumb logger to SDKRuntime to eliminate seL4_DebugPutChar
+// (or provide a logger alternative)
+
+use kata_os_common::logger::KataLogger;
+use kata_os_common::sel4_sys;
+
+use sel4_sys::seL4_IPCBuffer;
+
+const PAGE_SIZE: usize = 4096;
+
+#[no_mangle]
+#[thread_local]
+static mut __sel4_ipc_buffer: *mut seL4_IPCBuffer = 0 as _;
+
+#[repr(align(4096))]
+#[allow(dead_code)]
+struct PageAlign {
+ data: [u8; PAGE_SIZE],
+}
+static mut STATIC_TLS: PageAlign = PageAlign {
+ data: [0u8; PAGE_SIZE],
+};
+
+#[no_mangle]
+pub fn _start() {
+ unsafe {
+ asm!("
+ .option push
+ .option norelax
+ la gp, __global_pointer$
+ la tp, {tls}
+ lui t1,0
+ add t1,t1,tp
+ sw a0,0(t1) # __sel4_ipc_buffer>
+ addi sp,sp,-16
+ sw a0, 12(sp)
+ sw a1, 8(sp)
+ sw a2, 4(sp)
+ sw a3, 0(sp)
+ .option pop
+ j main",
+ tls = sym STATIC_TLS,
+ options(noreturn),
+ )
+ };
+}
+
+// Message output is sent through the kata-os-logger which calls logger_log
+// to deliver data to the console. We use seL4_DebugPutChar to write to the
+// console which only works if DEBUG_PRINTING is enabled in the kernel.
+#[no_mangle]
+#[allow(unused_variables)]
+pub fn logger_log(_level: u8, msg: *const cstr_core::c_char) {
+ #[cfg(feature = "CONFIG_PRINTING")]
+ unsafe {
+ for c in cstr_core::CStr::from_ptr(msg).to_bytes() {
+ let _ = sel4_sys::seL4_DebugPutChar(*c);
+ }
+ let _ = sel4_sys::seL4_DebugPutChar(b'\n');
+ }
+}
+
+#[no_mangle]
+// XXX need SDK specification of main, use hack for now
+pub fn main(a0: u32, a1: u32, a2: u32, a3: u32) {
+ // Setup logger; (XXX belongs in the SDKRuntime)
+ static KATA_LOGGER: KataLogger = KataLogger;
+ log::set_logger(&KATA_LOGGER).unwrap();
+ log::set_max_level(log::LevelFilter::Trace);
+
+ // XXX maybe setup a heap (XXX belongs in the SDKRuntime)
+
+ log::info!("I am a Rust app, hear me roar!");
+ log::info!("a0 {:x} a1 {:x} a2 {:x} a3 {:x}", a0, a1, a2, a3);
+ log::info!("__sel4_ipc_buffer {:p}", unsafe { __sel4_ipc_buffer });
+ log::info!("Done, wimper ...");
+}
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 c3370c5..6d2361e 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
@@ -246,6 +246,8 @@ impl seL4BundleImpl {
//
// NB: beware the order of this must match *_SLOT above
// TODO(sleffler): maybe construct the vec to avoid mismatches
+ // TODO(sleffler): the toplevel CNode has a fixed size which
+ // can overflow when nframes is non-trivial
let dynamic_objs = kata_object_alloc_in_toplevel(vec![
// control/main-thread TCB
ObjDesc::new(seL4_TCBObject, 1, TCB_SLOT),