1. A method of scanning an item of executable binary code prepared from a program written in a programming language, the method employing a model checker and executing on a host computer processor, the method comprising: preparing a data structure corresponding to the item of executable binary code, the data structure comprising executable elements parsed from the item of executable binary code; creating a composite model of the executable binary code by supplementing the data structure with metadata comprising at least security rules defined by a specification of the programming language, the composite model having a format for processing by the model checker; analyzing the composite model with the model checker to assess whether the executable binary code violates a rule defined by the programming language; and generating an output based on a result produced by the model checker, the output including an indication of whether the binary code possibly contains malware.