rules: let directmap pin take L4/L5 from a resolved Q_VA_BITS

directmap_kaslr_disabled_pin only read SF_VIRT_ADDR_BITS (proc_cpuinfo), so it
couldn't fire when cpuinfo was unavailable but a directmap leak had resolved the
paging level via x86_64_la57_from_directmap. Fall back to the resolved
Q_VA_BITS estimate to pick L4/L5.

Reading est[Q_VA_BITS] is cross-quantity (not a self-edge on the bases written)
and acyclic. New estimate_finset_value() accessor encapsulates the LK_FINSET
live-candidate bitmask so the rule doesn't touch the representation. Confidence
and lineage handle the no-observation estimate path (lineage 1, conf = disable
signal). Test adds the leak -> la57 -> pin path with no cpuinfo; architecture.md
notes the fallback.

Author: bcoles

docs/architecture.md

@@ -250,8 +250,10 @@ Key rules for cross-region derivation:
   (`SF_KASAN_ENABLED`) or KASLR is off (`SF_VIRT_KASLR_DISABLED`) the direct-map
   randomisation is suppressed (`kaslr_memory_enabled() = kaslr_enabled() &&
   !CONFIG_KASAN`), so `Q_PAGE_OFFSET` / `Q_VMALLOC_BASE` / `Q_VMEMMAP_BASE` are
-  pinned to their compile-time L4/L5 defaults — the paging level taken from
-  `SF_VIRT_ADDR_BITS`. Kernel TEXT KASLR is independent and stays randomised.
+  pinned to their compile-time L4/L5 defaults — the paging level from
+  `SF_VIRT_ADDR_BITS` (cpuinfo, leak-free) or, when that is unavailable, a
+  resolved `Q_VA_BITS` (e.g. from a direct-map leak). Kernel TEXT KASLR is
+  independent and stays randomised.
 
 ### Coupled vs decoupled architectures
 

src/estimate.c

@@ -253,6 +253,23 @@ int estimate_is_bottom(const struct estimate *e,
   return 0;
 }
 
+int estimate_finset_value(const struct quantity_def *qd,
+                          const struct estimate *e, unsigned long *out) {
+  if (qd->lattice != LK_FINSET)
+    return 0;
+  unsigned long mask =
+      e->lo; /* live-candidate bitmask, one bit per candidate */
+  if (mask == 0 || (mask & (mask - 1)) != 0)
+    return 0; /* zero, or more than one, candidate still live */
+  for (int i = 0; i < qd->n_candidates; i++) {
+    if (mask == (1ul << i)) {
+      *out = qd->candidates[i];
+      return 1;
+    }
+  }
+  return 0;
+}
+
 /* ------------------------------------------------------------------------
  * Greedy resolver.
  * ------------------------------------------------------------------------ */

src/include/kasld/estimate.h

@@ -83,6 +83,14 @@ void estimate_meet(struct estimate *e, const struct quantity_def *qd,
 /* True iff the estimate is lattice-bottom (unsatisfiable / empty). */
 int estimate_is_bottom(const struct estimate *e, const struct quantity_def *qd);
 
+/* If a finite-set (LK_FINSET) quantity's estimate has narrowed to exactly one
+ * live candidate, write its value to *out and return 1. Returns 0 when the
+ * quantity is not LK_FINSET, or zero / more than one candidate is still live.
+ * Encapsulates the live-candidate bitmask so callers (e.g. rules reading a
+ * resolved Q_VA_BITS) don't depend on the LK_FINSET representation. */
+int estimate_finset_value(const struct quantity_def *qd,
+                          const struct estimate *e, unsigned long *out);
+
 /* Resolve quantity q over the constraints in cs[0..n_cs), considering only
  * those with conf >= floor. Greedy strongest-first (conf DESC, lineage_count
  * DESC, id ASC); a constraint that would force bottom is skipped and

src/rules/directmap_kaslr_disabled_pin.c

@@ -17,18 +17,22 @@
 // KASAN overrides it at runtime — common on syzkaller / CTF / debug kernels.
 //
 // On a positive disable signal, pin all three bases to the paging-level default
-// (L4 = VA 48, L5 = VA 57), chosen by SF_VIRT_ADDR_BITS (proc_cpuinfo's "bits
-// virtual", which tracks the active level — leak-free, so the pin fires without
-// any direct-map leak). CONFIG_RANDOMIZE_BASE is independent of the memory
-// randomisation, so kernel TEXT stays randomised; this pins only the
+// (L4 = VA 48, L5 = VA 57). The level comes from SF_VIRT_ADDR_BITS
+// (proc_cpuinfo's "bits virtual", which tracks the active level — leak-free, so
+// the pin can fire without any direct-map leak), falling back to a resolved
+// Q_VA_BITS (e.g. x86_64_la57_from_directmap, from a directmap leak's top bits)
+// when cpuinfo is unavailable. CONFIG_RANDOMIZE_BASE is independent of the
+// memory randomisation, so kernel TEXT stays randomised; this pins only the
 // direct-map side.
 //
 // Soundness:
 //   * Fires only on a positive disable signal AND a resolved VA width.
 //   * The pinned values are exact, non-config-tunable kernel constants for the
-//     resolved level, so no window-containment read is needed — and an
-//     out-of-window C_EQUALS is dropped by the engine's meet as a conflict
-//     anyway (so no est[Q] read, no self-edge).
+//     resolved level — no window-containment read is needed, and an
+//     out-of-window C_EQUALS is dropped by the engine's meet as a conflict.
+//   * The only estimate read is est[Q_VA_BITS] (the level): cross-quantity, not
+//     a self-edge on the bases written here, and acyclic — Q_VA_BITS derives
+//     from the directmap observation, never from est[Q_PAGE_OFFSET].
 //   * A higher-confidence real direct-map leak still wins via the resolver's
 //     conflict handling.
 // ---
@@ -41,7 +45,6 @@
 int rule_directmap_kaslr_disabled_pin(const struct evidence_set *ev,
                                       const struct estimate *est,
                                       struct constraint *out, int out_max) {
-  (void)est;
 #if defined(__x86_64__) || defined(__amd64__)
   uint32_t sig_id = 0, va_id = 0;
   enum kasld_confidence sig_conf = CONF_UNKNOWN, va_conf = CONF_UNKNOWN;
@@ -63,7 +66,18 @@ int rule_directmap_kaslr_disabled_pin(const struct evidence_set *ev,
       va_conf = o->conf;
     }
   }
-  if (sig_id == 0 || va_bits == 0)
+  if (sig_id == 0)
+    return 0;
+
+  /* Paging level (L4 = VA 48 / L5 = VA 57): prefer the leak-free cpuinfo scalar
+   * (SF_VIRT_ADDR_BITS); fall back to a resolved Q_VA_BITS — e.g.
+   * x86_64_la57_from_directmap pins it from a directmap leak's top bits when
+   * cpuinfo is unavailable. Reading est[Q_VA_BITS] is cross-quantity (not a
+   * self-edge on the bases this rule writes) and acyclic — Q_VA_BITS derives
+   * from the directmap observation, never from est[Q_PAGE_OFFSET]. */
+  if (va_bits == 0)
+    estimate_finset_value(&quantities[Q_VA_BITS], &est[Q_VA_BITS], &va_bits);
+  if (va_bits == 0)
     return 0;
 
   /* Active paging level: 48-bit VA -> 4-level (L4), 57-bit -> 5-level (L5). */
@@ -84,7 +98,11 @@ int rule_directmap_kaslr_disabled_pin(const struct evidence_set *ev,
       {Q_VMEMMAP_BASE, l5 ? VMEMMAP_BASE_L5 : VMEMMAP_BASE_L4},
   };
 
-  enum kasld_confidence conf = (sig_conf < va_conf) ? sig_conf : va_conf;
+  /* When the level came from the cpuinfo scalar, corroborate with its
+   * confidence + id; when it came from the already-resolved estimate there is
+   * no observation to cite, so the pin rests on the disable signal alone. */
+  enum kasld_confidence conf =
+      va_id ? ((sig_conf < va_conf) ? sig_conf : va_conf) : sig_conf;
   int n = 0;
   for (int k = 0; k < 3 && n < out_max; k++) {
     struct constraint *c = &out[n++];
@@ -95,12 +113,13 @@ int rule_directmap_kaslr_disabled_pin(const struct evidence_set *ev,
     c->conf = conf;
     c->derived_from[0] = sig_id;
     c->derived_from[1] = va_id;
-    c->lineage_count = 2;
+    c->lineage_count = va_id ? 2 : 1;
     snprintf(c->origin, ORIGIN_LEN, "directmap_kaslr_disabled_pin");
   }
   return n;
 #else
   (void)ev;
+  (void)est;
   (void)out;
   (void)out_max;
   return 0;

tests/test_engine.c

@@ -3190,6 +3190,23 @@ static void test_directmap_kaslr_disabled_pin(void) {
   engine_run(&e4, rules, 1);
   assert(e4.est[Q_PAGE_OFFSET].lo == top.lo &&
          e4.est[Q_PAGE_OFFSET].hi == top.hi);
+
+  /* Fallback path: NO SF_VIRT_ADDR_BITS, but a directmap leak below the L4 VAS
+   * floor resolves Q_VA_BITS=57 via la57_from_directmap; the pin then takes the
+   * level from the estimate and still fires (here -> the L5 default). */
+  struct engine e5;
+  engine_init(&e5);
+  struct observation k5 = mk_scalar(SF_KASAN_ENABLED, 1, CONF_PARSED);
+  evidence_add(&e5.ev, &k5);
+  struct observation dm =
+      mk_obs(KASLD_TYPE_VIRT, REGION_DIRECTMAP, 0xff20000000000000ul,
+             LO_SET | SAMPLE_SET, POS_INTERIOR, CONF_PARSED);
+  evidence_add(&e5.ev, &dm);
+  const rule_fn rules_la57[] = {rule_x86_64_la57_from_directmap,
+                                rule_directmap_kaslr_disabled_pin};
+  engine_run(&e5, rules_la57, 2);
+  assert(e5.est[Q_PAGE_OFFSET].lo == PAGE_OFFSET_BASE_L5 &&
+         e5.est[Q_PAGE_OFFSET].hi == PAGE_OFFSET_BASE_L5);
 #endif
 }