{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:07:29Z","timestamp":1750306049300,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,5,3]],"date-time":"2017-05-03T00:00:00Z","timestamp":1493769600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2017,5,3]]},"abstract":"<jats:p>We explain how formal verification and program synthesis can be used to (1) detect side-channel leaks of software code running on portable devices, (2) prove the absence of side-channel leaks, and (3) transform software to eliminate such leaks. We use power side-channel leaks in cryptographic software as examples, but the underlying techniques are applicable to other types of side channels and software systems as well.<\/jats:p>","DOI":"10.1145\/3090064.3090071","type":"journal-article","created":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T22:53:21Z","timestamp":1585954401000},"page":"76-89","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Security by compilation"],"prefix":"10.1145","volume":"4","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[{"name":"University of Southern California"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Schaumont","sequence":"additional","affiliation":[{"name":"Virginia Tech"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,5,3]]},"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.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_15"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27954-6_2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950362"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978427"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_8"},{"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.1145\/2024724.2024778"},{"key":"e_1_2_1_11_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. URL : http:\/\/keccak.neokeon.org\/Keccak-implementation-3.2.pdf. (2013). Guido Bertoni, Joan Daemen, Michael Peeters, Gilles Van Assche, and Ronny Van Keer. 2013. Keccak implementation overview. URL: http:\/\/keccak.neokeon.org\/Keccak-implementation-3.2.pdf. (2013)."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646762.706179"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30564-4_5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28632-5_2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788857.1788884"},{"volume-title":"AAAI Conference on Artificial Intelligence. 1722--1730","author":"Chakraborty Supratik","key":"e_1_2_1_16_1","unstructured":"Supratik Chakraborty , Daniel J. Fremont , Kuldeep S. Meel , Sanjit A. Seshia , and Moshe Y. Vardi . 2014. Distribution-aware sampling and weighted model counting for SAT . In AAAI Conference on Artificial Intelligence. 1722--1730 . Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. 2014. Distribution-aware sampling and weighted model counting for SAT. In AAAI Conference on Artificial Intelligence. 1722--1730."},{"volume-title":"International Conference on Principles and Practice of Constraint Programming. 200--216","author":"Chakraborty Supratik","key":"e_1_2_1_17_1","unstructured":"Supratik Chakraborty , Kuldeep S. Meel , and Moshe Y. Vardi . 2013. A scalable approximate model counter . In International Conference on Principles and Practice of Constraint Programming. 200--216 . Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. 2013. A scalable approximate model counter. In International Conference on Principles and Practice of Constraint Programming. 200--216."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/646764.703964"},{"key":"e_1_2_1_19_1","unstructured":"E. M. Clarke O. Grumberg and D. A. Peled. 1999. Model Checking. MIT Press Cambridge MA.   E. M. Clarke O. Grumberg and D. A. Peled. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_20_1","unstructured":"Goran Doychev Dominik Feld Boris K\u00f6pf Laurent Mauborgne and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In USENIX Security. 431--446.   Goran Doychev Dominik Feld Boris K\u00f6pf Laurent Mauborgne and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In USENIX Security. 431--446."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85174-5_12"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2341931"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_8"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2685616"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593193"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2424951"},{"key":"e_1_2_1_28_1","volume-title":"Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits. In International Conference on Computer Aided Verification. 343--363","author":"Eldib Hassan","year":"2016","unstructured":"Hassan Eldib , Meng Wu , and Chao Wang . 2016 . Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits. In International Conference on Computer Aided Verification. 343--363 . Hassan Eldib, Meng Wu, and Chao Wang. 2016. Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits. In International Conference on Computer Aided Verification. 343--363."},{"volume-title":"AAAI Conference on Artificial Intelligence. 3885--3892","author":"Fremont Daniel J.","key":"e_1_2_1_29_1","unstructured":"Daniel J. Fremont , Markus N. Rabe , and Sanjit A. Seshia . 2017. Maximum model counting . In AAAI Conference on Artificial Intelligence. 3885--3892 . Daniel J. Fremont, Markus N. Rabe, and Sanjit A. Seshia. 2017. Maximum model counting. In AAAI Conference on Artificial Intelligence. 3885--3892."},{"key":"e_1_2_1_30_1","volume-title":"International Cryptology Conference. 444--461","author":"Genkin Daniel","year":"2014","unstructured":"Daniel Genkin , Adi Shamir , and Eran Tromer . 2014 . RSA key extraction via low-bandwidth acoustic crypt-analysis . In International Cryptology Conference. 444--461 . Daniel Genkin, Adi Shamir, and Eran Tromer. 2014. RSA key extraction via low-bandwidth acoustic crypt-analysis. In International Cryptology Conference. 444--461."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/648254.752571"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1782574.1782590"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993536"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.11"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11767480_16"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"volume-title":"IEEE International Symposium on High Performance Computer Architecture. 394--405","author":"Jiang Zhen Hang","key":"e_1_2_1_38_1","unstructured":"Zhen Hang Jiang , Yunsi Fei , and David R. Kaeli . 2016. A complete key recovery timing attack on a GPU . In IEEE International Symposium on High Performance Computer Architecture. 394--405 . Zhen Hang Jiang, Yunsi Fei, and David R. Kaeli. 2016. A complete key recovery timing attack on a GPU. In IEEE International Symposium on High Performance Computer Architecture. 394--405."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25286-0_5"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/646764.703989"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.21"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_40"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2015.7357115"},{"key":"e_1_2_1_45_1","volume-title":"The Cryptographers' Track at the RSA Conference","author":"Mangard Stefan","year":"2004","unstructured":"Stefan Mangard . 2004. Hardware countermeasures against DPA - A statistical analysis of their effectiveness . In The Cryptographers' Track at the RSA Conference 2004 . 222--235. Stefan Mangard. 2004. Hardware countermeasures against DPA - A statistical analysis of their effectiveness. In The Cryptographers' Track at the RSA Conference 2004. 222--235."},{"volume-title":"Symbolic Model Checking","author":"McMillan K. L.","key":"e_1_2_1_46_1","unstructured":"K. L. McMillan . 1994. Symbolic Model Checking . Kluwer Academic Publishers , Boston, MA . K. L. McMillan. 1994. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Thomas S. Messerges. 2000. Securing the AES finalists against power analysis attacks. In Fast Software Encryption. 150--164.   Thomas S. Messerges. 2000. Securing the AES finalists against power analysis attacks. In Fast Software Encryption. 150--164.","DOI":"10.1007\/3-540-44706-7_11"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046722"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2435264.2435282"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Amir Moradi Axel Poschmann San Ling Christof Paar and Huaxiong Wang. 2011. Pushing the limits: A very compact and a threshold implementation of AES. In EUROCRYPT. 69--88.   Amir Moradi Axel Poschmann San Ling Christof Paar and Huaxiong Wang. 2011. Pushing the limits: A very compact and a threshold implementation of AES. In EUROCRYPT. 69--88.","DOI":"10.1007\/978-3-642-20465-4_6"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33027-8_4"},{"key":"e_1_2_1_52_1","unstructured":"NIST. 2013. Keccak reference code submission to NIST's SHA-3 competition (Round 3). URL: http:\/\/csrc.nist.gov\/groups\/ST\/hash\/sha-3\/Round3\/documents\/Keccak_FinalRnd.zip. (2013).  NIST. 2013. Keccak reference code submission to NIST's SHA-3 competition (Round 3). URL: http:\/\/csrc.nist.gov\/groups\/ST\/hash\/sha-3\/Round3\/documents\/Keccak_FinalRnd.zip. (2013)."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_28"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33027-8_2"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_1_57_1","volume-title":"Cryptologic Spectrum","volume":"2","author":"TEMPEST.","year":"1972","unstructured":"TEMPEST. 1972 . A signal problem - the story of the discovery of various compromising radiations from communications and Comsec equipment . Cryptologic Spectrum , Vol. 2 , No. 3, National Security Agency, partially FOAI declassified 2007-09-27 (1972). TEMPEST. 1972. A signal problem - the story of the discovery of various compromising radiations from communications and Comsec equipment. Cryptologic Spectrum, Vol. 2, No. 3, National Security Agency, partially FOAI declassified 2007-09-27 (1972)."},{"key":"e_1_2_1_58_1","unstructured":"Xilinx. 2014. MicroBlaze soft processor core. (2014). URL: http:\/\/www.xilinx.com\/tools\/microblaze.htm.  Xilinx. 2014. MicroBlaze soft processor core. (2014). URL: http:\/\/www.xilinx.com\/tools\/microblaze.htm."}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3090064.3090071","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3090064.3090071","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:22Z","timestamp":1750215802000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3090064.3090071"}},"subtitle":["an automated approach to comprehensive side-channel resistance"],"short-title":[],"issued":{"date-parts":[[2017,5,3]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,5,3]]}},"alternative-id":["10.1145\/3090064.3090071"],"URL":"https:\/\/doi.org\/10.1145\/3090064.3090071","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2017,5,3]]},"assertion":[{"value":"2017-05-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}