Detecting traditional packers, decisively

Many of the important decidability results in malware analysis are based Turing machine models of computation. We exhibit computational models which use more realistic assumptions about machine and attacker resources. While seminal results such as [1-5] remain true for Turing machines, we show under more realistic assumptions, important tasks are decidable instead of undecidable. Specifically, we show that detecting traditional malware unpacking behavior - in which a payload is decompressed or decrypted and subsequently executed - is decidable under our assumptions. We then examine the issue of dealing with complex but decidable problems. We look for lessons from the hardware verification community, which has been striving to meet the challenge of intractable problems for the past three decades.