diff --git a/apps/sel4test-driver/include/test_init_data.h b/apps/sel4test-driver/include/test_init_data.h
index 15f569e6..7bf2911c 100644
--- a/apps/sel4test-driver/include/test_init_data.h
+++ b/apps/sel4test-driver/include/test_init_data.h
@@ -64,6 +64,11 @@ typedef struct {
     /* sched control cap */
     seL4_CPtr sched_ctrl;
 
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    /* smc cap */
+    seL4_CPtr smc;
+#endif /* CONFIG_ALLOW_SMC_CALLS */
+
     /* device frame cap */
     seL4_CPtr device_frame_cap;
 
diff --git a/apps/sel4test-driver/src/testtypes.c b/apps/sel4test-driver/src/testtypes.c
index 27c8de63..2b2b8611 100644
--- a/apps/sel4test-driver/src/testtypes.c
+++ b/apps/sel4test-driver/src/testtypes.c
@@ -227,6 +227,11 @@ void basic_set_up(uintptr_t e)
             sel4utils_copy_cap_to_process(&(env->test_process), &env->vka, sched_ctrl);
         }
     }
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    env->init->smc = sel4utils_copy_cap_to_process(&(env->test_process), &env->vka, simple_get_init_cap(&env->simple,
+                                                                                                        seL4_CapSMC));
+#endif /* CONFIG_ALLOW_SMC_CALLS */
+
     /* setup data about untypeds */
     env->init->untypeds = copy_untypeds_to_process(&(env->test_process), env->untypeds, env->num_untypeds, env);
     /* copy the fault endpoint - we wait on the endpoint for a message
diff --git a/apps/sel4test-tests/src/main.c b/apps/sel4test-tests/src/main.c
index d77a5423..60886cf1 100644
--- a/apps/sel4test-tests/src/main.c
+++ b/apps/sel4test-tests/src/main.c
@@ -198,6 +198,9 @@ int main(int argc, char **argv)
     env.asid_pool = init_data->asid_pool;
     env.asid_ctrl = init_data->asid_ctrl;
     env.sched_ctrl = init_data->sched_ctrl;
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    env.smc = init_data->smc;
+#endif
 #ifdef CONFIG_IOMMU
     env.io_space = init_data->io_space;
 #endif
diff --git a/apps/sel4test-tests/src/tests/smc.c b/apps/sel4test-tests/src/tests/smc.c
new file mode 100644
index 00000000..07736ec4
--- /dev/null
+++ b/apps/sel4test-tests/src/tests/smc.c
@@ -0,0 +1,77 @@
+/*
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <autoconf.h>
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <sel4/sel4.h>
+#include <sel4utils/arch/util.h>
+
+#include <vka/object.h>
+#include <vka/capops.h>
+
+#include "../test.h"
+#include "../helpers.h"
+#include "sel4/simple_types.h"
+
+#ifdef CONFIG_ALLOW_SMC_CALLS
+
+#define ARM_STD_SVC_VERSION    0x8400ff03
+#define UNASSIGNED_SMC         0x82000000
+
+static int test_smc_calls(env_t env)
+{
+    seL4_ARM_SMCContext smc_args;
+    seL4_ARM_SMCContext smc_results;
+    int error;
+
+    seL4_CPtr smc_cap = env->smc;
+    seL4_CPtr badged_smc_cap = get_free_slot(env);
+
+    error = cnode_mint(env, smc_cap, badged_smc_cap, seL4_AllRights, ARM_STD_SVC_VERSION);
+    test_error_eq(error, seL4_NoError);
+
+    /* Set function and arguments */
+    smc_args.x0 = ARM_STD_SVC_VERSION;
+    smc_args.x1 = 0;
+    smc_args.x2 = 2;
+    smc_args.x3 = 3;
+    smc_args.x4 = 0;
+    smc_args.x5 = 0;
+    smc_args.x6 = 0;
+    smc_args.x7 = 0;
+
+    /* This should succeed */
+    error = seL4_ARM_SMC_Call(badged_smc_cap, &smc_args, &smc_results);
+    test_error_eq(error, seL4_NoError);
+
+    /* Make sure the call returned something other than the input */
+    test_neq(smc_results.x0, smc_args.x0);
+
+    /* Check that the version returned is non-zero */
+    seL4_Word version_sum = smc_results.x0 + smc_results.x1;
+    test_geq(version_sum, 1UL);
+
+    /* Check that the remaining result registers are clobbered */
+    test_eq(smc_results.x2, 0UL);
+    test_eq(smc_results.x3, 0UL);
+
+    /* This should fail - SMC call with a different function id from badge */
+    smc_args.x0 = UNASSIGNED_SMC;
+    error = seL4_ARM_SMC_Call(badged_smc_cap, &smc_args, &smc_results);
+    test_error_eq(error, seL4_IllegalOperation);
+
+    /* This should fail - can't mint from cap with non-zero badge */
+    seL4_CPtr bad_badged_cap = get_free_slot(env);
+    error = cnode_mint(env, badged_smc_cap, bad_badged_cap, seL4_AllRights, UNASSIGNED_SMC);
+    test_error_eq(error, seL4_IllegalOperation);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(SMC0001, "Test SMC calls", test_smc_calls, true)
+
+#endif