Skip to content

Commit d4ddf21

Browse files
committed
inference: add kernel_image_phys_bound
Tighten phys_base bounds from PHYS witnesses tagged kernel_image, kernel_text, or kernel_data: phys_base_max ≤ min(W), phys_base_min ≥ max(W) − MAX_KERNEL_IMAGE_SIZE + 1, with a conflict guard when the witness spread exceeds the image-size budget. For BSS-resident witnesses, refine the upper bound to W − gap using image_size_from_text_data_gap's virtual TEXT/DATA gap as a lower bound on offset_of(swapper_pg_dir). On coupled arches the same bounds project into virt_text_base via phys_to_virt. Collapses phys entropy by ~6 bits from a single cr3 leak on x86-64.
1 parent 607521e commit d4ddf21

1 file changed

Lines changed: 296 additions & 0 deletions

File tree

Lines changed: 296 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,296 @@
1+
// This file is part of KASLD - https://github.com/bcoles/kasld
2+
//
3+
// Inference plugin: kernel-locating PHYS leak → tight phys_base bounds
4+
// (POST_COLLECTION)
5+
//
6+
// Components occasionally leak a *physical* address that is known to lie
7+
// within the kernel image. Examples:
8+
// - CR3 read (x86-64): swapper_pg_dir lives in the kernel BSS, so its
9+
// physical address is somewhere in [phys_base, phys_base + image_size).
10+
// - Kernel symbol address resolved via /proc/kcore on a coupled arch.
11+
// - Module loader leaking the physical mapping of a kernel page.
12+
//
13+
// These results are emitted as PHYS/* with the region tagged kernel_image,
14+
// kernel_text, or kernel_data — the renderer surfaces them as
15+
// "Kernel image (physical)" etc. They are not handled by dram_bound.c
16+
// (which uses the global RAM floor, agnostic to the kernel image) or by
17+
// phys_virt_synth.c (which requires a paired same-origin VIRT/PHYS leak).
18+
//
19+
// For any kernel-locating PHYS result P:
20+
// phys_base ≤ P (P is at or above the image start)
21+
// phys_base + image_size > P (P is strictly inside the image)
22+
//
23+
// Across all observed kernel-locating PHYS results in a single boot:
24+
// lo = min(P) → phys_base_max ≤ lo
25+
// hi = max(P) → phys_base_min ≥ hi − MAX_KERNEL_IMAGE_SIZE + 1
26+
//
27+
// Soundness note: MAX_KERNEL_IMAGE_SIZE is a generous *upper* bound (256 MiB,
28+
// matching text_cluster_filter.c). Real images are 50–150 MiB; any larger
29+
// build is still bounded. Using an upper bound for the lower-bound formula
30+
// guarantees we never push phys_base_min above the true value. The
31+
// upper-bound computation is exact (no image_size estimate needed).
32+
//
33+
// Conflict guard: if the spread (hi − lo) exceeds MAX_KERNEL_IMAGE_SIZE,
34+
// at least one of the extreme results is misclassified — they cannot both
35+
// lie within a single contiguous kernel image. Skip the plugin in that case
36+
// rather than emit a wrong bound; downstream invalidation by other plugins
37+
// (cluster filter, coupling validate) typically resolves the conflict in a
38+
// later pass.
39+
//
40+
// BSS-resident refinement (combined with image_size_from_text_data_gap):
41+
// When a witness is tagged KASLD_REGION_KERNEL_BSS, its symbol lives in the
42+
// kernel .bss section, so its offset from _stext is strictly greater than
43+
// data_end_offset (the boundary between .rodata and .bss). Because
44+
// KASLD_SECTION_DATA is contractually limited to .data/.rodata addresses,
45+
// the gap = max(VIRT/DATA) − min(VIRT/TEXT) is always ≤ data_end_offset.
46+
// Therefore gap < offset_of(any .bss symbol), and the tightened upper bound
47+
// phys_base ≤ W − gap
48+
// is sound for all KERNEL_BSS witnesses. No allow-list is needed: emitters
49+
// self-declare .bss residency via the region tag. The tightening fires when
50+
// gap > 0 (TEXT/DATA pair observed) and W > gap (no underflow).
51+
//
52+
// On coupled architectures (PHYS_VIRT_DECOUPLED=0), the same observation
53+
// projects through phys_to_virt to tighten virt_text_base bounds:
54+
// virt_text_base = page_offset + (phys_base − phys_offset) + text_offset
55+
// Both the upper and lower phys bounds are mapped accordingly.
56+
//
57+
// Phase: POST_COLLECTION — needs collected PHYS results.
58+
// Cross-arch (decoupled tightens phys_base bounds; coupled also tightens
59+
// virt_text_base bounds).
60+
// ---
61+
// <bcoles@gmail.com>
62+
63+
#define _POSIX_C_SOURCE 200809L
64+
65+
#include "../include/kasld_inference.h"
66+
67+
#include <limits.h>
68+
#include <stdio.h>
69+
#include <string.h>
70+
71+
/* Conservative upper bound on real kernel image size. Production kernels are
72+
* ~50-150 MiB; 256 MiB covers debug builds. Used only for the lower-bound
73+
* formula (where we must overestimate to stay sound). */
74+
#define MAX_KERNEL_IMAGE_SIZE (256ul * 1024 * 1024)
75+
76+
/* Plausibility cap on a physical kernel address. Guards against zero or
77+
* obviously-garbage values (sub-1 MiB or beyond 1 PiB). */
78+
#define MIN_PLAUSIBLE_KERNEL_PHYS (1ul * 1024 * 1024)
79+
#define MAX_PLAUSIBLE_KERNEL_PHYS (1ul << 50)
80+
81+
static int kipb_is_kernel_locating_region(const char *region) {
82+
if (!region || region[0] == '\0')
83+
return 0;
84+
return strcmp(region, KASLD_REGION_KERNEL_IMAGE) == 0 ||
85+
strcmp(region, KASLD_REGION_KERNEL_TEXT) == 0 ||
86+
strcmp(region, KASLD_REGION_KERNEL_DATA) == 0 ||
87+
strcmp(region, KASLD_REGION_KERNEL_BSS) == 0;
88+
}
89+
90+
/* Compute the virtual TEXT/DATA gap that image_size_from_text_data_gap.c
91+
* uses. Returns 0 if no valid pair is present (in which case the
92+
* BSS-resident tightening does not fire). */
93+
static unsigned long compute_virt_gap(const struct kasld_analysis_ctx *ctx) {
94+
unsigned long min_text = ULONG_MAX;
95+
unsigned long max_data = 0;
96+
97+
for (size_t i = 0; i < ctx->result_count; i++) {
98+
const struct result *r = &ctx->results[i];
99+
if (!r->valid || r->type != KASLD_ADDR_VIRT)
100+
continue;
101+
if (strcmp(r->section, KASLD_SECTION_TEXT) == 0) {
102+
if (r->raw < min_text)
103+
min_text = r->raw;
104+
} else if (strcmp(r->section, KASLD_SECTION_DATA) == 0) {
105+
if (r->raw > max_data)
106+
max_data = r->raw;
107+
}
108+
}
109+
110+
if (min_text == ULONG_MAX || max_data <= min_text)
111+
return 0;
112+
return max_data - min_text;
113+
}
114+
115+
/* Round v UP to the nearest multiple of align. align must be a power of two
116+
* and non-zero. */
117+
static unsigned long align_up(unsigned long v, unsigned long align) {
118+
return (v + align - 1) & ~(align - 1);
119+
}
120+
121+
static unsigned long align_down(unsigned long v, unsigned long align) {
122+
return v & ~(align - 1);
123+
}
124+
125+
static void kernel_image_phys_bound_run(struct kasld_analysis_ctx *ctx) {
126+
unsigned long virt_gap = compute_virt_gap(ctx);
127+
128+
/* Two-track upper-bound source: `lo_raw` is min over all witnesses (used
129+
* for the conflict guard and as the baseline upper bound on phys_base);
130+
* `lo_tight` additionally subtracts virt_gap for BSS-resident witnesses,
131+
* yielding a tighter phys_base_max when the refinement applies. */
132+
unsigned long lo_raw = ULONG_MAX;
133+
unsigned long lo_tight = ULONG_MAX;
134+
unsigned long hi = 0;
135+
int count = 0;
136+
int bss_witnesses = 0;
137+
138+
for (size_t i = 0; i < ctx->result_count; i++) {
139+
const struct result *r = &ctx->results[i];
140+
if (!r->valid)
141+
continue;
142+
if (r->type != KASLD_ADDR_PHYS)
143+
continue;
144+
if (!kipb_is_kernel_locating_region(r->region))
145+
continue;
146+
if (r->raw < MIN_PLAUSIBLE_KERNEL_PHYS ||
147+
r->raw > MAX_PLAUSIBLE_KERNEL_PHYS)
148+
continue;
149+
150+
if (r->raw < lo_raw)
151+
lo_raw = r->raw;
152+
if (r->raw > hi)
153+
hi = r->raw;
154+
155+
/* BSS-resident witnesses (KERNEL_BSS region) contribute a tightened
156+
* upper-bound candidate `W - virt_gap` provided gap is available and
157+
* won't underflow. Other witnesses contribute the raw value. */
158+
unsigned long contrib = r->raw;
159+
if (virt_gap > 0 && strcmp(r->region, KASLD_REGION_KERNEL_BSS) == 0 &&
160+
r->raw > virt_gap) {
161+
contrib = r->raw - virt_gap;
162+
bss_witnesses++;
163+
}
164+
if (contrib < lo_tight)
165+
lo_tight = contrib;
166+
167+
count++;
168+
}
169+
170+
if (count == 0)
171+
return;
172+
173+
/* Conflict guard uses raw values so the BSS-resident refinement cannot
174+
* trigger a false-positive contradiction. */
175+
if (hi - lo_raw > MAX_KERNEL_IMAGE_SIZE) {
176+
if (verbose && !quiet)
177+
fprintf(stdout,
178+
"[infer] kernel_image_phys_bound: contradictory PHYS witnesses"
179+
" (lo=%#lx hi=%#lx spread=%#lx > %#lx); skipping\n",
180+
lo_raw, hi, hi - lo_raw, (unsigned long)MAX_KERNEL_IMAGE_SIZE);
181+
return;
182+
}
183+
184+
/* `lo` for downstream use: tightest candidate (= lo_tight when BSS
185+
* refinement applied, else lo_raw). */
186+
unsigned long lo = lo_tight;
187+
188+
/* ---- Upper bound on phys_base: phys_base ≤ lo ---- */
189+
unsigned long new_phys_max = lo;
190+
unsigned long phys_align = ctx->arch->phys_kaslr_align;
191+
if (phys_align > 0)
192+
new_phys_max = align_down(new_phys_max, phys_align);
193+
194+
if (ctx->arch->phys_virt_decoupled) {
195+
if (new_phys_max > ctx->phys_base_min &&
196+
new_phys_max < ctx->phys_base_max) {
197+
if (verbose && !quiet) {
198+
if (bss_witnesses > 0)
199+
fprintf(stdout,
200+
"[infer] phys_base_max tightened by kernel_image_phys_bound:"
201+
" %#lx -> %#lx (lo=%#lx with bss-gap=%#lx applied to %d"
202+
" witness%s, %d total)\n",
203+
ctx->phys_base_max, new_phys_max, lo, virt_gap, bss_witnesses,
204+
bss_witnesses == 1 ? "" : "es", count);
205+
else
206+
fprintf(stdout,
207+
"[infer] phys_base_max tightened by kernel_image_phys_bound:"
208+
" %#lx -> %#lx (kernel_image_phys_min=%#lx, %d witness%s)\n",
209+
ctx->phys_base_max, new_phys_max, lo_raw, count,
210+
count == 1 ? "" : "es");
211+
}
212+
ctx->phys_base_max = new_phys_max;
213+
}
214+
}
215+
216+
/* ---- Lower bound on phys_base: phys_base ≥ hi − MAX_IMAGE_SIZE + 1 ---- */
217+
if (hi >= MAX_KERNEL_IMAGE_SIZE) {
218+
unsigned long new_phys_min = hi - MAX_KERNEL_IMAGE_SIZE + 1;
219+
if (phys_align > 0)
220+
new_phys_min = align_up(new_phys_min, phys_align);
221+
222+
if (ctx->arch->phys_virt_decoupled) {
223+
if (new_phys_min > ctx->phys_base_min &&
224+
new_phys_min < ctx->phys_base_max) {
225+
if (verbose && !quiet)
226+
fprintf(stdout,
227+
"[infer] phys_base_min tightened by kernel_image_phys_bound:"
228+
" %#lx -> %#lx (kernel_image_phys_max=%#lx, %d witness%s)\n",
229+
ctx->phys_base_min, new_phys_min, hi, count,
230+
count == 1 ? "" : "es");
231+
ctx->phys_base_min = new_phys_min;
232+
}
233+
}
234+
}
235+
236+
/* ---- Coupled arch: project phys bounds into virtual text-base bounds.
237+
*
238+
* On coupled arches phys_to_virt(P) = page_offset + (P − phys_offset),
239+
* and the kernel text base is phys_to_virt(phys_base) + text_offset:
240+
*
241+
* virt_text_base_max ≤ page_offset + (lo − phys_offset) + text_offset
242+
* virt_text_base_min ≥ page_offset + (hi − max_image_size + 1
243+
* − phys_offset) + text_offset
244+
*
245+
* Use the runtime page_offset from layout (set by layout_adjust). */
246+
if (!ctx->arch->phys_virt_decoupled) {
247+
unsigned long page_offset = ctx->layout->page_offset;
248+
unsigned long phys_offset = ctx->arch->phys_offset;
249+
unsigned long text_offset = ctx->arch->text_offset;
250+
unsigned long kaslr_align = ctx->arch->kaslr_align;
251+
unsigned long kaslr_min = ctx->arch->kaslr_base_min;
252+
253+
if (lo < phys_offset)
254+
return; /* impossible: a kernel-locating phys below PHYS_OFFSET. */
255+
256+
unsigned long virt_max = page_offset + (lo - phys_offset) + text_offset;
257+
if (kaslr_align > 0)
258+
virt_max = align_down(virt_max, kaslr_align);
259+
if (virt_max > kaslr_min && virt_max > ctx->text_base_min &&
260+
virt_max < ctx->text_base_max) {
261+
if (verbose && !quiet)
262+
fprintf(
263+
stdout,
264+
"[infer] virt_text_base_max tightened by kernel_image_phys_bound:"
265+
" %#lx -> %#lx (kernel_image_phys_min=%#lx, %d witness%s)\n",
266+
ctx->text_base_max, virt_max, lo, count, count == 1 ? "" : "es");
267+
ctx->text_base_max = virt_max;
268+
}
269+
270+
if (hi >= MAX_KERNEL_IMAGE_SIZE - 1 + phys_offset) {
271+
unsigned long phys_min_raw = hi - MAX_KERNEL_IMAGE_SIZE + 1;
272+
unsigned long virt_min =
273+
page_offset + (phys_min_raw - phys_offset) + text_offset;
274+
if (kaslr_align > 0)
275+
virt_min = align_up(virt_min, kaslr_align);
276+
if (virt_min > ctx->text_base_min && virt_min < ctx->text_base_max) {
277+
if (verbose && !quiet)
278+
fprintf(stdout,
279+
"[infer] virt_text_base_min tightened by"
280+
" kernel_image_phys_bound: %#lx -> %#lx"
281+
" (kernel_image_phys_max=%#lx, %d witness%s)\n",
282+
ctx->text_base_min, virt_min, hi, count,
283+
count == 1 ? "" : "es");
284+
ctx->text_base_min = virt_min;
285+
}
286+
}
287+
}
288+
}
289+
290+
static const struct kasld_inference kernel_image_phys_bound = {
291+
.name = "kernel_image_phys_bound",
292+
.phase = KASLD_INFER_PHASE_POST_COLLECTION,
293+
.run = kernel_image_phys_bound_run,
294+
};
295+
296+
KASLD_REGISTER_INFERENCE(kernel_image_phys_bound);

0 commit comments

Comments
 (0)