{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:45:02Z","timestamp":1778121902694,"version":"3.51.4"},"reference-count":51,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2018,9,24]],"date-time":"2018-09-24T00:00:00Z","timestamp":1537747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2019,1,11]]},"abstract":"<jats:p>Constant-time programming is an established discipline to secure programs against timing attackers. Several real-world secure C libraries such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We propose an advanced static analysis, based on state-of-the-art techniques from abstract interpretation, to report time leakage during programming. To that purpose, we analyze source C programs and use full context-sensitive and arithmetic-aware alias analyses to track the tainted flows.<\/jats:p>\n                  <jats:p>We give semantic evidence of the correctness of our approach on a core language. We also present a prototype implementation for C programs that is based on the CompCert compiler toolchain and its companion Verasco static analyzer. We present verification results on various real-world constant-time programs and report on a successful verification of a challenging SHA-256 implementation that was out of scope of previous tool-assisted approaches.<\/jats:p>","DOI":"10.3233\/jcs-181136","type":"journal-article","created":{"date-parts":[[2018,9,25]],"date-time":"2018-09-25T16:24:40Z","timestamp":1537892680000},"page":"137-163","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":18,"title":["Verifying constant-time implementations by abstract interpretation"],"prefix":"10.1177","volume":"27","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[{"name":"Univ Rennes, Inria, CNRS, IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"Univ Rennes, Inria, CNRS, IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alix","family":"Trieu","sequence":"additional","affiliation":[{"name":"Univ Rennes, Inria, CNRS, IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2018,9,24]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"O.\u00a0Acii\u00e7mez, \u00c7.K.\u00a0Ko\u00e7 and J.P.\u00a0Seifert, On the power of simple branch prediction analysis, in: ACM Symposium on Information, Computer and Communications Security, ACM, 2007, pp.\u00a0312\u2013320.","DOI":"10.1145\/1229285.1266999"},{"key":"ref002","unstructured":"J.\u00a0Almeida, M.\u00a0Barbosa, G.\u00a0Barthe, A.\u00a0Blot, B.\u00a0Gr\u00e9goire, V.\u00a0Laporte, T.\u00a0Oliveira, H.\u00a0Pacheco, B.\u00a0Schmidt and P.Y.\u00a0Strub, Jasmin: High-assurance and high-speed cryptography, in: CCS 2017\u00a0\u2013 Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017."},{"key":"ref003","unstructured":"J.B.\u00a0Almeida, M.\u00a0Barbosa, G.\u00a0Barthe, F.\u00a0Dupressoir and M.\u00a0Emmi, Verifying constant-time implementations, in: 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10\u201312, 2016, 2016, pp.\u00a053\u201370."},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"M.\u00a0Andrysco, D.\u00a0Kohlbrenner, K.\u00a0Mowery, R.\u00a0Jhala, S.\u00a0Lerner and H.\u00a0Shacham, On subnormal floating point and abnormal timing, in: Proceedings of the 2015 IEEE Symposium on Security and Privacy, SP \u201915, IEEE Computer Society, Washington, DC, USA, 2015, pp.\u00a0623\u2013639. ISBN 978-1-4673-6949-7. doi:10.1109\/SP.2015.44.","DOI":"10.1109\/SP.2015.44"},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"ref006","doi-asserted-by":"crossref","unstructured":"M.\u00a0Barnett, B.E.\u00a0Chang, R.\u00a0DeLine, B.\u00a0Jacobs and K.R.M.\u00a0Leino, Boogie: A modular reusable verifier for object-oriented programs, in: Proc. of FMCO 2005, 2005, pp.\u00a0364\u2013387.","DOI":"10.1007\/11804192_17"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2015.112"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, G.\u00a0Betarte, J.D.\u00a0Campo, C.D.\u00a0Luna and D.\u00a0Pichardie, System-level non-interference for constant-time cryptography, in: ACM SIGSAC Conference on Computer and Communications Security, 2014, pp.\u00a01267\u20131279.","DOI":"10.1145\/2660267.2660283"},{"key":"ref009","unstructured":"BearSSL, https:\/\/www.bearssl.org\/."},{"key":"ref010","unstructured":"L.\u00a0Beringer, A.\u00a0Petcher, Q.Y.\u00a0Katherine and A.W.\u00a0Appel, Verified correctness and security of OpenSSL HMAC., in: USENIX Security Symposium, 2015, pp.\u00a0207\u2013221."},{"key":"ref011","doi-asserted-by":"crossref","unstructured":"D.J.\u00a0Bernstein, Curve25519: New Diffie-Hellman speed records, M.\u00a0Yung, Y.\u00a0Dodis, A.\u00a0Kiayias and T.\u00a0Malkin, eds, Springer, Berlin, Heidelberg, 2006, pp.\u00a0207\u2013228. ISBN 978-3-540-33852-9.","DOI":"10.1007\/11745853_14"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"D.J.\u00a0Bernstein, T.\u00a0Lange and P.\u00a0Schwabe, The security impact of a new cryptographic library, in: International Conference on Cryptology and Information Security in Latin America, Springer, 2012, pp.\u00a0159\u2013176.","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, P.\u00a0Cousot, R.\u00a0Cousot, J.\u00a0Feret, L.\u00a0Mauborgne, A.\u00a0Min\u00e9, D.\u00a0Monniaux and X.\u00a0Rival, A static analyzer for large safety-critical software, in: Programming Language Design and Implementation, ACM, 2003, pp.\u00a0196\u2013207.","DOI":"10.1145\/781131.781153"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"S.\u00a0Blazy, V.\u00a0Laporte and D.\u00a0Pichardie, An abstract memory functor for verified C static analyzers, in: Proc. of the 21st ACM SIGPLAN Int. Conference on Functional Programming (ICFP 2016), ACM, 2016.","DOI":"10.1145\/2951913.2951937"},{"key":"ref015","unstructured":"B.\u00a0Bond, C.\u00a0Hawblitzel, M.\u00a0Kapritsos, K.R.M.\u00a0Leino, J.R.\u00a0Lorch, B.\u00a0Parno, A.\u00a0Rane, S.\u00a0Setty and L.\u00a0Thompson, Vale: Verifying high-performance cryptographic assembly code, in: Proceedings of the USENIX Security Symposium, 2017."},{"key":"ref016","doi-asserted-by":"crossref","unstructured":"J.W.\u00a0Bos, C.\u00a0Costello, M.\u00a0Naehrig and D.\u00a0Stebila, Post-quantum key exchange for the TLS protocol from the ring learning with errors problem, in: 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17\u201321, 2015, 2015, pp.\u00a0553\u2013570.","DOI":"10.1109\/SP.2015.40"},{"key":"ref017","doi-asserted-by":"crossref","unstructured":"B.\u00a0Canvel, A.\u00a0Hiltgen, S.\u00a0Vaudenay and M.\u00a0Vuagnoux, Password interception in a SSL\/TLS channel, in: CRYPTO, LNCS, Vol.\u00a02729, Springer, 2003, pp.\u00a0583\u2013599.","DOI":"10.1007\/978-3-540-45146-4_34"},{"key":"ref018","doi-asserted-by":"crossref","unstructured":"S.\u00a0Cauligi, G.\u00a0Soeller, F.\u00a0Brown, B.\u00a0Johannesmeyer, Y.\u00a0Huang, R.\u00a0Jhala and D.\u00a0Stefan, FaCT: A flexible, constant-time programming language, in: Cybersecurity Development (SecDev), 2017 IEEE, IEEE, 2017, pp.\u00a069\u201376. doi:10.1109\/SecDev.2017.24.","DOI":"10.1109\/SecDev.2017.24"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"P.\u00a0Cousot and R.\u00a0Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, ACM, 1977, pp.\u00a0238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"ref020","unstructured":"ctgrind, https:\/\/github.com\/agl\/ctgrind."},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"\u00c1.\u00a0Darvas, R.\u00a0H\u00e4hnle and D.\u00a0Sands, A theorem proving approach to analysis of secure information flow, in: Proc. 2nd International Conference on Security in Pervasive Computing, D.\u00a0Hutter and M.\u00a0Ullmann, eds, LNCS, Vol.\u00a03450, Springer-Verlag, 2005, pp.\u00a0193\u2013209. doi:10.1007\/978-3-540-32004-3_20.","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"ref022","doi-asserted-by":"crossref","unstructured":"L.\u00a0De Moura and N.\u00a0Bj\u00f8rner, Z3: An efficient SMT solver, in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, pp.\u00a0337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"ref024","unstructured":"donna, https:\/\/code.google.com\/archive\/p\/curve25519-donna."},{"key":"ref025","unstructured":"G.\u00a0Doychev, D.\u00a0Feld, B.\u00a0K\u00f6pf, L.\u00a0Mauborgne and J.\u00a0Reineke, CacheAudit: A tool for the static analysis of cache side channels, in: USENIX Conference on Security, USENIX Association, Berkeley, CA, USA, 2013, pp.\u00a0431\u2013446."},{"key":"ref026","doi-asserted-by":"crossref","unstructured":"A.\u00a0Erbsen, J.\u00a0Philipoom, J.\u00a0Gross, R.\u00a0Sloan and A.\u00a0Chlipala, Simple high-level code for cryptographic arithmetic\u00a0\u2013 With proofs, without compromises, in: Proceedings of the 40th IEEE Symposium on Security and Privacy (S&P\u201919), 2019.","DOI":"10.1109\/SP.2019.00005"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"N.J.A.\u00a0Fardan and K.G.\u00a0Paterson, Lucky thirteen: Breaking the TLS and DTLS record protocols, in: Symp. on Security and Privacy (SP 2013), IEEE Computer Society, 2013, pp.\u00a0526\u2013540. doi:10.1109\/SP.2013.42.","DOI":"10.1109\/SP.2013.42"},{"key":"ref028","doi-asserted-by":"crossref","unstructured":"J.\u00a0Feret, Static analysis of digital filters, in: European Symposium on Programming (ESOP\u201904), LNCS, Vol.\u00a02986, Springer, 2004.","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-009-0086-1"},{"key":"ref030","unstructured":"D.\u00a0Hedin and A.\u00a0Sabelfeld, A perspective on information-flow control, in: Software Safety and Security\u00a0\u2013 Tools for Analysis and Verification, IOS Press, 2012, pp.\u00a0319\u2013347."},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"J.H.\u00a0Jourdan, V.\u00a0Laporte, S.\u00a0Blazy, X.\u00a0Leroy and D.\u00a0Pichardie, A formally-verified C static analyzer, in: Proc. of the 42th ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages, POPL 2015, ACM, 2015, pp.\u00a0247\u2013259.","DOI":"10.1145\/2676726.2676966"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"P.\u00a0Kocher, Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems, in: Advances in Cryptology\u00a0\u2013 CRYPTO \u201996, LNCS, Vol.\u00a01109, Springer, 1996, pp.\u00a0104\u2013113.","DOI":"10.1007\/3-540-68697-5_9"},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"C.\u00a0Lattner, A.\u00a0Lenharth and V.S.\u00a0Adve, Making context-sensitive points-to analysis with heap cloning practical for the real world, in: Proc. of PLDI\u201907, 2007, pp.\u00a0278\u2013289. doi:10.1145\/1250734.1250766.","DOI":"10.1145\/1250734.1250766"},{"key":"ref034","doi-asserted-by":"crossref","unstructured":"K.R.M.\u00a0Leino, Dafny: An automatic program verifier for functional correctness, in: International Conference on Logic for Programming Artificial Intelligence and Reasoning, Springer, 2010, pp.\u00a0348\u2013370. doi:10.1007\/978-3-642-17511-4_20.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"ref035","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref036","unstructured":"mbed TLS (formerly known as PolarSSL), https:\/\/tls.mbed.org\/."},{"key":"ref037","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"ref038","doi-asserted-by":"crossref","unstructured":"A.\u00a0Min\u00e9, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, in: Proc. of the ACM SIGPLAN\u2013SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES\u201906), ACM, 2006, pp.\u00a054\u201363.","DOI":"10.1145\/1134650.1134659"},{"key":"ref039","doi-asserted-by":"crossref","unstructured":"A.C.\u00a0Myers, JFlow: Practical mostly-static information flow control, in: Proc. of POPL\u201999, 1999, pp.\u00a0228\u2013241. doi:10.1145\/292540.292561.","DOI":"10.1145\/292540.292561"},{"key":"ref040","unstructured":"Open Quantum Safe, https:\/\/openquantumsafe.org\/."},{"key":"ref041","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"O.\u00a0Reparaz, J.\u00a0Balasch and I.\u00a0Verbauwhede, Dude, is my code constant time, in: Proc. of DATE 2017, 2017.","DOI":"10.23919\/DATE.2017.7927267"},{"key":"ref043","doi-asserted-by":"crossref","unstructured":"B.\u00a0Rodrigues, F.M.\u00a0Quint\u00e3o Pereira and D.F.\u00a0Aranha, Sparse representation of implicit flows with applications to side-channel detection, in: Compiler Construction, ACM, 2016, pp.\u00a0110\u2013120.","DOI":"10.1145\/2892208.2892230"},{"key":"ref044","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"N.\u00a0Swamy, J.\u00a0Chen, C.\u00a0Fournet, P.\u00a0Strub, K.\u00a0Bhargavan and J.\u00a0Yang, Secure distributed programming with value-dependent types, in: Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, M.M.T.\u00a0Chakravarty, Z.\u00a0Hu and O.\u00a0Danvy, eds, ACM, 2011, pp.\u00a0266\u2013278, https:\/\/www.microsoft.com\/en-us\/research\/publication\/secure-distributed-programming-with-value-dependent-types\/. ISBN 978-1-4503-0865-6. doi:10.1145\/2034773.2034811.","DOI":"10.1145\/2034773.2034811"},{"key":"ref046","unstructured":"TIS-CT, http:\/\/trust-in-soft.com\/tis-ct\/."},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"D.J.\u00a0Wheeler and R.M.\u00a0Needham, TEA, a tiny encryption algorithm, B.\u00a0Preneel, ed. Springer, Berlin, Heidelberg, 1995, pp.\u00a0363\u2013366. ISBN 978-3-540-47809-6.","DOI":"10.1007\/3-540-60590-8_29"},{"key":"ref048","doi-asserted-by":"crossref","unstructured":"K.Q.\u00a0Ye, M.\u00a0Green, N.\u00a0Sanguansin, L.\u00a0Beringer, A.\u00a0Petcher and A.W.\u00a0Appel, Verified correctness and security of mbedTLS HMAC-DRBG, in: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201917, ACM, New York, NY, USA, 2017, pp.\u00a02007\u20132020, http:\/\/doi.acm.org\/10.1145\/3133956.3133974. ISBN 978-1-4503-4946-8. doi:10.1145\/3133956.3133974.","DOI":"10.1145\/3133956.3133974"},{"key":"ref049","doi-asserted-by":"crossref","unstructured":"J.\u00a0Zhao, S.\u00a0Zdancewic, S.\u00a0Nagarakatte and M.\u00a0Martin, Formalizing the LLVM intermediate representation for verified program transformation, in: POPL\u201912, ACM, New York, NY, USA, 2012, pp.\u00a0427\u2013440. doi:10.1145\/2103656.2103709.","DOI":"10.1145\/2103621.2103709"},{"key":"ref050","doi-asserted-by":"crossref","unstructured":"M.\u00a0Zhao and G.E.\u00a0Suh, FPGA-based remote power side-channel attacks, in: 2018 IEEE Symposium on Security and Privacy (SP), pp.\u00a0839\u2013854, doi.ieeecomputersociety.org\/10.1109\/SP.2018.00049. ISSN 2375-1207. doi:10.1109\/SP.2018.00049.","DOI":"10.1109\/SP.2018.00049"},{"key":"ref051","doi-asserted-by":"crossref","unstructured":"J.K.\u00a0Zinzindohou\u00e9, K.\u00a0Bhargavan, J.\u00a0Protzenko and B.\u00a0Beurdouche, HACL*: A verified modern cryptographic library, in: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201917, ACM, New York, NY, USA, 2017, pp.\u00a01789\u20131806, http:\/\/doi.acm.org\/10.1145\/3133956.3134043. ISBN 978-1-4503-4946-8. doi:10.1145\/3133956.3134043.","DOI":"10.1145\/3133956.3134043"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-181136","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-181136","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-181136","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:16Z","timestamp":1777495516000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-181136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,24]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,11]]}},"alternative-id":["10.3233\/JCS-181136"],"URL":"https:\/\/doi.org\/10.3233\/jcs-181136","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,24]]}}}