一句话：提出领域特定语言 ControlsDSL 编写云合规控制，借助 SMT 分析自动生成测试与场景并证明其可靠且完备。
云服务商依赖合规控制来确保客户资源配置符合安全最佳实践，但现有控制多以 Python、Java 等通用程序编写，难以分析、穷尽测试与维护。本文提出 ControlsDSL，一种用于编写合规控制的领域特定语言。其受限语义支持基于可满足性模理论（SMT）的分析：自动生成测试输入、验证不同控制版本间的语义等价、并支持场景生成。给定一条控制，ControlsDSL 会产出人类可读的场景集合，描述所有可能的执行路径及其预期结果，作者证明所生成场景既是可靠的（能准确预测控制行为），也是完备的（每个良类型输入至少被一个场景覆盖）。在 AWS 生产环境部署的 397 条控制上评估表明，ControlsDSL 表达力充足，控制比对应的 Python/Java 实现简洁 3.3 倍，支撑每日超十亿次合规评估；绝大多数控制的场景生成在一秒内完成，SMT 测试生成达到完全路径覆盖，中位控制数秒完成，复杂控制存在分钟级长尾。
Cloud providers rely on compliance controls to ensure that customer resources are configured according to security best practices -- from encryption of storage to network isolation of compute instances. Today, these controls are typically written as general-purpose programs (e.g., in Python or Java), making them difficult to analyze, test exhaustively, and maintain. We present ControlsDSL, a domain-specific language for writing compliance controls. ControlsDSL's restricted semantics enables analysis based on Satisfiability Modulo Theories (SMT), generating test inputs automatically, verifying semantic equivalence between control versions, and supporting scenario generation. Given a control, ControlsDSL produces a set of human-readable scenarios that describe every possible execution path and its expected result. We prove that generated scenarios are sound (they accurately predict the control's behavior) and complete (every well-typed input is covered by at least one scenario). We evaluate ControlsDSL on 397 compliance controls deployed in production at Amazon Web Services (AWS), demonstrating its expressiveness, the effectiveness of scenario generation, and the practical value of SMT-based analysis for control development and migration. ControlsDSL controls serve over one billion daily compliance evaluations and are 3.3x more concise than their Python/Java counterparts. Scenario generation completes in under one second for the vast majority of controls, and SMT-based test generation achieves complete path coverage—completing in seconds for the median control, with a heavy tail (minutes) for the more complex controls.
@inproceedings{paperbot12531,
title = {ControlsDSL: A Language for Verifiable Cloud Configuration Controls},
author = {Miyriee Alair and Shrutarshi Basu and Sean Cai and Loris D'Antoni and Julio Delgado Jr. and Antonio Filieri and Andrew Gacek and Anand Goyal and Sebastiaan Joosten and Varad Panch and Sorawee Porncharoenwase and Vishwanath Raman and Niloofar Razavi and Neha Rungta and Mike Schliep and Preethi Sekaran and Chase Johnson},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834488}
}