EXTp: A Soundness Theorem for Counterfactual Exploit Replay on Formally Verified Microkernels
Utku Erol · Zenodo (CERN European Organization for Nuclear Research) · 2026
Counterfactual exploit analysis -- determining which input parameter causally produced an observed outcome -- is pervasive in security research, but its current practice is epistemically unsound. Three gaps separate "different outcome" from "caused by the change": non-deterministic replay noise, replay-machinery side-effects, and causal pathways traversing microarchitectural state invisible to the analyst's surface. We present EXTp, a counterfactual replay framework on bare-metal seL4, and the Counterfactual Soundness Theorem (CST) -- the first formal soundness theorem for counterfactual causal attribution grounded in a verified microkernel substrate. EXTp realizes three observable properties: Capability Separation (Pearl modularity; Clopper-Pearson bound <= 0.37% at N=998), Strong Observational Equivalence (replay determinism: score_S = 1.0000 over N=34 cross-boot trials, Clopper-Pearson one-sided 95% upper bound on the per-run failure rate <= 10.4%), and Measurement Interference (calibrated timing threshold, realized false-positive rate 0.61%-2.78%). CST proves their composition grounds Pearl/Halpern-Pearl causal attribution within enumerated epistemic bounds; CST v1.0 establishes soundness under single-VCPU intervention scope and bare-metal microcode-stable configurations, with multi-VCPU and cross-configuration extensions charted as future work. A synthetic analog modeled on the CrackArmor confused-deputy pattern, executed on bare-metal Intel Alder Lake, exercises the pipeline end-to-end and shows the framework correctly detecting its own A1-modulo violations.