Using Safety Properties to Generate Vulnerability Patches

Explore an innovative approach to automatic program repair (APR) for security vulnerabilities in this 20-minute IEEE conference talk. Discover how property-based APR utilizes human-specified, program-independent, and vulnerability-specific safety properties to generate precise and complete source code patches. Learn about Senx, a system that detects violated safety properties from a single vulnerability-triggering input and generates corresponding patches. Understand how Senx overcomes challenges in property-based APR, including identifying necessary program expressions and variables, generating new code to avoid side effects, and implementing access range analysis to optimize patch placement. Examine the effectiveness of this method through an evaluation of 42 real-world vulnerabilities across 11 applications, including graphics/media file manipulation tools, programming language interpreters, and database engines.