diff --git a/src/arch/aarch64/virq.c b/src/arch/aarch64/virq.c
index eac507f3..298e4a22 100644
--- a/src/arch/aarch64/virq.c
+++ b/src/arch/aarch64/virq.c
@@ -3,6 +3,9 @@
 #include "../../util/util.h"
 #include "../../virq.h"
 
+/* Maps Microkit channel numbers with registered vIRQ */
+int virq_passthrough_map[MAX_PASSTHROUGH_IRQ] = {-1};
+
 #define SGI_RESCHEDULE_IRQ  0
 #define SGI_FUNC_CALL       1
 #define PPI_VTIMER_IRQ      27
@@ -51,3 +54,44 @@ bool virq_inject(size_t vcpu_id, int irq) {
 bool virq_register(size_t vcpu_id, size_t virq_num, virq_ack_fn_t ack_fn, void *ack_data) {
     return vgic_register_irq(vcpu_id, virq_num, ack_fn, ack_data);
 }
+
+static void virq_passthrough_ack(size_t vcpu_id, int irq, void *cookie) {
+    /* We are down-casting to microkit_channel so must first cast to size_t */
+    microkit_irq_ack((microkit_channel)(size_t)cookie);
+}
+
+bool virq_register_passthrough(size_t vcpu_id, size_t irq, microkit_channel irq_ch) {
+    assert(irq_ch < MICROKIT_MAX_CHANNELS);
+    if (irq_ch >= MICROKIT_MAX_CHANNELS) {
+        LOG_VMM_ERR("Invalid channel number given '0x%lx' for passthrough vIRQ 0x%lx\n", irq_ch, irq);
+        return false;
+    }
+
+    LOG_VMM("Register passthrough vIRQ 0x%lx on vCPU 0x%lx (IRQ channel: 0x%lx)\n", irq, vcpu_id, irq_ch);
+    virq_passthrough_map[irq_ch] = irq;
+
+    bool success = virq_register(GUEST_VCPU_ID, irq, &virq_passthrough_ack, (void *)(size_t)irq_ch);
+    assert(success);
+    if (!success) {
+        LOG_VMM_ERR("Failed to register passthrough vIRQ %d\n", irq);
+        return false;
+    }
+
+    return true;
+}
+
+bool virq_handle_passthrough(microkit_channel irq_ch) {
+    assert(virq_passthrough_map[irq_ch] >= 0);
+    if (virq_passthrough_map[irq_ch] < 0) {
+        LOG_VMM_ERR("attempted to handle invalid passthrough IRQ channel 0x%lx\n", irq_ch);
+        return false;
+    }
+
+    bool success = vgic_inject_irq(GUEST_VCPU_ID, virq_passthrough_map[irq_ch]);
+    if (!success) {
+        LOG_VMM_ERR("could not inject passthrough vIRQ 0x%lx, dropped on vCPU 0x%lx\n", virq_passthrough_map[irq_ch], GUEST_VCPU_ID);
+        return false;
+    }
+
+    return true;
+}
diff --git a/src/virq.h b/src/virq.h
index 78d2e628..8e1df31d 100644
--- a/src/virq.h
+++ b/src/virq.h
@@ -1,8 +1,26 @@
 #include <stddef.h>
 #include <stdbool.h>
+#include <microkit.h>
+
+#ifndef MAX_PASSTHROUGH_IRQ
+#define MAX_PASSTHROUGH_IRQ MICROKIT_MAX_CHANNELS
+#endif
 
 typedef void (*virq_ack_fn_t)(size_t vcpu_id, int irq, void *cookie);
 
 bool virq_controller_init(size_t boot_vcpu_id);
 bool virq_register(size_t vcpu_id, size_t virq_num, virq_ack_fn_t ack_fn, void *ack_data);
 bool virq_inject(size_t vcpu_id, int irq);
+
+/*
+ * These two APIs are convenient for when you want to directly passthrough an IRQ from
+ * the hardware to the guest as the same vIRQ. This is useful when the guest has direct
+ * passthrough access to a particular device on the hardware.
+ * After registering the passthrough IRQ, call `virq_handle_passthrough` when
+ * the IRQ has come through from seL4.
+ *
+ * @ivanv: currently this API assumes a Microkit environment. This should be changed
+ * if/when we make libvmm agnostic to the seL4 environment it is running in.
+ */
+bool virq_register_passthrough(size_t vcpu_id, size_t irq, microkit_channel irq_ch);
+bool virq_handle_passthrough(microkit_channel irq_ch);