{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:24:38Z","timestamp":1766067878310,"version":"3.41.0"},"reference-count":98,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2024,3,14]],"date-time":"2024-03-14T00:00:00Z","timestamp":1710374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62072309 and 61872340"],"award-info":[{"award-number":["62072309 and 61872340"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Strategic Priority Research Program of the Chinese Academy of Sciences","award":["XDA0320101"],"award-info":[{"award-number":["XDA0320101"]}]},{"name":"State Key Laboratory of Novel Software Technology, Nanjing University","award":["KFKT2022A03, KFKT2023A04"],"award-info":[{"award-number":["KFKT2022A03, KFKT2023A04"]}]},{"name":"Birkbeck BEI School Project"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>\n            Power side-channel attacks allow an adversary to efficiently and effectively steal secret information (e.g., keys) by exploiting the correlation between secret data and runtime power consumption, hence posing a serious threat to software security, particularly cryptographic implementations. Masking is a commonly used countermeasure against such attacks, which breaks the statistical dependence between secret data and side-channel leaks via randomization. In a nutshell, a variable is represented by a vector of shares armed with random variables, called\n            <jats:italic>masking encoding<\/jats:italic>\n            , on which cryptographic computations are performed. While compositional verification for the security of masked cryptographic implementations has received much attention because of its high efficiency, existing compositional approaches either use implicitly fixed pre-conditions that may not be fulfilled by state-of-the-art efficient implementations, or require user-provided hard-coded pre-conditions that are time consuming and highly non-trivial, even for an expert. In this article, we tackle the compositional verification problem of first-order masking countermeasures, where first-order means that the adversary is allowed to access only one intermediate computation result. Following the literature, we consider countermeasures given as gadgets, which are special procedures whose inputs are masking encodings of variables. We introduce a new security notion parameterized by an explicit pre-condition for each gadget, as well as composition rules for reasoning about masking countermeasures against power side-channel attacks. We propose accompanying efficient algorithms to automatically infer proper pre-conditions, based on which our new compositional approach can efficiently and automatically prove security for masked implementations. We implement our approaches as a tool\n            <jats:sc>MaskCV<\/jats:sc>\n            and conduct experiments on publicly available masked cryptographic implementations including 10 different full AES implementations. The experimental results confirm the effectiveness and efficiency of our approach.\n          <\/jats:p>","DOI":"10.1145\/3635707","type":"journal-article","created":{"date-parts":[[2023,12,5]],"date-time":"2023-12-05T12:02:39Z","timestamp":1701777759000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Compositional Verification of First-Order Masking Countermeasures against Power Side-Channel Attacks"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3800-2565","authenticated-orcid":false,"given":"Pengfei","family":"Gao","sequence":"first","affiliation":[{"name":"Bytedance, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0581-2679","authenticated-orcid":false,"given":"Fu","family":"Song","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China, and University of Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5993-1665","authenticated-orcid":false,"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[{"name":"Birkbeck, University of London, London, UK"}]}],"member":"320","published-online":{"date-parts":[[2024,3,14]]},"reference":[{"unstructured":"Figshare. 2022. MASKCV. Retrieved December 14 2023 from https:\/\/figshare.com\/s\/1fc592780ab44ccfa39e","key":"e_1_3_2_2_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_3_2","DOI":"10.1145\/2228360.2228376"},{"doi-asserted-by":"publisher","key":"e_1_3_2_4_2","DOI":"10.1007\/978-3-319-49812-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_5_2","DOI":"10.5555\/3241094.3241100"},{"key":"e_1_3_2_6_2","first-page":"Springer, 149\u20131","volume-title":"Deductive Software Verification: Future Perspectives\u2014Reflections on the Occasion of 20 Years of KeY","author":"Alshnakat Anoud","year":"2020","unstructured":"Anoud Alshnakat, Dilian Gurov, Christian Lidstr\u00f6m, and Philipp R\u00fcmmer. 2020. Constraint-based contract inference for deductive verification. In Deductive Software Verification: Future Perspectives\u2014Reflections on the Occasion of 20 Years of KeY. Springer, 149\u2013176."},{"doi-asserted-by":"publisher","key":"e_1_3_2_7_2","DOI":"10.1145\/3062341.3062378"},{"doi-asserted-by":"publisher","key":"e_1_3_2_8_2","DOI":"10.1145\/2950290.2950362"},{"doi-asserted-by":"publisher","key":"e_1_3_2_9_2","DOI":"10.1007\/s13389-018-00202-2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_10_2","DOI":"10.1145\/2976749.2978427"},{"doi-asserted-by":"publisher","key":"e_1_3_2_11_2","DOI":"10.1007\/978-3-030-29959-0_15"},{"doi-asserted-by":"publisher","key":"e_1_3_2_12_2","DOI":"10.1007\/978-3-319-56620-7_19"},{"doi-asserted-by":"publisher","key":"e_1_3_2_13_2","DOI":"10.46586\/tches.v2021.i2.189-228"},{"doi-asserted-by":"publisher","key":"e_1_3_2_14_2","DOI":"10.1145\/2024724.2024778"},{"doi-asserted-by":"publisher","key":"e_1_3_2_15_2","DOI":"10.1007\/978-3-662-49896-5_22"},{"doi-asserted-by":"publisher","key":"e_1_3_2_16_2","DOI":"10.1007\/978-3-319-63697-9_14"},{"doi-asserted-by":"publisher","key":"e_1_3_2_17_2","DOI":"10.1007\/978-3-030-56784-2_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_18_2","DOI":"10.1007\/978-3-030-45727-3_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_19_2","DOI":"10.1007\/978-3-030-03329-3_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_20_2","DOI":"10.1109\/SP46214.2022.9833600"},{"key":"e_1_3_2_21_2","first-page":"22","volume-title":"Proceedings of the International Conference on Smart Card Research and Advanced Applications","author":"Biryukov Alex","year":"2017","unstructured":"Alex Biryukov, Daniel Dinu, Yann Le Corre, and Aleksei Udovenko. 2017. Optimal first-order Boolean masking for embedded IoT devices. In Proceedings of the International Conference on Smart Card Research and Advanced Applications. 22\u201341."},{"doi-asserted-by":"publisher","key":"e_1_3_2_22_2","DOI":"10.1109\/TC.2016.2635650"},{"doi-asserted-by":"publisher","key":"e_1_3_2_23_2","DOI":"10.3233\/JCS-181136"},{"doi-asserted-by":"publisher","key":"e_1_3_2_24_2","DOI":"10.1007\/978-3-319-78375-8_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_25_2","DOI":"10.1007\/978-3-319-78375-8_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_26_2","DOI":"10.1007\/978-3-662-54455-6_13"},{"doi-asserted-by":"publisher","key":"e_1_3_2_27_2","DOI":"10.1007\/978-3-030-77886-6_10"},{"doi-asserted-by":"publisher","key":"e_1_3_2_28_2","DOI":"10.1109\/SP40000.2020.00007"},{"doi-asserted-by":"publisher","key":"e_1_3_2_29_2","DOI":"10.1145\/3377811.3380432"},{"doi-asserted-by":"publisher","key":"e_1_3_2_30_2","DOI":"10.1145\/3213846.3213867"},{"doi-asserted-by":"crossref","unstructured":"Ga\u00ebtan Cassiers Benjamin Gr\u00e9goire Itamar Levi and Fran\u00e7ois-Xavier Standaert. 2021. Hardware private circuits: From trivial composition to full verification. IEEE Transactions on Computers 70 10 (2021) 1677\u20131690.","key":"e_1_3_2_31_2","DOI":"10.1109\/TC.2020.3022979"},{"doi-asserted-by":"publisher","key":"e_1_3_2_32_2","DOI":"10.1109\/TIFS.2020.2971153"},{"doi-asserted-by":"publisher","key":"e_1_3_2_33_2","DOI":"10.1145\/3385412.3385970"},{"doi-asserted-by":"publisher","key":"e_1_3_2_34_2","DOI":"10.1145\/3133956.3134058"},{"doi-asserted-by":"publisher","key":"e_1_3_2_35_2","DOI":"10.1016\/j.cose.2021.102556"},{"doi-asserted-by":"publisher","key":"e_1_3_2_36_2","DOI":"10.1007\/3-540-44499-8_20"},{"doi-asserted-by":"publisher","key":"e_1_3_2_37_2","DOI":"10.5555\/648252.752381"},{"doi-asserted-by":"publisher","key":"e_1_3_2_38_2","DOI":"10.1007\/978-3-319-66787-4_5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_39_2","DOI":"10.1007\/978-3-319-93387-0_4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_40_2","DOI":"10.1007\/978-3-662-44709-3_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_41_2","DOI":"10.1007\/978-3-540-74735-2_3"},{"key":"e_1_3_2_42_2","first-page":"410","volume-title":"Proceedings of the 20th International Workshop on Fast Software Encryption","author":"Coron Jean-S\u00e9bastien","year":"2013","unstructured":"Jean-S\u00e9bastien Coron, Emmanuel Prouff, Matthieu Rivain, and Thomas Roche. 2013. Higher-order side channel security and mask refreshing. In Proceedings of the 20th International Workshop on Fast Software Encryption. 410\u2013424."},{"doi-asserted-by":"publisher","key":"e_1_3_2_43_2","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_3_2_44_2","volume-title":"Proceedings of the 28th Annual Network and Distributed System Security Symposium","author":"Daniel Lesly-Ann","year":"2021","unstructured":"Lesly-Ann Daniel, S\u00e9bastien Bardin, and Tamara Rezk. 2021. Hunting the haunter\u2014Efficient relational symbolic execution for spectre with haunted RelSE. In Proceedings of the 28th Annual Network and Distributed System Security Symposium."},{"doi-asserted-by":"publisher","key":"e_1_3_2_45_2","DOI":"10.1145\/3062341.3062388"},{"doi-asserted-by":"publisher","key":"e_1_3_2_46_2","DOI":"10.1145\/2756550"},{"doi-asserted-by":"publisher","key":"e_1_3_2_47_2","DOI":"10.1007\/978-3-319-08867-9_8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_48_2","DOI":"10.1145\/2685616"},{"doi-asserted-by":"publisher","key":"e_1_3_2_49_2","DOI":"10.1007\/978-3-642-54862-8_5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_50_2","DOI":"10.1145\/2593069.2593193"},{"doi-asserted-by":"publisher","key":"e_1_3_2_51_2","DOI":"10.1109\/TCAD.2015.2424951"},{"doi-asserted-by":"publisher","key":"e_1_3_2_52_2","DOI":"10.1007\/978-3-319-41540-6_19"},{"doi-asserted-by":"publisher","key":"e_1_3_2_53_2","DOI":"10.1145\/3428015"},{"doi-asserted-by":"publisher","key":"e_1_3_2_54_2","DOI":"10.1109\/TSE.2020.3008852"},{"doi-asserted-by":"publisher","key":"e_1_3_2_55_2","DOI":"10.1007\/978-3-030-17462-0_9"},{"doi-asserted-by":"publisher","key":"e_1_3_2_56_2","DOI":"10.1145\/3330392"},{"doi-asserted-by":"publisher","key":"e_1_3_2_57_2","DOI":"10.5555\/648252.752372"},{"doi-asserted-by":"publisher","key":"e_1_3_2_58_2","DOI":"10.1007\/978-3-319-56620-7_20"},{"doi-asserted-by":"publisher","key":"e_1_3_2_59_2","DOI":"10.1007\/s13389-018-0184-y"},{"doi-asserted-by":"publisher","key":"e_1_3_2_60_2","DOI":"10.1145\/3377811.3380428"},{"doi-asserted-by":"publisher","key":"e_1_3_2_61_2","DOI":"10.1145\/3428215"},{"doi-asserted-by":"publisher","key":"e_1_3_2_62_2","DOI":"10.1145\/3236024.3236028"},{"doi-asserted-by":"publisher","key":"e_1_3_2_63_2","DOI":"10.1007\/978-3-642-38574-2_21"},{"doi-asserted-by":"publisher","key":"e_1_3_2_64_2","DOI":"10.1007\/978-3-540-45146-4_27"},{"key":"e_1_3_2_65_2","first-page":"129","volume-title":"Proceedings of the 4th International Workshop on Cryptographic Hardware and Embedded Systems: Revised Papers","author":"Itoh Kouichi","year":"2002","unstructured":"Kouichi Itoh, Tetsuya Izu, and Masahiko Takenaka. 2002. Address-bit differential power analysis of cryptographic schemes OK-ECDH and OK-ECDSA. In Proceedings of the 4th International Workshop on Cryptographic Hardware and Embedded Systems: Revised Papers. 129\u2013143."},{"doi-asserted-by":"publisher","key":"e_1_3_2_66_2","DOI":"10.1145\/3540250.3558938"},{"doi-asserted-by":"publisher","key":"e_1_3_2_67_2","DOI":"10.1145\/3395363.3397365"},{"doi-asserted-by":"publisher","key":"e_1_3_2_68_2","DOI":"10.1007\/978-3-319-89641-0_10"},{"doi-asserted-by":"publisher","key":"e_1_3_2_69_2","DOI":"10.1007\/978-3-030-03329-3_10"},{"key":"e_1_3_2_70_2","first-page":"787","volume-title":"Proceedings of the 26th International Conference on the Theory and Application of Cryptology and Information Security","author":"Knichel David","year":"2020","unstructured":"David Knichel, Pascal Sasdrich, and Amir Moradi. 2020. SILVER\u2014Statistical independence and leakage verification. In Proceedings of the 26th International Conference on the Theory and Application of Cryptology and Information Security. 787\u2013816."},{"doi-asserted-by":"publisher","key":"e_1_3_2_71_2","DOI":"10.1109\/SP.2019.00002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_72_2","DOI":"10.1007\/3-540-68697-5_9"},{"doi-asserted-by":"publisher","key":"e_1_3_2_73_2","DOI":"10.5555\/646764.703989"},{"key":"e_1_3_2_74_2","volume-title":"Proceedings of the 27th USENIX Security Symposium","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading kernel memory from user space. In Proceedings of the 27th USENIX Security Symposium."},{"doi-asserted-by":"publisher","key":"e_1_3_2_75_2","DOI":"10.1145\/3240765.3240802"},{"doi-asserted-by":"publisher","key":"e_1_3_2_76_2","DOI":"10.1007\/978-3-319-24174-6_23"},{"key":"e_1_3_2_77_2","volume-title":"Proceedings of the International Workshop on Security Proofs for Embedded Systems","author":"Meunier Quentin L.","year":"2020","unstructured":"Quentin L. Meunier, In\u00e8s Ben El Ouahma, and Karine Heydemann. 2020. SELA: A symbolic expression leakage analyzer. In Proceedings of the International Workshop on Security Proofs for Embedded Systems."},{"key":"e_1_3_2_78_2","article-title":"LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions","author":"Meunier Quentin L.","year":"2021","unstructured":"Quentin L. Meunier, Etienne Pons, and Karine Heydemann. 2021. LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions. Report 2021\/1468. Cryptology ePrint Archive.","journal-title":"Cryptology ePrint Archive"},{"doi-asserted-by":"publisher","key":"e_1_3_2_79_2","DOI":"10.46586\/tches.v2019.i2.256-292"},{"doi-asserted-by":"publisher","key":"e_1_3_2_80_2","DOI":"10.1109\/ICSE.2019.00034"},{"key":"e_1_3_2_81_2","first-page":"35","volume-title":"Proceedings of the 5th International Workshop on Cryptographic Hardware and Embedded Systems","author":"\u00d6rs Siddika Berna","year":"2003","unstructured":"Siddika Berna \u00d6rs, Elisabeth Oswald, and Bart Preneel. 2003. Power-analysis attacks on an FPGA\u2014First experimental results. In Proceedings of the 5th International Workshop on Cryptographic Hardware and Embedded Systems. 35\u201350."},{"key":"e_1_3_2_82_2","volume-title":"Proceedings of the 6th International Workshop on Security Proofs for Embedded Systems","author":"Ouahma In\u00e8s Ben El","year":"2017","unstructured":"In\u00e8s Ben El Ouahma, Quentin Meunier, Karine Heydemann, and Emmanuelle Encrenaz. 2017. Symbolic approach for side-channel resistance analysis of masked assembly codes. In Proceedings of the 6th International Workshop on Security Proofs for Embedded Systems."},{"doi-asserted-by":"publisher","key":"e_1_3_2_83_2","DOI":"10.1109\/CSF.2016.34"},{"doi-asserted-by":"publisher","key":"e_1_3_2_84_2","DOI":"10.1109\/CSF.2017.8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_85_2","DOI":"10.1109\/TC.2009.15"},{"doi-asserted-by":"publisher","key":"e_1_3_2_86_2","DOI":"10.1145\/3540250.3549150"},{"doi-asserted-by":"publisher","key":"e_1_3_2_87_2","DOI":"10.46586\/tches.v2020.i3.307-335"},{"doi-asserted-by":"publisher","key":"e_1_3_2_88_2","DOI":"10.1007\/978-3-642-15031-9_28"},{"doi-asserted-by":"publisher","key":"e_1_3_2_89_2","DOI":"10.14722\/ndss.2019.23536"},{"key":"e_1_3_2_90_2","first-page":"119","volume-title":"Proceedings of the 19th International Conference on Smart Card Research and Advanced Applications","author":"Schamberger Thomas","year":"2020","unstructured":"Thomas Schamberger, Julian Renner, Georg Sigl, and Antonia Wachter-Zeh. 2020. A power side-channel attack on the CCA2-Secure HQC KEM. In Proceedings of the 19th International Conference on Smart Card Research and Advanced Applications. 119\u2013134."},{"doi-asserted-by":"publisher","key":"e_1_3_2_91_2","DOI":"10.1007\/11605805_14"},{"doi-asserted-by":"publisher","key":"e_1_3_2_92_2","DOI":"10.1109\/ICSE43902.2021.00079"},{"doi-asserted-by":"publisher","key":"e_1_3_2_93_2","DOI":"10.1145\/3338906.3338913"},{"doi-asserted-by":"publisher","key":"e_1_3_2_94_2","DOI":"10.1007\/978-3-030-64837-4_28"},{"doi-asserted-by":"publisher","key":"e_1_3_2_95_2","DOI":"10.5555\/3196160.3196244"},{"doi-asserted-by":"publisher","key":"e_1_3_2_96_2","DOI":"10.1145\/3290390"},{"doi-asserted-by":"publisher","key":"e_1_3_2_97_2","DOI":"10.1145\/3213846.3213851"},{"doi-asserted-by":"publisher","key":"e_1_3_2_98_2","DOI":"10.1109\/TrustCom\/BigDataSE.2018.00205"},{"doi-asserted-by":"publisher","key":"e_1_3_2_99_2","DOI":"10.1007\/978-3-319-96142-2_12"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3635707","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3635707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:59Z","timestamp":1750291019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3635707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,14]]},"references-count":98,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3635707"],"URL":"https:\/\/doi.org\/10.1145\/3635707","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2024,3,14]]},"assertion":[{"value":"2022-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-22","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}