@inproceedings{DBLP:conf/csfw/BartheBLPT17,
  author    = {Gilles Barthe and
               Sandrine Blazy and
               Vincent Laporte and
               David Pichardie and
               Alix Trieu},
  title     = {Verified Translation Validation of Static Analyses},
  booktitle = {30th {IEEE} Computer Security Foundations Symposium, {CSF} 2017, Santa
               Barbara, CA, USA, August 21-25, 2017},
  pages     = {405--419},
  year      = {2017},
  crossref  = {DBLP:conf/csfw/2017},
  url_preprint = {csf17.pdf},
  url_link  = {https://doi.org/10.1109/CSF.2017.16},
  doi       = {10.1109/CSF.2017.16},
  timestamp = {Mon, 16 Oct 2017 15:00:33 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/csfw/BartheBLPT17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  abstract  = {Motivated by applications to security and high efficiency , we propose an automated methodology for validating on low-level intermediate representations the results of a source-level static analysis. Our methodology relies on two main ingredients: a relative-safety checker, an instance of a relational verifier which proves that a program is "safer" than another, and a transformation of programs into defensive form which verifies the analysis results at runtime. We prove the soundness of the methodology, and provide a formally verified instantiation based on the Verasco verified C static analyzer and the CompCert verified C compiler. We experiment with the effectiveness of our approach with client optimizations at RTL level, and static analyses for cache-based timing side-channels and memory usage at pre-assembly levels.}
}

{"_id":"M7NdvRDFTqYCis7ff","bibbaseid":"barthe-blazy-laporte-pichardie-trieu-verifiedtranslationvalidationofstaticanalyses-2017","downloads":0,"creationDate":"2017-07-28T12:01:48.438Z","title":"Verified Translation Validation of Static Analyses","author_short":["Barthe, G.","Blazy, S.","Laporte, V.","Pichardie, D.","Trieu, A."],"year":2017,"bibtype":"inproceedings","biburl":"http://people.irisa.fr/Alix.Trieu/bibliography.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Gilles"],"propositions":[],"lastnames":["Barthe"],"suffixes":[]},{"firstnames":["Sandrine"],"propositions":[],"lastnames":["Blazy"],"suffixes":[]},{"firstnames":["Vincent"],"propositions":[],"lastnames":["Laporte"],"suffixes":[]},{"firstnames":["David"],"propositions":[],"lastnames":["Pichardie"],"suffixes":[]},{"firstnames":["Alix"],"propositions":[],"lastnames":["Trieu"],"suffixes":[]}],"title":"Verified Translation Validation of Static Analyses","booktitle":"30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21-25, 2017","pages":"405–419","year":"2017","crossref":"DBLP:conf/csfw/2017","url_preprint":"csf17.pdf","url_link":"https://doi.org/10.1109/CSF.2017.16","doi":"10.1109/CSF.2017.16","timestamp":"Mon, 16 Oct 2017 15:00:33 +0200","biburl":"https://dblp.org/rec/bib/conf/csfw/BartheBLPT17","bibsource":"dblp computer science bibliography, https://dblp.org","abstract":"Motivated by applications to security and high efficiency , we propose an automated methodology for validating on low-level intermediate representations the results of a source-level static analysis. Our methodology relies on two main ingredients: a relative-safety checker, an instance of a relational verifier which proves that a program is \"safer\" than another, and a transformation of programs into defensive form which verifies the analysis results at runtime. We prove the soundness of the methodology, and provide a formally verified instantiation based on the Verasco verified C static analyzer and the CompCert verified C compiler. We experiment with the effectiveness of our approach with client optimizations at RTL level, and static analyses for cache-based timing side-channels and memory usage at pre-assembly levels.","bibtex":"@inproceedings{DBLP:conf/csfw/BartheBLPT17,\n author = {Gilles Barthe and\n Sandrine Blazy and\n Vincent Laporte and\n David Pichardie and\n Alix Trieu},\n title = {Verified Translation Validation of Static Analyses},\n booktitle = {30th {IEEE} Computer Security Foundations Symposium, {CSF} 2017, Santa\n Barbara, CA, USA, August 21-25, 2017},\n pages = {405--419},\n year = {2017},\n crossref = {DBLP:conf/csfw/2017},\n url_preprint = {csf17.pdf},\n url_link = {https://doi.org/10.1109/CSF.2017.16},\n doi = {10.1109/CSF.2017.16},\n timestamp = {Mon, 16 Oct 2017 15:00:33 +0200},\n biburl = {https://dblp.org/rec/bib/conf/csfw/BartheBLPT17},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n abstract = {Motivated by applications to security and high efficiency , we propose an automated methodology for validating on low-level intermediate representations the results of a source-level static analysis. Our methodology relies on two main ingredients: a relative-safety checker, an instance of a relational verifier which proves that a program is \"safer\" than another, and a transformation of programs into defensive form which verifies the analysis results at runtime. We prove the soundness of the methodology, and provide a formally verified instantiation based on the Verasco verified C static analyzer and the CompCert verified C compiler. We experiment with the effectiveness of our approach with client optimizations at RTL level, and static analyses for cache-based timing side-channels and memory usage at pre-assembly levels.}\n}\n\n","author_short":["Barthe, G.","Blazy, S.","Laporte, V.","Pichardie, D.","Trieu, A."],"key":"DBLP:conf/csfw/BartheBLPT17","id":"DBLP:conf/csfw/BartheBLPT17","bibbaseid":"barthe-blazy-laporte-pichardie-trieu-verifiedtranslationvalidationofstaticanalyses-2017","role":"author","urls":{" preprint":"http://people.irisa.fr/Alix.Trieu/csf17.pdf"," link":"https://doi.org/10.1109/CSF.2017.16"},"downloads":0,"html":""},"search_terms":["verified","translation","validation","static","analyses","barthe","blazy","laporte","pichardie","trieu"],"keywords":["verified compilation ; coq proof assistant ; program analysis ; constant-time programming"],"authorIDs":[],"dataSources":["qnS8bQRQgefgSyTki"]}