diff --git a/include/plat/tk1/plat/machine.h b/include/plat/tk1/plat/machine.h
index 430360e12..d46e31212 100644
--- a/include/plat/tk1/plat/machine.h
+++ b/include/plat/tk1/plat/machine.h
@@ -211,13 +211,19 @@ enum IRQConstants {
     maxIRQ                          = 192
 } platform_interrupt_t;
 
-#define INTERRUPT_S_PGPT        INTERRUPT_PPI_13
-#define INTERRUPT_NS_PGPT       INTERRUPT_PPI_14
-#define INTERRUPT_VGPT          INTERRUPT_PPI_11
-#define INTERRUPT_HGPT          INTERRUPT_PPI_10
+#define INTERRUPT_VGIC_MAINTENANCE      INTERRUPT_PPI_9
+#define INTERRUPT_S_PGPT                INTERRUPT_PPI_13
+#define INTERRUPT_NS_PGPT               INTERRUPT_PPI_14
+#define INTERRUPT_VGPT                  INTERRUPT_PPI_11
+#define INTERRUPT_HGPT                  INTERRUPT_PPI_10
 
 /* the kernel runs in secure supervisor mode by default */
+
+#ifdef ARM_HYP
+#define KERNEL_TIMER_IRQ        INTERRUPT_HGPT
+#else
 #define KERNEL_TIMER_IRQ        INTERRUPT_S_PGPT
+#endif
 
 enum irqNumbers {
     irqInvalid = 255
diff --git a/include/plat/tk1/plat/machine/devices.h b/include/plat/tk1/plat/machine/devices.h
index a59baafa0..b7f6edf54 100644
--- a/include/plat/tk1/plat/machine/devices.h
+++ b/include/plat/tk1/plat/machine/devices.h
@@ -26,6 +26,10 @@
 #define GIC_DISTRIBUTOR_PADDR       GICD_PADDR
 #define GIC_CONTROLLER0_PADDR       GICI_PADDR
 
+/* HYP mode kernel devices */
+#define GIC_VCPUCTRL_PPTR           0xfff06000
+#define GIC_PL400_VCPUCTRL_PPTR     GIC_VCPUCTRL_PPTR
+#define GIC_VCPUCTRL_PADDR          (VGICI_REQ_PADDR)
 /*
  * many of the device regions are not 4K page aligned, so some regions may contain more than
  * one devices. it is the user's responsibilty to figure out how to use these regions
diff --git a/src/arch/arm/object/vcpu.c b/src/arch/arm/object/vcpu.c
index b3c6fc0d5..ae9343812 100644
--- a/src/arch/arm/object/vcpu.c
+++ b/src/arch/arm/object/vcpu.c
@@ -84,6 +84,12 @@
 #define VGIC_IRQ_ACTIVE      (0x2U << 28)
 #define VGIC_IRQ_MASK        (0x3U << 28)
 
+#define VIRQ_GROUP_MASK     (1)
+#define VIRQ_GROUP_SHIFT    (30)
+#define VIRQ_PRIORITY_MASK  (0x1f)
+#define VIRQ_PRIORITY_SHIFT (23)
+#define VIRQ_IRQ_MASK       (0x3ff)
+
 struct gich_vcpu_ctrl_map {
     uint32_t hcr;    /* 0x000 RW 0x00000000 Hypervisor Control Register */
     uint32_t vtr;    /* 0x004 RO IMPLEMENTATION DEFINED VGIC Type Register */
@@ -354,10 +360,18 @@ decodeVCPUReadReg(cap_t cap, unsigned int length, word_t* buffer)
     return invokeVCPUReadReg(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap)), field);
 }
 
+static uint32_t makeVIRQ(int group, int priority, int irq)
+{
+    uint32_t virq = ((group & VIRQ_GROUP_MASK) << VIRQ_GROUP_SHIFT);
+    virq |= ((priority & VIRQ_PRIORITY_MASK) << VIRQ_PRIORITY_SHIFT);
+    virq |= (irq & VIRQ_IRQ_MASK);
+    return virq;
+}
+
 exception_t
 invokeVCPUInjectIRQ(vcpu_t* vcpu, int index, int group, int priority, int irq)
 {
-    vcpu->vgic.lr[index] = (group << 30) | (priority << 23) | (irq << 0);
+    vcpu->vgic.lr[index] = makeVIRQ(group, priority, irq);
     vcpu->vgic.lr[index] |= VGIC_IRQ_PENDING | VGIC_LR_EOIIRQEN;
 
     setThreadState(ksCurThread, ThreadState_Restart);