From e8f5f1b8ca985632f06e3dd63ed410c950dee329 Mon Sep 17 00:00:00 2001 From: james Date: Tue, 20 Oct 2026 16:33:21 +0100 Subject: [PATCH] feat(report): serialise walks and mapping changes with replay fixtures --- examples/after | Bin 0 -> 20717 bytes examples/before | Bin 0 -> 20717 bytes lib/demo.ml | 29 +++++++++++++++++ lib/json.ml | 36 ++++++++++++++++++++ lib/report.ml | 85 ++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 150 insertions(+) create mode 100644 examples/after create mode 100644 examples/before create mode 100644 lib/demo.ml create mode 100644 lib/json.ml create mode 100644 lib/report.ml diff --git a/examples/after b/examples/after new file mode 100644 index 0000000000000000000000000000000000000000..fa1866fd08c37b9cb21d80944cb6174bde86dee4 GIT binary patch literal 20717 zcmeI%Jxar17y#hJAO%6t)#<}s@B%_XoLle&S|bLGl_mw0o#k#XC{6j;okdM;yhornL-v%Me!0-DR@1s{e@lRj+uw zD{s;=8-?rap`1?AgQ}V3`Lw*ayiG%Uc~KYjK8n%!K0Ufh^YM0l)8@f-+6(pBB0zuu z0RjXF5FkK+009C7IxP^|>3a2-3X1>%0t5&UAV7cs0RjXF5a_nRhWG!Zzdm|0T(4CG z2oNAZfB*pk1PBlyK!CtM6zI2mPM+IbMt}eT0t5&UAV7cs0RjXFbX4Hizy9Q9G2^VG nlNyTv0RjXF5FkK+009C72oR_QzVg?Pd3ZY+Oy=L8hwo26;LRl$ literal 0 HcmV?d00001 diff --git a/examples/before b/examples/before new file mode 100644 index 0000000000000000000000000000000000000000..79560495a5fdf67b4e15848ef359f72e6a532ffb GIT binary patch literal 20717 zcmeI%y-LGS7y!`3AQiEotBZGW6nun&2yPa90<94P#)?V7;?f6j=rcMw>*i!)Qer{e z4d+7g{REQxoh`}5$@%y+inpV79ak}_jyQ@JZL0~pO$e*zut_#n^)GR+>J{_*@-{8A zNw~?L%GqPOUp2ElpOu$acWLM@f7eC5k76=?NRO`5e7afRw0&@$4nlpl2oNAZfB*pk z1PBlyK!5;&UJHb7x Bytes.set_int64_le bytes (index * 8) entry) entries; + Bytes.to_string bytes + +let frames ~after = [ + 0x1000L, page [0, 0x2007L]; + 0x2000L, page [0, 0x3007L]; + 0x3000L, page [2, (if after then 0x4003L else 0x4001L); 4, 0x5003L]; + 0x4000L, page [0, 0x9003L]; + 0x5000L, page [0, Int64.logor 0x8000000000000000L (if after then 0xa003L else 0x9003L)] ] + +let capture ~after = Capture.make context (List.map (fun (address, bytes) -> Address.Physical.of_int64 address, Ok bytes) (frames ~after)) + +let write directory = + if not (Sys.file_exists directory) then Unix.mkdir directory 0o755; + Capture.save (Filename.concat directory "before") (capture ~after:false); + Capture.save (Filename.concat directory "after") (capture ~after:true) diff --git a/lib/json.ml b/lib/json.ml new file mode 100644 index 0000000..f9129f1 --- /dev/null +++ b/lib/json.ml @@ -0,0 +1,36 @@ +type t = Null | Bool of bool | Int of int | String of string | List of t list | Object of (string * t) list + +let string s = String s +let hex x = String (Address.hex x) +let option f = function None -> Null | Some x -> f x + +let rec output channel = function + | Null -> output_string channel "null" + | Bool b -> output_string channel (string_of_bool b) + | Int n -> output_string channel (string_of_int n) + | String s -> + output_char channel '"'; + String.iter (function + | '"' -> output_string channel "\\\"" + | '\\' -> output_string channel "\\\\" + | '\n' -> output_string channel "\\n" + | '\r' -> output_string channel "\\r" + | '\t' -> output_string channel "\\t" + | c when Char.code c < 32 || Char.code c > 126 -> + Printf.fprintf channel "\\u%04x" (Char.code c) + | c -> output_char channel c) s; + output_char channel '"' + | List values -> + output_char channel '['; + List.iteri (fun i value -> if i > 0 then output_char channel ','; output channel value) values; + output_char channel ']' + | Object fields -> + output_char channel '{'; + List.iteri (fun i (key, value) -> + if i > 0 then output_char channel ','; + output channel (String key); + output_char channel ':'; + output channel value) fields; + output_char channel '}' + +let print value = output stdout value; output_char stdout '\n' diff --git a/lib/report.ml b/lib/report.ml new file mode 100644 index 0000000..855a866 --- /dev/null +++ b/lib/report.ml @@ -0,0 +1,85 @@ +open Model +open Json + +let limitations = [ + "guest first-stage table state only; tlb and second-stage permissions are not observed"; + "ordinary explicit accesses only; implicit supervisor accesses and cross-page operations are not modelled"; + "pausing vcpus does not quiesce dma, device models, or other memory writers"; + "permissions describe architectural access, not speculative execution" ] + +let permissions p = Object ["writable", Bool p.writable; "user", Bool p.user; "executable", Bool p.executable] + +let context c = + let r = c.registers and f = c.features in + Object ["source", String c.source; "consistency", String c.consistency; "identity", String c.identity; + "domid", Int c.domid; "vcpu", Int c.vcpu; + "root", hex (Address.Physical.to_int64 (Model.root c)); "root_override", option hex c.root_override; + "features", Object ["phys_bits", Int f.phys_bits; "nx", Bool f.nx; "gb_pages", Bool f.gb_pages]; + "registers", Object ["cr0", hex r.cr0; "cr2", hex r.cr2; "cr3", hex r.cr3; "cr4", hex r.cr4; + "efer", hex r.efer; "rflags", hex r.rflags; "rip", hex r.rip]] + +let step (s : step) = Object ["level", Int s.level; "table", hex (Address.Physical.to_int64 s.table); + "index", Int s.index; "entry_address", hex Int64.(add (Address.Physical.to_int64 s.table) (of_int (s.index * 8))); + "raw", hex s.raw; "effective", permissions s.effective] + +let mapping (m : mapping) = Object [ + "virtual", hex (Address.Virtual.to_int64 m.virtual_address); + "physical", hex (Address.Physical.to_int64 m.physical_address); + "page_size", hex m.size; "permissions", permissions m.permissions; "leaf", hex m.leaf; + "trace", List (List.map step m.trace)] + +let fault f = Object ["vector", Int f.vector; "error_code", Int f.error_code; + "reason", String f.reason; "level", option (fun n -> Int n) f.level] + +let outcome = function + | Mapped m -> Object ["status", String "mapped"; "mapping", mapping m] + | Fault f -> Object ["status", String "fault"; "fault", fault f] + | Incomplete reason -> Object ["status", String "incomplete"; "reason", String reason] + +let state = function + | Paging.Present m -> Object ["status", String "mapped"; "mapping", mapping m] + | Paging.Unknown reason -> Object ["status", String "incomplete"; "reason", String reason] + | Paging.Broken reason -> Object ["status", String "invalid"; "reason", String reason] + +let region (r : Paging.region) = Object ["start", hex r.start; "length", hex r.length; "state", state r.state] + +let change (c : Analysis.change) = Object ["start", hex c.start; "length", hex c.length; + "kinds", List (List.map string c.kinds); "before", option state c.before; "after", option state c.after] + +let alias (a : Analysis.alias) = Object ["physical", hex a.physical; "length", hex a.length; + "writable", mapping a.writable; "executable", mapping a.executable] + +let envelope command c complete fields = Object ( + ["schema", String "scope.report.v1"; "command", String command; "context", context c; + "complete", Bool complete; "limitations", List (List.map string limitations)] @ fields) + +let rights p = Printf.sprintf "r%c%c/%c" (if p.writable then 'w' else '-') + (if p.executable then 'x' else '-') (if p.user then 'u' else 's') + +let print_context c = + Printf.printf "source=%S identity=%S domid=%d vcpu=%d cr3=%s root=%s phys_bits=%d nx=%b gb_pages=%b\n" + c.source c.identity c.domid c.vcpu (Address.hex c.registers.cr3) + (Address.hex (Address.Physical.to_int64 (Model.root c))) c.features.phys_bits c.features.nx c.features.gb_pages; + Printf.printf "consistency=%S\n" c.consistency; + Printf.printf "scope=guest-table-state tlb=unobserved second-stage=unobserved\n" + +let print_step (s : step) = + Printf.printf "l%d table=%s index=%03x raw=%s effective=%s\n" s.level + (Address.hex (Address.Physical.to_int64 s.table)) s.index (Address.hex s.raw) (rights s.effective) + +let print_mapping m = Printf.printf "%s -> %s size=%s %s\n" + (Address.hex (Address.Virtual.to_int64 m.virtual_address)) + (Address.hex (Address.Physical.to_int64 m.physical_address)) (Address.hex m.size) (rights m.permissions) + +let print_result result = + List.iter print_step result.trace; + match result.outcome with + | Mapped m -> print_mapping m + | Fault f -> Printf.printf "fault vector=%d error=0x%x level=%s reason=%s\n" f.vector f.error_code + (match f.level with None -> "-" | Some n -> string_of_int n) f.reason + | Incomplete reason -> Printf.printf "incomplete reason=%s\n" reason + +let print_region (r : Paging.region) = match r.state with + | Paging.Present m -> print_mapping m + | Paging.Unknown reason -> Printf.printf "%s length=%s incomplete=%s\n" (Address.hex r.start) (Address.hex r.length) reason + | Paging.Broken reason -> Printf.printf "%s length=%s invalid=%s\n" (Address.hex r.start) (Address.hex r.length) reason