diff --git a/libsel4dma/src/dma.c b/libsel4dma/src/dma.c
index 49341c1b0..49f3032ea 100644
--- a/libsel4dma/src/dma.c
+++ b/libsel4dma/src/dma.c
@@ -30,6 +30,8 @@
 #define DMA_MINALIGN_BYTES 32
 #elif defined(CONFIG_PLAT_ZYNQMP)
 #define DMA_MINALIGN_BYTES 32
+#elif defined(CONFIG_PLAT_STM32MP2)
+#define DMA_MINALIGN_BYTES 32
 #else
 #warning Unknown platform. DMA alignment defaulting to 32 bytes.
 #define DMA_MINALIGN_BYTES 32
diff --git a/libsel4vm/src/arch/arm/vgic/gicv2.h b/libsel4vm/src/arch/arm/vgic/gicv2.h
index 1616d63fb..c801b8894 100644
--- a/libsel4vm/src/arch/arm/vgic/gicv2.h
+++ b/libsel4vm/src/arch/arm/vgic/gicv2.h
@@ -24,6 +24,8 @@
 #define GIC_PADDR   0xc4300000
 #elif defined(CONFIG_PLAT_ZYNQMP)
 #define GIC_PADDR   0xf9000000
+#elif defined(CONFIG_PLAT_STM32MP2)
+#define GIC_PADDR   0x4ac00000
 #else
 #error "Unsupported platform for GIC"
 #endif
@@ -38,6 +40,11 @@
 #define GIC_CPU_PADDR        (GIC_PADDR + 0x20000)
 #define GIC_VCPU_CNTR_PADDR  (GIC_PADDR + 0x40000)
 #define GIC_VCPU_PADDR       (GIC_PADDR + 0x60000)
+#elif defined(CONFIG_PLAT_STM32MP2)
+#define GIC_DIST_PADDR       (GIC_PADDR + 0x10000)
+#define GIC_CPU_PADDR        (GIC_PADDR + 0x20000)
+#define GIC_VCPU_CNTR_PADDR  (GIC_PADDR + 0x40000)
+#define GIC_VCPU_PADDR       (GIC_PADDR + 0x60000)
 #else
 #define GIC_DIST_PADDR       (GIC_PADDR + 0x1000)
 #define GIC_CPU_PADDR        (GIC_PADDR + 0x2000)
diff --git a/libsel4vmmplatsupport/plat_include/stm32mp2/sel4vmmplatsupport/plat/guest_vcpu_util.h b/libsel4vmmplatsupport/plat_include/stm32mp2/sel4vmmplatsupport/plat/guest_vcpu_util.h
new file mode 100644
index 000000000..31cc53f9c
--- /dev/null
+++ b/libsel4vmmplatsupport/plat_include/stm32mp2/sel4vmmplatsupport/plat/guest_vcpu_util.h
@@ -0,0 +1,7 @@
+/*
+ * Copyright 2026, STMicroelectronics
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#define PLAT_CPU_COMPAT "arm,cortex-a35"
diff --git a/libsel4vmmplatsupport/plat_include/stm32mp2/sel4vmmplatsupport/plat/vpci.h b/libsel4vmmplatsupport/plat_include/stm32mp2/sel4vmmplatsupport/plat/vpci.h
new file mode 100644
index 000000000..c7e7bd4ec
--- /dev/null
+++ b/libsel4vmmplatsupport/plat_include/stm32mp2/sel4vmmplatsupport/plat/vpci.h
@@ -0,0 +1,26 @@
+/*
+ * Copyright 2026, STMicroelectronics
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#pragma once
+
+/* PCI host bridge memory regions are defined in the pci dts node
+ * supplied to the Linux guest. These values are also reflected here.
+ */
+
+/* PCI host bridge configration space */
+#define PCI_CFG_REGION_ADDR 0x3E000000
+/* PCI host bridge IO space */
+#define PCI_IO_REGION_ADDR 0x3D000000
+/* Size of PCI configuration space */
+#define PCI_CFG_REGION_SIZE 0x1000000
+/* Size of PCI IO space  */
+#define PCI_IO_REGION_SIZE 0x10000
+/* PCI memory space */
+#define PCI_MEM_REGION_ADDR 0x3F000000ull
+/* PCI memory space size */
+#define PCI_MEM_REGION_SIZE 0x1000000
+
+/* FDT IRQ controller address cells definition */
+#define GIC_ADDRESS_CELLS 0x1