{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:54Z","timestamp":1775873634687,"version":"3.50.1"},"reference-count":92,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2020,2,17]],"date-time":"2020-02-17T00:00:00Z","timestamp":1581897600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,2,17]],"date-time":"2020-02-17T00:00:00Z","timestamp":1581897600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10817-020-09548-x","type":"journal-article","created":{"date-parts":[[2020,2,17]],"date-time":"2020-02-17T15:06:56Z","timestamp":1581952016000},"page":"1685-1729","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory"],"prefix":"10.1007","volume":"64","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gustavo","family":"Betarte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan Diego","family":"Campo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9985-5927","authenticated-orcid":false,"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,2,17]]},"reference":[{"key":"9548_CR1","first-page":"186","volume":"2012","author":"G Barthe","year":"2012","unstructured":"Barthe, G., Betarte, G., Campo, J., Luna, C.: Cache-leakage resilient OS isolation in an idealized model of virtualization. CSF 2012, 186\u2013197 (2012)","journal-title":"CSF"},{"key":"9548_CR2","unstructured":"Bernstein, D.J.: Cache-timing attacks on AES (2005). Available from author\u2019s webpage"},{"issue":"1","key":"9548_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s00145-009-9049-y","volume":"23","author":"E Tromer","year":"2010","unstructured":"Tromer, E., Osvik, D.A., Shamir, A.: Efficient cache attacks on AES, and countermeasures. J. Cryptol. 23(1), 37\u201371 (2010)","journal-title":"J. Cryptol."},{"key":"9548_CR4","doi-asserted-by":"crossref","unstructured":"Wang, Z., Lee, R.B.: New cache designs for thwarting software cache-based side channel attacks. In: ISCA 2007, pp. 494\u2013505. ACM (2007)","DOI":"10.1145\/1273440.1250723"},{"key":"9548_CR5","unstructured":"Erlingsson, U., Abadi, M.: Operating system protection against side-channel attacks that exploit memory latency. Tech. Rep. MSR-TR-2007-117, Microsoft Research (2007)"},{"key":"9548_CR6","unstructured":"Kim, T., Peinado, M., Mainar-Ruiz, G.: STEALTHMEM: system-level protection against cache-based side channel attacks in the cloud. In: USENIX Security 2012, pp. 11\u201311. USENIX Association, Berkeley (2012)"},{"key":"9548_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9441-5","author":"G Barthe","year":"2017","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: System-level non-interference of constant-time cryptography part I: model. J. Autom. Reason. (2017). https:\/\/doi.org\/10.1007\/s10817-017-9441-5","journal-title":"J. Autom. Reason."},{"key":"9548_CR8","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual (2018)"},{"key":"9548_CR9","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"9548_CR10","unstructured":"Sison, R., Murray, T.C.: Verifying that a compiler preserves concurrent value-dependent information-flow security. CoRR abs\/1907.00713 (2019). http:\/\/arxiv.org\/abs\/1907.00713"},{"key":"9548_CR11","doi-asserted-by":"publisher","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201973, pp. 194\u2013206. ACM, New York (1973). https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"issue":"7","key":"9548_CR12","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977). https:\/\/doi.org\/10.1145\/359636.359712","journal-title":"Commun. ACM"},{"key":"9548_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X., Robert, V.: A formally-verified alias analysis. In: CPP, pp. 11\u201326 (2012)","DOI":"10.1007\/978-3-642-35308-6_5"},{"key":"9548_CR14","doi-asserted-by":"publisher","unstructured":"Hind, M.: Pointer analysis: Haven\u2019t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE \u201901, pp. 54\u201361. ACM, New York (2001). https:\/\/doi.org\/10.1145\/379605.379665","DOI":"10.1145\/379605.379665"},{"key":"9548_CR15","doi-asserted-by":"publisher","unstructured":"Chrz\u0105szcz, J.: Implementing modules in the Coq system. In: Basin, D., Wolff, B. (eds.) Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 2758, pp. 270\u2013286. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/10930755_18","DOI":"10.1007\/10930755_18"},{"key":"9548_CR16","doi-asserted-by":"crossref","unstructured":"K\u00e4sper, E., Schwabe, P.: Faster and timing-attack resistant AES-GCM. In: Clavier, C., Gaj, K. (eds.) CHES, Lecture Notes in Computer Science, vol. 5747, pp. 1\u201317. Springer (2009)","DOI":"10.1007\/978-3-642-04138-9_1"},{"key":"9548_CR17","doi-asserted-by":"crossref","unstructured":"Coppens, B., Verbauwhede, I., Bosschere, K.D., Sutter, B.D.: Practical mitigations for timing-based side-channel attacks on modern x86 processors. In: S&P 2009, pp. 45\u201360 (2009)","DOI":"10.1109\/SP.2009.19"},{"key":"9548_CR18","unstructured":"Advanced encryption standard (AES). Tech. Rep. FIPS PUB 197, Federal Information Processing Standards Publications (2001)"},{"key":"9548_CR19","unstructured":"ARM Limited.: mbed TLS. See https:\/\/tls.mbed.org\/"},{"key":"9548_CR20","unstructured":"Data encryption standard (DES). Tech. Rep. FIPS PUB 46, Federal Information Processing Standards Publications (1977)"},{"key":"9548_CR21","unstructured":"Schneier, B.: The Blowfish encryption algorithm. http:\/\/www.schneier.com\/blowfish.html"},{"key":"9548_CR22","doi-asserted-by":"crossref","unstructured":"Tsunoo, Y., Saito, T., Suzaki, T., Shigeri, M., Miyauchi, H.: Cryptanalysis of DES implemented on computers with cache. In: CHES 2003, LNCS, vol. 2779, pp. 62\u201376. Springer (2003)","DOI":"10.1007\/978-3-540-45238-6_6"},{"issue":"2\u20133","key":"9548_CR23","doi-asserted-by":"publisher","first-page":"141","DOI":"10.3233\/JCS-2000-82-304","volume":"8","author":"J Kelsey","year":"2000","unstructured":"Kelsey, J., Schneier, B., Wagner, D., Hall, C.: Side channel cryptanalysis of product ciphers. J. Comput. Secur. 8(2\u20133), 141\u2013158 (2000)","journal-title":"J. Comput. Secur."},{"key":"9548_CR24","unstructured":"Schneier, B.: The Blowfish source code. http:\/\/www.schneier.com\/blowfish-download.html"},{"key":"9548_CR25","unstructured":"3rd Generation Partnership\u00a0Project: Specification of the 3GPP confidentiality and integrity algorithms UEA2 & UIA2; document 2: SNOW 3G specification (2006)"},{"key":"9548_CR26","doi-asserted-by":"publisher","unstructured":"Leander, G., Zenner, E., Hawkes, P.: Cache timing analysis of LFSR-based stream ciphers. In: IMACC 2009, LNCS, vol. 5921, pp. 433\u2013445. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-10868-6_26","DOI":"10.1007\/978-3-642-10868-6_26"},{"key":"9548_CR27","doi-asserted-by":"crossref","unstructured":"Chardin, T., Fouque, P.A., Leresteux, D.: Cache timing analysis of RC4. In: ACNS 2011, LNCS, vol. 6715, pp. 110\u2013129 (2011)","DOI":"10.1007\/978-3-642-21554-4_7"},{"key":"9548_CR28","doi-asserted-by":"publisher","unstructured":"Wheeler, D., Needham, R.: TEA, a tiny encryption algorithm. In: Preneel, B. (ed.) Fast Software Encryption, Lecture Notes in Computer Science, vol. 1008, pp. 363\u2013366. Springer, Berlin (1995). https:\/\/doi.org\/10.1007\/3-540-60590-8_29","DOI":"10.1007\/3-540-60590-8_29"},{"key":"9548_CR29","unstructured":"Bernstein, D.: Salsa20 Specification (2005)"},{"key":"9548_CR30","unstructured":"Secure Hash Standard. Tech. Rep. FIPS PUB 180-4, Federal Information Processing Standards Publications (2012)"},{"key":"9548_CR31","doi-asserted-by":"publisher","unstructured":"Bogdanov, A., Khovratovich, D., Rechberger, C.: Biclique cryptanalysis of the full AES. In: Lee, D., Wang, X. (eds.) Advances in Cryptology\u2014ASIACRYPT 2011, Lecture Notes in Computer Science, vol. 7073, pp. 344\u2013371. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-25385-0_19","DOI":"10.1007\/978-3-642-25385-0_19"},{"key":"9548_CR32","doi-asserted-by":"publisher","unstructured":"Fouque, P.A., Jean, J., Peyrin, T.: Structural evaluation of AES and chosen-key distinguisher of 9-round AES-128. In: Canetti, R., Garay, J. (eds.) Advances in Cryptology\u2014CRYPTO 2013, Lecture Notes in Computer Science, vol. 8042, pp. 183\u2013203. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-40041-4_11","DOI":"10.1007\/978-3-642-40041-4_11"},{"key":"9548_CR33","unstructured":"Koeune, F., Quisquater, J.J.: A timing attack against Rijndael. Tech. rep. Universit\u00e9 Catholique de Louvain (1999)"},{"key":"9548_CR34","doi-asserted-by":"crossref","unstructured":"Bonneau, J., Mironov, I.: Cache collision timing attacks against AES. In: CHES \u201906 (2006)","DOI":"10.1007\/11894063_16"},{"key":"9548_CR35","doi-asserted-by":"crossref","unstructured":"Acii\u00e7mez, O., Schindler, W., Kaya\u00a0Ko\u00e7, \u00c7etin: Cache based remote timing attack on the AES. In: CT-RSA 2007, LNCS, vol. 4377, pp. 271\u2013286. Springer (2007)","DOI":"10.1007\/11967668_18"},{"key":"9548_CR36","unstructured":"Canteaut, A., Lauradoux, C., Seznec, A.: Understanding cache attacks. Rapport de recherche RR-5881, INRIA (2006). http:\/\/hal.inria.fr\/inria-00071387"},{"key":"9548_CR37","doi-asserted-by":"crossref","unstructured":"Gullasch, D., Bangerter, E., Krenn, S.: Cache games\u2014bringing access-based cache attacks on AES to practice. In: S&P 2011, pp. 490\u2013505 (2011)","DOI":"10.1109\/SP.2011.22"},{"key":"9548_CR38","doi-asserted-by":"crossref","unstructured":"Ristenpart, T., Tromer, E., Shacham, H., Savage, S.: Hey, you, get off of my cloud! Exploring information leakage in third-party compute clouds. In: CCS 2009, pp. 199\u2013212. ACM Press (2009)","DOI":"10.1145\/1653662.1653687"},{"key":"9548_CR39","unstructured":"Daemen, J., Daemen, J., Daemen, J., Rijmen, V., Rijmen, V.: AES proposal: Rijndael (1998)"},{"key":"9548_CR40","doi-asserted-by":"crossref","unstructured":"Kocher, P.: Timing attacks on implementations of Diffie\u2013Hellman, RSA, DSS, and Other Systems. In: CRYPTO\u201996, LNCS, vol. 1109, pp. 104\u2013113. Springer (1996)","DOI":"10.1007\/3-540-68697-5_9"},{"key":"9548_CR41","doi-asserted-by":"publisher","unstructured":"Aly, H., ElGayyar, M.: Attacking AES using Bernstein\u2019s attack on modern processors. In: Youssef, A., Nitaj, A., Hassanien, A. (eds.) Progress in Cryptology\u2014AFRICACRYPT 2013, Lecture Notes in Computer Science, vol. 7918, pp. 127\u2013139. Springer Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-38553-7_7","DOI":"10.1007\/978-3-642-38553-7_7"},{"key":"9548_CR42","unstructured":"Irazoqui, G., Inci, M.S., Eisenbarth, T., Sunar, B.: Fine grain cross-VM attacks on Xen and VMware are possible! IACR Cryptology ePrint Archive 2014, 248 (2014). http:\/\/eprint.iacr.org\/2014\/248"},{"key":"9548_CR43","doi-asserted-by":"publisher","unstructured":"Genkin, D., Valenta, L., Yarom, Y.: May the fourth be with you: A microarchitectural side channel attack on several real-world applications of curve25519. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, October 30\u2013November 03, 2017, pp. 845\u2013858. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134029","DOI":"10.1145\/3133956.3134029"},{"issue":"2","key":"9548_CR44","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s13389-017-0152-y","volume":"7","author":"Y Yarom","year":"2017","unstructured":"Yarom, Y., Genkin, D., Heninger, N.: Cachebleed: a timing attack on openssl constant-time RSA. J. Cryptogr. Eng. 7(2), 99\u2013112 (2017). https:\/\/doi.org\/10.1007\/s13389-017-0152-y","journal-title":"J. Cryptogr. Eng."},{"key":"9548_CR45","doi-asserted-by":"publisher","unstructured":"Ronen, E., Paterson, K.G., Shamir, A.: Pseudo constant time implementations of TLS are only pseudo secure. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, October 15\u201319, 2018, pp. 1397\u20131414. ACM (2018). https:\/\/doi.org\/10.1145\/3243734.3243775","DOI":"10.1145\/3243734.3243775"},{"key":"9548_CR46","doi-asserted-by":"publisher","unstructured":"Shi, J., Song, X., Chen, H., Zang, B.: Limiting cache-based side-channel in multi-tenant cloud using dynamic page coloring. In: Dependable Systems and Networks Workshops (DSN-W), 2011 IEEE\/IFIP 41st International Conference on, pp. 194\u2013199 (2011). https:\/\/doi.org\/10.1109\/DSNW.2011.5958812","DOI":"10.1109\/DSNW.2011.5958812"},{"key":"9548_CR47","doi-asserted-by":"crossref","unstructured":"Dziembowski, S., Pietrzak, K.: Leakage-resilient cryptography. In: FOCS, pp. 293\u2013302. IEEE Computer Society (2008)","DOI":"10.1109\/FOCS.2008.56"},{"key":"9548_CR48","unstructured":"Barbosa, M., Barthe, G., Bhargavan, K., Blanchet, B., Cremers, C., Liao, K., Parno, B.: Sok: Computer-aided cryptography. IACR Cryptology ePrint Archive 2019, 1393 (2019). https:\/\/eprint.iacr.org\/2019\/1393"},{"key":"9548_CR49","doi-asserted-by":"crossref","unstructured":"Agat, J.: Transforming out Timing Leaks. In: Proceedings POPL\u201900, pp. 40\u201353. ACM (2000)","DOI":"10.1145\/325694.325702"},{"key":"9548_CR50","first-page":"156","volume":"2005","author":"D Molnar","year":"2005","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: automatic detection and removal of control-flow side channel attacks. ICISC 2005, 156\u2013168 (2005)","journal-title":"ICISC"},{"key":"9548_CR51","doi-asserted-by":"publisher","unstructured":"Zhang, D., Askarov, A., Myers, A.C.: Predictive mitigation of timing channels in interactive systems. In: Chen, Y., Danezis, G., Shmatikov V. (eds.) Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17\u201321, pp. 563\u2013574. ACM (2011). https:\/\/doi.org\/10.1145\/2046707.2046772","DOI":"10.1145\/2046707.2046772"},{"key":"9548_CR52","doi-asserted-by":"crossref","unstructured":"Stefan, D., Buiras, P., Yang, E.Z., Levy, A., Terei, D., Russo, A., Mazi\u00e8res, D.: Eliminating cache-based timing attacks with instruction-based scheduling. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS, Lecture Notes in Computer Science, vol. 8134, pp. 718\u2013735. Springer (2013)","DOI":"10.1007\/978-3-642-40203-6_40"},{"key":"9548_CR53","first-page":"51","volume":"2013","author":"C Liu","year":"2013","unstructured":"Liu, C., Hicks, M., Shi, E.: Memory trace oblivious program execution. CSF 2013, 51\u201365 (2013)","journal-title":"CSF"},{"key":"9548_CR54","unstructured":"Doychev, G., Feld, D., K\u00f6pf, B., Mauborgne, L., Reineke, J.: Cacheaudit: A tool for the static analysis of cache side channels. In: Usenix Security (2013)"},{"key":"9548_CR55","doi-asserted-by":"publisher","unstructured":"Doychev, G., K\u00f6pf, B.: Rigorous analysis of software countermeasures against cache attacks. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, June 18\u201323, 2017, pp. 406\u2013421. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062388","DOI":"10.1145\/3062341.3062388"},{"key":"9548_CR56","doi-asserted-by":"crossref","unstructured":"Barthe, G., K\u00f6pf, B., Mauborgne, L., Ochoa, M.: Leakage resilience against concurrent cache attacks. In: POST (2014)","DOI":"10.1007\/978-3-642-54792-8_8"},{"issue":"1","key":"9548_CR57","first-page":"7","volume":"18","author":"S Chattopadhyay","year":"2019","unstructured":"Chattopadhyay, S., Beck, M., Rezine, A., Zeller, A.: Quantifying the information leakage in cache attacks via symbolic execution. ACM Trans. Embed. Comput. Syst. (TECS) 18(1), 7 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"9548_CR58","unstructured":"Wang, S., Wang, P., Liu, X., Zhang, D., Wu, D.: Cached: Identifying cache-based timing channels in production software. In: 26th $$\\{$$USENIX$$\\}$$ Security Symposium ($$\\{$$USENIX$$\\}$$ Security 17), pp. 235\u2013252 (2017)"},{"key":"9548_CR59","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Phan, Q.S., Malacaria, P.: Multi-run side-channel analysis using symbolic execution and max-smt. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 387\u2013400. IEEE (2016)","DOI":"10.1109\/CSF.2016.34"},{"key":"9548_CR60","doi-asserted-by":"publisher","unstructured":"Blazy, S., Pichardie, D., Trieu, A.: Verifying constant-time implementations by abstract interpretation. In: Foley, S.N., Gollmann, D., Snekkenes, E. (eds.) Computer Security\u2014ESORICS 2017\u201422nd European Symposium on Research in Computer Security, Oslo, September 11\u201315, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10492, pp. 260\u2013277. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66402-6_16","DOI":"10.1007\/978-3-319-66402-6_16"},{"key":"9548_CR61","doi-asserted-by":"publisher","unstructured":"Barthe, G., Blazy, S., Laporte, V., Pichardie, D., Trieu, A.: Verified translation validation of static analyses. In: 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21\u201325, 2017, pp. 405\u2013419. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/CSF.2017.16","DOI":"10.1109\/CSF.2017.16"},{"key":"9548_CR62","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: Holz, T., Savage, S. (eds.) 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10\u201312, 2016., pp. 53\u201370. USENIX Association (2016). https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"key":"9548_CR63","doi-asserted-by":"publisher","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M.J., Schulte, W. (eds.) FM 2011: Formal Methods\u201417th International Symposium on Formal Methods, Limerick, Ireland, June 20\u201324, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6664, pp. 200\u2013214. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17","DOI":"10.1007\/978-3-642-21437-0_17"},{"issue":"5","key":"9548_CR64","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1016\/j.jlamp.2016.05.004","volume":"85","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Log. Algebra Methods Progr. 85(5), 847\u2013859 (2016). https:\/\/doi.org\/10.1016\/j.jlamp.2016.05.004","journal-title":"J. Log. Algebra Methods Progr."},{"key":"9548_CR65","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Blot, A., Gr\u00e9goire, B., Laporte, V., Oliveira, T., Pacheco, H., Schmidt, B., Strub, P.: Jasmin: High-assurance and high-speed cryptography. In: Thuraisingham, B.M., Evans, D., Malkin,T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pp. 1807\u20131823. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134078","DOI":"10.1145\/3133956.3134078"},{"key":"9548_CR66","unstructured":"Bond, B., Hawblitzel, C., Kapritsos, M., Leino, K.R.M., Lorch, J.R., Parno, B., Rane, A., Setty, S.T.V., Thompson, L.: Vale: Verifying high-performance cryptographic assembly code. In: Kirda, E., Ristenpart, T. (eds.) 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, August 16\u201318, 2017., pp. 917\u2013934. USENIX Association (2017). https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"9548_CR67","doi-asserted-by":"publisher","unstructured":"Rodrigues, B., Pereira, F.M.Q., Aranha, D.F.: Sparse representation of implicit flows with applications to side-channel detection. In: Zaks, A., Hermenegildo, M.V. (eds.) Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, March 12\u201318, 2016, pp. 110\u2013120. ACM (2016). https:\/\/doi.org\/10.1145\/2892208.2892230","DOI":"10.1145\/2892208.2892230"},{"issue":"POPL","key":"9548_CR68","doi-asserted-by":"publisher","first-page":"77:1","DOI":"10.1145\/3290390","volume":"3","author":"C Watt","year":"2019","unstructured":"Watt, C., Renner, J., Popescu, N., Cauligi, S., Stefan, D.: Ct-wasm: type-driven secure cryptography for the web ecosystem. PACMPL 3(POPL), 77:1\u201377:29 (2019). https:\/\/doi.org\/10.1145\/3290390","journal-title":"PACMPL"},{"key":"9548_CR69","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic \u201cconstant-time\u201d. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9\u201312, 2018, pp. 328\u2013343. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00031","DOI":"10.1109\/CSF.2018.00031"},{"key":"9548_CR70","doi-asserted-by":"publisher","unstructured":"Wu, M., Guo, S., Schaumont, P., Wang, C.: Eliminating timing side-channel leaks using program repair. In: Tip, F., Bodden, E. (eds.) Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, Amsterdam, July 16\u201321, 2018, pp. 15\u201326. ACM (2018). https:\/\/doi.org\/10.1145\/3213846.3213851","DOI":"10.1145\/3213846.3213851"},{"key":"9548_CR71","doi-asserted-by":"crossref","unstructured":"Cauligi, S., Soeller, G., Brown, F., Renner, J., Johannesmeyer, B., Wahby, R.S., Gr\u00e9goire, B., Barthe, G., Jhala, R., Stefan, D.: FaCT: A dsl for timing-sensitive computation. In: Proceedings of PLDI 2019. ACM (2019)","DOI":"10.1145\/3314221.3314605"},{"key":"9548_CR72","doi-asserted-by":"publisher","unstructured":"Besson, F., Dang, A., Jensen, T.P.: Securing compilation against memory probing. In: Alvim, M.S., Delaune, S. (eds.) Proceedings of the 13th Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2018, Toronto, ON, October 15\u201319, 2018, pp. 29\u201340. ACM (2018). https:\/\/doi.org\/10.1145\/3264820.3264822","DOI":"10.1145\/3264820.3264822"},{"key":"9548_CR73","doi-asserted-by":"publisher","unstructured":"Besson, F., Dang, A., Jensen, T.P.: Information-flow preservation in compiler optimisations. In: 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, June 25\u201328, 2019, pp. 230\u2013242. IEEE (2019). https:\/\/doi.org\/10.1109\/CSF.2019.00023","DOI":"10.1109\/CSF.2019.00023"},{"key":"9548_CR74","unstructured":"Lipp, M., Schwarz, M., Gruss, D., Prescher, T., Haas, W., Fogh, A., Horn, J., Mangard, S., Kocher, P., Genkin, D., Yarom, Y., Hamburg, M.: Meltdown: Reading kernel memory from user space. In: 27th USENIX Security Symposium (USENIX Security 18) (2018)"},{"key":"9548_CR75","unstructured":"Van\u00a0Bulck, J., Minkin, M., Weisse, O., Genkin, D., Kasikci, B., Piessens, F., Silberstein, M., Wenisch, T.F., Yarom, Y., Strackx, R.: Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution. In: Proceedings of the 27th USENIX Security Symposium. USENIX Association (2018). (See also technical report Foreshadow-NG\u00a0[86])"},{"key":"9548_CR76","unstructured":"Weisse, O., Van\u00a0Bulck, J., Minkin, M., Genkin, D., Kasikci, B., Piessens, F., Silberstein, M., Strackx, R., Wenisch, T.F., Yarom, Y.: Foreshadow-NG: Breaking the virtual memory abstraction with transient out-of-order execution. Tech. Rep.(2018). (See also USENIX Security paper Foreshadow\u00a0[82])"},{"key":"9548_CR77","doi-asserted-by":"crossref","unstructured":"Kocher, P., Horn, J., Fogh, A., , Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: exploiting speculative execution. In: 40th IEEE Symposium on Security and Privacy (S&P\u201919) (2019)","DOI":"10.1109\/SP.2019.00002"},{"key":"9548_CR78","doi-asserted-by":"publisher","unstructured":"Cheang, K., Rasmussen, C., Seshia, S.A., Subramanyan, P.: A formal approach to secure speculation. In: 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, June 25\u201328, 2019, pp. 288\u2013303. IEEE (2019). https:\/\/doi.org\/10.1109\/CSF.2019.00027","DOI":"10.1109\/CSF.2019.00027"},{"key":"9548_CR79","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: POPL 2010. ACM (2010)","DOI":"10.1145\/1706299.1706350"},{"key":"9548_CR80","doi-asserted-by":"crossref","unstructured":"Dupressoir, F., Gordon, A.D., J\u00fcrjens, J., Naumann, D.A.: Guiding a general-purpose C verifier to prove cryptographic protocols. In: CSF 2011, pp. 3\u201317. IEEE Computer Society (2011)","DOI":"10.1109\/CSF.2011.8"},{"key":"9548_CR81","doi-asserted-by":"crossref","unstructured":"Cad\u00e9, D., Blanchet, B.: From computationally-proved protocol specifications to implementations. In: ARES 2012, pp. 65\u201374. IEEE Computer Society (2012)","DOI":"10.1109\/ARES.2012.63"},{"key":"9548_CR82","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Computational verification of C protocol implementations by symbolic execution. In: CCS 2012, pp. 712\u2013723. ACM (2012)","DOI":"10.1145\/2382196.2382271"},{"key":"9548_CR83","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In: CCS (2013)","DOI":"10.1145\/2508859.2516652"},{"key":"9548_CR84","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Zanella-B\u00e9guelin, S.: Computer-aided security proofs for the working cryptographer. In: CRYPTO 2011, LNCS, vol. 6841. Heidelberg (2011)","DOI":"10.1007\/978-3-642-22792-9_5"},{"issue":"2","key":"9548_CR85","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2701415","volume":"37","author":"AW Appel","year":"2015","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Progr. Lang. Syst. 37(2), 7:1\u20137:31 (2015). https:\/\/doi.org\/10.1145\/2701415","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"9548_CR86","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics\u2013for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W.: Program Logics\u2013for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"9548_CR87","unstructured":"Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of openssl HMAC. In: Jung, J., Holz, T. (eds.) 24th USENIX Security Symposium, USENIX Security 15, Washington, DC, August 12\u201314, 2015., pp. 207\u2013221. USENIX Association (2015). https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"key":"9548_CR88","doi-asserted-by":"publisher","unstructured":"Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedtls HMAC-DRBG. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, October 30\u2013November 03, 2017, pp. 2007\u20132020. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3133974","DOI":"10.1145\/3133956.3133974"},{"key":"9548_CR89","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: Hacl*: A verified modern cryptographic library. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, October 30\u2013November 03, 2017, pp. 1789\u20131806. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"},{"key":"9548_CR90","doi-asserted-by":"publisher","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, September 19\u201321, 2011, pp. 266\u2013278. ACM (2011). https:\/\/doi.org\/10.1145\/2034773.2034811","DOI":"10.1145\/2034773.2034811"},{"key":"9548_CR91","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic\u2014with proofs, without compromises. In: Proceedings of Security and Privacy (2019)","DOI":"10.1109\/SP.2019.00005"},{"key":"9548_CR92","doi-asserted-by":"crossref","unstructured":"Barthe, G., Rezk, T., Naumann, D.A.: Deriving an information flow checker and certifying compiler for java. In: S&P 2006, pp. 230\u2013242. IEEE Computer Society (2006)","DOI":"10.1109\/SP.2006.13"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09548-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-020-09548-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09548-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,18]],"date-time":"2021-02-18T23:17:18Z","timestamp":1613690238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-020-09548-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,17]]},"references-count":92,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["9548"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09548-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,17]]},"assertion":[{"value":"30 March 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}