Infrastructure as Code is a popular approach to computing infrastructure management that allows users to leverage tools such as version control, automatic deployments, and program analysis for infrastructure configurations. Benefits of IaC are well-known among practitioners: the entire infrastructure is described accurately by a configuration file, making it easy to debug or visualize the infrastructure. The infrastructure can be version controlled and documented as with any other programming language. The tools help guarantee identical configuration of hosts, making it an essential practice for security and maintainability.However, during an upgrade, the infrastructure goes through a series of partial updates. When not properly configured, some of these partial updates might contain a violation of the intended security policy,even if the initial infrastructure and the target infrastructure are both perfectly secure. An attacker could perform a “sniping attack” during the upgrade to access information or gain control of infrastructure they would normally not be able to. We empirically validated our claims by reenacting this in both Amazon’s AWS and Google Cloud.

In this work we have modeled IaC configurations as a dataflow graph between resources, where edges are protected by security resources. We use this representation to compute the intended security policy for the initial and target deployments and their resources. We statically analyze the two infrastructures and build a safe over-approximation of the possible intermediate states. We use this over-approximation to compute an under-approximation of the security level of resources, in any possible intermediate state.If a resource is more secure or as secure as its counter part in the initial or target deployment,the tool does not report any warnings. If a resource is less secure than intended, the tool reports a potential vulnerability and suggests adding a dependency to ensure IaC tools will follow a secure upgrade plan.