@inproceedings{gallagher_verifying_2014,
	title = {Verifying {Security} {Patches}},
	abstract = {In this paper, we introduce a formal framework for ensuring the correctness of security patches. We discuss the issues and provide a sketch of how one could implement a system that proves (in many cases) or provides robust evidence (in other cases) that a security patch fixes a bug, and changes nothing else about the semantics of a program. We make use of an analysis of "bug surfaces" the set of inputs that trigger a bug, to give a type theoretic characterization of the non-buggy surface of a program. We thus give credence to the Langsec notion that security flaws are often about input handling, and show how formal patch and bug analysis can be used to define a more correct input type for a program.},
	urldate = {2016-01-04TZ},
	booktitle = {Proc. of the {Int}'l {Workshop} on {Privacy} \& {Security} in {Programming}},
	author = {Gallagher, Jonathan and Gonzalez, Robin and Locasto, Michael E.},
	year = {2014},
	keywords = {formal methods, inoculation, patches, refinement types, security, veniok, verification}
}

{"_id":"4zgoiN6DbrQn6rBKq","bibbaseid":"gallagher-gonzalez-locasto-verifyingsecuritypatches-2014","downloads":0,"creationDate":"2016-10-15T13:23:04.495Z","title":"Verifying Security Patches","author_short":["Gallagher, J.","Gonzalez, R.","Locasto, M. E."],"year":2014,"bibtype":"inproceedings","biburl":"http://bibbase.org/zotero/pentarious","bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Verifying Security Patches","abstract":"In this paper, we introduce a formal framework for ensuring the correctness of security patches. We discuss the issues and provide a sketch of how one could implement a system that proves (in many cases) or provides robust evidence (in other cases) that a security patch fixes a bug, and changes nothing else about the semantics of a program. We make use of an analysis of \"bug surfaces\" the set of inputs that trigger a bug, to give a type theoretic characterization of the non-buggy surface of a program. We thus give credence to the Langsec notion that security flaws are often about input handling, and show how formal patch and bug analysis can be used to define a more correct input type for a program.","urldate":"2016-01-04TZ","booktitle":"Proc. of the Int'l Workshop on Privacy & Security in Programming","author":[{"propositions":[],"lastnames":["Gallagher"],"firstnames":["Jonathan"],"suffixes":[]},{"propositions":[],"lastnames":["Gonzalez"],"firstnames":["Robin"],"suffixes":[]},{"propositions":[],"lastnames":["Locasto"],"firstnames":["Michael","E."],"suffixes":[]}],"year":"2014","keywords":"formal methods, inoculation, patches, refinement types, security, veniok, verification","bibtex":"@inproceedings{gallagher_verifying_2014,\n\ttitle = {Verifying {Security} {Patches}},\n\tabstract = {In this paper, we introduce a formal framework for ensuring the correctness of security patches. We discuss the issues and provide a sketch of how one could implement a system that proves (in many cases) or provides robust evidence (in other cases) that a security patch fixes a bug, and changes nothing else about the semantics of a program. We make use of an analysis of \"bug surfaces\" the set of inputs that trigger a bug, to give a type theoretic characterization of the non-buggy surface of a program. We thus give credence to the Langsec notion that security flaws are often about input handling, and show how formal patch and bug analysis can be used to define a more correct input type for a program.},\n\turldate = {2016-01-04TZ},\n\tbooktitle = {Proc. of the {Int}'l {Workshop} on {Privacy} \\& {Security} in {Programming}},\n\tauthor = {Gallagher, Jonathan and Gonzalez, Robin and Locasto, Michael E.},\n\tyear = {2014},\n\tkeywords = {formal methods, inoculation, patches, refinement types, security, veniok, verification}\n}\n\n","author_short":["Gallagher, J.","Gonzalez, R.","Locasto, M. E."],"key":"gallagher_verifying_2014","id":"gallagher_verifying_2014","bibbaseid":"gallagher-gonzalez-locasto-verifyingsecuritypatches-2014","role":"author","urls":{},"keyword":["formal methods","inoculation","patches","refinement types","security","veniok","verification"],"downloads":0},"search_terms":["verifying","security","patches","gallagher","gonzalez","locasto"],"keywords":["formal methods","inoculation","patches","refinement types","security","veniok","verification"],"authorIDs":[],"dataSources":["QiRZ7m7shEMvADZkd"]}