Over the past ten years, the adoption of cloud services has grown rapidly, leading to the introduction of automated deployment tools to address the scale and complexity of the infrastructure that companies and users deploy. The practice of con guring, deploying, and updating systems resources from source code les is known as Infrastructure as Code (IaC) [17]. In addition to instructions relevant for resource creation, dependencies, and updates, IaC con guration les contain information about settings, data ow, and access control. Without the aid of automation, ensuring the security of such deployments becomes more and more challenging. In this study, we focus on the rst IaC tool ever introduced: Amazon Web Services' CloudFormation. In particular, we investigate the application of description logics to the formalization and reasoning over IaC deployments. We are interested in three aspects: (i) whether proposed cloud IaC con gurations comply with security best practices, (ii) how to aid users in building more secure infrastructure before deploying it, and (iii) to what extent formal automated techniques can support manual pre-deployment security reviews. We provide a framework to encode IaC into description logic, and investigate its e ectiveness in answering con guration queries and reasoning about data ow, trust boundaries, and potential issues within the system. Speci cally, we test DLs reasoning capabilities to infer new facts about underspeci ed resources (such as those not included in a given deployment but used by it) and leverage DLs open-world assumption to perform veri cation and refutation, depending on the property being checked. We formalize additional security knowledge that allows for checking system-level semantic properties; i.e., properties that consider the nature of the cloud environment and more complex reachability over an inferred graph representation of the infrastructure. Formalizing and Encoding Infrastructure as Code According to the IaC paradigm, resources are deployed on the cloud by writing one or more JSON-formatted con guration les, by which users con gure settings and communication of the desired instances. Con guration les must validate against the resource speci cations [10], which are les prescribing resource properties and their allowed values.
In this study, we formalized both con guration les and resource speci cations,
and encoded these into assertional and terminological knowledge, respectively.
Checking Compliance to Security Requirements We query the resulting models
with properties related to the security posture of the infrastructure being
deployed. Properties are grouped into three categories: security issues, mitigations,
and global protections, which we view in analogy to must and may speci cations,
which one would use to express that an issue may be present (vs. must be
absent) or that a protection must be in place (vs. may be missing). Di erent query
structure and pass/fail logic characterize each property type. We implement
the encoding and the security properties veri cation procedures in a
publiclyavailable tool, CloudFORMAL [
To the best of our knowledge, no formal automated technique currently exists to
verify cloud deployments during the design phase. Formal reasoning techniques
have been successfully applied to di erent aspects of the cloud, e.g. networks
and access policies [
All the results in this study can be generalized to other existing IaC frameworks. We plan to continue researching for an even better- tting description logic Security Assessment for Cloud Services through Semantic Reasoning formalism, query language, three-valued semantics, and decision procedures for veri cation and falsi cation of properties relevant to security analyses, such as data ows, trust boundaries, and threat modeling.