diff --git a/components/VM_Arm/src/main.c b/components/VM_Arm/src/main.c
index 4f98a6e8..0f27aa7b 100644
--- a/components/VM_Arm/src/main.c
+++ b/components/VM_Arm/src/main.c
@@ -127,6 +127,10 @@ seL4_CPtr camkes_get_smmu_cb_cap();
 seL4_CPtr camkes_get_smmu_sid_cap();
 #endif
 
+#ifdef CONFIG_ALLOW_SMC_CALLS
+seL4_CPtr camkes_get_smc_cap();
+#endif
+
 int get_crossvm_irq_num(void)
 {
     return free_plat_interrupts[0];
@@ -1233,6 +1237,10 @@ static int main_continued(void)
     err = vm_create_default_irq_controller(&vm);
     assert(!err);
 
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    vm.vm_smc = camkes_get_smc_cap();
+#endif
+
     /* Create CPUs and DTB node */
     for (int i = 0; i < NUM_VCPUS; i++) {
         vm_vcpu_t *new_vcpu = create_vmm_plat_vcpu(&vm, VM_PRIO - 1);