Continuous Compliance
Martin Kellogg, Martin Schäf, Serdar Tasiran, Michael D. Ernst
Abstract
Vendors who wish to provide software or services to large corporations and governments must often obtain numerous certificates of compliance. Each certificate asserts that the software satisfies a compliance regime, like SOC or the PCI DSS, to protect the privacy and security of sensitive data. The industry standard for obtaining a compliance certificate is an auditor manually auditing source code. This approach is expensive, error-prone, partial, and prone to regressions. We propose continuous compliance to guarantee that the codebase stays compliant on each code change using lightweight verification tools. Continuous compliance increases assurance and reduces costs. Continuous compliance is applicable to any source-code compliance requirement. To illustrate our approach, we built verification tools for five common audit controls related to data security: cryptographically unsafe algorithms must not be used, keys must be at least 256 bits long, credentials must not be hard-coded into program text, HTTPS must always be used instead of HTTP, and cloud data stores must not be world-readable. We evaluated our approach in three ways. ( 1 ) We applied our tools to over 5 million lines of open-source software. (2) We compared our tools to other publicly-available tools for detecting misuses of encryption on a previously-published benchmark, finding that only ours are suitable for continuous compliance. (3) We deployed a continuous compliance process at AWS, a large cloudservices company: we integrated verification tools into the compliance process (including auditors accepting their output as evidence) and ran them on over 68 million lines of code. Our tools and the data for the former two evaluations are publicly available. CCS CONCEPTS • Software and its engineering → Software verification; Automated static analysis; Data types and structures.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 681dfc04-0bb9-4d1f-8dbc-77a7cf68b290Cited by top-tier papers3
- Pluggable Type Inference for FreeMartin Kellogg, Daniel Daskiewicz, Loi Ngo Duc Nguyen, Muyeed Ahmed et al.ASE 2023 · 4 citations
- Static Program Reduction via Type-Directed SlicingLoi Ngo Duc Nguyen, Tahiatul Islam, Theron Wang, Sam Lenz et al.ISSTA 2025
- Verifying the Option Type with Rely-Guarantee ReasoningJames Yoo, Michael D. Ernst, René JustASE 2024
Builds on3
- CryptoGuard: High Precision Detection of Cryptographic Vulnerabilities in Massive-sized Java ProjectsSazzadur Rahaman, Ya Xiao, Sharmin Afrose, Fahad Shaon et al.CCS 2019 · 159 citations
- Security Certification in Payment Card Industry: Testbeds, Measurements, and RecommendationsSazzadur Rahaman, Gang Wang, Danfeng Daphne YaoCCS 2019 · 31 citations
- Verifying object constructionMartin Kellogg, Manli Ran, Manu Sridharan, Martin Schäf et al.ICSE 2020 · 10 citations
Related papers
- C-Verifier: Understanding and Formally Verifying Cross-Service Flaws in AWS CognitoZhen Chen, Ze Jin, Le Gong, Kexin Chen et al.S&P 2026
- Finding 709 Defects in 258 Projects: An Experience Report on Applying CodeQL to Open-Source Embedded Software (Experience Paper)Mingjie Shen, Akul Abhilash Pillai, Brian A. Yuan, James C. Davis et al.ISSTA 2025 · 1 citation
- Growlithe: A Developer-Centric Compliance Tool for Serverless ApplicationsPraveen Gupta, Arshia Moghimi, Devam Sisodraker, Mohammad Shahrad et al.S&P 2025
- Formally Verified Cloud-Scale AuthorizationAleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks et al.ICSE 2025 · 1 citation
- Continuous Intrusion: Characterizing the Security of Continuous Integration ServicesYacong Gu, Lingyun Ying, Huajun Chai, Chu Qiao et al.S&P 2023
