@inproceedings{DBLP:conf/esorics/BlazyPT17,
  author    = {Sandrine Blazy and
               David Pichardie and
               Alix Trieu},
  title     = {Verifying Constant-Time Implementations by Abstract Interpretation},
  booktitle = {Computer Security - {ESORICS} 2017 - 22nd European Symposium on Research
               in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings,
               Part {I}},
  pages     = {260--277},
  year      = {2017},
  crossref  = {DBLP:conf/esorics/2017-1},
  url_preprint = {esorics17.pdf},
  url_link  = {https://doi.org/10.1007/978-3-319-66402-6_16},
  doi       = {10.1007/978-3-319-66402-6_16},
  timestamp = {Thu, 21 Sep 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/esorics/BlazyPT17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  abstract  = {Constant-time programming is an established discipline to secure programs against timing attacks. 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. We give semantic evidences 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.}
}

{"_id":"X8dGGnk8jZMZyLrJa","bibbaseid":"blazy-pichardie-trieu-verifyingconstanttimeimplementationsbyabstractinterpretation-2017","downloads":0,"creationDate":"2017-07-28T12:01:48.437Z","title":"Verifying Constant-Time Implementations by Abstract Interpretation","author_short":["Blazy, S.","Pichardie, D.","Trieu, A."],"year":2017,"bibtype":"inproceedings","biburl":"http://people.irisa.fr/Alix.Trieu/bibliography.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Sandrine"],"propositions":[],"lastnames":["Blazy"],"suffixes":[]},{"firstnames":["David"],"propositions":[],"lastnames":["Pichardie"],"suffixes":[]},{"firstnames":["Alix"],"propositions":[],"lastnames":["Trieu"],"suffixes":[]}],"title":"Verifying Constant-Time Implementations by Abstract Interpretation","booktitle":"Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I","pages":"260–277","year":"2017","crossref":"DBLP:conf/esorics/2017-1","url_preprint":"esorics17.pdf","url_link":"https://doi.org/10.1007/978-3-319-66402-6_16","doi":"10.1007/978-3-319-66402-6_16","timestamp":"Thu, 21 Sep 2017 01:00:00 +0200","biburl":"https://dblp.org/rec/bib/conf/esorics/BlazyPT17","bibsource":"dblp computer science bibliography, https://dblp.org","abstract":"Constant-time programming is an established discipline to secure programs against timing attacks. 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. We give semantic evidences 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.","bibtex":"@inproceedings{DBLP:conf/esorics/BlazyPT17,\n author = {Sandrine Blazy and\n David Pichardie and\n Alix Trieu},\n title = {Verifying Constant-Time Implementations by Abstract Interpretation},\n booktitle = {Computer Security - {ESORICS} 2017 - 22nd European Symposium on Research\n in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings,\n Part {I}},\n pages = {260--277},\n year = {2017},\n crossref = {DBLP:conf/esorics/2017-1},\n url_preprint = {esorics17.pdf},\n url_link = {https://doi.org/10.1007/978-3-319-66402-6_16},\n doi = {10.1007/978-3-319-66402-6_16},\n timestamp = {Thu, 21 Sep 2017 01:00:00 +0200},\n biburl = {https://dblp.org/rec/bib/conf/esorics/BlazyPT17},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n abstract = {Constant-time programming is an established discipline to secure programs against timing attacks. 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. We give semantic evidences 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.}\n}\n\n","author_short":["Blazy, S.","Pichardie, D.","Trieu, A."],"key":"DBLP:conf/esorics/BlazyPT17","id":"DBLP:conf/esorics/BlazyPT17","bibbaseid":"blazy-pichardie-trieu-verifyingconstanttimeimplementationsbyabstractinterpretation-2017","role":"author","urls":{" preprint":"http://people.irisa.fr/Alix.Trieu/esorics17.pdf"," link":"https://doi.org/10.1007/978-3-319-66402-6_16"},"downloads":0,"html":""},"search_terms":["verifying","constant","time","implementations","abstract","interpretation","blazy","pichardie","trieu"],"keywords":[],"authorIDs":["597b27ac4f2ff86d35000006","5afab302b7108710000001ad","xKZ4Zs6QwvGGG8Grp"],"dataSources":["qnS8bQRQgefgSyTki"]}