{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T10:34:03Z","timestamp":1791282843374,"version":"4.1.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,12,23]],"date-time":"2014-12-23T00:00:00Z","timestamp":1419292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-1128903"],"award-info":[{"award-number":["CNS-1128903"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-13-1-0527"],"award-info":[{"award-number":["N00014-13-1-0527"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2014,12,23]]},"abstract":"<jats:p>\n            A common strategy for designing countermeasures against power-analysis-based side-channel attacks is using\n            <jats:italic>random masking<\/jats:italic>\n            techniques to remove the statistical dependency between sensitive data and side-channel emissions. However, this process is both labor intensive and error prone and, currently, there is a lack of automated tools to formally assess how secure a countermeasure really is. We propose the first SMT-solver-based method for formally verifying the security of a masking countermeasure against such attacks. In addition to checking whether the sensitive data are\n            <jats:italic>masked<\/jats:italic>\n            by random variables, we also check whether they are\n            <jats:italic>perfectly masked<\/jats:italic>\n            , that is, whether the intermediate computation results in the implementation of a cryptographic algorithm are independent of the secret key. We encode this verification problem using a series of quantifier-free first-order logic formulas, whose satisfiability can be decided by an off-the-shelf SMT solver. We have implemented the proposed method in a software verification tool based on the LLVM compiler frontend and the Yices SMT solver. Our experiments on a set of recently proposed masking countermeasures for cryptographic algorithms such as AES and MAC-Keccak show the method is both effective in detecting power side-channel leaks and scalable for practical use.\n          <\/jats:p>","DOI":"10.1145\/2685616","type":"journal-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T13:27:09Z","timestamp":1420464429000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Formal Verification of Software Countermeasures against Side-Channel Attacks"],"prefix":"10.1145","volume":"24","author":[{"given":"Hassan","family":"Eldib","sequence":"first","affiliation":[{"name":"Virginia Polytechnic Institute and State University, Blacksburg, VA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"Virginia Polytechnic Institute and State University, Blacksburg, VA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrick","family":"Schaumont","sequence":"additional","affiliation":[{"name":"Virginia Polytechnic Institute and State University, Blacksburg, VA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,12,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325702"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228376"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27954-6_2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_8"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40349-1_17"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024778"},{"key":"e_1_2_1_8_1","volume-title":"Gilles Van Assche, and Ronny Van Keer","author":"Bertoni Guido","year":"2013","unstructured":"Guido Bertoni , Joan Daemen , Michael Peeters , Gilles Van Assche, and Ronny Van Keer . 2013 . Keccak implementation overview. http:\/\/keccak.neokeon.org\/Keccak-implementation-3.2.pdf. Guido Bertoni, Joan Daemen, Michael Peeters, Gilles Van Assche, and Ronny Van Keer. 2013. Keccak implementation overview. http:\/\/keccak.neokeon.org\/Keccak-implementation-3.2.pdf."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646762.706179"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30564-4_5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788857.1788884"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646764.703964"},{"key":"e_1_2_1_14_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 1999 . Model Checking. MIT Press , Cambridge, MA. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 22nd USENIX Conference on Security (SEC'13)","author":"Doychev Goran","year":"2013","unstructured":"Goran Doychev , Dominik Feld , Boris Kopf , Laurent Mauborgne , and Jan Reineke . 2013 . CacheAudit: A tool for the static analysis of cache side channels . In Proceedings of the 22nd USENIX Conference on Security (SEC'13) . 431--446. Goran Doychev, Dominik Feld, Boris Kopf, Laurent Mauborgne, and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In Proceedings of the 22nd USENIX Conference on Security (SEC'13). 431--446."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_8"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_5"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593193"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/648254.752571"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1782574.1782590"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11767480_16"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11545262_22"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/646764.703989"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.21"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_40"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the IEEE\/ACM International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization (CGO'04)","author":"Lattner Chris","unstructured":"Chris Lattner and Vikram S. Adve . 2004. LLVM: A compilation framework for lifelong program analysis and transformation . In Proceedings of the IEEE\/ACM International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization (CGO'04) . 75--88. Chris Lattner and Vikram S. Adve. 2004. LLVM: A compilation framework for lifelong program analysis and transformation. In Proceedings of the IEEE\/ACM International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization (CGO'04). 75--88."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0169-2"},{"key":"e_1_2_1_30_1","volume-title":"Power Analysis Attacks - Revealing the Secrets of Smart Cards","author":"Mangard Stefan","unstructured":"Stefan Mangard , Elisabeth Oswald , and Thomas Popp . 2007. Power Analysis Attacks - Revealing the Secrets of Smart Cards . Springer . Stefan Mangard, Elisabeth Oswald, and Thomas Popp. 2007. Power Analysis Attacks - Revealing the Secrets of Smart Cards. Springer."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647935.740925"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046722"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2008684.2008693"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33027-8_4"},{"key":"e_1_2_1_35_1","unstructured":"NIST. 2013. Keccak reference code submission to NIST's SHA-3 competition (round 3). http:\/\/csrc.nist.gov\/groups\/ST\/hash\/sha-3\/Round3\/documents\/Keccak FinalRnd.zip.  NIST. 2013. Keccak reference code submission to NIST's SHA-3 competition (round 3). http:\/\/csrc.nist.gov\/groups\/ST\/hash\/sha-3\/Round3\/documents\/Keccak FinalRnd.zip."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_28"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/FDTC.2009.44"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38348-9_9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41383-4_5"},{"key":"e_1_2_1_41_1","volume-title":"Abstraction Refinement for Large Scale Model Checking","author":"Wang Chao","unstructured":"Chao Wang , Gary D. Hachhtel , and Fabio Somenzi . 2006. Abstraction Refinement for Large Scale Model Checking . Springer . Chao Wang, Gary D. Hachhtel, and Fabio Somenzi. 2006. Abstraction Refinement for Large Scale Model Checking. Springer."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1230800.1230802"},{"key":"e_1_2_1_43_1","unstructured":"XILINX. 2014. MicroBlaze soft processor core. http:\/\/www.xilinx.com\/tools\/microblaze.htm.  XILINX. 2014. MicroBlaze soft processor core. http:\/\/www.xilinx.com\/tools\/microblaze.htm."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455229.1455239"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2685616","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2685616","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:21Z","timestamp":1750227201000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2685616"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,23]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,12,23]]}},"alternative-id":["10.1145\/2685616"],"URL":"https:\/\/doi.org\/10.1145\/2685616","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,23]]},"assertion":[{"value":"2014-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}