diff --git a/docs/manual.md b/docs/manual.md index c45eaae37..a7612c04d 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -482,6 +482,12 @@ It is important to note that this is largely just for debugging purposes and the highly tied to a specific version and configuration of the kernel. When using this option the kernel should be the same version and compiled with the same configuration options. +If the `--viper-output PREFIX` argument is set, then for each protection domain `name` specified in +the system description file, a file `PREFIX/name.vpr` will be output, containing a description of the +capability table of the given PD in the Viper verification language. These output files can be used +for verification purposes, but the exact format may change in future versions of the tool. + + ## Image format ### ARM diff --git a/example/hello/Makefile b/example/hello/Makefile index 0773536c1..e33ce05eb 100644 --- a/example/hello/Makefile +++ b/example/hello/Makefile @@ -67,4 +67,4 @@ $(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS)) $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hello.system - $(MICROKIT_TOOL) hello.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) + $(MICROKIT_TOOL) hello.system --search-path $(BUILD_DIR) --viper-output ${BUILD_DIR}/viper --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) diff --git a/tool/microkit/src/argparse.rs b/tool/microkit/src/argparse.rs index 8860ff30d..5a99fddd3 100644 --- a/tool/microkit/src/argparse.rs +++ b/tool/microkit/src/argparse.rs @@ -29,6 +29,7 @@ pub fn print_help(sdk: &Sdk) { ); println!(" --config CONFIG"); println!(" --capdl-json CAPDL_SPEC (JSON format)"); + println!(" --viper-output DIRECTORY_PATH"); println!(" --search-path [SEARCH_PATH ...]"); } @@ -69,6 +70,7 @@ pub struct Args { pub config: String, pub report_path: PathBuf, pub capdl_json_path: Option, + pub viper_output_dir: Option, pub output_path: PathBuf, pub search_paths: Vec, pub requested_image_type: RequestedImageType, @@ -167,6 +169,7 @@ impl Args { let mut output_path = PathBuf::from("loader.img"); let mut report_path = PathBuf::from("report.txt"); let mut capdl_json_path = None; + let mut viper_output_dir = None; let mut search_paths = Vec::new(); let mut sdf_path = None; @@ -205,6 +208,9 @@ impl Args { let params = consume_parameters(&mut args); search_paths.extend(params.into_iter().map(PathBuf::from)); } + "--viper-output" => { + viper_output_dir = Some(consume_parameter(&mut args, "--viper-output")?.into()); + } "--image-type" => { let value = consume_parameter(&mut args, "--image-type")?; match RequestedImageType::parse(value.as_str()) { @@ -262,6 +268,7 @@ impl Args { config, report_path, capdl_json_path, + viper_output_dir, output_path, search_paths, requested_image_type, diff --git a/tool/microkit/src/lib.rs b/tool/microkit/src/lib.rs index c7956986f..31c19178c 100644 --- a/tool/microkit/src/lib.rs +++ b/tool/microkit/src/lib.rs @@ -23,6 +23,7 @@ pub mod sel4; pub mod symbols; pub mod uimage; pub mod util; +pub mod viper; // Note that these values are used in the monitor so should also be changed there // if any of these were to change. diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index a9e29b0bb..0129c6810 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -29,6 +29,7 @@ use microkit_tool::util::{ get_full_path, human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down, round_up, }; +use microkit_tool::viper; use microkit_tool::{DisjointMemoryRegion, MemoryRegion}; use std::collections::HashMap; use std::fs::{self, metadata}; @@ -122,7 +123,7 @@ fn main() -> Result<(), String> { std::process::exit(1); } }; - args.search_paths.push(std::env::current_dir().unwrap()); + args.search_paths.push(sdk.cwd.clone()); // NB safe unwrap: argparse would already have bailed if the config did not // exist. @@ -694,6 +695,33 @@ fn main() -> Result<(), String> { fs::write(capdl_json, &serialised).unwrap(); }; + if let Some(viper_output_dir) = args.viper_output_dir { + // NB returns Ok if the directory already exists, that's fine + fs::create_dir_all(&viper_output_dir).unwrap_or_else(|source| { + eprintln!( + "ERROR: cannot write Viper output directory {}: {source}", + &viper_output_dir.display() + ); + std::process::exit(1); + }); + for view in viper::get_combined_views(&spec_container, &system) { + let mut output = format!( + "// exported invariants for PD {} in {}\n", + view.pd_name, + &args.sdf_path.display(), + ); + view.export(&mut output); + let path = viper_output_dir.join(format!("{}.vpr", view.pd_name)); + fs::write(&path, output).unwrap_or_else(|source| { + eprintln!( + "ERROR: cannot write Viper output file {}: {source}", + &path.display() + ); + std::process::exit(1); + }); + } + } + write_report(&spec_container, &kernel_config, &args.report_path); system_built = true; break; diff --git a/tool/microkit/src/viper.rs b/tool/microkit/src/viper.rs new file mode 100644 index 000000000..bc220f4da --- /dev/null +++ b/tool/microkit/src/viper.rs @@ -0,0 +1,360 @@ +// +// Copyright 2026, UNSW +// +// SPDX-License-Identifier: BSD-2-Clause + +use sel4_capdl_initializer_types::{Cap, Object}; + +use crate::capdl::CapDLSpecContainer; +use crate::sdf::SysMapPerms; +use crate::sdf::SystemDescription; + +fn export_define_set(name: &'static str, vector: &[u64], target: &mut String) { + if vector.is_empty() { + target.push_str(&format!("define {name}(x) (false)\n")); + target.push_str(&format!("define f_{name}(heap,gv,x) ({name}(x))\n")); + return; + } + + let items = vector + .iter() + .map(u64::to_string) + .collect::>() + .join(","); + + target.push_str(&format!("define {name}(x) (x in Set({items}))\n")); + target.push_str(&format!("define f_{name}(heap,gv,x) ({name}(x))\n")); +} + +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct CapView { + pub occupied_slots: Vec, + + pub endpoint_caps: Vec, + pub notification_caps: Vec, + pub reply_caps: Vec, + pub page_table_caps: Vec, + pub irq_handler_caps: Vec, + pub tcb_caps: Vec, + pub vcpu_caps: Vec, + pub ioport_caps: Vec, + pub arm_smc_caps: Vec, +} + +impl CapView { + pub fn export(&self, target: &mut String) { + export_define_set("pansel4_has_cap", &self.occupied_slots, target); + export_define_set("pansel4_has_endpoint_cap", &self.endpoint_caps, target); + export_define_set( + "pansel4_has_notification_cap", + &self.notification_caps, + target, + ); + export_define_set("pansel4_has_reply_cap", &self.reply_caps, target); + export_define_set("pansel4_has_page_table_cap", &self.page_table_caps, target); + export_define_set( + "pansel4_has_irq_handler_cap", + &self.irq_handler_caps, + target, + ); + export_define_set("pansel4_has_tcb_cap", &self.tcb_caps, target); + export_define_set("pansel4_has_vcpu_cap", &self.vcpu_caps, target); + export_define_set("pansel4_has_ioport_cap", &self.ioport_caps, target); + export_define_set("pansel4_has_arm_smc_cap", &self.arm_smc_caps, target); + } + + fn sort_and_dedup(&mut self) { + fn go(v: &mut Vec) { + v.sort_unstable(); + v.dedup(); + } + go(&mut self.occupied_slots); + go(&mut self.endpoint_caps); + go(&mut self.notification_caps); + go(&mut self.reply_caps); + go(&mut self.page_table_caps); + go(&mut self.irq_handler_caps); + go(&mut self.tcb_caps); + go(&mut self.vcpu_caps); + go(&mut self.ioport_caps); + go(&mut self.arm_smc_caps); + } +} + +pub fn get_cap_view( + capdl_spec: &CapDLSpecContainer, + system: &SystemDescription, + current_pd: usize, +) -> Option { + let pd = system.protection_domains.get(current_pd)?; + let cnode_name = format!("cnode_{}", pd.name); + + let named_obj = capdl_spec + .spec + .objects + .iter() + .find(|obj| obj.name.as_deref() == Some(cnode_name.as_str()))?; + + let Object::CNode(cnode) = &named_obj.object else { + return None; + }; + + let mut view = CapView::default(); + + for cte in &cnode.slots { + let slot = u64::from(cte.slot.0); + view.occupied_slots.push(slot); + + match &cte.cap { + Cap::Endpoint(_) => { + view.endpoint_caps.push(slot); + } + Cap::Notification(_) => { + view.notification_caps.push(slot); + } + Cap::Reply(_) => { + view.reply_caps.push(slot); + } + Cap::PageTable(_) => { + view.page_table_caps.push(slot); + } + Cap::ArmIrqHandler(_) + | Cap::IrqHandler(_) + | Cap::IrqIOApicHandler(_) + | Cap::IrqMsiHandler(_) + | Cap::RiscvIrqHandler(_) => { + view.irq_handler_caps.push(slot); + } + Cap::Tcb(_) => { + view.tcb_caps.push(slot); + } + Cap::VCpu(_) => { + view.vcpu_caps.push(slot); + } + Cap::IOPorts(_) => { + view.ioport_caps.push(slot); + } + Cap::ArmSmc(_) => { + view.arm_smc_caps.push(slot); + } + + Cap::AsidPool(_) + | Cap::CNode(_) + | Cap::DomainSet(_) + | Cap::Frame(_) + | Cap::SchedContext(_) + | Cap::Untyped(_) => { + /* ^ The caps above can occupy CSpace slots, but Viper + * verification currently has no use for them, so we + * intentionally do not emit anything here. + */ + } + } + } + + view.sort_and_dedup(); + Some(view) +} + +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct SdfView { + // the world, from the perspective of a single PD + pub channel_ends: Vec, + pub protected_sources: Vec, + pub ppcall_targets: Vec, + pub notified_sources: Vec, + pub notify_targets: Vec, + pub irqs: Vec, + pub children: Vec, +} + +impl SdfView { + pub fn export(&self, target: &mut String) { + export_define_set("mk_is_protected_source", &self.protected_sources, target); + + export_define_set("mk_is_ppcall_target", &self.ppcall_targets, target); + + export_define_set("mk_is_notified_source", &self.notified_sources, target); + + export_define_set("mk_is_notify_target", &self.notify_targets, target); + + export_define_set("mk_is_irq_channel", &self.irqs, target); + + export_define_set("mk_is_child", &self.children, target); + } +} + +pub fn get_sdf_view(system: &SystemDescription, current_pd: usize) -> Option { + let current = system.protection_domains.get(current_pd)?; + + let mut view = SdfView { + ..Default::default() + }; + + for irq in ¤t.irqs { + view.notified_sources.push(irq.id); + view.irqs.push(irq.id); + } + + for ch in &system.channels { + let (local, remote) = if ch.end_a.pd == current_pd { + (&ch.end_a, &ch.end_b) + } else if ch.end_b.pd == current_pd { + (&ch.end_b, &ch.end_a) + } else { + continue; + }; + + view.channel_ends.push(local.id); + + let local_prio = current.priority; + let remote_prio = system.protection_domains[remote.pd].priority; + + if local.pp && local_prio < remote_prio { + view.ppcall_targets.push(local.id); + } + + if remote.pp && remote_prio < local_prio { + view.protected_sources.push(local.id); + } + + if remote.notify { + view.notified_sources.push(local.id); + } + + if local.notify { + view.notify_targets.push(local.id); + } + } + + for pd in &system.protection_domains { + if pd.parent == Some(current_pd) { + if let Some(id) = pd.id { + view.children.push(id) + } + } + } + + Some(view) +} + +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct Mem { + pub name: String, + pub start: u64, + pub end: u64, +} + +impl Mem { + pub fn export(&self, target: &mut String) { + let name: &String = &self.name; + let start: u64 = self.start; + let end: u64 = self.end; + target.push_str(&format!( + "define mem_{name}_contains(x) ({start} <= x && x < {end})\n" + )); + } +} + +fn export_define_mem_set(perm: &'static str, vector: &[Mem], target: &mut String) { + if vector.is_empty() { + target.push_str(&format!("define mem_{perm}(x) (false)\n")); + target.push_str(&format!("define f_mem_{perm}(heap,gv,x) (mem_{perm}(x))\n")); + return; + } + let items = vector + .iter() + .map(|x| format!("mem_{}_contains(x)", x.name)) + .collect::>() + .join(" || "); + + target.push_str(&format!("define mem_{perm}(x) ({items})\n")); + target.push_str(&format!("define f_mem_{perm}(heap,gv,x) (mem_{perm}(x))\n")); +} + +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct MemView { + pub read: Vec, + pub readwrite: Vec, +} + +impl MemView { + pub fn export(&self, target: &mut String) { + for mr in &self.read { + mr.export(target); + } + + export_define_mem_set("readable", &self.read, target); + export_define_mem_set("writeable", &self.readwrite, target); + } +} + +pub fn get_mem_view(system: &SystemDescription, current_pd: usize) -> Option { + let current = system.protection_domains.get(current_pd)?; + + let mut view = MemView { + ..Default::default() + }; + + for mr in &system.memory_regions { + let mmaps_into_current_pd = current.maps.iter().filter(|map| map.mr == mr.name); + + for mmap in mmaps_into_current_pd { + let start = mmap.vaddr; + let end = start + mr.size; + if end < start { + // we catch bonkers mappings elsewhere, ignore them here! + continue; + } + let name = mr.name.clone(); + let mem: Mem = Mem { name, start, end }; + view.read.push(mem.clone()); + + let writeable = (mmap.perms & SysMapPerms::Write as u8) != 0; + if writeable { + view.readwrite.push(mem); + } + } + } + + Some(view) +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct CombinedView { + pub pd_name: String, + pub sdf: SdfView, + pub cap: CapView, + pub mem: MemView, +} + +impl CombinedView { + pub fn export(&self, target: &mut String) { + self.sdf.export(target); + self.cap.export(target); + self.mem.export(target); + } +} + +pub fn get_combined_views( + capdl_spec: &CapDLSpecContainer, + system: &SystemDescription, +) -> Vec { + system + .protection_domains + .iter() + .enumerate() + .filter_map(|(current_pd, pd)| { + let sdf = get_sdf_view(system, current_pd)?; + let cap = get_cap_view(capdl_spec, system, current_pd)?; + let mem = get_mem_view(system, current_pd)?; + + Some(CombinedView { + pd_name: pd.name.clone(), + sdf, + cap, + mem, + }) + }) + .collect() +}