diff --git a/src/arch/aarch64/smc.c b/src/arch/aarch64/smc.c
index 21a6c5f2..7c5ed5bd 100644
--- a/src/arch/aarch64/smc.c
+++ b/src/arch/aarch64/smc.c
@@ -7,6 +7,7 @@
 
 #include "smc.h"
 #include "psci.h"
+#include "fault.h"
 #include "../../util/util.h"
 
 // Values in this file are taken from:
@@ -32,6 +33,69 @@ typedef enum {
     SMC_CALL_RESERVED = 64,
 } smc_call_id_t;
 
+#if defined(CONFIG_ALLOW_SMC_CALLS)
+/* SMC Call Cap that the library makes SMC calls on; passed from an application */
+seL4_CPtr smc_cap_current;
+
+/* Set SMC Call Cap to use by the library API;
+   should be called before an application starts
+   handling exceptions from a VM thread
+*/
+bool smc_set_cap(seL4_CPtr smcccap)
+{
+    if (!smcccap)
+    {
+        LOG_VMM_ERR("SMC forwarding: attempted to set zero SMC Call cap\n");
+        return false;
+    }
+    smc_cap_current = smcccap;
+    return true;
+}
+#endif /*CONFIG_ALLOW_SMC_CALLS*/
+
+#if defined(CONFIG_ALLOW_SMC_CALLS)
+
+/* Service handlers for services that require "physical" access to EL3 components
+   (vs emulation) are listed here.
+
+   'Active' handler is a pointer to a fucntion that actually will be invoked;
+   by default active handlers are set to NULL. Application should assign to an active handler
+   wheither a default handler that unconditionally forwards calls to Secure Monitor:
+
+        smc_set_handler_xxx_service(smc_default_handle_service);
+
+   or assign a custom handler impelemnting some forwarding policy:
+
+        smc_set_handler_xxx_service(wary_handle_service);
+
+   To remove active handler invoke:
+
+        smc_set_handler_xxx_service(NULL);
+
+   Note: application code should include smc.h
+*/
+
+/* 'smc_handle_sip()' is an active handler of SiP Service calls */
+smc_handle_service_type smc_handle_sip = NULL;
+
+/* 'smc_set_handler_sip_service()' assigns/removes active SiP Service handler;
+   NULL is a valid value to remove an earlier assigned handler;
+   function returns 'True' if handler was initialized with pointer to a function,
+   and 'False' if a handler was removed */
+bool smc_set_handler_sip_service (smc_handle_service_type handler_func)
+{
+    if (handler_func == NULL)
+    {
+        smc_handle_sip = NULL;
+        return false;
+    }
+    else
+        smc_handle_sip = handler_func;
+
+    return true;
+}
+#endif /*CONFIG_ALLOW_SMC_CALLS*/
+
 static smc_call_id_t smc_get_call(size_t func_id)
 {
     uint64_t service = ((func_id >> SMC_SERVICE_CALL_SHIFT) & SMC_SERVICE_CALL_MASK);
@@ -109,6 +173,10 @@ bool handle_smc(size_t vcpu_id, uint32_t hsr)
             }
             LOG_VMM_ERR("Unhandled SMC: standard service call %lu\n", fn_number);
             break;
+#if defined(CONFIG_ALLOW_SMC_CALLS)
+        case SMC_CALL_SIP_SERVICE:
+            return smc_handle_sip(vcpu_id, &regs, fn_number);
+#endif
         default:
             LOG_VMM_ERR("Unhandled SMC: unknown value service: 0x%lx, function number: 0x%lx\n", service, fn_number);
             break;
@@ -116,3 +184,33 @@ bool handle_smc(size_t vcpu_id, uint32_t hsr)
 
     return false;
 }
+
+#if defined(CONFIG_ALLOW_SMC_CALLS)
+/* Default handler of calls to a Service (group of Functions) running at Secure Monitor level;
+  forwards all the calls without applying any policy
+*/
+bool smc_default_handle_service(size_t vcpu_id, seL4_UserContext *regs, uint64_t fn_number)
+{
+
+    seL4_ARM_SMCContext request;
+    seL4_ARM_SMCContext response;
+
+    request.x0 = regs->x0; request.x1 = regs->x1;
+    request.x2 = regs->x2; request.x3 = regs->x3;
+    request.x4 = regs->x4; request.x5 = regs->x5;
+    request.x6 = regs->x6; request.x7 = regs->x7;
+
+    seL4_ARM_SMC_Call(smc_cap_current, &request, &response);
+
+    regs->x0 = response.x0; regs->x1 = response.x1;
+    regs->x2 = response.x2; regs->x3 = response.x3;
+    regs->x4 = response.x4; regs->x5 = response.x5;
+    regs->x6 = response.x6; regs->x7 = response.x7;
+
+
+    bool success = fault_advance_vcpu(vcpu_id, regs);
+    assert(success);
+
+    return success;
+}
+#endif /*CONFIG_ALLOW_SMC_CALLS*/
diff --git a/src/arch/aarch64/smc.h b/src/arch/aarch64/smc.h
index bc5e6abf..009b5511 100644
--- a/src/arch/aarch64/smc.h
+++ b/src/arch/aarch64/smc.h
@@ -20,3 +20,21 @@ void smc_set_return_value(seL4_UserContext *u, uint64_t val);
 
 /* Gets the value of x1-x6 */
 uint64_t smc_get_arg(seL4_UserContext *u, uint64_t arg);
+
+#if defined(CONFIG_ALLOW_SMC_CALLS)
+
+/* Default handler of calls to a SMC Service */
+bool smc_default_handle_service(size_t vcpu_id, seL4_UserContext *regs, uint64_t fn_number);
+
+/* Service handler type */
+typedef bool (* smc_handle_service_type)(size_t, seL4_UserContext *, uint64_t);
+
+/* API for user: */
+
+/* Set SMC Call Cap to use by the library API */
+bool smc_set_cap(seL4_CPtr smcccap);
+
+/* 'set_handler_sip_service()' assigns/removes active SiP Service handler */
+bool smc_set_handler_sip_service(smc_handle_service_type handler_func);
+
+#endif