Securing Existing Software using Formally Verified Libraries