  In this paper, we introduce a formal notion of partial compliance, called
Attack-resistance, of a computer program running together with a defense
mechanism w.r.t a non-exploitability specification. In our setting, a program
may contain exploitable vulnerabilities, such as buffer overflows, but
appropriate defense mechanisms built into the program or the operating system
render such vulnerabilities hard to exploit by certain attackers, usually
relying on the strength of the randomness of a probabilistic transformation of
the environment or the program and some knowledge on the attacker's goals and
attack strategy. We are motivated by the reality that most large-scale programs
have vulnerabilities despite our best efforts to get rid of them. Security
researchers have responded to this state of affairs by coming up with ingenious
defense mechanisms such as address space layout randomization (ASLR) or
instruction set randomization (ISR) that provide some protection against
exploitation. However, implementations of such mechanism have been often shown
to be insecure, even against the attacks they were designed to prevent. By
formalizing this notion of attack-resistance we pave the way towards addressing
the questions: "How do we formally analyze defense mechanisms? Is there a
mathematical way of distinguishing effective defense mechanisms from
ineffective ones? Can we quantify and show that these defense mechanisms
provide formal security guarantees, albeit partial, even in the presence of
exploitable vulnerabilities?". To illustrate our approach we discuss under
which circumstances ISR implementations comply with the Attack-resistance
definition.
