Static Verification of Worm and virus Behavior in binary Executables using Model Checking

- Use offormal methods in any application scenario requires a precise characterization and representation of the properties that need to be verified The target, which is desired rifiedfor these properties, needs to be abstracted in a suitableform that can befed to a mechanical theoremprover. 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 verifLing functional behavior to detect malicious behavior in binary executables.

• Type: Conference
• Year: 2003
• Where: IAW
• Authors: Prabhat K. Singh, Arun Lakhotia
• Keywords: Core Functional Components, IAW 2003, Information Management, Precise Characterization, Use Offormal Methods