{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:05Z","timestamp":1784675045146,"version":"3.55.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"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":"publisher","award":["62072309"],"award-info":[{"award-number":["62072309"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CAS Project for Young Scientists in Basic Research","award":["YSBR-040"],"award-info":[{"award-number":["YSBR-040"]}]},{"name":"ISCAS New Cultivation Project","award":["ISCAS-PYFX-202201"],"award-info":[{"award-number":["ISCAS-PYFX-202201"]}]},{"name":"State Key Laboratory of Novel Software Technology, Nanjing University","award":["KFKT2022A03"],"award-info":[{"award-number":["KFKT2022A03"]}]},{"name":"Birkbeck BEI School Project","award":["EFFECT"],"award-info":[{"award-number":["EFFECT"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Masking is one of the most effective countermeasures for securely implementing cryptographic algorithms against power side-channel attacks, the design of which however turns out to be intricate and error-prone. While techniques have been proposed to rigorously verify implementations of cryptographic algorithms, currently they are limited in scalability. To address this issue, compositional approaches have been investigated, but insofar they fail to prove the security of recent efficient implementations. To fill this gap, we propose a novel compositional verification approach. In particular, we introduce two new language-level security notions based on which we propose composition strategies and verification algorithms. Our approach is able to prove efficient implementations, which cannot be done by prior compositional approaches. We implement our approach as a tool CONVINCE and conduct extensive experiments to confirm its efficacy. We also use CONVINCE to further explore the design space of the AES Sbox with least refreshing by replacing its implementation for finite-field multiplication with more efficient counterparts. We automatically prove leakage-freeness of these new versions. As a result, we can effectively reduce 1,600 randomness and 3,200 XOR-operations of the state-of-the-art AES implementation.<\/jats:p>","DOI":"10.1145\/3622862","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1817-1847","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3800-2565","authenticated-orcid":false,"given":"Pengfei","family":"Gao","sequence":"first","affiliation":[{"name":"ShanghaiTech University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1005-2114","authenticated-orcid":false,"given":"Yedi","family":"Zhang","sequence":"additional","affiliation":[{"name":"ShanghaiTech University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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 and, Beijing, China \/ University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7444-0285","authenticated-orcid":false,"given":"Francois-Xavier","family":"Standaert","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Catholique de Louvain, Louvain-la-Neuve, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228376"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-018-00202-2"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46800-5_18"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978427"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29959-0_15"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-56620-7_19"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.46586\/tches.v2021.i2.189-228"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024778"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40349-1_17"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_22"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63697-9_14"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45727-3_11"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03329-3_12"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833600"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75208-2_2"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-78375-8_11"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_13"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-77886-6_10"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34047-5_21"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2020.3022979"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2020.2971153"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48059-5_25"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-55220-5_25"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-93387-0_4"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48116-5_7"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44709-3_11"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43933-3_21"},{"key":"e_1_2_1_28_1","volume-title":"Secure multiparty computation","author":"Cramer Ronald","unstructured":"Ronald Cramer and Ivan Bjerre Damg\u00e5rd . 2015. Secure multiparty computation . Cambridge University Press . Ronald Cramer and Ivan Bjerre Damg\u00e5rd. 2015. Secure multiparty computation. Cambridge University Press."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46800-5_16"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2685616"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428015"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.3008852"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_9"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3330392"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8416208"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 30th USENIX Security Symposium. 1469\u20131468","author":"Gigerl Barbara","year":"2021","unstructured":"Barbara Gigerl , Vedad Hadzic , Robert Primas , Stefan Mangard , and Roderick Bloem . 2021 . Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs . In Proceedings of the 30th USENIX Security Symposium. 1469\u20131468 . Barbara Gigerl, Vedad Hadzic, Robert Primas, Stefan Mangard, and Roderick Bloem. 2021. Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs. In Proceedings of the 30th USENIX Security Symposium. 1469\u20131468."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44709-1_2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48059-5_15"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-56620-7_20"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-018-0184-y"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_9"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45146-4_27"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36400-5_11"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89641-0_10"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03329-3_10"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23951-9_7"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64837-4_26"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48405-1_25"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46877-3_35"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240802"},{"key":"e_1_2_1_52_1","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. 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_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33027-8_4"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.29007\/hhnf"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.15"},{"key":"e_1_2_1_56_1","first-page":"948","article-title":"Generic Side-channel attacks on CCA-secure lattice-based PKE and KEM schemes","volume":"2019","author":"Ravi Prasanna","year":"2019","unstructured":"Prasanna Ravi , Sujoy Sinha Roy , Anupam Chattopadhyay , and Shivam Bhasin . 2019 . Generic Side-channel attacks on CCA-secure lattice-based PKE and KEM schemes . IACR Cryptol. ePrint Arch. , 2019 (2019), 948 . Prasanna Ravi, Sujoy Sinha Roy, Anupam Chattopadhyay, and Shivam Bhasin. 2019. Generic Side-channel attacks on CCA-secure lattice-based PKE and KEM schemes. IACR Cryptol. ePrint Arch., 2019 (2019), 948.","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15031-9_28"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68487-7_8"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/359168.359176"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338913"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64837-4_28"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2017.2787985"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622862","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622862","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":63,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622862"],"URL":"https:\/\/doi.org\/10.1145\/3622862","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}