{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:31Z","timestamp":1750306531840,"version":"3.41.0"},"publisher-location":"New York, New York, USA","reference-count":35,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1145\/2687148.2687151","type":"proceedings-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T13:32:15Z","timestamp":1420464735000},"page":"11-18","source":"Crossref","is-referenced-by-count":2,"title":["Verifying security patches"],"prefix":"10.1145","author":[{"given":"Jonathan","family":"Gallagher","sequence":"first","affiliation":[]},{"given":"Robin","family":"Gonzalez","sequence":"additional","affiliation":[]},{"given":"Michael E.","family":"Locasto","sequence":"additional","affiliation":[]}],"member":"320","reference":[{"key":"key-10.1145\/2687148.2687151-1","doi-asserted-by":"crossref","unstructured":"Andreas Blass and Yuri Gurevich. Inadequacy of Computable Loop Invariants. ACM Trans. Comput. Logic, 2(1):1--11, January 2001.","DOI":"10.1145\/371282.371285"},{"key":"key-10.1145\/2687148.2687151-2","unstructured":"F. Bobot, Filliâtre J., C. Marché, and A. Paskevich. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53--64. Microsoft Research, 2011."},{"key":"key-10.1145\/2687148.2687151-3","unstructured":"D. Brumley, T. Chiueh, R. Johnson, H. Lin, and D. Song. RICH: Automatically Protecting against Integer-based Vulnerabilities. In Network and Distributed Systems Security, 2007."},{"key":"key-10.1145\/2687148.2687151-4","doi-asserted-by":"crossref","unstructured":"C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, and D. Engler. EXE: Automatically Generating Inputs of Death. In 13th ACM conference on Computer and Communications Security, pages 322--335. ACM, 2006.","DOI":"10.1145\/1180405.1180445"},{"key":"key-10.1145\/2687148.2687151-5","unstructured":"Dustin Childs. KB2839011 Released to Addresss Security Bulletin Update Issue. Microsoft Security Response Center, April 2013."},{"key":"key-10.1145\/2687148.2687151-6","doi-asserted-by":"crossref","unstructured":"E. Clarke and D. Kroening. A Tool for Checking ANSI-C Programs. In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2988, pages 168--176. Springer, 2004.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"key-10.1145\/2687148.2687151-7","doi-asserted-by":"crossref","unstructured":"J. Cocktt and C. Pastro. The Logic of Message-Passing. Science of Computer Programming, 74:489--533, 2009.","DOI":"10.1016\/j.scico.2007.11.005"},{"key":"key-10.1145\/2687148.2687151-8","doi-asserted-by":"crossref","unstructured":"Manuel Costa, Miguel Castro, Lidong Zhou, Lintao Zhang, and Marcus Peinado. Bouncer: Securing Software by Blocking Bad Input. In Proceedings of Twenty-first ACM SIGOPS Symposium on Operating Systems Principles, SOSP '07, pages 117--130, New York, NY, USA, 2007. ACM.","DOI":"10.1145\/1294261.1294274"},{"key":"key-10.1145\/2687148.2687151-9","doi-asserted-by":"crossref","unstructured":"Manuel Costa, Jon Crowcroft, Miguel Castro, Antony Rowstron, Lidong Zhou, Lintao Zhang, and Paul Barham. Vigilante: End-to-end Containment of Internet Worms. In Proceedings of the Twentieth ACM Symposium on Operating Systems Principles, SOSP '05, pages 133--147, New York, NY, USA, 2005. ACM.","DOI":"10.1145\/1095810.1095824"},{"key":"key-10.1145\/2687148.2687151-10","doi-asserted-by":"crossref","unstructured":"P. Cuoq, J. Signoles, P. Baudin, R. Bonichon, G. Canet, L. Correnson, B. Monate, V. Prevosto, and A. Pucceti. Experience Report: OCaml for an Industrial-Strength Static Analysis Framework. In ACM SIGPLAN International Conference on Functional Programming, pages 281--286. ACM, 2009.","DOI":"10.1145\/1596550.1596591"},{"key":"key-10.1145\/2687148.2687151-11","doi-asserted-by":"crossref","unstructured":"J. Eyolfson, L. Tan, and P. Lam. Do Time of Day and Developer Experience Affect Commit Bugginesss? In 8th Working Conference on Mining Software Repositories, pages 154--162. ACM, 2011.","DOI":"10.1145\/1985441.1985464"},{"key":"key-10.1145\/2687148.2687151-12","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and Shaz Qadeer. Predicate Abstraction for Software Verification. SIGPLAN Not., 37(1):191--202, January 2002.","DOI":"10.1145\/565816.503291"},{"key":"key-10.1145\/2687148.2687151-13","doi-asserted-by":"crossref","unstructured":"T. Freeman and F. Pfenning. Refinement Types for ML. In Programming Language Design and Implementation, pages 268--277. ACM, 1991.","DOI":"10.1145\/113446.113468"},{"key":"key-10.1145\/2687148.2687151-14","doi-asserted-by":"crossref","unstructured":"S. Gay and M. Hole. Types and Subtypes for Client-Server Interactions. In 8th European Symposium on Programming Languages and Systems, pages 74--90. Springer, 1999.","DOI":"10.1007\/3-540-49099-X_6"},{"key":"key-10.1145\/2687148.2687151-15","doi-asserted-by":"crossref","unstructured":"Z. Gu, E. Barr, D. Hamilton, and Z. Su. Has the Bug Really Been Fixed? In 32nd ACM\/IEEE International Conference on Software Engineering, volume 1, pages 55--64, 2010.","DOI":"10.1145\/1806799.1806812"},{"key":"key-10.1145\/2687148.2687151-16","doi-asserted-by":"crossref","unstructured":"Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Reb^elo. SYMDIFF: A Language-agnostic Semantic Di Tool for Imperative Programs. In Proceedings of the 24th International Conference on Computer Aided Verification, CAV'12, pages 712--717, Berlin, Heidelberg, 2012. Springer-Verlag.","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"key-10.1145\/2687148.2687151-17","unstructured":"Richard Lawler. PS3 Users Report 4.45 Update Locks Up Systems, may be Tied to Large HDDs. Engadget, June 2013."},{"key":"key-10.1145\/2687148.2687151-18","doi-asserted-by":"crossref","unstructured":"Wei Le and Shannon D. Pattison. Patch Verification via Multiversion Interprocedural Control Flow Graphs. In Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pages 1047--1058, New York, NY, USA, 2014. ACM.","DOI":"10.1145\/2568225.2568304"},{"key":"key-10.1145\/2687148.2687151-19","unstructured":"M. Locasto, M. Burnside, and A. Keromytis. Bloodhound: Searching Out Malicious Input in Network Flows for Automatic Repair Validation. Technical report, Columbia University, 2006."},{"key":"key-10.1145\/2687148.2687151-20","unstructured":"M. Locasto, A. Stavrou, and G. Cretu. Life after Self-Healing: Assessing Post-Repair Program Behavior. Technical report, George Mason University, 2008."},{"key":"key-10.1145\/2687148.2687151-21","unstructured":"Matthew Maurer and David Brumley. TACHYON: Tandem Execution for Efficient Live Patch Testing. In Proceedings of the 21st USENIX Conference on Security Symposium, Security'12, pages 43--43, Berkeley, CA, USA, 2012. USENIX Association."},{"key":"key-10.1145\/2687148.2687151-22","doi-asserted-by":"crossref","unstructured":"P. Mell, T. Bergeron, and D. Henning. Creating a Patch and Vulnerability Management Program. Technical report, NIST, 2005.","DOI":"10.6028\/NIST.SP.800-40ver2"},{"key":"key-10.1145\/2687148.2687151-23","unstructured":"Elinor MIlls. Symantec Pulls Norton Patch AFter Error Reports. CNET, August 2009."},{"key":"key-10.1145\/2687148.2687151-24","unstructured":"Jon Oberheide, Evan Cooke, and Farnam Jahanian. If It Ain'T Broke, Don'T Fix It: Challenges and New Directions for Inferring the Impact of Software Patches. In Proceedings of the 12th Conference on Hot Topics in Operating Systems, HotOS'09, pages 17--17, Berkeley, CA, USA, 2009. USENIX Association."},{"key":"key-10.1145\/2687148.2687151-25","unstructured":"Nilay Patel. Botched McAfee Update Shutting Down Corporate XP Machines Worldwide. Engadget, April 2010."},{"key":"key-10.1145\/2687148.2687151-26","unstructured":"Bogdan Popa. Windows 8 Update Fails on KB2770917. Softpedia, November 2012."},{"key":"key-10.1145\/2687148.2687151-27","doi-asserted-by":"crossref","unstructured":"P. Rondon, A. Bakst, M. Kawaguchi, and R. Jhala. CSolve: Verifying C with Liquid Types. In Computer Aided Verification, pages 744--750. Springer, 2012.","DOI":"10.1007\/978-3-642-31424-7_59"},{"key":"key-10.1145\/2687148.2687151-28","doi-asserted-by":"crossref","unstructured":"P. Rondon, M. Kawaguchi, and R. Jhala. Liquid Types. In Programming Language Design and Implementation, 2008.","DOI":"10.1145\/1375581.1375602"},{"key":"key-10.1145\/2687148.2687151-29","doi-asserted-by":"crossref","unstructured":"J. T. Schwartz. Fast Probabilistic Algorithms for Verification of Polynomial Identities. J. ACM, 27(4):701--717, October 1980.","DOI":"10.1145\/322217.322225"},{"key":"key-10.1145\/2687148.2687151-30","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual. LogiCal project, 2004. Version 8.0."},{"key":"key-10.1145\/2687148.2687151-31","doi-asserted-by":"crossref","unstructured":"Joseph Tucek, Weiwei Xiong, and Yuanyuan Zhou. Efficient Online Validation with Delta Execution. In Proceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XIV, pages 193--204, New York, NY, USA, 2009. ACM.","DOI":"10.1145\/1508244.1508267"},{"key":"key-10.1145\/2687148.2687151-32","doi-asserted-by":"crossref","unstructured":"N. Vazou, E. Seidel, and R. Jhala. LiquidHLiquid: Experience with Refinement Types in the Real World. In Haskell Symposium. ACM, 2014.","DOI":"10.1145\/2628136.2628161"},{"key":"key-10.1145\/2687148.2687151-33","unstructured":"Verizon. 2014 Verizon Data Breach Report. Technical report, 2014."},{"key":"key-10.1145\/2687148.2687151-34","doi-asserted-by":"crossref","unstructured":"Fabian Yamaguchi, Christian Wressnegger, Hugo Gascon, and Konrad Rieck. Chucky: Exposing Missing Checks in Source Code for Vulnerability Discovery. In Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, CCS '13, pages 499--510, New York, NY, USA, 2013. ACM.","DOI":"10.1145\/2508859.2516665"},{"key":"key-10.1145\/2687148.2687151-35","doi-asserted-by":"crossref","unstructured":"Richard Zippel. Probabilistic Algorithms for Sparse Polynomials. In Proceedings of the International Symposiumon on Symbolic and Algebraic Computation, EUROSAM '79, pages 216--226, London, UK, UK, 1979. Springer-Verlag.","DOI":"10.1007\/3-540-09519-5_73"}],"event":{"number":"2014","sponsor":["SIGAda, ACM Special Interest Group on Ada Programming Language","SIGPLAN, ACM Special Interest Group on Programming Languages"],"acronym":"PSP '14","name":"the 2014 International Workshop","start":{"date-parts":[[2014,10,21]]},"location":"Portland, Oregon, USA","end":{"date-parts":[[2014,10,21]]}},"container-title":["Proceedings of the 2014 International Workshop on Privacy & Security in Programming - PSP '14"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2687148.2687151","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=2687151&ftid=1523853&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:13Z","timestamp":1750227133000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=2687148.2687151"}},"subtitle":[],"proceedings-subject":"Privacy & Security in Programming","short-title":[],"issued":{"date-parts":[[2014]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1145\/2687148.2687151","relation":{},"subject":[],"published":{"date-parts":[[2014]]}}}