Using Safety Properties to Generate Vulnerability Patches

Explore a groundbreaking approach to automatic program repair (APR) for security vulnerabilities in this conference talk from the 2019 IEEE Symposium on Security & Privacy. Delve into the concept of property-based APR, which utilizes human-specified, program-independent, and vulnerability-specific safety properties to generate precise and complete source code patches. Learn about Senx, an innovative system that detects violated safety properties and creates corresponding patches to remove vulnerabilities. Discover how Senx overcomes challenges in property-based APR, including identifying necessary program expressions and variables, generating new code to avoid unwanted side effects, and implementing a novel access range analysis technique to optimize patch placement. Examine the effectiveness of this approach through an evaluation of 42 real-world vulnerabilities across 11 applications, including graphics/media file manipulation tools, programming language interpreters, and database engines.