{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T20:37:42Z","timestamp":1791491862918,"version":"4.3.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","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,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"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>Infrastructure as Code is a new approach to computing infrastructure management that allows users to leverage tools such as version control, automatic deployments, and program analysis for infrastructure configurations. This approach allows for faster and more homogeneous configuration of a complete infrastructure. Infrastructure as Code languages, such as CloudFormation or TerraForm, use a declarative model so that users only need to describe the desired state of the infrastructure. However, in practice, these languages are not processed atomically. During an upgrade, the infrastructure goes through a series of intermediate states. We identify a security vulnerability that occurs during an upgrade even when the initial and final states of the infrastructure are secure, and we show that those vulnerability are possible in Amazon\u2019s AWS and Google Cloud. We call such attacks intra-update sniping vulnerabilities. In order to mitigate this shortcoming, we present a technique that detects such vulnerabilities and pinpoints the root causes of insecure deployment migrations. We implement this technique in a tool, H\u00e4yh\u00e4, that uses dataflow graph analysis. We evaluate our tool on a set of open-source CloudFormation templates and find that it is scalable and could be used as part of a deployment workflow.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_6","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"105-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2284-5488","authenticated-orcid":false,"given":"Julien","family":"Lepiller","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8646-4364","authenticated-orcid":false,"given":"Mark","family":"Santolucito","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"6_CR1","unstructured":"Julian Wood: Building well-architected serverless applications: Controlling serverless API access. AWS Compute Blog, https:\/\/aws.amazon.com\/blogs\/compute\/building-well-architected-serverless-applications-controlling-serverless-api-access-part-1\/"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Al-Shaer, E., Marrero, W., El-Atawy, A., ElBadawi, K.: Network configuration in a box: towards end-to-end verification of network reachability and security. In: 2009 17th IEEE International Conference on Network Protocols (2009)","DOI":"10.1109\/ICNP.2009.5339690"},{"key":"6_CR3","unstructured":"Amazon.com Inc: CloudFormation, aws.amazon.com"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using smt. In: 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (2014)","DOI":"10.1145\/2594291.2594317"},{"key":"6_CR6","unstructured":"Chef misc Inc: Chef, https:\/\/www.chef.io"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Cito, J., Schermann, G., Wittern, J.E., Leitner, P., Zumberi, S., Gall, H.C.: An empirical analysis of the docker container ecosystem on github. In: 2017 IEEE\/ACM 14th International Conference on Mining Software Repositories (MSR). IEEE (2017)","DOI":"10.1109\/MSR.2017.67"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Continella, A., Polino, M., Pogliani, M., Zanero, S.: There\u2019s a hole in that bucket! a large-scale analysis of misconfigured S3 buckets. In: Proceedings of the 34th Annual Computer Security Applications Conference. ACSAC \u201918, Association for Computing Machinery, New York, NY, USA (2018)","DOI":"10.1145\/3274694.3274736"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Cook, B.: Formal reasoning about the security of amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification (CAV). Springer International Publishing (2018)","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the 4th Symp. on Principles of Programming Languages. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"6_CR11","unstructured":"Hashicorp: Terraform, https:\/\/www.terraform.io"},{"key":"6_CR12","unstructured":"Hashicorp: What is mutable vs. immutable infrastructure?, https:\/\/www.hashicorp.com\/resources\/what-is-mutable-vs-immutable-infrastructure\/"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Huang, W., Ganjali, A., Kim, B.H., Oh, S., Lie, D.: The state of public infrastructure-as-a-service cloud security. ACM Comput. Surv. 47(4) (Jun 2015)","DOI":"10.1145\/2767181"},{"key":"6_CR14","unstructured":"Hummer, W., Rosenberg, F., Oliveira, F., Eilam, T.: Testing idempotence for infrastructure as code. In: ACM\/IFIP\/USENIX International Conference on Distributed Systems Platforms and Open Distributed Processing. Springer (2013)"},{"key":"6_CR15","unstructured":"Ian Mckay: S3 Bucket Namesquatting - Abusing predictable S3 bucket names, https:\/\/onecloudplease.com\/blog\/s3-bucket-namesquatting"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Ponce-de Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: Portability analysis for weak memory models porthos: One tool for all models. In: Ranzato, F. (ed.) Static Analysis Symposium. pp. 299\u2013320. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-66706-5_15"},{"key":"6_CR17","unstructured":"Lepiller, J., Piskac, R., Sch\u00e4f, M., Santolucito, M.: H\u00e4yh\u00e4 (2021), https:\/\/gitlab.com\/rose-yale\/hayha"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Liu, J., Hallahan, W., Schlesinger, C., Sharif, M., Lee, J., Soul\u00e9, R., Wang, H., Ca\u015fcaval, C., McKeown, N., Foster, N.: P4v: Practical verification for programmable data planes. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. SIGCOMM \u201918, Association for Computing Machinery, New York, NY, USA (2018)","DOI":"10.1145\/3230543.3230582"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Meshman, Y., Dan, A.M., Vechev, M.T., Yahav, E.: Synthesis of memory fences via refinement propagation. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11\u201313, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8723, pp. 237\u2013252. Springer (2014)","DOI":"10.1007\/978-3-319-10936-7_15"},{"key":"6_CR20","unstructured":"Michael DeHaan and Contributors: Ansible, https:\/\/www.ansible.com"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Parker, J., Vazou, N., Hicks, M.: Lweb: Information flow security for multi-tier web applications. Proc. ACM Program. Lang. 3(POPL) (Jan 2019)","DOI":"10.1145\/3290388"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Piskac, R.: New applications of software synthesis: Verification of configuration files and firewall repair. In: Podelski, A. (ed.) Static Analysis Symposium (SAS). Springer International Publishing (2018)","DOI":"10.1007\/978-3-319-99725-4_6"},{"key":"6_CR23","unstructured":"Puppet Inc: Puppet, https:\/\/www.puppet.com"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Raad, A., Doko, M., Ro\u017ei\u0107, L., Lahav, O., Vafeiadis, V.: On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3(POPL) (Jan 2019). https:\/\/doi.org\/10.1145\/3290381, https:\/\/doi.org\/10.1145\/3290381","DOI":"10.1145\/3290381"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Rahman, A., Parnin, C., Williams, L.: The seven sins: Security smells in infrastructure as code scripts. In: 2019 IEEE\/ACM 41st International Conference on misc Engineering (ICSE) (2019)","DOI":"10.1109\/ICSE.2019.00033"},{"key":"6_CR26","unstructured":"Rahman, A.A.U., Williams, L.: misc security in devops: Synthesizing practitioners\u2019 perceptions and practices. In: 2016 IEEE\/ACM International Workshop on Continuous misc Evolution and Delivery (CSED) (2016)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Rahman, A., Parnin, C., Williams, L.: The seven sins: security smells in infrastructure as code scripts. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE). pp. 164\u2013175. IEEE (2019)","DOI":"10.1109\/ICSE.2019.00033"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Santolucito, M., Zhai, E., Dhodapkar, R., Shim, A., Piskac, R.: Synthesizing configuration file specifications with association rule learning. Proceedings of the ACM on Programming Languages 1(OOPSLA) (2017)","DOI":"10.1145\/3133888"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Santolucito, M., Zhai, E., Piskac, R.: Probabilistic automated language learning for configuration files. In: International Conference on Computer Aided Verification. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_5"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Shambaugh, R., Weiss, A., Guha, A.: Rehearsal: A configuration verification tool for puppet. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2016)","DOI":"10.1145\/2908080.2908083"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:10:04Z","timestamp":1616436604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_6","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":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"141","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":"41","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":"21","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":"29% - 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":"The conference changed to an online format due to the COVID-19 pandemic","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)"}}]}}