{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:33Z","timestamp":1750309353717,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":71,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,11,4]],"date-time":"2024-11-04T00:00:00Z","timestamp":1730678400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1942219","CNS-2106751","CNS-2106388","CNS-2214272"],"award-info":[{"award-number":["CNS-1942219","CNS-2106751","CNS-2106388","CNS-2214272"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,11,4]]},"DOI":"10.1145\/3694715.3695974","type":"proceedings-article","created":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T19:28:18Z","timestamp":1731698898000},"page":"574-589","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-9328-3205","authenticated-orcid":false,"given":"Yiming","family":"Qiu","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, US"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4944-8706","authenticated-orcid":false,"given":"Patrick Tser Jern","family":"Kon","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, US"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7844-2026","authenticated-orcid":false,"given":"Ryan","family":"Beckett","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, US"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8326-8124","authenticated-orcid":false,"given":"Ang","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, US"}]}],"member":"320","published-online":{"date-parts":[[2024,11,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"AWS cloud development kit. https:\/\/github.com\/aws\/aws-cdk."},{"key":"e_1_3_2_1_2_1","unstructured":"AWS CloudFormation. https:\/\/aws.amazon.com\/cloudformation\/."},{"key":"e_1_3_2_1_3_1","unstructured":"Azure Bicep. https:\/\/learn.microsoft.com\/en-us\/azure\/azure-resource-manager\/bicep\/."},{"key":"e_1_3_2_1_4_1","unstructured":"Azure site-to-site VPN connection. https:\/\/learn.microsoft.com\/en-us\/azure\/vpn-gateway\/tutorial-site-to-site-portal."},{"key":"e_1_3_2_1_5_1","unstructured":"Azure SQL Managed Instance management. https:\/\/learn.microsoft.com\/en-us\/azure\/azure-sql\/managed-instance\/management-operations-overview?view=azuresql."},{"key":"e_1_3_2_1_6_1","unstructured":"Azure Storage Account Redundancy. https:\/\/learn.microsoft.com\/en-us\/azure\/storage\/common\/storage-account-overview."},{"key":"e_1_3_2_1_7_1","unstructured":"Azure subscription and service limits quotas and constraints. https:\/\/learn.microsoft.com\/en-us\/azure\/azure-resource-manager\/management\/azure-subscription-service-limits."},{"key":"e_1_3_2_1_8_1","unstructured":"Checking for IaC Programs where APPGW uses Basic IP Address with Dynamic Allocation Method. https:\/\/github.com\/search?q=azurerm_public_ip+allocation_method++Dynamic+NOT+static+azurerm_application_gateway+resource+NOT+each+language%3AHCL+&type=code."},{"key":"e_1_3_2_1_9_1","unstructured":"Checking for IaC Programs where APPGW with non-WAF v2 sku uses Web Application Firewall. https:\/\/github.com\/search?q=waf_configuration+NOT+WAF_v2+azurerm_application_gateway++NOT+variable+NOT+output+language%3AHCL+&type=code."},{"key":"e_1_3_2_1_10_1","unstructured":"Checking for IaC Programs where the Request Routing Rule of Standard v2 APPGW does not Specify Priority. https:\/\/github.com\/search?q=+azurerm_application_gateway+request_routing_rule+NOT+priority+Standard_v2+language%3AHCL&type=code."},{"key":"e_1_3_2_1_11_1","unstructured":"Checkov: ship code that's secure by default. https:\/\/bridgecrew.io\/checkov\/."},{"key":"e_1_3_2_1_12_1","unstructured":"Cloud development kit for terraform. https:\/\/developer.hashicorp.com\/terraform\/cdktf."},{"key":"e_1_3_2_1_13_1","unstructured":"Example Usage within azurerm_application_gateway Documentation Cannot be Deployed Successfully. https:\/\/github.com\/hashicorp\/terraform-provider-azurerm\/issues\/27065."},{"key":"e_1_3_2_1_14_1","unstructured":"Example Usage within azurerm_dedicated_hardware_security_moduleDocumentation Cannot be Deployed Successfully. https:\/\/github.com\/hashicorp\/terraform-provider-azurerm\/issues\/27078."},{"key":"e_1_3_2_1_15_1","unstructured":"Example Usage within azurerm_mssql_database Documentation Cannot be Deployed Successfully. https:\/\/github.com\/hashicorp\/terraform-provider-azurerm\/issues\/27194."},{"key":"e_1_3_2_1_16_1","unstructured":"Example Usage within azurerm_network_interface_application_gateway_backend_address_pool_association Documentation Cannot be Deployed Successfully. https:\/\/github.com\/hashicorp\/terraform-provider-azurerm\/issues\/27222."},{"key":"e_1_3_2_1_17_1","unstructured":"Microsoft Azure Fsv2-series VM. https:\/\/learn.microsoft.com\/en-us\/azure\/virtual-machines\/fsv2-series."},{"key":"e_1_3_2_1_18_1","unstructured":"Opa's native query language rego. https:\/\/www.openpolicyagent.org\/docs\/latest\/policy-language\/."},{"key":"e_1_3_2_1_19_1","unstructured":"Open world assumptions. https:\/\/www.sciencedirect.com\/topics\/computer-science\/open-world-assumption."},{"key":"e_1_3_2_1_20_1","unstructured":"OpenTofu: The open source infrastructure as code tool. https:\/\/opentofu.org\/."},{"key":"e_1_3_2_1_21_1","unstructured":"Pulumi ai. https:\/\/www.pulumi.com\/ai."},{"key":"e_1_3_2_1_22_1","unstructured":"Pulumi: Infrastructure as code in any programming language. https:\/\/www.pulumi.com\/."},{"key":"e_1_3_2_1_23_1","unstructured":"Regions for virtual machines in azure. https:\/\/learn.microsoft.com\/en-us\/azure\/virtual-machines\/regions#special-azure-regions."},{"key":"e_1_3_2_1_24_1","unstructured":"Shift testing left with unit tests. https:\/\/learn.microsoft.com\/en-us\/devops\/develop\/shift-left-make-testing-fast-reliable."},{"key":"e_1_3_2_1_25_1","unstructured":"Terraform by Hashicorp. https:\/\/www.terraform.io\/."},{"key":"e_1_3_2_1_26_1","unstructured":"Terraform Resource: Manages the association between a Network Interface and a Application Gateway's Backend Address Pool. https:\/\/registry.terraform.io\/providers\/hashicorp\/azurerm\/3.97.0\/docs\/resources\/network_interface_application_gateway_backend_address_pool_association."},{"key":"e_1_3_2_1_27_1","unstructured":"Terraform v.s. alternatives. https:\/\/developer.hashicorp.com\/terraform\/intro\/vs\/cloudformation."},{"key":"e_1_3_2_1_28_1","unstructured":"Terrascan: Detect compliance and security violations across Infrastructure as Code to mitigate risk before provisioning cloud native infrastructure. https:\/\/runterrascan.io\/."},{"key":"e_1_3_2_1_29_1","unstructured":"TFLint: A Pluggable Terraform Linter. https:\/\/github.com\/terraform-linters\/tflint."},{"key":"e_1_3_2_1_30_1","unstructured":"TFSec: Security Scanner for Your Terraform Code. https:\/\/github.com\/aquasecurity\/tfsec."},{"key":"e_1_3_2_1_31_1","unstructured":"Zodiac: Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs. https:\/\/github.com\/824728350\/Zodiac."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503275"},{"key":"e_1_3_2_1_33_1","volume-title":"20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23)","author":"Arashloo Mina Tahmasbi","year":"2023","unstructured":"Mina Tahmasbi Arashloo, Ryan Beckett, and Rachit Agarwal. Formal methods for network performance analysis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), 2023."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00083"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST46399.2020.00046"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_37_1","volume-title":"A review on fact extraction and verification. ACM Computing Surveys (CSUR), 55(1):1--35","author":"Bekoulis Giannis","year":"2021","unstructured":"Giannis Bekoulis, Christina Papagiannopoulou, and Nikos Deligiannis. A review on fact extraction and verification. ACM Computing Surveys (CSUR), 55(1):1--35, 2021."},{"key":"e_1_3_2_1_38_1","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Campbell Eric Hayden","year":"2021","unstructured":"Eric Hayden Campbell, William T Hallahan, Priya Srikumar, Carmelo Cascone, Jed Liu, Vignesh Ramamurthy, Hossein Hojjat, Ruzica Piskac, Robert Soul\u00e9, and Nate Foster. Avenir: Managing data plane diversity with control plane synthesis. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21), 2021."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_36"},{"key":"e_1_3_2_1_40_1","volume-title":"The daikon system for dynamic detection of likely invariants. Science of computer programming, 69(1-3):35--45","author":"Ernst Michael D","year":"2007","unstructured":"Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Science of computer programming, 69(1-3):35--45, 2007."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2017.12.047"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523450"},{"key":"e_1_3_2_1_45_1","volume-title":"18th USENIX symposium on networked systems design and implementation (NSDI 21)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. Finding invariants of distributed systems: It's a small (enough) world after all. In 18th USENIX symposium on networked systems design and implementation (NSDI 21), 2021."},{"key":"e_1_3_2_1_46_1","volume-title":"Challenges and applications of large language models. arXiv preprint arXiv:2307.10169","author":"Kaddour Jean","year":"2023","unstructured":"Jean Kaddour, Joshua Harris, Maximilian Mozes, Herbie Bradley, Roberta Raileanu, and Robert McHardy. Challenges and applications of large language models. arXiv preprint arXiv:2307.10169, 2023."},{"key":"e_1_3_2_1_47_1","volume-title":"Alessandro Orso. Adaptive REST API Testing with Reinforcement Learning. In IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Kim Myeongsoo","year":"2023","unstructured":"Myeongsoo Kim, Saurabh Sinha, and Alessandro Orso. Adaptive REST API Testing with Reinforcement Learning. In IEEE\/ACM International Conference on Automated Software Engineering (ASE), 2023."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635890"},{"key":"e_1_3_2_1_49_1","volume-title":"Towards few-shot fact-checking via perplexity. arXiv preprint arXiv:2103.09535","author":"Lee Nayeon","year":"2021","unstructured":"Nayeon Lee, Yejin Bang, Andrea Madotto, Madian Khabsa, and Pascale Fung. Towards few-shot fact-checking via perplexity. arXiv preprint arXiv:2103.09535, 2021."},{"key":"e_1_3_2_1_50_1","volume-title":"Language models as fact checkers? arXiv preprint arXiv:2006.04102","author":"Lee Nayeon","year":"2020","unstructured":"Nayeon Lee, Belinda Z Li, Sinong Wang, Wen-tau Yih, Hao Ma, and Madian Khabsa. Language models as fact checkers? arXiv preprint arXiv:2006.04102, 2020."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.238"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_6"},{"key":"e_1_3_2_1_53_1","first-page":"9459","article-title":"Retrieval-augmented generation for knowledgeintensive nlp tasks","volume":"33","author":"Lewis Patrick","year":"2020","unstructured":"Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich K\u00fcttler, Mike Lewis, Wen-tau Yih, Tim Rockt\u00e4schel, et al. Retrieval-augmented generation for knowledgeintensive nlp tasks. Advances in Neural Information Processing Systems, 33:9459--9474, 2020.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464799"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.abq1158"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_57_1","volume-title":"USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Mehta Sonu","year":"2020","unstructured":"Sonu Mehta, Ranjita Bhagwan, Rahul Kumar, Chetan Bansal, Chandra Maddila, Balasubramanyan Ashok, Sumit Asthana, Christian Bird, and Aditya Kumar. Rex: Preventing bugs and misconfiguration in large services using correlated change analysis. In USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), 2020."},{"key":"e_1_3_2_1_58_1","volume-title":"20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23)","author":"Qiu Yiming","year":"2023","unstructured":"Yiming Qiu, Ryan Beckett, and Ang Chen. Synthesizing runtime programmable switch updates. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), 2023."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411763.3451760"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133888"},{"key":"e_1_3_2_1_61_1","volume-title":"Computer Aided Verification: 28th International Conference, (CAV 16), Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part II 28","author":"Santolucito Mark","year":"2016","unstructured":"Mark Santolucito, Ennan Zhai, and Ruzica Piskac. Probabilistic automated language learning for configuration files. In Computer Aided Verification: 28th International Conference, (CAV 16), Toronto, ON, Canada, July 17--23, 2016, Proceedings, Part II 28. Springer, 2016."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2017.11.007"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST46399.2020.00024"},{"key":"e_1_3_2_1_64_1","volume-title":"6th Symposium on Operating Systems Design & Implementation (OSDI 04)","author":"Wang Helen J.","year":"2004","unstructured":"Helen J. Wang, John C. Platt, Yu Chen, Ruyun Zhang, and Yi-Min Wang. Automatic misconfiguration troubleshooting with PeerPressure. In 6th Symposium on Operating Systems Design & Implementation (OSDI 04), 2004."},{"key":"e_1_3_2_1_65_1","volume-title":"Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203.11171","author":"Wang Xuezhi","year":"2022","unstructured":"Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203.11171, 2022."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510151"},{"key":"e_1_3_2_1_67_1","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), 2022."},{"key":"e_1_3_2_1_68_1","volume-title":"15th USENIX symposium on operating systems design and implementation (OSDI 21)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. Distai:data-driven automated invariant learning for distributed protocols. In 15th USENIX symposium on operating systems design and implementation (OSDI 21), 2021."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485517"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541983"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771817"}],"event":{"name":"SOSP '24: ACM SIGOPS 30th Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"],"location":"Austin TX USA","acronym":"SOSP '24"},"container-title":["Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3694715.3695974","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3694715.3695974","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3694715.3695974","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:48Z","timestamp":1750291548000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3694715.3695974"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,4]]},"references-count":71,"alternative-id":["10.1145\/3694715.3695974","10.1145\/3694715"],"URL":"https:\/\/doi.org\/10.1145\/3694715.3695974","relation":{},"subject":[],"published":{"date-parts":[[2024,11,4]]},"assertion":[{"value":"2024-11-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}