Can we certify systems for freedom from malware

Malicious code is any code that has been modified with the intention of harming its usage or the user. Typical categories of malicious code include Trojan Horses, viruses, worms etc. With the growth in complexity of computing systems, detection of malicious code is becoming horrendously complex. For security of embedded devices it is important to ensure the integrity of software running in it. The general virus detection is undecidable. However, in the case of embedded systems or personal systems, the software and hardware configurations are known a priori. We are experimenting to see whether we can certify such systems for malware freedom. Most of the current efforts on malware detection rely heavily on detection of syntactic patterns. Malware writers are resorting to simple syntactic transformations (which preserve the program semantics) such as various compiler optimizations and program obfuscation techniques to evade detection. Our work is based on semantic behaviour of programs. We are working towards developing a model of the behaviour of a program executing in an environment. Our approach to detect tampering is based on benchmarking the behaviour of a program executing in an environment, and then matching the observed behaviour of the program in a similar environment with the benchmark (a la translation validation in a sense or bisimulation that is widely used in model checking). Since execution behaviour remains the same in majority of obfuscations, our approach is resilient to such exploits. We have performed several experiments in this direction and obtained encouraging results. Differences between the benchmarked behaviour and the observed behaviour quantifies the damage due to a virus. This enables us to arrive at refined notions of "harm" done by a virus and appropriate measures for protection.