diff --git a/tool/microkit/src/elf.rs b/tool/microkit/src/elf.rs
index 2d05e235e..4201834b0 100644
--- a/tool/microkit/src/elf.rs
+++ b/tool/microkit/src/elf.rs
@@ -6,6 +6,7 @@
 
 use crate::sel4::PageSize;
 use crate::util::{bytes_to_struct, round_down, struct_to_bytes};
+use std::borrow::Cow;
 use std::collections::HashMap;
 use std::fs::{self, metadata, File};
 use std::io::Write;
@@ -13,6 +14,7 @@ use std::path::{Path, PathBuf};
 use std::slice::from_raw_parts;
 
 #[repr(C, packed)]
+#[derive(Copy, Clone)]
 struct ElfHeader32 {
     ident_magic: u32,
     ident_class: u8,
@@ -48,6 +50,7 @@ struct ElfSymbol64 {
 }
 
 #[repr(C, packed)]
+#[derive(Copy, Clone)]
 struct ElfSectionHeader64 {
     name: u32,
     type_: u32,
@@ -62,6 +65,7 @@ struct ElfSectionHeader64 {
 }
 
 #[repr(C, packed)]
+#[derive(Copy, Clone)]
 struct ElfProgramHeader64 {
     type_: u32,
     flags: u32,
@@ -74,6 +78,7 @@ struct ElfProgramHeader64 {
 }
 
 #[repr(C, packed)]
+#[derive(Copy, Clone)]
 struct ElfHeader64 {
     ident_magic: u32,
     ident_class: u8,
@@ -186,6 +191,41 @@ pub struct ElfFile {
 
 impl ElfFile {
     pub fn from_path(path: &Path) -> Result<ElfFile, String> {
+        Self::from_split_paths(path, None)
+    }
+
+    pub fn from_split_paths(
+        path: &Path,
+        path_for_symbols: Option<&Path>,
+    ) -> Result<ElfFile, String> {
+        let reader = ElfFileReader::from_path(path)?;
+        let reader_for_symbols = match path_for_symbols {
+            Some(path_for_symbols) => Cow::Owned(ElfFileReader::from_path(path_for_symbols)?),
+            None => Cow::Borrowed(&reader),
+        };
+        let segments = reader.segments()?;
+        let symbols = reader_for_symbols.symbols()?;
+        Ok(ElfFile {
+            path: path.to_owned(),
+            word_size: reader.word_size,
+            entry: reader.hdr.entry,
+            machine: reader.hdr.machine,
+            segments,
+            symbols,
+        })
+    }
+}
+
+#[derive(Clone)]
+struct ElfFileReader<'a> {
+    path: &'a Path,
+    bytes: Vec<u8>,
+    word_size: usize,
+    hdr: ElfHeader64,
+}
+
+impl<'a> ElfFileReader<'a> {
+    fn from_path(path: &'a Path) -> Result<Self, String> {
         let bytes = match fs::read(path) {
             Ok(bytes) => bytes,
             Err(err) => return Err(format!("Failed to read ELF '{}': {}", path.display(), err)),
@@ -218,9 +258,17 @@ impl ElfFile {
             }
         };
 
+        if word_size != 64 {
+            return Err(format!(
+                "ELF '{}': unsupported word size: '{}'",
+                path.display(),
+                word_size
+            ));
+        }
+
         // Now need to read the header into a struct
         let hdr_bytes = &bytes[..hdr_size];
-        let hdr = unsafe { bytes_to_struct::<ElfHeader64>(hdr_bytes) };
+        let hdr = *unsafe { bytes_to_struct::<ElfHeader64>(hdr_bytes) };
 
         // We have checked this above but we should check again once we actually cast it to
         // a struct.
@@ -234,18 +282,30 @@ impl ElfFile {
             ));
         }
 
-        let entry = hdr.entry;
+        Ok(Self {
+            path,
+            bytes,
+            word_size,
+            hdr,
+        })
+    }
+
+    fn segments(&self) -> Result<Vec<ElfSegment>, String> {
+        let hdr = &self.hdr;
 
         // Read all the segments
         if hdr.phnum == 0 {
-            return Err(format!("ELF '{}': has no program headers", path.display()));
+            return Err(format!(
+                "ELF '{}': has no program headers",
+                self.path.display()
+            ));
         }
 
         let mut segments = Vec::with_capacity(hdr.phnum as usize);
         for i in 0..hdr.phnum {
             let phent_start = hdr.phoff + (i * hdr.phentsize) as u64;
             let phent_end = phent_start + (hdr.phentsize as u64);
-            let phent_bytes = &bytes[phent_start as usize..phent_end as usize];
+            let phent_bytes = &self.bytes[phent_start as usize..phent_end as usize];
 
             let phent = unsafe { bytes_to_struct::<ElfProgramHeader64>(phent_bytes) };
 
@@ -258,7 +318,7 @@ impl ElfFile {
 
             let mut segment_data_bytes = vec![0; phent.memsz as usize];
             segment_data_bytes[..phent.filesz as usize]
-                .copy_from_slice(&bytes[segment_start..segment_end]);
+                .copy_from_slice(&self.bytes[segment_start..segment_end]);
 
             let segment_data = ElfSegmentData::RealData(segment_data_bytes);
 
@@ -274,6 +334,12 @@ impl ElfFile {
             segments.push(segment)
         }
 
+        Ok(segments)
+    }
+
+    fn symbols(&self) -> Result<HashMap<String, (ElfSymbol64, bool)>, String> {
+        let hdr = &self.hdr;
+
         // Read all the section headers
         let mut shents = Vec::with_capacity(hdr.shnum as usize);
         let mut symtab_shent: Option<&ElfSectionHeader64> = None;
@@ -281,7 +347,7 @@ impl ElfFile {
         for i in 0..hdr.shnum {
             let shent_start = hdr.shoff + (i as u64 * hdr.shentsize as u64);
             let shent_end = shent_start + hdr.shentsize as u64;
-            let shent_bytes = &bytes[shent_start as usize..shent_end as usize];
+            let shent_bytes = &self.bytes[shent_start as usize..shent_end as usize];
 
             let shent = unsafe { bytes_to_struct::<ElfSectionHeader64>(shent_bytes) };
             match shent.type_ {
@@ -295,7 +361,7 @@ impl ElfFile {
         if shstrtab_shent.is_none() {
             return Err(format!(
                 "ELF '{}': unable to find string table section",
-                path.display()
+                self.path.display()
             ));
         }
 
@@ -303,19 +369,19 @@ impl ElfFile {
         if symtab_shent.is_none() {
             return Err(format!(
                 "ELF '{}': unable to find symbol table section",
-                path.display()
+                self.path.display()
             ));
         }
 
         // Reading the symbol table
         let symtab_start = symtab_shent.unwrap().offset as usize;
         let symtab_end = symtab_start + symtab_shent.unwrap().size as usize;
-        let symtab = &bytes[symtab_start..symtab_end];
+        let symtab = &self.bytes[symtab_start..symtab_end];
 
         let symtab_str_shent = shents[symtab_shent.unwrap().link as usize];
         let symtab_str_start = symtab_str_shent.offset as usize;
         let symtab_str_end = symtab_str_start + symtab_str_shent.size as usize;
-        let symtab_str = &bytes[symtab_str_start..symtab_str_end];
+        let symtab_str = &self.bytes[symtab_str_start..symtab_str_end];
 
         // Read all the symbols
         let mut symbols: HashMap<String, (ElfSymbol64, bool)> = HashMap::new();
@@ -347,16 +413,11 @@ impl ElfFile {
             offset += symbol_size;
         }
 
-        Ok(ElfFile {
-            path: path.to_owned(),
-            word_size,
-            entry,
-            machine: hdr.machine,
-            segments,
-            symbols,
-        })
+        Ok(symbols)
     }
+}
 
+impl ElfFile {
     pub fn find_symbol(&self, variable_name: &str) -> Result<(u64, u64), String> {
         if let Some((sym, duplicate)) = self.symbols.get(variable_name) {
             if *duplicate {
@@ -393,7 +454,9 @@ impl ElfFile {
 
         None
     }
+}
 
+impl<'a> ElfFileReader<'a> {
     fn get_string(strtab: &[u8], idx: usize) -> Result<&str, String> {
         match strtab[idx..].iter().position(|&b| b == 0) {
             Some(null_byte_pos) => {
@@ -410,7 +473,9 @@ impl ElfFile {
             )),
         }
     }
+}
 
+impl ElfFile {
     pub fn lowest_vaddr(&self) -> u64 {
         // This unwrap is safe as we have ensured that there will always be at least 1 segment when parsing the ELF.
         let existing_vaddrs: Vec<u64> = self
diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs
index 40cf84d27..a2110f108 100644
--- a/tool/microkit/src/main.rs
+++ b/tool/microkit/src/main.rs
@@ -539,7 +539,22 @@ fn main() -> Result<(), String> {
     for pd in &system.protection_domains {
         match get_full_path(&pd.program_image, &search_paths) {
             Some(path) => {
-                system_elfs.push(ElfFile::from_path(&path)?);
+                let path_for_symbols = pd
+                    .program_image_for_symbols
+                    .as_ref()
+                    .map(|path_suffix| {
+                        get_full_path(path_suffix, &search_paths).ok_or_else(|| {
+                            format!(
+                                "unable to find program image for symbols: '{}'",
+                                path_suffix.display()
+                            )
+                        })
+                    })
+                    .transpose()?;
+                system_elfs.push(ElfFile::from_split_paths(
+                    &path,
+                    path_for_symbols.as_deref(),
+                )?);
             }
             None => {
                 return Err(format!(
diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index d0f770449..31bf18cdb 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -246,6 +246,7 @@ pub struct ProtectionDomain {
     pub stack_size: u64,
     pub smc: bool,
     pub program_image: PathBuf,
+    pub program_image_for_symbols: Option<PathBuf>,
     pub maps: Vec<SysMap>,
     pub irqs: Vec<SysIrq>,
     pub ioports: Vec<IOPort>,
@@ -560,6 +561,7 @@ impl ProtectionDomain {
         let mut child_pds = Vec::new();
 
         let mut program_image = None;
+        let mut program_image_for_symbols = None;
         let mut virtual_machine = None;
 
         // Default to minimum priority
@@ -584,7 +586,7 @@ impl ProtectionDomain {
 
             match child.tag_name().name() {
                 "program_image" => {
-                    check_attributes(xml_sdf, &child, &["path"])?;
+                    check_attributes(xml_sdf, &child, &["path", "path_for_symbols"])?;
                     if program_image.is_some() {
                         return Err(value_error(
                             xml_sdf,
@@ -595,6 +597,9 @@ impl ProtectionDomain {
 
                     let program_image_path = checked_lookup(xml_sdf, &child, "path")?;
                     program_image = Some(Path::new(program_image_path).to_path_buf());
+
+                    program_image_for_symbols =
+                        child.attribute("path_for_symbols").map(PathBuf::from);
                 }
                 "map" => {
                     let map_max_vaddr = config.pd_map_max_vaddr(stack_size);
@@ -1043,6 +1048,7 @@ impl ProtectionDomain {
             stack_size,
             smc,
             program_image: program_image.unwrap(),
+            program_image_for_symbols,
             maps,
             irqs,
             ioports,