From 149423fc8891152959ae927d11751f26a4042733 Mon Sep 17 00:00:00 2001 From: james Date: Fri, 16 Oct 2026 18:42:09 +0100 Subject: [PATCH] feat(paging): walk four-level tables and predict access faults --- lib/paging.ml | 140 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 140 insertions(+) create mode 100644 lib/paging.ml diff --git a/lib/paging.ml b/lib/paging.ml new file mode 100644 index 0000000..6d16759 --- /dev/null +++ b/lib/paging.ml @@ -0,0 +1,140 @@ +open Model + +type entry = Absent | Invalid of string | Table of Address.Physical.t | Leaf of int * Address.Physical.t + +let shift level = 12 + (9 * (level - 1)) +let span level = Int64.shift_left 1L (shift level) + +let decode features ~nxe ~level raw = + let open Address in + if not (bit raw 0) then Absent + else if bit raw 63 && not nxe then Invalid "nx bit with nxe disabled" + else if Int64.logand raw (Int64.logand (mask 52) (Int64.lognot (mask features.phys_bits))) <> 0L then + Invalid "physical address uses reserved high bits" + else if level = 4 && bit raw 7 then Invalid "page size bit in pml4 entry" + else if level = 3 && bit raw 7 && not features.gb_pages then Invalid "1 gib pages are not exposed to the guest" + else + let address = Int64.logand raw (Int64.logand (mask features.phys_bits) (Int64.lognot 0xfffL)) in + if level = 1 then Leaf (12, Physical.of_int64 address) + else if bit raw 7 then + let bits = shift level in + (* huge leaf: [ frame | reserved | pat | flags ], bit 12 stays out of the frame *) + if Int64.logand raw (Int64.logand (mask bits) (Int64.lognot 0x1fffL)) <> 0L then + Invalid "misaligned huge page uses reserved address bits" + else Leaf (bits, Physical.of_int64 (align address bits)) + else Table (Physical.of_int64 address) + +let error_code context request ~present ~reserved = + (if present then 1 else 0) + lor (if request.access = Write then 2 else 0) + lor (if request.privilege = User then 4 else 0) + lor (if reserved then 8 else 0) + lor (if request.access = Execute && + (Address.bit context.registers.efer 11 || Address.bit context.registers.cr4 20) then 16 else 0) + +let walk context read address = + validate context; + let virtual_raw = Address.Virtual.to_int64 address in + if not (Address.canonical virtual_raw) then + { trace = []; outcome = Fault { vector = 13; error_code = 0; reason = "noncanonical linear address"; level = None } } + else + let rec go level table permissions trace = + match read table with + | Error reason -> { trace = List.rev trace; outcome = Incomplete reason } + | Ok page when String.length page <> 4096 -> + { trace = List.rev trace; outcome = Incomplete "table read is not 4096 bytes" } + | Ok page -> + let index = Int64.(to_int (logand (shift_right_logical virtual_raw (shift level)) 511L)) in + let raw = String.get_int64_le page (index * 8) in + let effective = narrow permissions raw in + let step = { level; table; index; raw; effective } in + let trace = step :: trace in + match decode context.features ~nxe:(Address.bit context.registers.efer 11) ~level raw with + | Absent -> { trace = List.rev trace; outcome = Fault { + vector = 14; error_code = 0; reason = "entry not present"; level = Some level } } + | Invalid reason -> { trace = List.rev trace; outcome = Fault { + vector = 14; error_code = 9; reason; level = Some level } } + | Table next -> go (level - 1) next effective trace + | Leaf (bits, base) -> + let trace = List.rev trace in + let physical_address = Address.Physical.of_int64 + Int64.(add (Address.Physical.to_int64 base) (logand virtual_raw (Address.mask bits))) in + { trace; outcome = Mapped { virtual_address = address; physical_address; + size = Int64.shift_left 1L bits; permissions = effective; leaf = raw; trace } } + in + go 4 (root context) unrestricted [] + +let explain context read address request = + let result = walk context read address in + let fault reason level = + { result with outcome = Fault { vector = 14; + error_code = error_code context request ~present:true ~reserved:false; + reason; level } } + in + match result.outcome with + | Incomplete _ -> result + | Fault f when f.vector = 13 -> result + | Fault f -> { result with outcome = Fault { f with error_code = + error_code context request ~present:(f.error_code land 1 <> 0) + ~reserved:(f.error_code land 8 <> 0) } } + | Mapped mapping -> + let p = mapping.permissions and r = context.registers in + let first predicate = + List.find_opt predicate result.trace |> Option.map (fun (step : step) -> step.level) + in + if request.privilege = User && not p.user then + fault "supervisor mapping denies user access" (first (fun s -> not (Address.bit s.raw 2))) + else if request.access = Write && not p.writable && + (request.privilege = User || Address.bit r.cr0 16) then + fault "read-only entry denies write" (first (fun s -> not (Address.bit s.raw 1))) + else if request.access = Execute && not p.executable then + fault "nx entry denies instruction fetch" (first (fun s -> Address.bit s.raw 63)) + else if request.privilege = Supervisor && p.user && request.access = Execute && Address.bit r.cr4 20 then + fault "smep denies supervisor fetch from user mapping" None + else if request.privilege = Supervisor && p.user && request.access <> Execute && + Address.bit r.cr4 21 && not request.ac then + fault "smap denies explicit supervisor data access with ac clear" None + else result + +type state = Present of mapping | Unknown of string | Broken of string +type region = { start : int64; length : int64; state : state } + +let last region = Int64.pred (Int64.add region.start region.length) + +let enumerate ?(max_entries = 2_000_000) context read = + validate context; + let count = ref 0 and acc = ref [] in + let emit start length state = acc := { start; length; state } :: !acc in + let canonicalise x = + if Address.bit x 47 then Int64.logor x 0xffff000000000000L else x + in + let rec go level table prefix permissions trace = + match read table with + | Error reason -> + if level = 4 then begin + emit 0L 0x800000000000L (Unknown reason); + emit 0xffff800000000000L 0x800000000000L (Unknown reason) + end else emit (canonicalise prefix) (Int64.mul 512L (span level)) (Unknown reason) + | Ok page -> + if String.length page <> 4096 then invalid_arg "table read is not 4096 bytes"; + for index = 0 to 511 do + incr count; + if !count > max_entries then raise (Limit "page-table traversal budget exceeded"); + let raw = String.get_int64_le page (index * 8) in + let prefix = Int64.logor prefix (Int64.shift_left (Int64.of_int index) (shift level)) in + let start = canonicalise prefix in + let effective = narrow permissions raw in + let trace = { level; table; index; raw; effective } :: trace in + match decode context.features ~nxe:(Address.bit context.registers.efer 11) ~level raw with + | Absent -> () + | Invalid reason -> emit start (span level) (Broken reason) + | Table next -> go (level - 1) next prefix effective trace + | Leaf (bits, physical_address) -> + let trace = List.rev trace in + let mapping = { virtual_address = Address.Virtual.of_int64 start; physical_address; + size = Int64.shift_left 1L bits; permissions = effective; leaf = raw; trace } in + emit start mapping.size (Present mapping) + done + in + go 4 (root context) 0L unrestricted []; + List.rev !acc