Corelab Seminar

Vassilis Zikas
Provable Virus Detection: Using The Observer Effect To Protect Against Malware

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, making the quest for a solution more pressing than ever. The problem has attracted little attention in the theoretical computer science community, where there is even a lack of formal definitions.

In this work we propose a novel provably secure and practically efficient paradigm for detecting malicious code injection onto a system's memory. Our system has the following desirable properties: 1) it protects even systems executing a dynamically updating code; 2) it requires no changes to the CPU to protect against long continuous injections, and requires minor changes to the CPU to protect against any (arbitrary short and scattered) injection attacks that can not read the code before they inject its software; 3) it only effects the performance of the program by a modest amount. The first property allows us to protect both a program and its data without knowing the current state in the execution (the program might have modified its data while executing). The second property implies that it can already be used on today's computers. The third property means that our method is potentially practical, since performance is critical in most applications; this is obvious even in its simplified form presented here, where various optimizations have been avoided for the sake of clarity in the presentation. Finally, we allow attacks to have both spatial and temporal freedom: the attack can occur at any time during the execution and on any part of the memory. It can attack code as well as data.

Our solutions are accompanied by mathematical proofs that any injection will be caught with arbitrary high probability. For our security proofs we provide the first, to our knowledge, formal cryptographic model tailored to software attestation (detection of malware injection) in modern computers, which we believe is of independent interest and paves the way to a thorough theoretical investigation of the problem.

This is joint work with Richard Lipton and Rafail Ostrovsky.