diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index 9cbdd61..ca7dade 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -324,19 +324,22 @@ static int make_memory_node(const struct domain *d,
     return res;
 }
 
-static int make_hypervisor_node(struct domain *d,
-                                void *fdt, const struct dt_device_node *parent)
+static int make_hypervisor_node(struct domain *d, struct kernel_info *kinfo,
+                                const struct dt_device_node *parent)
 {
     const char compat[] =
         "xen,xen-"__stringify(XEN_VERSION)"."__stringify(XEN_SUBVERSION)"\0"
         "xen,xen";
     __be32 reg[4];
     gic_interrupt_t intr;
-    __be32 *cells;
+    __be32 *cells, *_cells;
     int res;
     int addrcells = dt_n_addr_cells(parent);
     int sizecells = dt_n_size_cells(parent);
     paddr_t gnttab_start, gnttab_size;
+    const struct dt_device_node *dev;
+    struct hvm_iommu *hd = domain_hvm_iommu(d);
+    void *fdt = kinfo->fdt;
 
     DPRINT("Create hypervisor node\n");
 
@@ -384,6 +387,39 @@ static int make_hypervisor_node(struct domain *d,
     if ( res )
         return res;
 
+    if ( kinfo->num_dev_protected )
+    {
+        /* Don't need to take dtdevs_lock here */
+        cells = xmalloc_array(__be32, kinfo->num_dev_protected *
+                              dt_size_to_cells(sizeof(dt_phandle)));
+        if ( !cells )
+            return -FDT_ERR_XEN(ENOMEM);
+
+        _cells = cells;
+
+        DPRINT("  List of protected devices\n");
+        list_for_each_entry( dev, &hd->dt_devices, next_assigned )
+        {
+            DPRINT("    - %s\n", dt_node_full_name(dev));
+            if ( !dev->phandle )
+            {
+                printk(XENLOG_ERR "Unable to handle protected device (%s)"
+                       "with no phandle", dt_node_full_name(dev));
+                xfree(cells);
+                return -FDT_ERR_XEN(EINVAL);
+            }
+            dt_set_cell(&_cells, dt_size_to_cells(sizeof(dt_phandle)),
+                        dev->phandle);
+        }
+
+        res = fdt_property(fdt, "protected-devices", cells,
+                           sizeof (dt_phandle) * kinfo->num_dev_protected);
+
+        xfree(cells);
+        if ( res )
+            return res;
+    }
+
     res = fdt_end_node(fdt);
 
     return res;
@@ -670,7 +706,8 @@ static int make_timer_node(const struct domain *d, void *fdt,
 }
 
 /* Map the device in the domain */
-static int map_device(struct domain *d, struct dt_device_node *dev)
+static int map_device(struct domain *d, struct kernel_info *kinfo,
+                      struct dt_device_node *dev)
 {
     unsigned int nirq;
     unsigned int naddr;
@@ -695,6 +732,7 @@ static int map_device(struct domain *d, struct dt_device_node *dev)
                    dt_node_full_name(dev));
             return res;
         }
+        kinfo->num_dev_protected++;
     }
 
     /* Map IRQs */
@@ -844,7 +882,7 @@ static int handle_node(struct domain *d, struct kernel_info *kinfo,
     if ( !dt_device_type_is_equal(node, "memory") &&
          dt_device_is_available(node) )
     {
-        res = map_device(d, node);
+        res = map_device(d, kinfo, node);
 
         if ( res )
             return res;
@@ -875,7 +913,7 @@ static int handle_node(struct domain *d, struct kernel_info *kinfo,
 
     if ( node == dt_host )
     {
-        res = make_hypervisor_node(d, kinfo->fdt, node);
+        res = make_hypervisor_node(d, kinfo, node);
         if ( res )
             return res;
 
@@ -1028,6 +1066,7 @@ int construct_dom0(struct domain *d)
 
     d->max_pages = ~0U;
 
+    kinfo.num_dev_protected = 0;
     kinfo.unassigned_mem = dom0_mem;
 
     allocate_memory(d, &kinfo);
diff --git a/xen/arch/arm/kernel.h b/xen/arch/arm/kernel.h
index b48c2c9..3af5c50 100644
--- a/xen/arch/arm/kernel.h
+++ b/xen/arch/arm/kernel.h
@@ -18,6 +18,9 @@ struct kernel_info {
     paddr_t unassigned_mem; /* RAM not (yet) assigned to a bank */
     struct dt_mem_info mem;
 
+    /* Number of devices protected by an IOMMU */
+    unsigned int num_dev_protected;
+
     paddr_t dtb_paddr;
     paddr_t entry;
 
