Using Safety Properties to Generate Vulnerability Patches

Automatic Program Repair (APR) methods attempt to fix vulnerabilities in programs comprehensively and without introducing new defects. Senx uses novel safety properties to generate patches, and it succeeds in generating patches for 32 of 42 real-world vulnerabilities. We explain how Senx works, compare it to other APR methods, and demonstrate why Senx is better at repairing source code.