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…
Every application deployed on Amazon Web Services (AWS) requires Identity and Access Management (IAM) policies that specify which API actions the application is authorized to perform. AWS offers managed policies as a convenience to simplify policy authoring. However, these policies are designed to cover common scenarios which can lead to unnecessarily broad permissions beyond what a specific use …
Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guara…
Cedar is a popular authorization language designed to support sound and complete policy analysis by reduction to SMT. But building these analyses is error-prone: subtle encoding mistakes can silently compromise soundness or completeness, and are hard to catch through testing alone. Cedar's high-assurance development process therefore requires writing and maintaining formal proofs of correctn…
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates co…
Large Language Models (LLMs) are increasingly integrated into software systems as automated decision-making components. These systems rely on instruction prompts written in natural language to encode complex workflows. However, debugging these prompts when LLMs produce undesired outputs remains challenging due to their black-box nature and the impracticality of manually inspecting large, complex …
The results of software verification are only as trustworthy as the provided specification. Errors or incompleteness in the specification can result in unwarranted confidence in the implementation. Previous work, particularly in the realm of model checking, has investigated a notion of coverage in verification. Portions of the system that could be replaced arbitrarily without causing verification…
All critical systems must evolve to meet the needs of a growing and diversifying user base. But supporting that evolution is challenging at increasing scale: Maintainers must find a way to ensure that each change does only what is intended, and will not inadvertently change behavior for existing users. This paper presents how we addressed this challenge for the Amazon Web Services (AWS) authoriza…
We introduce SMT-D, a tool for portfolio-based distributed SMT solving. We propose a general architecture consisting of two main components: (i) solvers extended with the capability of sharing and importing information on the fly while solving; and (ii) a central manager that orchestrates and monitors solvers while also deciding which information to share with which solvers. We introduce new info…
As cloud computing gains widespread adoption across various industries, securing cloud resources has become a top priority for cloud providers. However, ensuring configuration security among highly interconnected cloud resources is challenging due to the complexities of resource modeling, correlation analysis, and large-scale security checks. To tackle those practical challenges, we propose Secur…
