Hi Folks,
They present an overview of the latest developments in the detection of metamorphic and virtualization- based malware using an algebraic specification of the Intel 64 assembly programming language. After giving an overview of related work, they describe the development of a specification of a subset of the Intel 64 instruction set in Maude, an advanced formal algebraic specification tool.
They have been developing the technique of metamorphic malware detection based on equivalence-in-context so that it is applica- ble to imperative programming languages in general. They finally give two examples of how this might be used in a practical setting to detect metamorphic malware.
From Webster and Malcolm's
paperThe image shows their basic concept. Signature-based detection of a metamorphic computer virus, by application of "equivalence- in-context".Instruction sequences c and σ are semi-equivalent with respect to W . Applying the result in Corollary 1 (If p1 ≡W p2 and p1; ψ ≡W ∪Vout (ψ) p2; ψ for instruction se- quences p1, p2, ψ and W ∪ Vout(ψ) = V , then p1;ψ ≡ p2;ψ.) to c,σ and ψ reveals that in fact c;ψ ≡ σ;ψ and therefore c has been identified as equivalent to signature σ, resulting in detection of the virus. This method could result in a false positive as there may be a non-malware instruction sequence which is equivalent-in-context of some signature.
It's not an easy paper to be read (at least for myself), but I think it is something very useful to know. I am not interested in the details so far, but having the possibility to know what you can do (in term of Malware detection) through formal analysis let you open new doors in terms of detections.
