Source-linked AI summary
Don't Trust the Code, Check Its Effects: Runtime Refinement for Regenerated Systems Code Under an Adversarial Generator
Jinhao Hu, Ashvin Goel, Laurent Bindschaedler
TL;DR
The paper addresses regenerated systems code with irreversible effects and potentially adversarial generators, where re-execution cannot undo effects and verification assumptions may fail silently. It proposes giving generated code planning authority only, while a fixed mediator adjudicates effects, and characterizes six conditions defining when this mediation is possible.
Problem
Irreversible effects and adversarial generators make validation by re-execution unavailable, while verification depends on assumptions that may fail during regeneration and execution.
Method
The generated component only proposes effects, while a fixed trusted mediator observes and checks intent, deltas, results, and durability before committing them.
Results
The paper instantiates mediation as a reference monitor for regenerated drivers and defines six effect-vocabulary conditions that determine its mediability envelope.
Takeaways & Limitations
Trust can be placed in effect authority held by a mediator rather than in regenerated code, but only at interfaces whose vocabulary supports the required checks.
Takeaways & Limitations
This position paper provides no formal semantics, mechanized proof, implementation, or measurement, and mediation becomes costly or infeasible when the mediator must reproduce too much of the implementation.
Abstract
from arXiv · showhide
Recent work uses large language models to generate systems code from specifications, treating the specification as the durable artifact and the implementation as disposable. Regenerating the implementation specializes it to each workload and device. However, that work lives in a forgiving setting: a component's externally visible effects, its writes and device commands, are recoverable, and the generator is honest, so trust is discharged by re-execution. We target the unforgiving setting: systems code whose effects are irreversible, produced by a generator that may be adversarial. There, re-execution cannot check an effect after the fact, and a proof fails silently when its assumptions do. We take the position that the only safe way to operate here is to deny the generated code the authority to act. The generated code only plans, while a fixed trusted mediator owns every effect and performs one only when the specification would have produced it. Because the guarantee lives in the mediator, not the code, it survives regeneration. We instantiate this as a reference monitor for regenerated device drivers, and characterize the mediability envelope, six conditions on the effect vocabulary: legibility, spec-input observability, correlatability, completeness, outcome enumerability, and explicit durability. They decide when such mediation is possible.
1 Generating Systems Components
Regenerated systems code enables workload- and hardware-specific specialization, but conventional trust mechanisms assume recoverable effects and an honest generator. This paper targets irreversible effects under adversarial generation, where re-execution cannot undo or validate what already reached the host.
- 1 Generating Systems Components: Regeneration lets systems components specialize to each deployment without manually editing the implementation.A model searches design choices for hardware and workload, then emits a new implementation per deployment.
- 1 Generating Systems Components: Prior approaches remain tractable because their externally visible effects are recoverable and their generators are treated as honest.Queries can be rerun, engines re-benchmarked, and wrong outputs recomputed, allowing validation by re-execution.
- 1 Generating Systems Components: Irreversible effects such as device commands, packet sends, and disk writes cannot be recalled once they reach the host.Therefore, re-execution cannot check an effect after the fact.
- 1 Generating Systems Components: An adversarial generator may emit native code that issues an out-of-spec effect, including through branches absent from test coverage.The threat includes compromised providers, poisoned training sets, and prompt injection.
- 1 Generating Systems Components: Device drivers provide the running example because they translate kernel block requests into device commands while managing queues, DMA, and interrupts.Their most dangerous effect, DMA into arbitrary host memory, is irreversible and unconfined by construction.
2 From Verification to Enforcement
The paper argues that verification alone is conditional on assumptions adversarial regeneration and irreversible effects can break. It instead removes effect authority from generated code and places runtime adjudication in a fixed mediator whose guarantee survives regeneration.
- 2 From Verification to Enforcement: A Byzantine generated component may compute arbitrarily, hide effects behind untested branches, and misreport every value it supplies.The threat model treats all component-provided values as untrusted.
- 2 From Verification to Enforcement: Verification alone can fail when proof, hardware-model, toolchain, or artifact-binding assumptions do not hold across regeneration.A broken assumption can leave the component able to commit an irreversible effect despite the proof.
- 2 From Verification to Enforcement: The generated component therefore acts only as a planner, while a fixed handwritten mediator owns and checks every effect against the specification and its state.The mediator refuses the effect at the last point where it can still be blocked.
- 2 From Verification to Enforcement: The mediator’s guarantee survives regeneration because its compiler checks the unchanged specification rather than repeatedly proving each regenerated implementation.A regenerated driver gains no authority merely by being regenerated.
- 2 From Verification to Enforcement: Verification can still be safe with a stack verified down to a trusted machine model, but under the target setting safety must rest on enforcement.Verification may improve availability by making proposals usually correct.
- 2 From Verification to Enforcement: The paper contributes an effect-authority framing, a reference monitor for regenerated drivers, and six conditions defining the mediability envelope.It is explicitly a position paper without formal semantics, mechanized proof, implementation, or measurement.
3 The Boundary, by Example
The driver can only observe state and propose commands; a trusted mediator validates each proposal against the specification before committing any irreversible effect. Tokens, serialized validation, and outcome handling prevent stale, replayed, or out-of-spec proposals from reaching the device.
- Proposal-commit separation: Proposal-commit separation confines the driver to Observe and Propose while the mediator alone owns the specification and effect primitives.The mediator commits only effects that refine the specification.
- Validation: Fresh sealed tokens bind proposals to one request and state snapshot, while commit-lock revalidation rejects replayed, expired, superseded, or stale proposals.Token consumption ensures one request cannot produce a second effect by replaying a token.
- Commit: The mediator classifies the trusted primitive’s actual outcome using the specification’s closed outcome set and records the corresponding abstract-state transition.A specified device error is committed and reported as an outcome, whereas validation failure occurs before the irreversible primitive runs.
- Validation: The mediator re-derives request-bound fields and checks freely chosen fields against the specification and observed abstract state.For WRITE, the pending request, queue slots, and DMA grants determine what may be committed.
- Catching a wrong write: A wrong LBA is rejected before the doorbell rings because the mediator compares the proposed command with the pending request that it holds.The same mechanism rejects wrong lengths or DMA sources, while invalid slots fail against the permitted set.
- Guarantee: Committed-trace safety requires complete mediation, trusted primitives, serialized commits, enumerable outcomes, explicit durability, and a stated crash model.The guarantee excludes liveness, availability, timing channels, and defects in the specification itself.
4 The Mediability Envelope
The mediability envelope specifies when a mediator can check effects at the specification’s interface without reconstructing the implementation. Six conditions divide into vocabulary properties and deployment requirements, with abstraction altitude determining feasibility and cost.
- Envelope: Mediability requires checking intent, changed state, reported results, and crash-surviving records at the specification’s abstraction altitude.The six conditions are legibility, spec-input observability, correlatability, completeness, outcome enumerability, and explicit durability.
- Vocabulary conditions: Legibility requires each effect to identify its operation independently, whereas block writes can represent several filesystem operations or corruption.Device commands such as WRITE are legible from their own encoding.
- Vocabulary conditions: Spec-input observability requires the mediator to see every input read by the specification, including caller credentials or authorized DMA sources.The block layer strips credentials needed for permission-dependent transitions.
- Vocabulary conditions: Correlatability requires effects to form per-operation transactions with recoverable ordering, which self-delimiting device commands provide but interleaved block writes do not.Commit serialization supplies ordering but cannot recover operation identity discarded by the vocabulary.
- Deployment conditions: Completeness requires every externally visible state change to cross the mediated boundary, excluding or reifying writable mappings and DMA paths.Any unmediated third path voids the safety guarantee.
- Deployment conditions: Outcome enumerability and explicit durability require closed primitive outcomes and first-class persistence effects such as flushes or barriers.A successful WRITE reaching the device does not by itself establish crash survival.
- Altitude and cost: At lower abstraction levels, mediation becomes reimplementation: block-layer checking must reconstruct read paths, concurrency control, recovery, intent, and authority.Altitude separates feasible checking from the economic cost of owning extensive standing state.
5 Related Work
Related approaches differ by when they check regenerated systems code and whether they check permission or correctness. The paper places its mediator in the commit-time, correctness-checking cell, emphasizing functional refinement at the specification interface.
- Design space: Table 1 organizes prior approaches by admission-time versus commit-time checking and permission versus correctness checking.Admission-time checks must be repeated after regeneration, while commit-time checks can remain in the mediator.
- Design space: Proof-based approaches certify artifacts before execution, but every regenerated implementation must re-earn its proof and satisfy the associated toolchain assumptions.The paper contrasts this with a mediator whose compiler checks the persistent specification.
- Design space: Policy approaches withhold authority and check whether effects are permitted, rather than checking whether they functionally refine the specification.The paper distinguishes permission enforcement from its own correctness-oriented mediation.
- Closest work: The closest driver work uses commit-time specification monitoring for device safety, whereas this paper checks functional refinement under on-demand driver regeneration.Both mediate interactions at commit, but their enforced properties differ.
- Adjacent work: Filesystem monitors such as Recon check metadata consistency and atomicity below specification altitude, so they catch structural corruption rather than permitted-but-wrong outcomes.The paper identifies altitude and caller-request visibility as the distinction.
- Adjacent work: Tool-boundary mediation for LLM agents operates above regenerated native systems code and generally assumes an honest generator.The paper targets adversarial generators acting through native systems components.
6 What a Realization Must Answer
A realization must address practical costs, adapter trust, availability, and unknown outcomes in addition to establishing mediability. These questions determine whether the proposed trust boundary remains viable in deployment.
- 6 What a Realization Must Answer: Four engineering questions extend beyond mediability: cost, adapter trust, availability, and unknown unknowns.They cover trusted-code size and latency, hardware-facing adapter assurance, Byzantine-component progress, and specification or outcome gaps.
- 6 What a Realization Must Answer: Mediator cost must remain bounded relative to the guarded component, with small abstract state and acceptable serialized-commit latency.If the mediator grows with the implementation, the mediability envelope was drawn at the wrong altitude.
- 6 What a Realization Must Answer: Each adapter that translates validated commands into register writes and DMA descriptors must be verified, audited, or excluded from the trusted base.The adapter is trusted code connecting each validated effect primitive to the device.
- 6 What a Realization Must Answer: Deployments need deadlines, budgets, or fallbacks because a Byzantine component can propose nothing, stall, or exhaust permitted choices.Availability remains a realization concern even when effects are mediated.
- 6 What a Realization Must Answer: Unknown outcomes and specification defects require fail-stop behavior because defects are enforced faithfully and unenumerated outcomes break outcome enumerability.The trust boundary is useful only when it survives regeneration without masking these failure modes.