diff --git a/repos/base-fiasco/include/base/native_types.h b/repos/base-fiasco/include/base/native_types.h
index 76dab1764..c731d0293 100644
--- a/repos/base-fiasco/include/base/native_types.h
+++ b/repos/base-fiasco/include/base/native_types.h
@@ -63,14 +63,6 @@ namespace Genode {
 		return tid.raw;
 	}
 
-	/**
-	 * Empty UTCB type expected by the thread library
-	 *
-	 * On this kernel, UTCBs are not placed within the the stack area. Each
-	 * thread can request its own UTCB pointer using the kernel interface.
-	 */
-	typedef struct { } Native_utcb;
-
 	typedef Native_capability_tpl<Cap_dst_policy> Native_capability;
 	typedef Fiasco::l4_threadid_t Native_connection_state;
 }
diff --git a/repos/base-fiasco/src/include/base/internal/native_utcb.h b/repos/base-fiasco/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..7fa25fe56
--- /dev/null
+++ b/repos/base-fiasco/src/include/base/internal/native_utcb.h
@@ -0,0 +1,23 @@
+/*
+ * \brief  UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ *
+ * On this kernel, UTCBs are not placed within the the stack area. Each
+ * thread can request its own UTCB pointer using the kernel interface.
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+namespace Genode { struct Native_utcb { }; }
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
+
diff --git a/repos/base-foc/include/base/native_types.h b/repos/base-foc/include/base/native_types.h
index eab76d37d..d4d493c08 100644
--- a/repos/base-foc/include/base/native_types.h
+++ b/repos/base-foc/include/base/native_types.h
@@ -95,17 +95,6 @@ namespace Genode {
 	typedef Fiasco::l4_cap_idx_t Native_task;
 
 
-	struct Native_utcb
-	{
-		/*
-		 * The 'Native_utcb' is located within the stack slot of the thread.
-		 * We merely use it for remembering a pointer to the real UTCB, which
-		 * resides somewhere in the kernel's address space.
-		 */
-		Fiasco::l4_utcb_t *foc_utcb = nullptr;
-	};
-
-
 	/**
 	 * Native_capability in Fiasco.OC is just a reference to a Cap_index.
 	 *
diff --git a/repos/base-foc/src/include/base/internal/native_utcb.h b/repos/base-foc/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..93fe8e37f
--- /dev/null
+++ b/repos/base-foc/src/include/base/internal/native_utcb.h
@@ -0,0 +1,33 @@
+/*
+ * \brief  UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ *
+ * The 'Native_utcb' is located within the stack slot of the thread. We merely
+ * use it for remembering a pointer to the real UTCB, which resides somewhere
+ * in the kernel's address space.
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+namespace Fiasco {
+#include <l4/sys/utcb.h>
+}
+
+namespace Genode { struct Native_utcb; }
+
+struct Genode::Native_utcb
+{
+	Fiasco::l4_utcb_t *foc_utcb = nullptr;
+};
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
+
diff --git a/repos/base-hw/include/base/native_types.h b/repos/base-hw/include/base/native_types.h
index b69758a27..932f40bb9 100644
--- a/repos/base-hw/include/base/native_types.h
+++ b/repos/base-hw/include/base/native_types.h
@@ -39,21 +39,6 @@ namespace Genode
 	 * Coherent address region
 	 */
 	struct Native_region;
-
-	/**
-	 * Get the the minimal supported page-size log 2
-	 */
-	constexpr size_t get_page_size_log2() { return 12; }
-
-	/**
-	 * Get the the minimal supported page-size
-	 */
-	constexpr size_t get_page_size() { return 1 << get_page_size_log2(); }
-
-	/**
-	 * Memory region that is exclusive to every thread and known by the kernel
-	 */
-	class Native_utcb;
 }
 
 
@@ -74,95 +59,6 @@ struct Genode::Native_region
 };
 
 
-class Genode::Native_utcb
-{
-	public:
-
-		enum { MAX_CAP_ARGS = Msgbuf_base::MAX_CAP_ARGS};
-
-		enum Offsets { THREAD_MYSELF, PARENT, UTCB_DATASPACE };
-
-	private:
-
-		Kernel::capid_t _caps[MAX_CAP_ARGS]; /* capability buffer  */
-		size_t          _cap_cnt;            /* capability counter */
-		size_t          _size;               /* bytes to transfer  */
-		uint8_t         _buf[get_page_size() - sizeof(_caps) -
-		                     sizeof(_cap_cnt) - sizeof(_size)];
-
-	public:
-
-		Native_utcb& operator= (const Native_utcb &o)
-		{
-			_cap_cnt = 0;
-			_size    = o._size;
-			memcpy(_buf, o._buf, _size);
-			return *this;
-		}
-
-		/**
-		 * Set the destination capability id (server object identity)
-		 */
-		void destination(Kernel::capid_t id) {
-			*reinterpret_cast<long*>(_buf) = id; }
-
-		/**
-		 * Return the count of capabilities in the UTCB
-		 */
-		size_t cap_cnt() { return _cap_cnt; }
-
-		/**
-		 * Set the count of capabilities in the UTCB
-		 */
-		void cap_cnt(size_t cnt) { _cap_cnt = cnt;  }
-
-		/**
-		 * Return the start address of the payload data
-		 */
-		void const * base() const { return &_buf; }
-
-		/**
-		 * Copy data from the message buffer 'o' to this UTCB
-		 */
-		void copy_from(Msgbuf_base &o, size_t size)
-		{
-			_size = size;
-
-			_cap_cnt = o._snd_cap_cnt;
-			for (unsigned i = 0; i < _cap_cnt; i++)
-				_caps[i] = o._caps[i].dst();
-
-			memcpy(_buf, o.buf, min(_size, o._size));
-		}
-
-		/**
-		 * Copy data from this UTCB to the message buffer 'o'
-		 */
-		void copy_to(Msgbuf_base &o)
-		{
-			o._snd_cap_cnt = _cap_cnt;
-			for (unsigned i = 0; i < _cap_cnt; i++) {
-				o._caps[i] = _caps[i];
-				if (o._caps[i].valid()) Kernel::ack_cap(o._caps[i].dst());
-			}
-
-			memcpy(o.buf, _buf, min(_size, o._size));
-		}
-
-		/**
-		 * Return the capability id at index 'i'
-		 */
-		Kernel::capid_t cap_get(unsigned i) {
-			return (i < _cap_cnt) ? _caps[i] : Kernel::cap_id_invalid(); }
-
-		/**
-		 * Set the capability id 'cap_id' at the next index
-		 */
-		void cap_add(Kernel::capid_t cap_id) {
-			if (_cap_cnt < MAX_CAP_ARGS) _caps[_cap_cnt++] = cap_id; }
-};
-
-
 namespace Genode
 {
 	static constexpr addr_t VIRT_ADDR_SPACE_START = 0x1000;
diff --git a/repos/base-hw/src/base/ipc/ipc.cc b/repos/base-hw/src/base/ipc/ipc.cc
index ee98c5d0d..dd706fb1f 100644
--- a/repos/base-hw/src/base/ipc/ipc.cc
+++ b/repos/base-hw/src/base/ipc/ipc.cc
@@ -20,6 +20,9 @@
 #include <util/construct_at.h>
 #include <util/retry.h>
 
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
+
 /* base-hw includes */
 #include <kernel/interface.h>
 #include <kernel/log.h>
diff --git a/repos/base-hw/src/base/signal/signal.cc b/repos/base-hw/src/base/signal/signal.cc
index 1b66f54e6..6b300c4d2 100644
--- a/repos/base-hw/src/base/signal/signal.cc
+++ b/repos/base-hw/src/base/signal/signal.cc
@@ -18,6 +18,9 @@
 #include <base/env.h>
 #include <base/trace/events.h>
 
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
+
 /* base-hw includes */
 #include <kernel/interface.h>
 
diff --git a/repos/base-hw/src/base/thread/bootstrap.cc b/repos/base-hw/src/base/thread/bootstrap.cc
index cf7c61fc3..1b8645e7d 100644
--- a/repos/base-hw/src/base/thread/bootstrap.cc
+++ b/repos/base-hw/src/base/thread/bootstrap.cc
@@ -19,6 +19,7 @@
 
 /* base-internal includes */
 #include <base/internal/stack.h>
+#include <base/internal/native_utcb.h>
 
 /* base-hw includes */
 #include <kernel/interface.h>
diff --git a/repos/base-hw/src/base/thread/start.cc b/repos/base-hw/src/base/thread/start.cc
index ad074e7f6..5ae364ba4 100644
--- a/repos/base-hw/src/base/thread/start.cc
+++ b/repos/base-hw/src/base/thread/start.cc
@@ -20,6 +20,7 @@
 
 /* base-internal includes */
 #include <base/internal/stack_allocator.h>
+#include <base/internal/native_utcb.h>
 
 using namespace Genode;
 
diff --git a/repos/base-hw/src/core/include/kernel/core_interface.h b/repos/base-hw/src/core/include/kernel/core_interface.h
index 93bd7dbe0..dd36994b4 100644
--- a/repos/base-hw/src/core/include/kernel/core_interface.h
+++ b/repos/base-hw/src/core/include/kernel/core_interface.h
@@ -14,6 +14,9 @@
 #ifndef _CORE__INCLUDE__KERNEL__CORE_INTERFACE_H_
 #define _CORE__INCLUDE__KERNEL__CORE_INTERFACE_H_
 
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
+
 /* base-hw includes */
 #include <kernel/interface.h>
 
diff --git a/repos/base-hw/src/core/include/kernel/ipc_node.h b/repos/base-hw/src/core/include/kernel/ipc_node.h
index 408161b83..ab28f9baa 100644
--- a/repos/base-hw/src/core/include/kernel/ipc_node.h
+++ b/repos/base-hw/src/core/include/kernel/ipc_node.h
@@ -18,6 +18,9 @@
 /* Genode includes */
 #include <util/construct_at.h>
 
+/* base-local includes */
+#include <base/internal/native_utcb.h>
+
 /* core includes */
 #include <kernel/fifo.h>
 #include <kernel/interface.h>
diff --git a/repos/base-hw/src/core/include/platform_thread.h b/repos/base-hw/src/core/include/platform_thread.h
index f2f140a2d..657e60a1a 100644
--- a/repos/base-hw/src/core/include/platform_thread.h
+++ b/repos/base-hw/src/core/include/platform_thread.h
@@ -20,6 +20,9 @@
 #include <base/native_types.h>
 #include <base/thread.h>
 
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
+
 /* core includes */
 #include <address_space.h>
 #include <object.h>
diff --git a/repos/base-hw/src/core/include/util.h b/repos/base-hw/src/core/include/util.h
index 3f510860e..be86c7b9a 100644
--- a/repos/base-hw/src/core/include/util.h
+++ b/repos/base-hw/src/core/include/util.h
@@ -18,6 +18,9 @@
 #include <rm_session/rm_session.h>
 #include <base/printf.h>
 
+/* base-internal includes */
+#include <base/internal/page_size.h>
+
 namespace Genode
 {
 	enum {
diff --git a/repos/base-hw/src/core/kernel/ipc_node.cc b/repos/base-hw/src/core/kernel/ipc_node.cc
index 493bcc70a..3e9af268f 100644
--- a/repos/base-hw/src/core/kernel/ipc_node.cc
+++ b/repos/base-hw/src/core/kernel/ipc_node.cc
@@ -16,6 +16,9 @@
 #include <util/string.h>
 #include <base/native_types.h>
 
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
+
 /* core includes */
 #include <assert.h>
 #include <platform_pd.h>
diff --git a/repos/base-hw/src/core/kernel/thread.cc b/repos/base-hw/src/core/kernel/thread.cc
index abc7b0614..7012e0a18 100644
--- a/repos/base-hw/src/core/kernel/thread.cc
+++ b/repos/base-hw/src/core/kernel/thread.cc
@@ -19,6 +19,7 @@
 
 /* base-internal includes */
 #include <base/internal/unmanaged_singleton.h>
+#include <base/internal/native_utcb.h>
 
 /* core includes */
 #include <assert.h>
diff --git a/repos/base-hw/src/core/platform_thread.cc b/repos/base-hw/src/core/platform_thread.cc
index 0e9c84e0d..2935d01d1 100644
--- a/repos/base-hw/src/core/platform_thread.cc
+++ b/repos/base-hw/src/core/platform_thread.cc
@@ -20,9 +20,11 @@
 #include <rm_session_component.h>
 #include <map_local.h>
 
-#include <kernel/pd.h>
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
 
 /* kernel includes */
+#include <kernel/pd.h>
 #include <kernel/kernel.h>
 
 using namespace Genode;
diff --git a/repos/base-hw/src/core/thread_start.cc b/repos/base-hw/src/core/thread_start.cc
index 307e1e726..c2a0c2586 100644
--- a/repos/base-hw/src/core/thread_start.cc
+++ b/repos/base-hw/src/core/thread_start.cc
@@ -19,6 +19,7 @@
 
 /* base-internal stack */
 #include <base/internal/stack.h>
+#include <base/internal/native_utcb.h>
 
 /* core includes */
 #include <map_local.h>
diff --git a/repos/base-hw/src/include/base/internal/native_utcb.h b/repos/base-hw/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..fecfe1456
--- /dev/null
+++ b/repos/base-hw/src/include/base/internal/native_utcb.h
@@ -0,0 +1,118 @@
+/*
+ * \brief  UTCB definition
+ * \author Martin Stein
+ * \author Stefan Kalkowski
+ * \date   2012-01-02
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+/* Genode includes */
+#include <base/stdint.h>
+#include <base/ipc_msgbuf.h>
+
+/* base-internal includes */
+#include <base/internal/page_size.h>
+
+/* kernel includes */
+#include <kernel/interface.h>
+
+namespace Genode { struct Native_utcb; }
+
+class Genode::Native_utcb
+{
+	public:
+
+		enum { MAX_CAP_ARGS = Msgbuf_base::MAX_CAP_ARGS};
+
+		enum Offsets { THREAD_MYSELF, PARENT, UTCB_DATASPACE };
+
+	private:
+
+		Kernel::capid_t _caps[MAX_CAP_ARGS]; /* capability buffer  */
+		size_t          _cap_cnt;            /* capability counter */
+		size_t          _size;               /* bytes to transfer  */
+		uint8_t         _buf[get_page_size() - sizeof(_caps) -
+		                     sizeof(_cap_cnt) - sizeof(_size)];
+
+	public:
+
+		Native_utcb& operator= (const Native_utcb &o)
+		{
+			_cap_cnt = 0;
+			_size    = o._size;
+			memcpy(_buf, o._buf, _size);
+			return *this;
+		}
+
+		/**
+		 * Set the destination capability id (server object identity)
+		 */
+		void destination(Kernel::capid_t id) {
+			*reinterpret_cast<long*>(_buf) = id; }
+
+		/**
+		 * Return the count of capabilities in the UTCB
+		 */
+		size_t cap_cnt() { return _cap_cnt; }
+
+		/**
+		 * Set the count of capabilities in the UTCB
+		 */
+		void cap_cnt(size_t cnt) { _cap_cnt = cnt;  }
+
+		/**
+		 * Return the start address of the payload data
+		 */
+		void const * base() const { return &_buf; }
+
+		/**
+		 * Copy data from the message buffer 'o' to this UTCB
+		 */
+		void copy_from(Msgbuf_base &o, size_t size)
+		{
+			_size = size;
+
+			_cap_cnt = o._snd_cap_cnt;
+			for (unsigned i = 0; i < _cap_cnt; i++)
+				_caps[i] = o._caps[i].dst();
+
+			memcpy(_buf, o.buf, min(_size, o._size));
+		}
+
+		/**
+		 * Copy data from this UTCB to the message buffer 'o'
+		 */
+		void copy_to(Msgbuf_base &o)
+		{
+			o._snd_cap_cnt = _cap_cnt;
+			for (unsigned i = 0; i < _cap_cnt; i++) {
+				o._caps[i] = _caps[i];
+				if (o._caps[i].valid()) Kernel::ack_cap(o._caps[i].dst());
+			}
+
+			memcpy(o.buf, _buf, min(_size, o._size));
+		}
+
+		/**
+		 * Return the capability id at index 'i'
+		 */
+		Kernel::capid_t cap_get(unsigned i) {
+			return (i < _cap_cnt) ? _caps[i] : Kernel::cap_id_invalid(); }
+
+		/**
+		 * Set the capability id 'cap_id' at the next index
+		 */
+		void cap_add(Kernel::capid_t cap_id) {
+			if (_cap_cnt < MAX_CAP_ARGS) _caps[_cap_cnt++] = cap_id; }
+};
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
diff --git a/repos/base-hw/src/test/cpu_scheduler/target.mk b/repos/base-hw/src/test/cpu_scheduler/target.mk
index ea8af5d3f..84439640b 100644
--- a/repos/base-hw/src/test/cpu_scheduler/target.mk
+++ b/repos/base-hw/src/test/cpu_scheduler/target.mk
@@ -12,3 +12,6 @@ LIBS += core
 
 # add C++ sources
 SRC_CC += kernel/test.cc
+
+# allow the test to use base-internal headers, i.e., page_size.h
+INC_DIR += $(BASE_DIR)/src/include
diff --git a/repos/base-linux/include/base/native_types.h b/repos/base-linux/include/base/native_types.h
index b3af6a5b1..162b2273a 100644
--- a/repos/base-linux/include/base/native_types.h
+++ b/repos/base-linux/include/base/native_types.h
@@ -95,11 +95,6 @@ namespace Genode {
 		static void copy(void* dst, Native_capability_tpl<Cap_dst_policy>* src);
 	};
 
-	/**
-	 * Empty UTCB type expected by the thread library, unused on Linux
-	 */
-	typedef struct { } Native_utcb;
-
 	typedef Native_capability_tpl<Cap_dst_policy> Native_capability;
 
 	/**
diff --git a/repos/base-linux/src/include/base/internal/native_utcb.h b/repos/base-linux/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..05e08f038
--- /dev/null
+++ b/repos/base-linux/src/include/base/internal/native_utcb.h
@@ -0,0 +1,19 @@
+/*
+ * \brief  UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+namespace Genode { struct Native_utcb { }; }
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
diff --git a/repos/base-nova/include/base/native_types.h b/repos/base-nova/include/base/native_types.h
index 1b230678c..f5eabe095 100644
--- a/repos/base-nova/include/base/native_types.h
+++ b/repos/base-nova/include/base/native_types.h
@@ -43,32 +43,13 @@ namespace Genode {
 		return (t1.ec_sel == t2.ec_sel) &&
 		       (t1.exc_pt_sel == t2.exc_pt_sel);
 	}
+
 	inline bool operator != (Native_thread_id t1, Native_thread_id t2)
 	{
 		return (t1.ec_sel != t2.ec_sel) &&
 		       (t1.exc_pt_sel != t2.exc_pt_sel);
 	}
 
-	class Native_utcb
-	{
-		private:
-
-			/**
-			 * Size of the NOVA-specific user-level thread-control
-			 * block
-			 */
-			enum { UTCB_SIZE = 4096 };
-
-			/**
-			 * User-level thread control block
-			 *
-			 * The UTCB is one 4K page, shared between the kernel
-			 * and the user process. It is not backed by a
-			 * dataspace but provided by the kernel.
-			 */
-			addr_t _utcb[UTCB_SIZE/sizeof(addr_t)];
-	};
-
 	class Native_capability
 	{
 		public:
diff --git a/repos/base-nova/include/nova/syscall-generic.h b/repos/base-nova/include/nova/syscall-generic.h
index 2d4db229d..dbaeeca2c 100644
--- a/repos/base-nova/include/nova/syscall-generic.h
+++ b/repos/base-nova/include/nova/syscall-generic.h
@@ -442,6 +442,11 @@ namespace Nova {
 	 */
 	struct Utcb
 	{
+		/**
+		 * Return physical size of UTCB in bytes
+		 */
+		static constexpr mword_t size() { return 4096; }
+
 		/**
 		 * Number of untyped items uses lowest 16 bit, number of typed items
 		 * uses bit 16-31, bit 32+ are ignored on 64bit
diff --git a/repos/base-nova/src/base/thread/stack.cc b/repos/base-nova/src/base/thread/stack.cc
index c82a8069f..bed75f644 100644
--- a/repos/base-nova/src/base/thread/stack.cc
+++ b/repos/base-nova/src/base/thread/stack.cc
@@ -24,6 +24,7 @@
 /* base-internal includes */
 #include <base/internal/stack.h>
 #include <base/internal/stack_area.h>
+#include <base/internal/native_utcb.h>
 
 /* base-nova includes */
 #include <base/cap_map.h>
diff --git a/repos/base-nova/src/core/platform.cc b/repos/base-nova/src/core/platform.cc
index 8876ab717..8c3fd9c44 100644
--- a/repos/base-nova/src/core/platform.cc
+++ b/repos/base-nova/src/core/platform.cc
@@ -29,6 +29,7 @@
 
 /* base-internal includes */
 #include <base/internal/stack_area.h>
+#include <base/internal/native_utcb.h>
 
 /* NOVA includes */
 #include <nova/syscalls.h>
diff --git a/repos/base-nova/src/include/base/internal/native_utcb.h b/repos/base-nova/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..1f9d7a4fc
--- /dev/null
+++ b/repos/base-nova/src/include/base/internal/native_utcb.h
@@ -0,0 +1,42 @@
+/*
+ * \brief  UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+#include <base/stdint.h>
+
+namespace Genode { struct Native_utcb; }
+
+class Genode::Native_utcb
+{
+	private:
+
+		/**
+		 * Size of the NOVA-specific user-level thread-control
+		 * block
+		 */
+		enum { UTCB_SIZE = 4096 };
+
+		/**
+		 * User-level thread control block
+		 *
+		 * The UTCB is one 4K page, shared between the kernel
+		 * and the user process. It is not backed by a
+		 * dataspace but provided by the kernel.
+		 */
+		addr_t _utcb[UTCB_SIZE/sizeof(addr_t)];
+};
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
+
diff --git a/repos/base-okl4/include/base/native_types.h b/repos/base-okl4/include/base/native_types.h
index f84a4a2ab..8b31361b2 100644
--- a/repos/base-okl4/include/base/native_types.h
+++ b/repos/base-okl4/include/base/native_types.h
@@ -71,14 +71,6 @@ namespace Genode {
 		return tid.raw;
 	}
 
-	/**
-	 * Empty UTCB type expected by the thread library, unused on OKL4
-	 *
-	 * On this kernel, UTCBs are not placed within the stack area. Each
-	 * thread can request its own UTCB pointer using the kernel interface.
-	 */
-	typedef struct { } Native_utcb;
-
 	struct Cap_dst_policy
 	{
 		typedef Okl4::L4_ThreadId_t Dst;
diff --git a/repos/base-okl4/src/include/base/internal/native_utcb.h b/repos/base-okl4/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..000a00d69
--- /dev/null
+++ b/repos/base-okl4/src/include/base/internal/native_utcb.h
@@ -0,0 +1,23 @@
+/*
+ * \brief  UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ *
+ * On this kernel, UTCBs are not placed within the stack area. Each thread
+ * can request its own UTCB pointer using the kernel interface.
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+namespace Genode { struct Native_utcb { }; }
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
+
diff --git a/repos/base-pistachio/include/base/native_types.h b/repos/base-pistachio/include/base/native_types.h
index e86377aec..86a7bd71c 100644
--- a/repos/base-pistachio/include/base/native_types.h
+++ b/repos/base-pistachio/include/base/native_types.h
@@ -53,23 +53,6 @@ namespace Genode {
 		Platform_thread *pt;
 	};
 
-	inline unsigned long convert_native_thread_id_to_badge(Native_thread_id tid)
-	{
-		/*
-		 * Pistachio has no server-defined badges for page-fault messages.
-		 * Therefore, we have to interpret the sender ID as badge.
-		 */
-		return tid.raw;
-	}
-
-	/**
-	 * Empty UTCB type expected by the thread library
-	 *
-	 * On this kernel, UTCBs are not placed within the stack area. Each thread
-	 * can request its own UTCB pointer using the kernel interface.
-	 */
-	typedef struct { } Native_utcb;
-
 	typedef Native_capability_tpl<Cap_dst_policy> Native_capability;
 
 	typedef Pistachio::L4_ThreadId_t Native_connection_state;
diff --git a/repos/base-pistachio/src/core/include/platform_thread.h b/repos/base-pistachio/src/core/include/platform_thread.h
index 42797a7c5..fb382d695 100644
--- a/repos/base-pistachio/src/core/include/platform_thread.h
+++ b/repos/base-pistachio/src/core/include/platform_thread.h
@@ -28,6 +28,17 @@ namespace Pistachio {
 #include <l4/types.h>
 }
 
+
+inline unsigned long convert_native_thread_id_to_badge(Genode::Native_thread_id tid)
+{
+	/*
+	 * Pistachio has no server-defined badges for page-fault messages.
+	 * Therefore, we have to interpret the sender ID as badge.
+	 */
+	return tid.raw;
+}
+
+
 namespace Genode {
 
 	class Platform_pd;
diff --git a/repos/base-pistachio/src/include/base/internal/native_utcb.h b/repos/base-pistachio/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..a7408785f
--- /dev/null
+++ b/repos/base-pistachio/src/include/base/internal/native_utcb.h
@@ -0,0 +1,23 @@
+/*
+ * \brief  Pistachio-specific UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ *
+ * On this kernel, UTCBs are not placed within the stack area. Each thread
+ * can request its own UTCB pointer using the kernel interface.
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+namespace Genode { struct Native_utcb { }; }
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
+
diff --git a/repos/base-sel4/include/base/native_types.h b/repos/base-sel4/include/base/native_types.h
index a8175b821..14c33aaa8 100644
--- a/repos/base-sel4/include/base/native_types.h
+++ b/repos/base-sel4/include/base/native_types.h
@@ -108,24 +108,6 @@ namespace Genode {
 			bool valid() const;
 	};
 
-	struct Native_utcb
-	{
-		/**
-		 * On seL4, the UTCB is called IPC buffer. We use one page
-		 * for each IPC buffer.
-		 */
-		enum { IPC_BUFFER_SIZE = 4096 };
-
-		union {
-
-			addr_t raw[IPC_BUFFER_SIZE/sizeof(addr_t)];
-
-			struct {
-				addr_t ep_sel;
-			};
-		};
-	};
-
 	typedef int Native_connection_state;
 }
 
diff --git a/repos/base-sel4/src/core/platform_thread.cc b/repos/base-sel4/src/core/platform_thread.cc
index acf2f81fc..2f04c1e5e 100644
--- a/repos/base-sel4/src/core/platform_thread.cc
+++ b/repos/base-sel4/src/core/platform_thread.cc
@@ -21,6 +21,7 @@
 
 /* base-internal includes */
 #include <base/internal/capability_space_sel4.h>
+#include <base/internal/native_utcb.h>
 
 using namespace Genode;
 
diff --git a/repos/base-sel4/src/include/base/internal/native_utcb.h b/repos/base-sel4/src/include/base/internal/native_utcb.h
new file mode 100644
index 000000000..b404bfbb4
--- /dev/null
+++ b/repos/base-sel4/src/include/base/internal/native_utcb.h
@@ -0,0 +1,37 @@
+/*
+ * \brief  UTCB definition
+ * \author Norman Feske
+ * \date   2016-03-08
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+#define _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_
+
+#include <base/stdint.h>
+
+namespace Genode { struct Native_utcb; }
+
+struct Genode::Native_utcb
+{
+	/**
+	 * On seL4, the UTCB is called IPC buffer. We use one page
+	 * for each IPC buffer.
+	 */
+	enum { IPC_BUFFER_SIZE = 4096 };
+
+	union {
+
+		addr_t raw[IPC_BUFFER_SIZE/sizeof(addr_t)];
+
+		struct { addr_t ep_sel; };
+	};
+};
+
+#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */
diff --git a/repos/base/include/base/thread.h b/repos/base/include/base/thread.h
index 7b03a82a5..e3d1f1fe0 100644
--- a/repos/base/include/base/thread.h
+++ b/repos/base/include/base/thread.h
@@ -28,6 +28,7 @@
 
 namespace Genode {
 
+	struct Native_utcb;
 	class Rm_session;
 	class Thread_base;
 	class Stack;
diff --git a/repos/base/src/base/thread/thread_utcb.cc b/repos/base/src/base/thread/thread_utcb.cc
index a55273809..a0d3b732c 100644
--- a/repos/base/src/base/thread/thread_utcb.cc
+++ b/repos/base/src/base/thread/thread_utcb.cc
@@ -16,6 +16,7 @@
 
 /* base-internal includes */
 #include <base/internal/stack.h>
+#include <base/internal/native_utcb.h>
 
 using namespace Genode;
 
diff --git a/repos/base/src/include/base/internal/page_size.h b/repos/base/src/include/base/internal/page_size.h
new file mode 100644
index 000000000..5768624bd
--- /dev/null
+++ b/repos/base/src/include/base/internal/page_size.h
@@ -0,0 +1,23 @@
+/*
+ * \brief  Page size utilities
+ * \author Norman Feske
+ * \date   2016-03-08
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _INCLUDE__BASE__INTERNAL__PAGE_SIZE_H_
+#define _INCLUDE__BASE__INTERNAL__PAGE_SIZE_H_
+
+namespace Genode
+{
+	constexpr size_t get_page_size_log2() { return 12; }
+	constexpr size_t get_page_size()      { return 1 << get_page_size_log2(); }
+}
+
+#endif /* _INCLUDE__BASE__INTERNAL__PAGE_SIZE_H_ */
diff --git a/repos/base/src/include/base/internal/stack.h b/repos/base/src/include/base/internal/stack.h
index c084e939a..9f7aa464d 100644
--- a/repos/base/src/include/base/internal/stack.h
+++ b/repos/base/src/include/base/internal/stack.h
@@ -59,6 +59,9 @@
 #include <cpu/consts.h>
 #include <ram_session/ram_session.h>  /* for 'Ram_dataspace_capability' type */
 
+/* base-internal includes */
+#include <base/internal/native_utcb.h>
+
 namespace Genode { class Stack; }
 
 
diff --git a/repos/ports/include/vmm/printf.h b/repos/ports/include/vmm/printf.h
index 9d92228a1..99b497303 100644
--- a/repos/ports/include/vmm/printf.h
+++ b/repos/ports/include/vmm/printf.h
@@ -19,6 +19,9 @@
 #include <base/lock.h>
 #include <base/printf.h>
 
+/* NOVA includes */
+#include <nova/syscalls.h>
+
 namespace Vmm {
 
 	using namespace Genode;
@@ -35,17 +38,19 @@ inline void Vmm::printf(const char *format, ...)
 	va_list list;
 	va_start(list, format);
 
+	struct Utcb_backup { char buf[Nova::Utcb::size()]; };
+
 	static Lock        lock;
-	static Native_utcb utcb_backup;
+	static Utcb_backup utcb_backup;
 
 	Lock::Guard guard(lock);
 
-	utcb_backup = *Thread_base::myself()->utcb();
+	utcb_backup = *(Utcb_backup *)Thread_base::myself()->utcb();
 
 	Genode::printf("VMM: ");
 	Genode::vprintf(format, list);
 
-	*Thread_base::myself()->utcb() = utcb_backup;
+	*(Utcb_backup *)Thread_base::myself()->utcb() = utcb_backup;
 
 	va_end(list);
 }
diff --git a/repos/ports/include/vmm/utcb_guard.h b/repos/ports/include/vmm/utcb_guard.h
index c27bffb4b..c125f16cd 100644
--- a/repos/ports/include/vmm/utcb_guard.h
+++ b/repos/ports/include/vmm/utcb_guard.h
@@ -30,13 +30,17 @@ namespace Vmm {
 
 class Vmm::Utcb_guard
 {
+	public:
+
+		struct Utcb_backup { char buf[Nova::Utcb::size()]; };
+
 	private:
 
-		Native_utcb &_backup_utcb;
+		Utcb_backup &_backup_utcb;
 
 	public:
 
-		Utcb_guard(Native_utcb &backup_utcb) : _backup_utcb(backup_utcb)
+		Utcb_guard(Utcb_backup &backup_utcb) : _backup_utcb(backup_utcb)
 		{
 			Nova::Utcb *utcb =
 				reinterpret_cast<Nova::Utcb *>(Thread_base::myself()->utcb());
diff --git a/repos/ports/src/app/seoul/disk.cc b/repos/ports/src/app/seoul/disk.cc
index cd0a8f8ec..0c04cd4dd 100644
--- a/repos/ports/src/app/seoul/disk.cc
+++ b/repos/ports/src/app/seoul/disk.cc
@@ -181,7 +181,7 @@ void Vancouver_disk::_signal_dispatch_entry(unsigned disknr)
 
 bool Vancouver_disk::receive(MessageDisk &msg)
 {
-	static Genode::Native_utcb utcb_backup;
+	static Vmm::Utcb_guard::Utcb_backup utcb_backup;
 	Vmm::Utcb_guard guard(utcb_backup);
 
 	if (msg.disknr >= MAX_DISKS)
diff --git a/repos/ports/src/app/seoul/main.cc b/repos/ports/src/app/seoul/main.cc
index ae55481cd..9070b2949 100644
--- a/repos/ports/src/app/seoul/main.cc
+++ b/repos/ports/src/app/seoul/main.cc
@@ -52,6 +52,7 @@
 #include <vmm/guest_memory.h>
 #include <vmm/vcpu_thread.h>
 #include <vmm/vcpu_dispatcher.h>
+#include <vmm/utcb_guard.h>
 
 /* NOVA includes that come with Genode */
 #include <nova/syscalls.h>
@@ -77,7 +78,10 @@ enum { verbose_debug = false };
 enum { verbose_npt   = false };
 enum { verbose_io    = false };
 
-static Genode::Native_utcb utcb_backup;
+typedef Vmm::Utcb_guard::Utcb_backup Utcb_backup;
+
+static Utcb_backup utcb_backup;
+
 Genode::Lock *utcb_lock()
 {
 	static Genode::Lock inst;
@@ -1143,7 +1147,9 @@ class Machine : public StaticReceiver<Machine>
 		bool receive(MessageTime &msg)
 		{
 			Genode::Lock::Guard guard(*utcb_lock());
-			utcb_backup = *Genode::Thread_base::myself()->utcb();
+
+			Vmm::Utcb_guard utcb_guard(utcb_backup);
+			utcb_backup = *(Utcb_backup *)Genode::Thread_base::myself()->utcb();
 
 			if (!_rtc) {
 				try {
@@ -1152,7 +1158,7 @@ class Machine : public StaticReceiver<Machine>
 					Logging::printf("No RTC present, returning dummy time.\n");
 					msg.wallclocktime = msg.timestamp = 0;
 
-					*Genode::Thread_base::myself()->utcb() = utcb_backup;
+					*(Utcb_backup *)Genode::Thread_base::myself()->utcb() = utcb_backup;
 
 					return true;
 				}
@@ -1166,7 +1172,7 @@ class Machine : public StaticReceiver<Machine>
 			Logging::printf("Got time %llx\n", msg.wallclocktime);
 			msg.timestamp = _unsynchronized_motherboard.clock()->clock(MessageTime::FREQUENCY);
 
-			*Genode::Thread_base::myself()->utcb() = utcb_backup;
+			*(Utcb_backup *)Genode::Thread_base::myself()->utcb() = utcb_backup;
 
 			return true;
 		}
@@ -1176,7 +1182,8 @@ class Machine : public StaticReceiver<Machine>
 			if (msg.type != MessageNetwork::PACKET) return false;
 
 			Genode::Lock::Guard guard(*utcb_lock());
-			utcb_backup = *Genode::Thread_base::myself()->utcb();
+
+			Vmm::Utcb_guard utcb_guard(utcb_backup);
 
 			if (msg.buffer == _forward_pkt) {
 				/* don't end in an endless forwarding loop */
@@ -1211,8 +1218,6 @@ class Machine : public StaticReceiver<Machine>
 			/* release sent packet to free the space in the tx communication buffer */
 			_nic->tx()->release_packet(tx_packet);
 
-			*Genode::Thread_base::myself()->utcb() = utcb_backup;
-
 			return true;
 		}
 
diff --git a/repos/ports/src/app/seoul/nova_user_env.cc b/repos/ports/src/app/seoul/nova_user_env.cc
index 35c898849..48009790c 100644
--- a/repos/ports/src/app/seoul/nova_user_env.cc
+++ b/repos/ports/src/app/seoul/nova_user_env.cc
@@ -17,6 +17,9 @@
 #include <base/sleep.h>
 #include <base/thread.h>
 
+/* VMM utils */
+#include <vmm/utcb_guard.h>
+
 /* NOVA userland includes */
 #include <service/logging.h>
 #include <service/memory.h>
@@ -31,7 +34,9 @@ Genode::Lock *printf_lock()
 }
 
 
-static Genode::Native_utcb utcb_backup;
+typedef Vmm::Utcb_guard::Utcb_backup Utcb_backup;
+
+static Utcb_backup utcb_backup;
 
 
 void Logging::printf(const char *format, ...)
@@ -41,12 +46,12 @@ void Logging::printf(const char *format, ...)
 
 	Genode::Lock::Guard guard(*printf_lock());
 
-	utcb_backup = *Genode::Thread_base::myself()->utcb();
+	utcb_backup = *(Utcb_backup *)Genode::Thread_base::myself()->utcb();
 
 	Genode::printf("VMM: ");
 	Genode::vprintf(format, list);
 
-	*Genode::Thread_base::myself()->utcb() = utcb_backup;
+	*(Utcb_backup *)Genode::Thread_base::myself()->utcb() = utcb_backup;
 
 	va_end(list);
 }
@@ -56,13 +61,13 @@ void Logging::vprintf(const char *format, va_list &ap)
 {
 	Genode::Lock::Guard guard(*printf_lock());
 
-	utcb_backup = *Genode::Thread_base::myself()->utcb();
+	utcb_backup = *(Utcb_backup *)Genode::Thread_base::myself()->utcb();
 
 	Genode::printf("VMM: ");
 	Genode::printf(format);
 	PWRN("Logging::vprintf not implemented");
 
-	*Genode::Thread_base::myself()->utcb() = utcb_backup;
+	*(Utcb_backup *)Genode::Thread_base::myself()->utcb() = utcb_backup;
 }
 
 
diff --git a/repos/ports/src/virtualbox/pgm.cc b/repos/ports/src/virtualbox/pgm.cc
index f4ecd5ef2..4cde517da 100644
--- a/repos/ports/src/virtualbox/pgm.cc
+++ b/repos/ports/src/virtualbox/pgm.cc
@@ -15,8 +15,6 @@
 #include <base/printf.h>
 #include <util/string.h>
 
-#include <vmm/printf.h>
-
 /* VirtualBox includes */
 #include "PGMInternal.h" /* enable access to pgm.s.* */
 #include "EMInternal.h"
@@ -644,8 +642,8 @@ extern "C" int MMIO2_MAPPED_SYNC(PVM pVM, RTGCPHYS GCPhys, size_t cbWrite,
 			return VINF_SUCCESS;
 		}
 		
-		Vmm::printf("%s: GCPhys=0x%llx failed - unexpected rc=%d\n",
-		            __func__, (Genode::uint64_t)GCPhys, rc);
+//		Vmm::printf("%s: GCPhys=0x%llx failed - unexpected rc=%d\n",
+//		            __func__, (Genode::uint64_t)GCPhys, rc);
 		return rc;
 	}
 
@@ -659,10 +657,10 @@ extern "C" int MMIO2_MAPPED_SYNC(PVM pVM, RTGCPHYS GCPhys, size_t cbWrite,
 	Assert(pv);
 
 	fli = Flexpage_iterator((addr_t)pv, map_size, map_start, map_size, map_start);
-	if (verbose_debug)
-		Vmm::printf("%s: GCPhys=0x%llx - %llx+%zx\n", __func__,
-		            (Genode::uint64_t)GCPhys, (Genode::uint64_t)map_start,
-		            map_size);
+//	if (verbose_debug)
+//		Vmm::printf("%s: GCPhys=0x%llx - %llx+%zx\n", __func__,
+//		            (Genode::uint64_t)GCPhys, (Genode::uint64_t)map_start,
+//		            map_size);
 
 	*ppv = pv;
 
diff --git a/repos/ports/src/virtualbox/thread.cc b/repos/ports/src/virtualbox/thread.cc
index cea061706..b0815cc5b 100644
--- a/repos/ports/src/virtualbox/thread.cc
+++ b/repos/ports/src/virtualbox/thread.cc
@@ -68,8 +68,10 @@ static int create_thread(pthread_t *thread, const pthread_attr_t *attr,
 
 	Assert(rtthread);
 
+	size_t const utcb_size = 4096;
+
 	size_t stack_size = Genode::Thread_base::stack_virtual_size() -
-	                    sizeof(Genode::Native_utcb) - 2 * (1UL << 12);
+	                    utcb_size - 2 * (1UL << 12);
 
 	if (rtthread->cbStack < stack_size)
 		stack_size = rtthread->cbStack;