Ironpatch: Automatic Generation of Assured Micropatches

The goal of the Ironpatch proposal is to develop rigorous program transformation, analysis, and
verification techniques to generate assured micropatches for mission-critical software. To accomplish
this goal, we will develop automated binary patching techniques for platforms ranging from commodity
connected systems to embedded real-time cyberphysical systems, and to networked distributed cyberphysical systems. Furthermore, we will develop symbolic program comparison and non-interference proof techniques to ensure that (1) the vulnerabilities are indeed patched, and (2) the baseline functionality of the patched programs remains unchanged.