~james/scope

feat(core): define typed addresses and captured register state

commit
b1b249cd6fbbce57ed295d729b9efc69513686bd browse tree
author
james <j@cpl0.zip>
signature
Verified ~james signed with a key registered by ~james
date
2026-10-15 10:24 UTC

7 files changed, +198 −0

.gitignore added

@@ -0,0 +1,4 @@
1+_build/
2+*.install
3+guest/build/
4+__pycache__/

dune-project added

@@ -0,0 +1,8 @@
1+(lang dune 3.10)
2+(name scope)
3+(version 0.1.0)
4+(generate_opam_files true)
5+(package
6+ (name scope)
7+ (synopsis "Inspect and replay Xen guest page tables")
8+ (depends (ocaml (>= 4.14)) dune))

lib/address.ml added

@@ -0,0 +1,33 @@
1+module Virtual = struct
2+ type t = int64
3+ let of_int64 x = x
4+ let to_int64 x = x
5+end
6+
7+module Physical = struct
8+ type t = int64
9+ let of_int64 x = x
10+ let to_int64 x = x
11+end
12+
13+module Machine = struct
14+ type t = int64
15+ let of_int64 x = x
16+ let to_int64 x = x
17+end
18+
19+let compare = Int64.unsigned_compare
20+let hex x = Printf.sprintf "0x%016Lx" x
21+
22+let parse s =
23+ if String.length s = 0 || s.[0] = '-' || s.[0] = '+' then
24+ invalid_arg ("invalid unsigned address: " ^ s);
25+ try Int64.of_string (if String.starts_with ~prefix:"0x" s then s else "0u" ^ s)
26+ with Failure _ -> invalid_arg ("invalid unsigned address: " ^ s)
27+
28+let bit x n = Int64.logand x (Int64.shift_left 1L n) <> 0L
29+let mask n = Int64.pred (Int64.shift_left 1L n)
30+let align x n = Int64.logand x (Int64.lognot (mask n))
31+let canonical x =
32+ let high = Int64.shift_right x 47 in
33+ high = 0L || high = -1L

lib/address.mli added

@@ -0,0 +1,25 @@
1+module Virtual : sig
2+ type t
3+ val of_int64 : int64 -> t
4+ val to_int64 : t -> int64
5+end
6+
7+module Physical : sig
8+ type t
9+ val of_int64 : int64 -> t
10+ val to_int64 : t -> int64
11+end
12+
13+module Machine : sig
14+ type t
15+ val of_int64 : int64 -> t
16+ val to_int64 : t -> int64
17+end
18+
19+val compare : int64 -> int64 -> int
20+val hex : int64 -> string
21+val parse : string -> int64
22+val bit : int64 -> int -> bool
23+val mask : int -> int64
24+val align : int64 -> int -> int64
25+val canonical : int64 -> bool

lib/dune added

@@ -0,0 +1,4 @@
1+(library
2+ (name scope)
3+ (public_name scope)
4+ (libraries unix))

lib/model.ml added

@@ -0,0 +1,101 @@
1+type features = { phys_bits : int; nx : bool; gb_pages : bool }
2+
3+type registers = {
4+ cr0 : int64;
5+ cr2 : int64;
6+ cr3 : int64;
7+ cr4 : int64;
8+ efer : int64;
9+ rflags : int64;
10+ rip : int64;
11+}
12+
13+type context = {
14+ registers : registers;
15+ root_override : int64 option;
16+ features : features;
17+ source : string;
18+ consistency : string;
19+ identity : string;
20+ domid : int;
21+ vcpu : int;
22+}
23+
24+type permissions = { writable : bool; user : bool; executable : bool }
25+type access = Read | Write | Execute
26+type privilege = Supervisor | User
27+type request = { access : access; privilege : privilege; ac : bool }
28+
29+type step = {
30+ level : int;
31+ table : Address.Physical.t;
32+ index : int;
33+ raw : int64;
34+ effective : permissions;
35+}
36+
37+type mapping = {
38+ virtual_address : Address.Virtual.t;
39+ physical_address : Address.Physical.t;
40+ size : int64;
41+ permissions : permissions;
42+ leaf : int64;
43+ trace : step list;
44+}
45+
46+type fault = {
47+ vector : int;
48+ error_code : int;
49+ reason : string;
50+ level : int option;
51+}
52+
53+type outcome = Mapped of mapping | Fault of fault | Incomplete of string
54+type result = { trace : step list; outcome : outcome }
55+type reader = Address.Physical.t -> (string, string) Stdlib.result
56+
57+exception Limit of string
58+
59+let unrestricted = { writable = true; user = true; executable = true }
60+
61+let narrow permissions raw = {
62+ writable = permissions.writable && Address.bit raw 1;
63+ user = permissions.user && Address.bit raw 2;
64+ executable = permissions.executable && not (Address.bit raw 63);
65+}
66+
67+let validate context =
68+ let r = context.registers and f = context.features in
69+ let require predicate reason = if not predicate then invalid_arg reason in
70+ require (Sys.word_size = 64) "scope requires a 64-bit runtime";
71+ require (f.phys_bits >= 32 && f.phys_bits <= 52) "physical width must be between 32 and 52";
72+ require (Address.bit r.cr0 0 && Address.bit r.cr0 31) "protected paging must be enabled";
73+ require (Address.bit r.cr4 5 && Address.bit r.efer 10) "only ia-32e paging is supported";
74+ require (not (Address.bit r.cr4 12)) "five-level paging is unsupported";
75+ require (not (Address.bit r.cr4 22 || Address.bit r.cr4 24)) "protection keys are unsupported";
76+ require (not (Address.bit r.cr4 23)) "cet is unsupported";
77+ require (not (Address.bit r.cr4 27)) "linear address space separation is unsupported";
78+ require (not (Address.bit r.cr4 28)) "supervisor linear address masking is unsupported";
79+ require (not (Address.bit r.efer 11) || f.nx) "nxe requires the guest nx feature";
80+ let validate_root root =
81+ require (Int64.logand root (Int64.lognot (Address.mask f.phys_bits)) = 0L)
82+ "cr3 exceeds the physical width or uses unsupported address masking"
83+ in
84+ validate_root r.cr3;
85+ Option.iter validate_root context.root_override;
86+ require (context.domid >= 0 && context.vcpu >= 0) "negative domain or vcpu"
87+
88+let root context = Address.Physical.of_int64
89+ (Address.align (Option.value context.root_override ~default:context.registers.cr3) 12)
90+let access_name = function Read -> "read" | Write -> "write" | Execute -> "execute"
91+let privilege_name = function Supervisor -> "supervisor" | User -> "user"
92+
93+let context_changes before after =
94+ let a = before.registers and b = after.registers in
95+ List.filter_map (fun (changed, field) -> if changed then Some field else None) [
96+ (a.cr0 <> b.cr0, "cr0"); (a.cr3 <> b.cr3, "cr3"); (a.cr4 <> b.cr4, "cr4");
97+ (root before <> root after, "root");
98+ (a.efer <> b.efer, "efer"); (Address.bit a.rflags 18 <> Address.bit b.rflags 18, "ac");
99+ (before.features.phys_bits <> after.features.phys_bits, "phys_bits");
100+ (before.features.nx <> after.features.nx, "nx");
101+ (before.features.gb_pages <> after.features.gb_pages, "gb_pages") ]

scope.opam added

@@ -0,0 +1,23 @@
1+# This file is generated by dune, edit dune-project instead
2+opam-version: "2.0"
3+version: "0.1.0"
4+synopsis: "Inspect and replay Xen guest page tables"
5+depends: [
6+ "ocaml" {>= "4.14"}
7+ "dune" {>= "3.10"}
8+ "odoc" {with-doc}
9+]
10+build: [
11+ ["dune" "subst"] {dev}
12+ [
13+ "dune"
14+ "build"
15+ "-p"
16+ name
17+ "-j"
18+ jobs
19+ "@install"
20+ "@runtest" {with-test}
21+ "@doc" {with-doc}
22+ ]
23+]