Static verification of worm and virus behavior in binary executables using model checking

Use of formal methods in any application scenario requires a precise characterization and representation of the properties that need to be verified. The target, which is desired to be verified for these properties, needs to be abstracted in a suitable form that can be fed to a mechanical theorem prover. The most challenging question that arises in the case of malicious code is: "What are the properties that need to be proved?" We provide a decomposition of virus and worm programs based on their core functional components and a method of formally encoding and verifying functional behavior to detect malicious behavior in binary executables.