Incremental verification of ω-regions on binary control flow graph for computer virus detection

Generally, a computer virus, or virus, consists of two major parts, including a syntactic pattern of signature and code segment performing the core malicious actions. Currently, most of commercial security programs rely on signature matching techniques for virus detection, thus suffering difficulty from some advanced polymorphic viruses which can infinitely change their signatures. In research community, model checking has been proposed to overcome this problem. Representing core malicious actions as temporal logic formulas, a model checker can then verify presence of malicious actions on a control flow graph (CFG) extracted from a binary executable. However, model-checking-based approaches encounter the infamous state explosion problem. In this paper, we tackle this problem by suggesting to partition the binary-extracted CFG into specific sub-graphs, known as ω-regions. Based on empirical observation on real virus samples, we argue that the code segment corresponding for a viral core malicious action should not occupy more than one ω-region. The tactic for location of those ω-regions from a CFG is also presented. This approach allows us to reduce the verification complexity by means of an incremental verification strategy. As a result, we enjoy significant performance improvement when experimenting with real dataset of viruses.