Protecting software from malware injection is the holy grail of modern computer security. Despite intensive efforts by the scientific and engineering community, the number of successful attacks continues to increase. 

We have a breakthrough in preventing adversaries from inserting malware into programs. The key idea is to use the very insertion of the malware itself to allow for the systems to detect it. This is, in our opinion, close in spirit to the famous Heisenberg Uncertainty Principle. The attackers, no matter how clever, no matter when or how they insert their malware, change the state of the system they are attacking. This fundamental idea is a game changer. And our system does not rely on heuristics;  instead, our scheme enjoys the unique property that it is proved secure in a formal and precise mathematical sense and with minimal and realistic CPU modification achieves strong provable security guarantees.  Thus, we anticipate our system and formal mathematical security treatment to open new directions in software protection. 

This is joint work with Richard Lipton and Rafail Ostrovsky.