{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T16:59:05Z","timestamp":1770224345531,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":107,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T00:00:00Z","timestamp":1667779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-2145675 CCF-2124225"],"award-info":[{"award-number":["CNS-2145675 CCF-2124225"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Youth Innovation Promotion Association CAS","award":["2019163"],"award-info":[{"award-number":["2019163"]}]},{"name":"Strategic Priority Research Program of Chinese Academy of Sciences","award":["XDC02040100"],"award-info":[{"award-number":["XDC02040100"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,11,7]]},"DOI":"10.1145\/3548606.3560680","type":"proceedings-article","created":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T11:41:28Z","timestamp":1667821288000},"page":"1647-1661","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["P-Verifier"],"prefix":"10.1145","author":[{"given":"Ze","family":"Jin","sequence":"first","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences & School of Cyber Security, University of Chinese Academy of Sciences & Indiana University Bloomington, Beijing, China"}]},{"given":"Luyi","family":"Xing","sequence":"additional","affiliation":[{"name":"Indiana University Bloomington, Bloomington, IN, USA"}]},{"given":"Yiwei","family":"Fang","sequence":"additional","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences & School of Cyber Security, University of Chinese Academy of Sciences & Indiana University Bloomington, Beijing, China"}]},{"given":"Yan","family":"Jia","sequence":"additional","affiliation":[{"name":"Nankai University, Tianjin, China"}]},{"given":"Bin","family":"Yuan","sequence":"additional","affiliation":[{"name":"HuaZhong University of Science and Technology, Wuhan, China"}]},{"given":"Qixu","family":"Liu","sequence":"additional","affiliation":[{"name":"Institute of Information Engineering, Chinese Academy of Sciences & School of Cyber Security, University of Chinese Academy of Sciences, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2022,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2019. MQTT Version 5.0. https:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v5.0\/mqttv5.0.html.  2019. MQTT Version 5.0. https:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v5.0\/mqttv5.0.html."},{"key":"e_1_3_2_1_2_1","first-page":"2019","article-title":"Publish--subscribe pattern. https:\/\/en.wikipedia.org\/wiki\/Publishsubscribe_pattern","year":"2019","unstructured":"2019 . Publish--subscribe pattern. https:\/\/en.wikipedia.org\/wiki\/Publishsubscribe_pattern . Accessed : 2019 - 2007 . 2019. Publish--subscribe pattern. https:\/\/en.wikipedia.org\/wiki\/Publishsubscribe_pattern. Accessed: 2019-07.","journal-title":"Accessed"},{"key":"e_1_3_2_1_3_1","unstructured":"2020. Security Best Practices for Amazon S3. https:\/\/techcommunity.microsoft. com\/t5\/azure-architecture-blog\/azure-policy-prevent-the-use-of-wildcardfor-source-in-azure\/ba-p\/1783844.  2020. Security Best Practices for Amazon S3. https:\/\/techcommunity.microsoft. com\/t5\/azure-architecture-blog\/azure-policy-prevent-the-use-of-wildcardfor-source-in-azure\/ba-p\/1783844."},{"key":"e_1_3_2_1_4_1","unstructured":"2021. Air Puri!er o$cial page. https:\/\/molekule.com\/.  2021. Air Puri!er o$cial page. https:\/\/molekule.com\/."},{"key":"e_1_3_2_1_5_1","unstructured":"2021. Molekule Air Mini Receives FDA clearance to destroy viruses and bacteria. https:\/\/molekule.science\/molekule-air-mini-receives-fda-510k-clearance\/.  2021. Molekule Air Mini Receives FDA clearance to destroy viruses and bacteria. https:\/\/molekule.science\/molekule-air-mini-receives-fda-510k-clearance\/."},{"key":"e_1_3_2_1_6_1","volume-title":"MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols. In 30th USENIX Security Symposium (USENIX Security 21)","unstructured":"2021. MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols. In 30th USENIX Security Symposium (USENIX Security 21) . USENIX Association. https:\/\/www.usenix.org\/conference\/ usenixsecurity21\/presentation\/wan-qinying 2021. MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association. https:\/\/www.usenix.org\/conference\/ usenixsecurity21\/presentation\/wan-qinying"},{"key":"e_1_3_2_1_7_1","unstructured":"2021. Security best practices in AWS IoT Core. https:\/\/docs.aws.amazon.com\/ iot\/latest\/developerguide\/security-best-practices.html.  2021. Security best practices in AWS IoT Core. https:\/\/docs.aws.amazon.com\/ iot\/latest\/developerguide\/security-best-practices.html."},{"key":"e_1_3_2_1_8_1","unstructured":"2022. Automata theory . https:\/\/en.wikipedia.org\/wiki\/Automata_theory.  2022. Automata theory . https:\/\/en.wikipedia.org\/wiki\/Automata_theory."},{"key":"e_1_3_2_1_9_1","unstructured":"2022. Avoiding wildcard permissions in IAM policies. https:\/\/docs.aws.amazon. com\/lambda\/latest\/operatorguide\/wildcard-permissions-iam.html.  2022. Avoiding wildcard permissions in IAM policies. https:\/\/docs.aws.amazon. com\/lambda\/latest\/operatorguide\/wildcard-permissions-iam.html."},{"key":"e_1_3_2_1_10_1","unstructured":"2022. AWS IoT Core. https:\/\/aws.amazon.com\/en\/iot-core\/.  2022. AWS IoT Core. https:\/\/aws.amazon.com\/en\/iot-core\/."},{"key":"e_1_3_2_1_11_1","unstructured":"2022. AWS IoT Core endpoints and quotas. https:\/\/docs.aws.amazon.com\/ general\/latest\/gr\/iot-core.html#security-limits\/.  2022. AWS IoT Core endpoints and quotas. https:\/\/docs.aws.amazon.com\/ general\/latest\/gr\/iot-core.html#security-limits\/."},{"key":"e_1_3_2_1_12_1","unstructured":"2022. AWS IoT Core policy variables - AWS IoT Core. https:\/\/docs.aws.amazon. com\/iot\/latest\/developerguide\/iot-policy-variables.html.  2022. AWS IoT Core policy variables - AWS IoT Core. https:\/\/docs.aws.amazon. com\/iot\/latest\/developerguide\/iot-policy-variables.html."},{"key":"e_1_3_2_1_13_1","unstructured":"2022. AWS IoT Defender. https:\/\/docs.aws.amazon.com\/iot\/latest\/ developerguide\/device-defender.html.  2022. AWS IoT Defender. https:\/\/docs.aws.amazon.com\/iot\/latest\/ developerguide\/device-defender.html."},{"key":"e_1_3_2_1_14_1","unstructured":"2022. AWS IoT o$cial documentation about thing registry. https:\/\/docs.aws. amazon.com\/iot\/latest\/developerguide\/thing-registry.html.  2022. AWS IoT o$cial documentation about thing registry. https:\/\/docs.aws. amazon.com\/iot\/latest\/developerguide\/thing-registry.html."},{"key":"e_1_3_2_1_15_1","unstructured":"2022. AWS IoT policies overly permissive. https:\/\/docs.aws.amazon.com\/iot\/ latest\/developerguide\/audit-chk-iot-policy-permissive.html.  2022. AWS IoT policies overly permissive. https:\/\/docs.aws.amazon.com\/iot\/ latest\/developerguide\/audit-chk-iot-policy-permissive.html."},{"key":"e_1_3_2_1_16_1","unstructured":"2022. AWS IoT Policy actions. https:\/\/docs.aws.amazon.com\/iot\/latest\/ developerguide\/iot-policy-actions.html.  2022. AWS IoT Policy actions. https:\/\/docs.aws.amazon.com\/iot\/latest\/ developerguide\/iot-policy-actions.html."},{"key":"e_1_3_2_1_17_1","unstructured":"2022. AWS Publish\/Subscribe IoT policy examples. https:\/\/docs.aws.amazon. com\/iot\/latest\/developerguide\/pub-sub-policy.html.  2022. AWS Publish\/Subscribe IoT policy examples. https:\/\/docs.aws.amazon. com\/iot\/latest\/developerguide\/pub-sub-policy.html."},{"key":"e_1_3_2_1_18_1","unstructured":"2022. AWS python SDK boto3 IoT api attach policy. https: \/\/boto3.amazonaws.com\/v1\/documentation\/api\/latest\/reference\/services\/ iot.html#IoT.Client.attach_policy.  2022. AWS python SDK boto3 IoT api attach policy. https: \/\/boto3.amazonaws.com\/v1\/documentation\/api\/latest\/reference\/services\/ iot.html#IoT.Client.attach_policy."},{"key":"e_1_3_2_1_19_1","unstructured":"2022. AWS S3 Policy Example. https:\/\/docs.aws.amazon.com\/AmazonS3\/latest\/ userguide\/example-policies-s3.html.  2022. AWS S3 Policy Example. https:\/\/docs.aws.amazon.com\/AmazonS3\/latest\/ userguide\/example-policies-s3.html."},{"key":"e_1_3_2_1_20_1","unstructured":"2022. AWS SDK for Android - 2.22.1. https:\/\/aws-amplify.github.io\/aws-sdkandroid\/docs\/reference\/.  2022. AWS SDK for Android - 2.22.1. https:\/\/aws-amplify.github.io\/aws-sdkandroid\/docs\/reference\/."},{"key":"e_1_3_2_1_21_1","unstructured":"2022. Azure IoT Hub. https:\/\/azure.microsoft.com\/en-us\/services\/iot-hub\/.  2022. Azure IoT Hub. https:\/\/azure.microsoft.com\/en-us\/services\/iot-hub\/."},{"key":"e_1_3_2_1_22_1","unstructured":"2022. Azure Policy de!nition structure. https:\/\/docs.microsoft.com\/en-us\/azure\/ governance\/policy\/concepts\/de!nition-structure.  2022. Azure Policy de!nition structure. https:\/\/docs.microsoft.com\/en-us\/azure\/ governance\/policy\/concepts\/de!nition-structure."},{"key":"e_1_3_2_1_23_1","unstructured":"2022. Azure Policy Example. https:\/\/github.com\/Azure\/azure-policy.  2022. Azure Policy Example. https:\/\/github.com\/Azure\/azure-policy."},{"key":"e_1_3_2_1_24_1","unstructured":"2022. Biobeat o$cial page. https:\/\/www.bio-beat.com\/.  2022. Biobeat o$cial page. https:\/\/www.bio-beat.com\/."},{"key":"e_1_3_2_1_25_1","unstructured":"2022. Broiking o$cial page. https:\/\/broilkingbbq.com\/.  2022. Broiking o$cial page. https:\/\/broilkingbbq.com\/."},{"key":"e_1_3_2_1_26_1","unstructured":"2022. Controlling access to a bucket with user policies. https:\/\/docs.aws.amazon. com\/AmazonS3\/latest\/userguide\/walkthrough1.html.  2022. Controlling access to a bucket with user policies. https:\/\/docs.aws.amazon. com\/AmazonS3\/latest\/userguide\/walkthrough1.html."},{"key":"e_1_3_2_1_27_1","unstructured":"2022. Dynamodb Policy Example. https:\/\/docs.aws.amazon.com\/IAM\/latest\/ UserGuide\/reference_policies_examples_dynamodb_speci!c-table.html.  2022. Dynamodb Policy Example. https:\/\/docs.aws.amazon.com\/IAM\/latest\/ UserGuide\/reference_policies_examples_dynamodb_speci!c-table.html."},{"key":"e_1_3_2_1_28_1","unstructured":"2022. eXtensible Access Control Markup Language (XACML) Version 3.0. http: \/\/docs.oasis-open.org\/xacml\/3.0\/xacml-3.0-core-spec-os-en.html.  2022. eXtensible Access Control Markup Language (XACML) Version 3.0. http: \/\/docs.oasis-open.org\/xacml\/3.0\/xacml-3.0-core-spec-os-en.html."},{"key":"e_1_3_2_1_29_1","unstructured":"2022. Failing Security|CISA. https:\/\/us-cert.cisa.gov\/bsi\/articles\/knowledge\/ principles\/failing-securely.  2022. Failing Security|CISA. https:\/\/us-cert.cisa.gov\/bsi\/articles\/knowledge\/ principles\/failing-securely."},{"key":"e_1_3_2_1_30_1","unstructured":"2022. Github o$cial page. https:\/\/github.com.  2022. Github o$cial page. https:\/\/github.com."},{"key":"e_1_3_2_1_31_1","unstructured":"2022. IAM JSON policy elements: Resource. https:\/\/docs.aws.amazon.com\/IAM\/ latest\/UserGuide\/reference_policies_elements_resource.html.  2022. IAM JSON policy elements: Resource. https:\/\/docs.aws.amazon.com\/IAM\/ latest\/UserGuide\/reference_policies_elements_resource.html."},{"key":"e_1_3_2_1_32_1","unstructured":"2022. KISS Principle. https:\/\/en.wikipedia.org\/wiki\/KISS_principle.  2022. KISS Principle. https:\/\/en.wikipedia.org\/wiki\/KISS_principle."},{"key":"e_1_3_2_1_33_1","unstructured":"2022. Kubernetes' ABAC access control. https:\/\/kubernetes.io\/docs\/reference\/ access-authn-authz\/abac\/.  2022. Kubernetes' ABAC access control. https:\/\/kubernetes.io\/docs\/reference\/ access-authn-authz\/abac\/."},{"key":"e_1_3_2_1_34_1","unstructured":"2022. Least privilege. https:\/\/en.wikipedia.org\/wiki\/Principle_of_least_ privilege.  2022. Least privilege. https:\/\/en.wikipedia.org\/wiki\/Principle_of_least_ privilege."},{"key":"e_1_3_2_1_35_1","unstructured":"2022. MQTT Version 3.1.1 speci!cation. http:\/\/docs.oasis-open.org\/mqtt\/mqtt\/ v3.1.1\/os\/mqtt-v3.1.1-os.html.  2022. MQTT Version 3.1.1 speci!cation. http:\/\/docs.oasis-open.org\/mqtt\/mqtt\/ v3.1.1\/os\/mqtt-v3.1.1-os.html."},{"key":"e_1_3_2_1_36_1","unstructured":"2022. P3P Language. https:\/\/www.w3.org\/TR\/P3P-preferences\/.  2022. P3P Language. https:\/\/www.w3.org\/TR\/P3P-preferences\/."},{"key":"e_1_3_2_1_37_1","unstructured":"2022. Policies and permissions in IAM. https:\/\/docs.aws.amazon.com\/IAM\/ latest\/UserGuide\/access_policies.html.  2022. Policies and permissions in IAM. https:\/\/docs.aws.amazon.com\/IAM\/ latest\/UserGuide\/access_policies.html."},{"key":"e_1_3_2_1_38_1","unstructured":"2022. Publish and subscribe with Azure IoT Edge | Microsoft Docs . https:\/\/docs.microsoft.com\/en-us\/azure\/iot-edge\/how-to-publish-subscribe\" view=iotedge-2020--11.  2022. Publish and subscribe with Azure IoT Edge | Microsoft Docs . https:\/\/docs.microsoft.com\/en-us\/azure\/iot-edge\/how-to-publish-subscribe\" view=iotedge-2020--11."},{"key":"e_1_3_2_1_39_1","unstructured":"2022. Rules for AWS IoT - AWS IoT Core. https:\/\/docs.aws.amazon.com\/iot\/ latest\/developerguide\/iot-rules.html.  2022. Rules for AWS IoT - AWS IoT Core. https:\/\/docs.aws.amazon.com\/iot\/ latest\/developerguide\/iot-rules.html."},{"key":"e_1_3_2_1_40_1","unstructured":"2022. Scaling authorization policies with AWS IoT Core. https:\/\/aws.amazon. com\/blogs\/iot\/scaling-authorization-policies-with-aws-iot-core\/.  2022. Scaling authorization policies with AWS IoT Core. https:\/\/aws.amazon. com\/blogs\/iot\/scaling-authorization-policies-with-aws-iot-core\/."},{"key":"e_1_3_2_1_41_1","unstructured":"2022. Security Best Practices for Amazon S3. https:\/\/docs.aws.amazon.com\/ AmazonS3\/latest\/userguide\/security-best-practices.html.  2022. Security Best Practices for Amazon S3. https:\/\/docs.aws.amazon.com\/ AmazonS3\/latest\/userguide\/security-best-practices.html."},{"key":"e_1_3_2_1_42_1","unstructured":"2022. Sun-Pro google play store page. https:\/\/play.google.com\/store\/apps\/ details\"id=com.SunProtection.  2022. Sun-Pro google play store page. https:\/\/play.google.com\/store\/apps\/ details\"id=com.SunProtection."},{"key":"e_1_3_2_1_43_1","unstructured":"2022. Supporting website for P-Veri!er. https:\/\/sites.google.com\/view\/p-verify\/ home.  2022. Supporting website for P-Veri!er. https:\/\/sites.google.com\/view\/p-verify\/ home."},{"key":"e_1_3_2_1_44_1","unstructured":"2022. Tuya IoT Cloud. https:\/\/www.tuya.com\/.  2022. Tuya IoT Cloud. https:\/\/www.tuya.com\/."},{"key":"e_1_3_2_1_45_1","unstructured":"2022. Using provable security to enhance IoT -- An industry di#erentiator. https:\/\/docs.aws.amazon.com\/whitepapers\/latest\/securing-iot-with-aws\/ using-provable-security-to-enhance-iot-an-industry-di#erentiator.html.  2022. Using provable security to enhance IoT -- An industry di#erentiator. https:\/\/docs.aws.amazon.com\/whitepapers\/latest\/securing-iot-with-aws\/ using-provable-security-to-enhance-iot-an-industry-di#erentiator.html."},{"key":"e_1_3_2_1_46_1","unstructured":"2022. What is Amazon CloudWatch Logs\" https:\/\/docs.aws.amazon.com\/ AmazonCloudWatch\/latest\/logs\/WhatIsCloudWatchLogs.html.  2022. What is Amazon CloudWatch Logs\" https:\/\/docs.aws.amazon.com\/ AmazonCloudWatch\/latest\/logs\/WhatIsCloudWatchLogs.html."},{"key":"e_1_3_2_1_47_1","unstructured":"2022. Wikipedia page Deterministic !nite automaton. https:\/\/en.wikipedia.org\/ wiki\/Deterministic_!nite_automaton.  2022. Wikipedia page Deterministic !nite automaton. https:\/\/en.wikipedia.org\/ wiki\/Deterministic_!nite_automaton."},{"key":"e_1_3_2_1_48_1","unstructured":"2022. XACML policy language OASIS standard. http:\/\/docs.oasis-open.org\/ xacml\/3.0\/xacml-3.0-core-spec-os-en.html.  2022. XACML policy language OASIS standard. http:\/\/docs.oasis-open.org\/ xacml\/3.0\/xacml-3.0-core-spec-os-en.html."},{"key":"e_1_3_2_1_49_1","unstructured":"2022. Z3 String Constraint Solver. https:\/\/z3string.github.io\/.  2022. Z3 String Constraint Solver. https:\/\/z3string.github.io\/."},{"key":"e_1_3_2_1_50_1","unstructured":"2022. Z3Py. https:\/\/ericpony.github.io\/z3py-tutorial\/guide-examples.htm.  2022. Z3Py. https:\/\/ericpony.github.io\/z3py-tutorial\/guide-examples.htm."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Ava Ahadipour and Martin Schanzenbach. 2017. A Survey on Authorization in Distributed Systems: Information Storage Data Retrieval and Trust Evaluation. In 2017 IEEE Trustcom\/BigDataSE\/ICESS. 1016--1023. https:\/\/doi.org\/10.1109\/ Trustcom\/BigDataSE\/ICESS.2017.346  Ava Ahadipour and Martin Schanzenbach. 2017. A Survey on Authorization in Distributed Systems: Information Storage Data Retrieval and Trust Evaluation. In 2017 IEEE Trustcom\/BigDataSE\/ICESS. 1016--1023. https:\/\/doi.org\/10.1109\/ Trustcom\/BigDataSE\/ICESS.2017.346","DOI":"10.1109\/Trustcom\/BigDataSE\/ICESS.2017.346"},{"key":"e_1_3_2_1_52_1","volume-title":"SoK: Security Evaluation of Home-Based IoT Deployments. In 2019 IEEE Symposium on Security and Privacy (SP). 1362--1380","author":"Alrawi Omar","year":"2019","unstructured":"Omar Alrawi , Chaz Lever , Manos Antonakakis , and Fabian Monrose . 2019 . SoK: Security Evaluation of Home-Based IoT Deployments. In 2019 IEEE Symposium on Security and Privacy (SP). 1362--1380 . https:\/\/doi.org\/10.1109\/SP.2019.00013 10.1109\/SP.2019.00013 Omar Alrawi, Chaz Lever, Manos Antonakakis, and Fabian Monrose. 2019. SoK: Security Evaluation of Home-Based IoT Deployments. In 2019 IEEE Symposium on Security and Privacy (SP). 1362--1380. https:\/\/doi.org\/10.1109\/SP.2019.00013"},{"key":"e_1_3_2_1_53_1","volume-title":"International Conference on Computer Aided Veri!cation. Springer, 165--176","author":"Backes John","year":"2020","unstructured":"John Backes , Ulises Berrueco , Tyler Bray , Daniel Brim , Byron Cook , Andrew Gacek , Ranjit Jhala , Kasper Luckow , Sean McLaughlin , Madhav Menon , 2020 . Strati!ed abstraction of access control policies . In International Conference on Computer Aided Veri!cation. Springer, 165--176 . John Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Luckow, Sean McLaughlin, Madhav Menon, et al. 2020. Strati!ed abstraction of access control policies. In International Conference on Computer Aided Veri!cation. Springer, 165--176."},{"key":"e_1_3_2_1_54_1","volume-title":"FMCAD 2018","author":"Backes John","year":"2018","unstructured":"John Backes , Pauline Bolignano , Byron Cook , Catherine Dodge , Andrew Gacek , Kasper S\u00f8e Luckow , Neha Rungta , Oksana Tkachuk , and Carsten Varming . 2018 . Semantic-based Automated Reasoning for AWS Access Policies using SMT. In 2018 Formal Methods in Computer Aided Design , FMCAD 2018 , Austin, TX, USA, October 30 - November 2, 2018, Nikolaj Bj\u00f8rner and Arie Gur!nkel (Eds.). IEEE, 1--9. https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994 10.23919\/FMCAD.2018.8602994 John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper S\u00f8e Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming. 2018. Semantic-based Automated Reasoning for AWS Access Policies using SMT. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, Nikolaj Bj\u00f8rner and Arie Gur!nkel (Eds.). IEEE, 1--9. https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243841"},{"key":"e_1_3_2_1_56_1","volume-title":"17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004","author":"Moritz","year":"2004","unstructured":"Moritz Y. Becker and Peter Sewell. 2004. Cassandra: Flexible Trust Management, Applied to Electronic Health Records . In 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004 ), 28--30 June 2004 , Paci!c Grove, CA, USA. IEEE Computer Society, 139--154. https:\/\/doi.org\/10.1109\/CSFW. 2004.7 10.1109\/CSFW.2004.7 Moritz Y. Becker and Peter Sewell. 2004. Cassandra: Flexible Trust Management, Applied to Electronic Health Records. In 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28--30 June 2004, Paci!c Grove, CA, USA. IEEE Computer Society, 139--154. https:\/\/doi.org\/10.1109\/CSFW.2004.7"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2004.22"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-64701-2_57"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1996.502679"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409728"},{"key":"e_1_3_2_1_62_1","volume-title":"Sensitive Information Tracking in Commodity IoT. arXiv preprint arXiv:1802.08307","author":"Celik Z Berkay","year":"2018","unstructured":"Z Berkay Celik , Leonardo Babun , Amit K Sikder , Hidayet Aksu , Gang Tan , Patrick McDaniel , and A Selcuk Uluagac . 2018. Sensitive Information Tracking in Commodity IoT. arXiv preprint arXiv:1802.08307 ( 2018 ). Z Berkay Celik, Leonardo Babun, Amit K Sikder, Hidayet Aksu, Gang Tan, Patrick McDaniel, and A Selcuk Uluagac. 2018. Sensitive Information Tracking in Commodity IoT. arXiv preprint arXiv:1802.08307 (2018)."},{"key":"e_1_3_2_1_63_1","volume-title":"Soteria: Automated IoT Safety and Security Analysis. In 2018 USENIX Annual Technical Conference (USENIX ATC 18)","author":"Celik Z. Berkay","year":"2018","unstructured":"Z. Berkay Celik , Patrick McDaniel , and Gang Tan . 2018 . Soteria: Automated IoT Safety and Security Analysis. In 2018 USENIX Annual Technical Conference (USENIX ATC 18) . Boston, MA, 147--158. Z. Berkay Celik, Patrick McDaniel, and Gang Tan. 2018. Soteria: Automated IoT Safety and Security Analysis. In 2018 USENIX Annual Technical Conference (USENIX ATC 18). Boston, MA, 147--158."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Z Berkay Celik Gang Tan and Patrick D McDaniel. 2019. IoTGuard: Dynamic Enforcement of Security and Safety Policy in Commodity IoT.. In NDSS.  Z Berkay Celik Gang Tan and Patrick D McDaniel. 2019. IoTGuard: Dynamic Enforcement of Security and Safety Policy in Commodity IoT.. In NDSS.","DOI":"10.14722\/ndss.2019.23326"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3423339"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN48063.2020.00056"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2002.1004365"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243865"},{"key":"e_1_3_2_1_69_1","volume-title":"IOTSAFE: Enforcing Safety and Security Policy with Real IoT Physical Interaction Discovery.","author":"Ding Wenbo","year":"2021","unstructured":"Wenbo Ding , Hongxin Hu , and Long Cheng . 2021 . IOTSAFE: Enforcing Safety and Security Policy with Real IoT Physical Interaction Discovery. (2021). Wenbo Ding, Hongxin Hu, and Long Cheng. 2021. IOTSAFE: Enforcing Safety and Security Policy with Real IoT Physical Interaction Discovery. (2021)."},{"key":"e_1_3_2_1_70_1","volume-title":"Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006, Proceedings (Lecture Notes in Computer Science","volume":"646","author":"Dougherty Daniel J.","year":"2006","unstructured":"Daniel J. Dougherty , Kathi Fisler , and Shriram Krishnamurthi . 2006 . Specifying and Reasoning About Dynamic Access-Control Policies. In Automated Reasoning , Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006, Proceedings (Lecture Notes in Computer Science , Vol. 4130), Ulrich Furbach and Natarajan Shankar (Eds.). Springer, 632-- 646 . Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2006. Specifying and Reasoning About Dynamic Access-Control Policies. In Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4130), Ulrich Furbach and Natarajan Shankar (Eds.). Springer, 632--646."},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510233"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.44"},{"key":"e_1_3_2_1_73_1","volume-title":"Decentralized Action Integrity for Trigger-Action IoT Platforms. In 22nd Network and Distributed Security Symposium (NDSS","author":"Fernandes Earlence","year":"2018","unstructured":"Earlence Fernandes , Amir Rahmati , Jaeyeon Jung , and Atul Prakash . 2018 . Decentralized Action Integrity for Trigger-Action IoT Platforms. In 22nd Network and Distributed Security Symposium (NDSS 2018). Earlence Fernandes, Amir Rahmati, Jaeyeon Jung, and Atul Prakash. 2018. Decentralized Action Integrity for Trigger-Action IoT Platforms. In 22nd Network and Distributed Security Symposium (NDSS 2018)."},{"key":"e_1_3_2_1_74_1","volume-title":"27th International Conference on Software Engineering (ICSE 2005","author":"Fisler Kathi","year":"2005","unstructured":"Kathi Fisler , Shriram Krishnamurthi , Leo A. Meyerovich , and Michael Carl Tschantz . 2005 . Veri!cation and change-impact analysis of access-control policies . In 27th International Conference on Software Engineering (ICSE 2005 ), 15--21 May 2005, St. Louis, Missouri, USA, Gruia-Catalin Roman, William G. Griswold, and Bashar Nuseibeh (Eds.). ACM, 196--205. Kathi Fisler, Shriram Krishnamurthi, Leo A. Meyerovich, and Michael Carl Tschantz. 2005. Veri!cation and change-impact analysis of access-control policies. In 27th International Conference on Software Engineering (ICSE 2005), 15--21 May 2005, St. Louis, Missouri, USA, Gruia-Catalin Roman, William G. Griswold, and Bashar Nuseibeh (Eds.). ACM, 196--205."},{"key":"e_1_3_2_1_75_1","volume-title":"Model-Checking Access Control Policies","author":"Guelev Dimitar P.","unstructured":"Dimitar P. Guelev , Mark Ryan , and Pierre Yves Schobbens . 2004. Model-Checking Access Control Policies . In Information Security, Kan Zhang and Yuliang Zheng (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 219--230. Dimitar P. Guelev, Mark Ryan, and Pierre Yves Schobbens. 2004. Model-Checking Access Control Policies. In Information Security, Kan Zhang and Yuliang Zheng (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 219--230."},{"key":"e_1_3_2_1_76_1","volume-title":"SkillExplorer: Understanding the Behavior of Skills in Large Scale. In 29th USENIX Security Symposium (USENIX Security 20)","author":"Guo Zhixiu","year":"2020","unstructured":"Zhixiu Guo , Zijin Lin , Pan Li , and Kai Chen . 2020 . SkillExplorer: Understanding the Behavior of Skills in Large Scale. In 29th USENIX Security Symposium (USENIX Security 20) . 2649--2666. Zhixiu Guo, Zijin Lin, Pan Li, and Kai Chen. 2020. SkillExplorer: Understanding the Behavior of Skills in Large Scale. In 29th USENIX Security Symposium (USENIX Security 20). 2649--2666."},{"key":"e_1_3_2_1_77_1","volume-title":"Automated repair by example for !rewalls. In 2017 Formal Methods in Computer Aided Design (FMCAD)","author":"Hallahan William T","unstructured":"William T Hallahan , Ennan Zhai , and Ruzica Piskac . 2017. Automated repair by example for !rewalls. In 2017 Formal Methods in Computer Aided Design (FMCAD) . IEEE , 220--229. William T Hallahan, Ennan Zhai, and Ruzica Piskac. 2017. Automated repair by example for !rewalls. In 2017 Formal Methods in Computer Aided Design (FMCAD). IEEE, 220--229."},{"key":"e_1_3_2_1_78_1","volume-title":"Art Manion, and Chris King","author":"Householder Allen D","year":"2017","unstructured":"Allen D Householder , Garret Wassermann , Art Manion, and Chris King . 2017 . The cert guide to coordinated vulnerability disclosure. Technical Report. CarnegieMellon Univ Pittsburgh Pa Pittsburgh United States . Allen D Householder, Garret Wassermann, Art Manion, and Chris King. 2017. The cert guide to coordinated vulnerability disclosure. Technical Report. CarnegieMellon Univ Pittsburgh Pa Pittsburgh United States."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPW50608.2020.00029"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0087-9"},{"key":"e_1_3_2_1_81_1","unstructured":"Andrew Hunt. 1900. The pragmatic programmer. Pearson Education India.  Andrew Hunt. 1900. The pragmatic programmer. Pearson Education India."},{"key":"e_1_3_2_1_82_1","volume-title":"Automated analysis and debugging of network connectivity policies. Microsoft Research","author":"Jayaraman Karthick","year":"2014","unstructured":"Karthick Jayaraman , Nikolaj Bj\u00f8rner , Geo# Outhred, and Charlie Kaufman . 2014. Automated analysis and debugging of network connectivity policies. Microsoft Research ( 2014 ), 1--11. Karthick Jayaraman, Nikolaj Bj\u00f8rner, Geo# Outhred, and Charlie Kaufman. 2014. Automated analysis and debugging of network connectivity policies. Microsoft Research (2014), 1--11."},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00051"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23051"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2001.924291"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/ENABL.2003.1231406"},{"key":"e_1_3_2_1_87_1","volume-title":"Skill Squatting Attacks on Amazon Alexa. In 27th USENIX Security Symposium (USENIX Security 18)","author":"Kumar Deepak","year":"2018","unstructured":"Deepak Kumar , Riccardo Paccagnella , Paul Murley , Eric Hennenfent , Joshua Mason , Adam Bates , and Michael Bailey . 2018 . Skill Squatting Attacks on Amazon Alexa. In 27th USENIX Security Symposium (USENIX Security 18) . Baltimore, MD, 33--47. Deepak Kumar, Riccardo Paccagnella, Paul Murley, Eric Hennenfent, Joshua Mason, Adam Bates, and Michael Bailey. 2018. Skill Squatting Attacks on Amazon Alexa. In 27th USENIX Security Symposium (USENIX Security 18). Baltimore, MD, 33--47."},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/605434.605438"},{"key":"e_1_3_2_1_89_1","volume-title":"Mitchell","author":"Li Ninghui","year":"2003","unstructured":"Ninghui Li and John C . Mitchell . 2003 . Datalog with Constraints : A Foundation for Trust Management Languages. In Practical Aspects of Declarative Languages, Veronica Dahl and Philip Wadler (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 58--73. Ninghui Li and John C. Mitchell. 2003. Datalog with Constraints: A Foundation for Trust Management Languages. In Practical Aspects of Declarative Languages, Veronica Dahl and Philip Wadler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 58--73."},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/1237500.1237501"},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3427228.3427250"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCNC.2015.7158101"},{"key":"e_1_3_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993601"},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1109\/POLICY.2002.1011295"},{"key":"e_1_3_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/3432233"},{"key":"e_1_3_2_1_96_1","unstructured":"William Stallings Lawrie Brown Michael D Bauer and Arup Kumar Bhattacharjee. 2012. Computer security: principles and practice. Pearson Education Upper Saddle River NJ USA.  William Stallings Lawrie Brown Michael D Bauer and Arup Kumar Bhattacharjee. 2012. Computer security: principles and practice. Pearson Education Upper Saddle River NJ USA."},{"key":"e_1_3_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/3038912.3052709"},{"key":"e_1_3_2_1_98_1","volume-title":"SmartAuth: User-Centered Authorization for the Internet of Things. In 26th USENIX Security Symposium (USENIX Security . USENIX Association","author":"Tian Yuan","year":"2017","unstructured":"Yuan Tian , Nan Zhang , Yueh-Hsun Lin , XiaoFeng Wang , Blase Ur , Xianzheng Guo , and Patrick Tague . 2017 . SmartAuth: User-Centered Authorization for the Internet of Things. In 26th USENIX Security Symposium (USENIX Security . USENIX Association , Vancouver, BC, 361--378. https:\/\/www.usenix.org\/ conference\/usenixsecurity17\/technical-sessions\/presentation\/tian Yuan Tian, Nan Zhang, Yueh-Hsun Lin, XiaoFeng Wang, Blase Ur, Xianzheng Guo, and Patrick Tague. 2017. SmartAuth: User-Centered Authorization for the Internet of Things. In 26th USENIX Security Symposium (USENIX Security . USENIX Association, Vancouver, BC, 361--378. https:\/\/www.usenix.org\/ conference\/usenixsecurity17\/technical-sessions\/presentation\/tian"},{"key":"e_1_3_2_1_99_1","volume-title":"9th USENIX Workshop on O#ensive Technologies (WOOT 15)","author":"Vaidya Tavish","year":"2015","unstructured":"Tavish Vaidya , Yuankai Zhang , Micah Sherr , and Clay Shields . 2015 . Cocaine Noodles: Exploiting the Gap between Human and Machine Speech Recognition . In 9th USENIX Workshop on O#ensive Technologies (WOOT 15) . Washington, D.C. Tavish Vaidya, Yuankai Zhang, Micah Sherr, and Clay Shields. 2015. Cocaine Noodles: Exploiting the Gap between Human and Machine Speech Recognition. In 9th USENIX Workshop on O#ensive Technologies (WOOT 15). Washington, D.C."},{"key":"e_1_3_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3345662"},{"key":"e_1_3_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1145\/3322431.3325107"},{"key":"e_1_3_2_1_102_1","first-page":"2020","article-title":"Sneak into Your Room","author":"Yan Jia Yuqing Zhang","year":"2019","unstructured":"Yuqing Zhang Yan Jia , Luyi Xing . 2019 . Sneak into Your Room : Security Holes in the Integration and Management of Messaging Protocols on Commercial IoT Clouds. Accessed : 2020 - 2008 . Yuqing Zhang Yan Jia, Luyi Xing. 2019. Sneak into Your Room: Security Holes in the Integration and Management of Messaging Protocols on Commercial IoT Clouds. Accessed: 2020-08.","journal-title":"Accessed"},{"key":"e_1_3_2_1_103_1","volume-title":"29th {USENIX} Security Symposium ({USENIX} Security 20). 1183--1200.","author":"Yuan Bin","unstructured":"Bin Yuan , Yan Jia , Luyi Xing , Dongfang Zhao , XiaoFeng Wang , and Yuqing Zhang . 2020. Shattered chain of trust: Understanding security risks in crosscloud iot access delegation . In 29th {USENIX} Security Symposium ({USENIX} Security 20). 1183--1200. Bin Yuan, Yan Jia, Luyi Xing, Dongfang Zhao, XiaoFeng Wang, and Yuqing Zhang. 2020. Shattered chain of trust: Understanding security risks in crosscloud iot access delegation. In 29th {USENIX} Security Symposium ({USENIX} Security 20). 1183--1200."},{"key":"e_1_3_2_1_104_1","volume-title":"CommanderSong: A Systematic Approach for Practical Adversarial Voice Recognition. In 27th USENIX Security Symposium (USENIX Security 18)","author":"Yuan Xuejing","unstructured":"Xuejing Yuan , Yuxuan Chen , Yue Zhao , Yunhui Long , Xiaokang Liu , Kai Chen , Shengzhi Zhang , Heqing Huang , XiaoFeng Wang , and Carl A. Gunter . 2018 . CommanderSong: A Systematic Approach for Practical Adversarial Voice Recognition. In 27th USENIX Security Symposium (USENIX Security 18) . Baltimore, MD, 49--64. Xuejing Yuan, Yuxuan Chen, Yue Zhao, Yunhui Long, Xiaokang Liu, Kai Chen, Shengzhi Zhang, Heqing Huang, XiaoFeng Wang, and Carl A. Gunter. 2018. CommanderSong: A Systematic Approach for Practical Adversarial Voice Recognition. In 27th USENIX Security Symposium (USENIX Security 18). Baltimore, MD, 49--64."},{"key":"e_1_3_2_1_105_1","doi-asserted-by":"crossref","unstructured":"Nan Zhang Xianghang Mi Xuan Feng XiaoFeng Wang Yuan Tian and Feng Qian. 2019. Dangerous Skills: Understanding and Mitigating Security Risks of Voice-Controlled Third-Party Functions on Virtual Personal Assistant Systems. In 2019 IEEE Symposium on Security and Privacy (SP). 1381--1396.  Nan Zhang Xianghang Mi Xuan Feng XiaoFeng Wang Yuan Tian and Feng Qian. 2019. Dangerous Skills: Understanding and Mitigating Security Risks of Voice-Controlled Third-Party Functions on Virtual Personal Assistant Systems. In 2019 IEEE Symposium on Security and Privacy (SP). 1381--1396.","DOI":"10.1109\/SP.2019.00016"},{"key":"e_1_3_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23525"},{"key":"e_1_3_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560590"},{"key":"e_1_3_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00009"}],"event":{"name":"CCS '22: 2022 ACM SIGSAC Conference on Computer and Communications Security","location":"Los Angeles CA USA","acronym":"CCS '22","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3548606.3560680","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3548606.3560680","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3548606.3560680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:59Z","timestamp":1750182539000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3548606.3560680"}},"subtitle":["Understanding and Mitigating Security Risks in Cloud-based IoT Access Policies"],"short-title":[],"issued":{"date-parts":[[2022,11,7]]},"references-count":107,"alternative-id":["10.1145\/3548606.3560680","10.1145\/3548606"],"URL":"https:\/\/doi.org\/10.1145\/3548606.3560680","relation":{},"subject":[],"published":{"date-parts":[[2022,11,7]]},"assertion":[{"value":"2022-11-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}