diff --git a/libsel4/Kconfig b/libsel4/Kconfig
index 383a07212..e5b0d6c81 100644
--- a/libsel4/Kconfig
+++ b/libsel4/Kconfig
@@ -26,6 +26,16 @@ config LIB_SEL4_INLINE_INVOCATIONS
         for verification, so setting to 'n' will forcively prevent the function
         from being inlined
 
+config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
+    bool "use only IPC buffer for syscalls"
+    depends on LIB_SEL4
+    default n
+    help
+        When generating syscall wrappers, only use the IPC buffer for
+        marshalling and unmarshalling arguments. Without this option set,
+        arguments will be passed in registers where possible for better
+        performance.
+
 config HAVE_LIB_SEL4
     bool
 endmenu
diff --git a/libsel4/Makefile b/libsel4/Makefile
index 3a0e2d86e..fd472308d 100644
--- a/libsel4/Makefile
+++ b/libsel4/Makefile
@@ -121,5 +121,5 @@ include/interfaces/sel4_client.h: \
 	@mkdir -p $(dir $@)
 	@${CHANGED_PATH} $@ \
         ${PYTHON} ${SOURCE_DIR}/tools/syscall_stub_gen.py \
-        --buffer \
+        $(if ${CONFIG_LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY},--buffer,) \
         -a $(SEL4_ARCH) -c ${srctree}/.config -o $@ $^