Towards a Formal Model for Software Tamper Resistance

A major challenge in software protection is the problem of tampering where an adversary modifies a program and uses it in a way that was not intended or desired. Several ad hoc techniques for software tamper resistance have been proposed, some of which provide a significant level of resilience against tampering. However, the literature lacks a formal definition of tampering that takes into account a model of the attacker’s goals. One effect of this lack is the inability of easily comparing the actual efficacy of proposed tamper resistance mechanisms and evaluating the practical limits of tamper resistance. This paper is a step towards addressing this shortcoming. We consider the two players: the defender who wishes to protect the program, and an adversary who wishes to modify the program as well as the assets embedded within the program to his advantage. We propose a way of expressing the intent of the defender and the attacker based on predicates defined over program traces. Based on these expressions, we present formal definitions for software tamper resistance, and software tamper verification. With a practical tamper verification scheme, we show how this formal model can be used in a reactive protection setting.