不要信任代码，要检查其效果：对抗性生成器下再生系统代码的运行时精化
Don't Trust the Code, Check Its Effects: Runtime Refinement for Regenerated Systems Code Under an Adversarial Generator
浏览论文内容
中文总结 AI 辅助
针对对抗性生成器生成的效果不可逆的再生系统代码，本文提出由固定可信中介执行效果的运行时精化方法，并刻画了可中介性范围的六个条件，以保障系统安全。
中文摘要 AI 辅助
近期研究使用大语言模型从规格生成系统代码，将规格视为持久产物，实现视为可丢弃的内容，再生实现可针对每个工作负载和设备进行专门化。但该研究处于宽容环境：组件的外部可见效果（其写入操作和设备命令）可恢复，且生成器是诚实的，因此通过重新执行即可确认信任。本文针对的是不宽容环境：效果不可逆的系统代码，由可能具有对抗性的生成器生成。在这种环境下，重新执行无法事后检查效果，且证明会在假设不成立时静默失败。本文认为，在此类环境下唯一安全的操作方式是剥夺生成代码的执行权限：生成代码仅负责规划，而固定的可信中介拥有所有效果，仅在规格会产生该效果时才执行它。由于保证存在于中介而非代码中，因此可在再生后保留。本文将其实例化为再生设备驱动的引用监视器，并刻画了可中介性范围，即对效果词汇的六个条件：可读性、规格输入可观测性、相关性、完整性、结果可枚举性和显式持久性，这些条件决定了此类中介是否可行。
英文摘要
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.
发表机构
- Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
- University of Toronto（多伦多大学）
机构由 AI 辅助整理，请以论文原文为准。
