Using Software Generation and Repair for Cyber-Defense

: This work investigates the use of medium-grained synthetic diversity to inhibit an attacker s ability to identify and exploit weaknesses in a networked application. We specify the application and use formal refinements to generate numerous implementations that use different combinations of algorithms and data representations. By deploying different implementations we make it more difficult for an attacker to learn details about how any particular implementation works, what resources it uses and what operating system or network services it uses such information is a critical prerequisite for many cyber attacks. We also use semantic constraints in specifications and refinements to generate run-time monitors that can detect compromised data. The semantic information also enables either total or approximate repair of the data, allowing an application to recover from an attack. We also use formal transformations on specifications to augment data structures with additional semantic constraints to enhance monitoring and repair.