{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T20:43:20Z","timestamp":1769978600141,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>\n\nOver 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 companies and users deploy. Without the aid of automation, ensuring the security of an ever-increasing number of deployments becomes more and more challenging. To the best of our knowledge, no formal automated technique currently exists to verify cloud deployments during the design phase. In this case study, we show that Description Logic modeling and inference capabilities can be used to improve the safety of cloud configurations. We focus on the Amazon Web Services (AWS) proprietary declarative language, CloudFormation, and develop a tool to encode template files into logic. We query the resulting models with properties related to security posture and report on our findings. By extending the models with dataflow-specific knowledge, we use more comprehensive semantic reasoning to further support security reviews. When applying the developed toolchain to publicly available deployment files, we find numerous violations of widely-recognized security best practices, which suggests that streamlining the methodologies developed for this case study would be beneficial.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_36","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"767-780","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning"],"prefix":"10.1007","author":[{"given":"Claudia","family":"Cauli","sequence":"first","affiliation":[]},{"given":"Meng","family":"Li","sequence":"additional","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Oksana","family":"Tkachuk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"36_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003)"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017)","DOI":"10.1017\/9781139025355"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Horrocks, I., Sattler, U.: Description logics. In: Handbook of Knowledge Representation, Foundations of Artificial Intelligence, vol. 3, pp. 135\u2013179. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03003-9"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-25543-5_14","volume-title":"Computer Aided Verification","author":"J Backes","year":"2019","unstructured":"Backes, J., et al.: Reachability analysis for AWS-based networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 231\u2013241. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_14"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Backes, J., et al.: Semantic-based automated reasoning for AWS access policies using SMT. In: FMCAD, pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"36_CR6","doi-asserted-by":"publisher","unstructured":"Binz, T., Breitenb\u00fccher, U., Kopp, O., Leymann, F.: TOSCA: portable automated deployment and management of cloud applications. In: Bouguettaya, A., Sheng, Q., Daniel, F. (eds.) Advanced Web Services, pp. 527\u2013549. Springer, New York (2014). https:\/\/doi.org\/10.1007\/978-1-4614-7535-4_22","DOI":"10.1007\/978-1-4614-7535-4_22"},{"issue":"2","key":"36_CR7","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2506164.2506167","volume":"47","author":"S Bouchenak","year":"2013","unstructured":"Bouchenak, S., Chockler, G.V., Chockler, H., Gheorghe, G., Santos, N., Shraer, A.: Verifying cloud services: present and future. Operating Syst. Rev. 47(2), 6\u201319 (2013)","journal-title":"Operating Syst. Rev."},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_25"},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27836-8_26","volume-title":"Automata, Languages and Programming","author":"G Bruns","year":"2004","unstructured":"Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281\u2013293. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_26"},{"key":"36_CR10","unstructured":"The AWS CloudFormation Linter (2020). https:\/\/github.com\/aws-cloudformation\/cfn-python-lint. Accessed 15 Oct 2020"},{"key":"36_CR11","unstructured":"The CFnNag Linting Tool (2020). https:\/\/github.com\/stelligent\/cfn_nag. Accessed 15 Oct 2020"},{"key":"36_CR12","unstructured":"Challita, S.: Inferring models from Cloud APIs and reasoning over them: a tooled and formal approach. (Inf\u00e9rer des mod\u00e8les \u00e0 partir d\u2019APIs cloud et raisonner dessus: une approche outill\u00e9e et formelle). Ph.D. thesis, Lille University of Science and Technology, France (2018)"},{"key":"36_CR13","unstructured":"Infrastructure Security, Compliance, and Governance (2020). http:\/\/www.cloudconformity.com\/. Accessed 04 Aug 2020"},{"key":"36_CR14","unstructured":"CloudFORMAL: Prototype Implementation. http:\/\/github.com\/claudiacauli\/CloudFORMAL. Accessed 15 Oct 2020"},{"key":"36_CR15","unstructured":"Resource Specification (2020). https:\/\/docs.aws.amazon.com\/AWSCloudFormation\/latest\/UserGuide\/cfn-resource-specification.html. Accessed 13 Aug 2020"},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-96145-3_3","volume-title":"Computer Aided Verification","author":"B Cook","year":"2018","unstructured":"Cook, B.: Formal reasoning about the security of Amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 38\u201347. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3"},{"key":"36_CR17","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: ASE, pp. 475\u2013476. IEEE Computer Society (2008)","DOI":"10.1109\/ASE.2008.78"},{"issue":"3","key":"36_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-014-9305-1","volume":"53","author":"B Glimm","year":"2014","unstructured":"Glimm, B., Horrocks, I., Motik, B., Stoilos, G., Wang, Z.: Hermit: An OWL 2 reasoner. J. Autom. Reason. 53(3), 245\u2013269 (2014)","journal-title":"J. Autom. Reason."},{"key":"36_CR19","unstructured":"Google Deployment Manager. https:\/\/cloud.google.com\/deployment-manager. Accessed 28 Jan 2021"},{"issue":"4","key":"36_CR20","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/j.websem.2008.05.001","volume":"6","author":"BC Grau","year":"2008","unstructured":"Grau, B.C., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P.F., Sattler, U.: OWL 2: the next step for OWL. J. Web Semant. 6(4), 309\u2013322 (2008)","journal-title":"J. Web Semant."},{"key":"36_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11817963_18","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Yasm: a software model-checker for verification and refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170\u2013174. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_18"},{"issue":"1","key":"36_CR22","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3233\/SW-2011-0025","volume":"2","author":"M Horridge","year":"2011","unstructured":"Horridge, M., Bechhofer, S.: The OWL API: a Java API for OWL ontologies. Semant. Web 2(1), 11\u201321 (2011)","journal-title":"Semant. Web"},{"issue":"1","key":"36_CR23","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/j.websem.2003.07.001","volume":"1","author":"I Horrocks","year":"2003","unstructured":"Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From SHIQ and RDF to OWL: the making of a web ontology language. J. Web Semant. 1(1), 7\u201326 (2003)","journal-title":"J. Web Semant."},{"key":"36_CR24","unstructured":"Kr\u00f6tzsch, M., Simancik, F., Horrocks, I.: A description logic primer. CoRR abs\/1201.4089 (2012)"},{"issue":"4","key":"36_CR25","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1093\/logcom\/6.4.523","volume":"6","author":"O Kupferman","year":"1996","unstructured":"Kupferman, O., Grumberg, O.: Buy one, get one free!!! J. Log. Comput. 6(4), 523\u2013539 (1996)","journal-title":"J. Log. Comput."},{"key":"36_CR26","unstructured":"McGuinness, D.L., Resnick, L.A., Isbell, C.L., Jr.: Description logic in practice: a classic application. In: IJCAI, pp. 2045\u20132046. Morgan Kaufmann (1995)"},{"issue":"4","key":"36_CR27","first-page":"333","volume":"12","author":"DL McGuinness","year":"1998","unstructured":"McGuinness, D.L., Wright, J.R.: Conceptual modelling for configuration: a description logic-based approach. AI EDAM 12(4), 333\u2013344 (1998)","journal-title":"AI EDAM"},{"key":"36_CR28","unstructured":"Microsoft Azure Resource Manager (2020). https:\/\/azure.microsoft.com\/en-us\/features\/resource-manager\/. Accessed 28 Jan 2021"},{"key":"36_CR29","unstructured":"Morris, K.: Infrastructure as Code: Managing Servers in the Cloud. O\u2019Reilly Media, Inc. (2016)"},{"issue":"4","key":"36_CR30","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/2757001.2757003","volume":"1","author":"MA Musen","year":"2015","unstructured":"Musen, M.A.: The prot\u00e9g\u00e9 project: a look back and a look forward. AI Matters 1(4), 4\u201312 (2015)","journal-title":"AI Matters"},{"key":"36_CR31","unstructured":"OWASP Ontology-driven Threat Modeling. https:\/\/github.com\/OWASP\/OdTM. Accessed 14 May 2021"},{"key":"36_CR32","unstructured":"Patel-Schneider, P., Grau, B.C., Motik, B.: OWL 2 web ontology language direct semantics (second edition). W3C recommendation, W3C (December 2012). http:\/\/www.w3.org\/TR\/2012\/REC-owl2-direct-semantics-20121211\/"},{"key":"36_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-45744-5_7","volume-title":"Automated Reasoning","author":"U Sattler","year":"2001","unstructured":"Sattler, U., Vardi, M.Y.: The hybrid $${\\mu }$$-calculus. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 76\u201391. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_7"},{"issue":"1","key":"36_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M Schmidt-Schau\u00df","year":"1991","unstructured":"Schmidt-Schau\u00df, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1\u201326 (1991)","journal-title":"Artif. Intell."},{"key":"36_CR35","unstructured":"Multi-cloud Security Auditing Tool (2020). http:\/\/github.com\/nccgroup\/ScoutSuite. Accessed 4 Aug 2020"},{"issue":"2","key":"36_CR36","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.websem.2007.03.004","volume":"5","author":"E Sirin","year":"2007","unstructured":"Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: a practical OWL-DL reasoner. J. Web Semant. 5(2), 51\u201353 (2007)","journal-title":"J. Web Semant."},{"key":"36_CR37","unstructured":"Terraform. https:\/\/www.terraform.io\/. Accessed 28 Jan 2021"},{"key":"36_CR38","unstructured":"Static Analysis Security Scanner for Terraform (2020). https:\/\/tfsec.dev\/. Accessed 10 May 2021"},{"key":"36_CR39","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292\u2013297. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_26"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:10:55Z","timestamp":1626480655000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}