Skip to content

Commit 3c9cfdd

Browse files
committed
engine: add a direct-constraint input channel for computed bounds
A component can now emit a bound on a named quantity (>=, <=) that it computed but cannot state as a located address, via a new OBS_CONSTRAINT record and `C <quantity> <op> value=` wire line. It is not an address, so the anchor rules never read it and a below-region bound can no longer be misread as a text or page-offset witness. - text_pin_from_observation no longer widens a sub-floor base into a slot window; a witness pins the one slot it names, so exact offset-table pins (kernfs, bpf) are no longer smeared into two slots. - perf and mmap_brute_vmsplit emit their floors as lower bounds through the new channel instead of below-region positional records; perf's interior sample still supplies the upper bound, bracketing the base. - Gate range_from_interior and riscv64_fdt_kaslr_seed on OBS_ADDRESS so the new kind is invisible to every anchor reader by construction. - Fold constraint-op token lookup into one table; replace the ineffective wire-table completeness typedef with a runtime test.
1 parent c177904 commit 3c9cfdd

17 files changed

Lines changed: 605 additions & 138 deletions

src/components/mmap_brute_vmsplit.c

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@
5555
#define _GNU_SOURCE
5656
#include "include/kasld/api.h"
5757
#include "include/kasld/cli.h"
58+
#include "include/kasld/constraint.h"
5859
#include "include/kasld/task_size.h"
5960
#include <limits.h>
6061
#include <stdio.h>
@@ -169,11 +170,15 @@ int main(void) {
169170
/* Everywhere else the split sits BELOW PAGE_OFFSET by a distance the
170171
* architecture fixes and this probe cannot see (arm32 reserves 16 MiB for
171172
* modules, ppc32 a smaller gap, riscv32 the fixmap, PCI-IO and vmemmap
172-
* regions). The measurement is then a lower bound on the base, emitted as
173-
* the window it proves; the upper edge is the highest base the architecture
174-
* admits, which holds against any target. */
175-
kasld_result_range(KASLD_TYPE_VIRT, REGION_PAGE_OFFSET, addr,
176-
(unsigned long)PAGE_OFFSET_MAX, NULL, CONF_INFERRED);
173+
* regions). So the measurement is a pure LOWER BOUND on the base. Emit it
174+
* on the constraint channel rather than as a positional range: the value
175+
* sits below the linear-map region, which the anchor and coupling rules
176+
* (reading a page-offset witness as a located address) would misread; a
177+
* constraint is not an address, so they never see it. The range form's
178+
* upper edge was PAGE_OFFSET_MAX, which is exactly Q_PAGE_OFFSET's own top,
179+
* so stating only the lower bound loses nothing. Sound (gated on `exact`),
180+
* hence CONF_INFERRED: it holds in the guaranteed window. */
181+
kasld_emit_constraint(Q_PAGE_OFFSET, C_LOWER_BOUND, addr, CONF_INFERRED);
177182
#endif
178183
}
179184

src/components/perf_amd_branch_user.c

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@
6363
#define _GNU_SOURCE
6464
#include "include/kasld/api.h"
6565
#include "include/kasld/cli.h"
66+
#include "include/kasld/constraint.h"
6667
#include "include/kasld/perf_branch.h"
6768
#include <errno.h>
6869
#include <linux/perf_event.h>
@@ -192,12 +193,16 @@ int main(int argc, char *argv[]) {
192193
CONF_PARSED);
193194

194195
/* Entry-text branch-from sites sit in the base's own slot, so flooring the
195-
* lowest to the base grid is a within-one-slot GUESS: emit it as a
196-
* CONF_HEURISTIC base pin shaping only the LIKELY window, never the
197-
* guaranteed one. Gated on the 2 MiB grid (x86 only), as in the sibling. */
196+
* lowest to the base grid is a within-one-slot GUESS: the base is that slot
197+
* or one below it. Emit the lower bound (floor - one slot) on the constraint
198+
* channel, at CONF_HEURISTIC so it shapes only the LIKELY window; a below-
199+
* _text bound is not an address and so is invisible to the anchor rules. The
200+
* interior sample supplies the sound upper bound. Gated on the 2 MiB grid
201+
* (x86 only), as in the sibling. */
198202
#if KASLR_VIRT_ALIGN >= 2 * MB
199-
kasld_result_base(KASLD_TYPE_VIRT, REGION_KERNEL_IMAGE,
200-
kasld_floor_text_base(acc.min_addr), NULL, CONF_HEURISTIC);
203+
kasld_emit_constraint(Q_VIRT_IMAGE_BASE, C_LOWER_BOUND,
204+
kasld_floor_text_base(acc.min_addr) - KASLR_VIRT_ALIGN,
205+
CONF_HEURISTIC);
201206
#endif
202207
return 0;
203208
}

src/components/perf_event_open.c

Lines changed: 22 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
#define _GNU_SOURCE
3232
#include "include/kasld/api.h"
3333
#include "include/kasld/cli.h"
34+
#include "include/kasld/constraint.h"
3435
#include <errno.h>
3536
#include <linux/perf_event.h>
3637
#include <poll.h>
@@ -266,25 +267,30 @@ int main(void) {
266267
kasld_result_sample(KASLD_TYPE_VIRT, REGION_KERNEL_TEXT, addr, NULL,
267268
CONF_PARSED);
268269

269-
/* On large-page arches the lowest sampled IP also yields a speculative base
270-
* GUESS: flooring it to KASLR_VIRT_ALIGN lands on the image base whenever the
271-
* lowest sampled function sits in the base's own slot — the common case on a
272-
* busy system, where low text executes constantly. It overshoots by one slot
273-
* only when the base's slot holds nothing the sampler caught (un-executed
274-
* head/entry text on an idle, freshly booted kernel). So emit it as a base
275-
* pin, but at CONF_HEURISTIC: "the floored slot is the base" is a heuristic,
276-
* so the pin sits BELOW the sound floor and shapes the speculative LIKELY
277-
* window only — never the guaranteed one, which keeps the sound interior
278-
* upper bound above. Region KERNEL_IMAGE so the value is read as _text
279-
* directly, with no _stext head-gap subtraction. kasld_floor_text_base
280-
* preserves the sub-alignment residue so the floor never drops below _text.
270+
/* On large-page arches the lowest sampled IP also brackets the base from
271+
* below. Flooring it to the KASLR grid lands on the base's own slot whenever
272+
* the lowest sampled function sits there — the common case on a busy system,
273+
* where low text executes constantly — and overshoots by exactly one slot
274+
* when the base's slot holds nothing the sampler caught (un-executed
275+
* head/entry text on an idle, freshly booted kernel). So the base is the
276+
* floored slot or one slot below it: a LOWER bound of floor - one slot.
277+
*
278+
* Emit it on the constraint channel rather than as a positional base pin.
279+
* The bound value sits one slot below _text, which the anchor rules — which
280+
* read a base witness as a located address — would misread as text; a
281+
* constraint is not an address, so they never see it. At CONF_HEURISTIC the
282+
* bound sits below the sound floor and shapes the speculative LIKELY window
283+
* only, never the guaranteed one; combined with the interior sample's sound
284+
* upper bound (base <= floored, via grid alignment) it brackets the base to
285+
* two slots, which an agreeing exact pin collapses to one.
281286
*
282287
* Gated to KASLR_VIRT_ALIGN >= 2 MiB: on fine-granule arches the lowest
283-
* sampled IP can sit many slots above the base, so flooring it is not a
284-
* within-one-slot guess; there the interior upper bound is the only claim. */
288+
* sampled IP can sit many slots above the base, so "within one slot" does not
289+
* hold; there the interior upper bound is the only claim. */
285290
#if KASLR_VIRT_ALIGN >= 2 * MB
286-
kasld_result_base(KASLD_TYPE_VIRT, REGION_KERNEL_IMAGE,
287-
kasld_floor_text_base(addr), NULL, CONF_HEURISTIC);
291+
kasld_emit_constraint(Q_VIRT_IMAGE_BASE, C_LOWER_BOUND,
292+
kasld_floor_text_base(addr) - KASLR_VIRT_ALIGN,
293+
CONF_HEURISTIC);
288294
#endif
289295

290296
return 0;

src/components/perf_lbr_sampling.c

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@
5353
#define _GNU_SOURCE
5454
#include "include/kasld/api.h"
5555
#include "include/kasld/cli.h"
56+
#include "include/kasld/constraint.h"
5657
#include "include/kasld/perf_branch.h"
5758
#include <errno.h>
5859
#include <linux/perf_event.h>
@@ -176,19 +177,21 @@ int main(int argc, char *argv[]) {
176177
kasld_result_sample(KASLD_TYPE_VIRT, REGION_KERNEL_TEXT, acc.min_addr, NULL,
177178
CONF_PARSED);
178179

179-
/* On large-page arches the lowest sample also yields a speculative base
180-
* GUESS: flooring it to the base grid lands on the image base whenever the
181-
* lowest sampled branch sits in the base's own slot. Emit it as a base pin at
182-
* CONF_HEURISTIC so it shapes only the speculative LIKELY window, never the
183-
* guaranteed one (which keeps the sound interior upper bound above). Region
184-
* KERNEL_IMAGE so the value is read as _text directly; kasld_floor_text_base
185-
* preserves the sub-alignment residue so the floor never drops below _text.
180+
/* On large-page arches the lowest sample also brackets the base from below:
181+
* flooring it to the base grid lands on the image base whenever the lowest
182+
* sampled branch sits in the base's own slot, and one slot high otherwise —
183+
* so the base is the floored slot or one below it. Emit the lower bound
184+
* (floor - one slot) on the constraint channel at CONF_HEURISTIC so it shapes
185+
* only the speculative LIKELY window, never the guaranteed one; the interior
186+
* sample keeps the sound upper bound. A below-_text bound is not an address,
187+
* so the anchor rules never read it.
186188
* LBR is x86-only today (KASLR_VIRT_ALIGN = 2 MiB, so the gate always holds);
187189
* the gate keeps this correct-by-construction should LBR ever gain a finer
188190
* target, where flooring the lowest sample is not a within-one-slot guess. */
189191
#if KASLR_VIRT_ALIGN >= 2 * MB
190-
kasld_result_base(KASLD_TYPE_VIRT, REGION_KERNEL_IMAGE,
191-
kasld_floor_text_base(acc.min_addr), NULL, CONF_HEURISTIC);
192+
kasld_emit_constraint(Q_VIRT_IMAGE_BASE, C_LOWER_BOUND,
193+
kasld_floor_text_base(acc.min_addr) - KASLR_VIRT_ALIGN,
194+
CONF_HEURISTIC);
192195
#endif
193196
return 0;
194197
}

src/engine_rules.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,9 @@ static const rule_fn k_rules[] = {
9393
/* Text-base pin from POS_BASE kernel-image observation */
9494
rule_text_pin_from_observation,
9595

96+
/* Direct-constraint channel: fold OBS_CONSTRAINT bounds into the meet */
97+
rule_constraint_passthrough,
98+
9699
/* Symmetric phys↔virt text-base coupling synthesizer */
97100
rule_text_base_coupling_synth,
98101

src/include/kasld/constraint.h

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,36 @@ enum constraint_op {
4444
* CRT combines repeats) */
4545
};
4646

47+
/* constraint_op <-> wire token. Total over the enum so the mapping round-trips
48+
* both ways (the engine emits every op internally); the direct-constraint input
49+
* channel (kasld_emit_constraint) only *carries* the two inequality-bound ops.
50+
*/
51+
static const char *const kasld_constraint_op_wire_table[] = {
52+
[C_LOWER_BOUND] = ">=", [C_UPPER_BOUND] = "<=",
53+
[C_EQUALS] = "==", [C_AT_LEAST_ALIGN] = "align>=",
54+
[C_EXCLUDE] = "exclude", [C_STRIDE] = "stride",
55+
};
56+
57+
static inline const char *kasld_constraint_op_wire(enum constraint_op op) {
58+
unsigned n = sizeof(kasld_constraint_op_wire_table) / sizeof(char *);
59+
if ((unsigned)op >= n)
60+
return NULL;
61+
return kasld_constraint_op_wire_table[op];
62+
}
63+
64+
/* Returns 1 and sets *out on a known token; 0 otherwise. */
65+
static inline int kasld_constraint_op_from_wire(const char *s,
66+
enum constraint_op *out) {
67+
unsigned n = sizeof(kasld_constraint_op_wire_table) / sizeof(char *);
68+
for (unsigned i = 0; i < n; i++)
69+
if (kasld_constraint_op_wire_table[i] &&
70+
strcmp(s, kasld_constraint_op_wire_table[i]) == 0) {
71+
*out = (enum constraint_op)i;
72+
return 1;
73+
}
74+
return 0;
75+
}
76+
4777
struct constraint {
4878
enum kasld_quantity q;
4979
enum constraint_op op;
@@ -68,4 +98,48 @@ struct constraint {
6898
uint32_t id; /* monotonic, assigned at emission */
6999
};
70100

101+
/* Emit one direct constraint on a quantity:
102+
* C <quantity> <op> conf=<c> value=0x<hex>
103+
*
104+
* For a component that has *computed a bound on a known quantity* but cannot
105+
* state it as a located address (the motivating case is perf's lowest sampled
106+
* IP, a lower bound on the text base that lands below _text). The channel
107+
* carries inequality bounds only (>=, <=); the orchestrator turns each into
108+
* that C_* constraint for the meet. It is not an address, so the anchor rules
109+
* never read it — a below-base bound cannot be misread as a text anchor. An
110+
* exact value is deliberately NOT on this channel: a located address uses the
111+
* positional emitters (kasld_result_base/sample/...), where it also
112+
* corroborates and classifies; an exact non-address measurement uses the scalar
113+
* channel. This channel is for a computed bound and nothing else. */
114+
static inline int kasld_emit_constraint(enum kasld_quantity q,
115+
enum constraint_op op,
116+
unsigned long value,
117+
enum kasld_confidence c) {
118+
const char *qw = kasld_quantity_wire(q);
119+
const char *ow = kasld_constraint_op_wire(op);
120+
if (!qw) {
121+
fprintf(stderr,
122+
"kasld_emit_constraint: invalid quantity %d; nothing "
123+
"emitted\n",
124+
(int)q);
125+
return 0;
126+
}
127+
if (op != C_LOWER_BOUND && op != C_UPPER_BOUND) {
128+
fprintf(stderr,
129+
"kasld_emit_constraint: op %s not carried on this channel "
130+
"(inequality bounds only); nothing emitted\n",
131+
ow ? ow : "?");
132+
return 0;
133+
}
134+
if (c == CONF_UNKNOWN) {
135+
fprintf(stderr,
136+
"kasld_emit_constraint: CONF_UNKNOWN for %s; nothing "
137+
"emitted\n",
138+
qw);
139+
return 0;
140+
}
141+
printf("C %s %s conf=%s value=0x%lx\n", qw, ow, kasld_conf_wire(c), value);
142+
return 1;
143+
}
144+
71145
#endif /* KASLD_CONSTRAINT_H */

src/include/kasld/engine_rules.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -329,6 +329,7 @@ R(efi_loader_kernel_pick);
329329

330330
/* Text-base pin from POS_BASE kernel-image observation */
331331
R(text_pin_from_observation);
332+
R(constraint_passthrough);
332333

333334
/* Symmetric phys↔virt text-base coupling synthesizer */
334335
R(text_base_coupling_synth);

src/include/kasld/internal.h

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
#define KASLD_INTERNAL_H
1212

1313
#include "api.h"
14+
#include "constraint.h" /* struct constraint_fact_record enums */
1415
#include "regions.h" /* canonical is_phys_dram_region / is_kernel_image_region */
1516

1617
#include <stddef.h>
@@ -879,6 +880,23 @@ struct scalar_fact_record {
879880
extern struct scalar_fact_record scalar_facts[MAX_SCALAR_FACTS];
880881
extern int num_scalar_facts;
881882

883+
/* Direct constraints collected from components' `C` wire records, parallel to
884+
* scalar_facts[]. The engine bridge copies these to OBS_CONSTRAINT
885+
* observations, which a passthrough rule folds into the meet as the named C_*
886+
* constraint. A component uses this channel for a bound on a known quantity it
887+
* cannot state as a located address (see kasld_emit_constraint). */
888+
struct constraint_fact_record {
889+
enum kasld_quantity q;
890+
enum constraint_op op;
891+
unsigned long value;
892+
enum kasld_confidence conf;
893+
int origin; /* discovery slot of the producing component; -1 if unattributed
894+
*/
895+
};
896+
#define MAX_CONSTRAINT_FACTS 64
897+
extern struct constraint_fact_record constraint_facts[MAX_CONSTRAINT_FACTS];
898+
extern int num_constraint_facts;
899+
882900
/* =========================================================================
883901
* Shared functions (defined in orchestrator.c)
884902
* ========================================================================= */

src/include/kasld/observation.h

Lines changed: 25 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,8 @@
1616
#ifndef KASLD_OBSERVATION_H
1717
#define KASLD_OBSERVATION_H
1818

19-
#include "api.h" /* NAME_LEN, ORIGIN_LEN wire-field widths */
19+
#include "api.h" /* NAME_LEN, ORIGIN_LEN wire-field widths */
20+
#include "constraint.h" /* enum kasld_quantity, enum constraint_op (OBS_CONSTRAINT) */
2021

2122
#include <stdint.h>
2223

@@ -39,18 +40,26 @@ enum kasld_set_bits {
3940
#define HAS_BASE_ALIGN(r) ((r)->set_mask & BASE_ALIGN_SET)
4041
#endif
4142

42-
/* An observation carries either an address fact (region + extent — the
43-
* leak/landmark shape) or a scalar system fact (a bare number with a
44-
* named meaning). Scalar facts exist because components are the sole
45-
* inference I/O boundary — a component must be able to emit raw
46-
* measurements that are NOT addresses (MemTotal, physical-address bits,
47-
* kernel image size, VA bits). A rule reads these by `scalar_fact` and
48-
* turns them into constraints; keeping them raw on the observation
49-
* preserves measure/reason separation (components measure; rules
50-
* interpret). */
43+
/* An observation carries one of three input kinds. Components are the sole
44+
* inference I/O boundary, so each is something a component must be able to
45+
* state:
46+
* - OBS_ADDRESS: a region + extent (the leak/landmark shape).
47+
* - OBS_SCALAR: a bare measurement with a named meaning that is NOT an
48+
* address (MemTotal, physical-address bits, image size, VA bits). A rule
49+
* reads it by `scalar_fact` and turns it into constraints.
50+
* - OBS_CONSTRAINT: an inequality bound on a named quantity the component
51+
* computed but cannot state as a located address (perf's lowest sampled IP
52+
* is a lower bound on the text base that sits below _text). It carries a
53+
* quantity, a bound operator (>= or <=), and a value; a passthrough rule
54+
* emits it as that C_* directly. Because it is not an address, the ~44
55+
* anchor rules (which gate on OBS_ADDRESS) never read it — a below-base
56+
* bound cannot be misread as a text anchor.
57+
* Keeping non-address facts raw on the observation preserves measure/reason
58+
* separation (components measure; rules interpret). */
5159
enum obs_value_kind {
5260
OBS_ADDRESS = 0, /* region + lo/hi/sample (default) */
5361
OBS_SCALAR, /* scalar_fact + scalar_value */
62+
OBS_CONSTRAINT, /* c_quantity + c_op + scalar_value (reused as the value) */
5463
};
5564

5665
/* enum kasld_scalar_fact + its wire table live in api.h (the component-facing
@@ -71,8 +80,12 @@ struct observation {
7180
enum kasld_position pos;
7281
/* OBS_SCALAR: */
7382
enum kasld_scalar_fact scalar_fact;
74-
unsigned long scalar_value;
75-
/* both: */
83+
unsigned long
84+
scalar_value; /* OBS_CONSTRAINT reuses this as the bound value */
85+
/* OBS_CONSTRAINT: */
86+
enum kasld_quantity c_quantity;
87+
enum constraint_op c_op;
88+
/* all kinds: */
7689
enum kasld_confidence conf;
7790
char origin[ORIGIN_LEN]; /* producing component */
7891

src/include/kasld/quantity.h

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,43 @@ enum kasld_quantity {
3636
Q__COUNT,
3737
};
3838

39+
/* Q_* <-> wire token, single source of truth for both directions. Header-only
40+
* (like kasld_scalar_fact_wire_table in api.h) so a component's emit side and
41+
* the orchestrator's parse side share one mapping without linking quantities.c
42+
* — the tokens match the human `name` field in that table. */
43+
static const char *const kasld_quantity_wire_table[Q__COUNT] = {
44+
[Q_VIRT_IMAGE_BASE] = "virt_image_base",
45+
[Q_PHYS_IMAGE_BASE] = "phys_image_base",
46+
[Q_PAGE_OFFSET] = "virt_page_offset",
47+
[Q_VMALLOC_BASE] = "virt_vmalloc_base",
48+
[Q_VMEMMAP_BASE] = "virt_vmemmap_base",
49+
[Q_MODULE_BASE] = "virt_module_base",
50+
[Q_VIRT_KASLR_ALIGN] = "virt_kaslr_align",
51+
[Q_PHYS_KASLR_ALIGN] = "phys_kaslr_align",
52+
[Q_VA_BITS] = "va_bits",
53+
};
54+
/* The [Q__COUNT] dimension keeps the table indexable for every Q_* (a missing
55+
* entry is a NULL hole, not out of bounds); it does NOT make the table
56+
* complete. Completeness — every Q_* has a non-NULL token, and tokens
57+
* round-trip — is enforced at runtime by test_wire_tables_complete
58+
* (tests/test_engine.c), since a sizeof check cannot see a NULL interior
59+
* initialiser. */
60+
61+
static inline const char *kasld_quantity_wire(enum kasld_quantity q) {
62+
if ((unsigned)q >= Q__COUNT)
63+
return NULL;
64+
return kasld_quantity_wire_table[q];
65+
}
66+
67+
/* Returns Q__COUNT when the token names no known quantity. */
68+
static inline enum kasld_quantity kasld_quantity_from_wire(const char *s) {
69+
for (int i = 0; i < Q__COUNT; i++)
70+
if (kasld_quantity_wire_table[i] &&
71+
strcmp(s, kasld_quantity_wire_table[i]) == 0)
72+
return (enum kasld_quantity)i;
73+
return Q__COUNT;
74+
}
75+
3976
/* Lattice kind selects the meet operation and the bottom test.
4077
* - LK_INTERVAL: value is [lo, hi]; meet narrows the interval; bottom = lo>hi.
4178
* - LK_MAXALIGN: value is the largest known alignment (power of two); meet

0 commit comments

Comments
 (0)