diff --git a/examples/after b/examples/after new file mode 100644 index 0000000..fa1866f Binary files /dev/null and b/examples/after differ diff --git a/examples/before b/examples/before new file mode 100644 index 0000000..7956049 Binary files /dev/null and b/examples/before differ diff --git a/lib/demo.ml b/lib/demo.ml new file mode 100644 index 0000000..9a5f4a2 --- /dev/null +++ b/lib/demo.ml @@ -0,0 +1,29 @@ +open Model + +let context = { + registers = { cr0 = 0x80010001L; cr2 = 0L; cr3 = 0x1000L; cr4 = 0x20L; + efer = 0xd00L; rflags = 2L; rip = 0L }; + features = { phys_bits = 48; nx = true; gb_pages = true }; + root_override = None; + source = "synthetic fixture"; consistency = "immutable synthetic tables"; + identity = "scope-demo"; domid = 0; vcpu = 0; +} + +let page entries = + let bytes = Bytes.make 4096 '\000' in + List.iter (fun (index, entry) -> 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