[0001] CROSS-REFERENCE TO RELATED APPLICATIONS

This application claims the benefit of U.S . Patent Application No. 15/255,452, filed on September 2, 2016, which is herein incorporated by reference in its entirety.

STATEMENT OF GOVERNMENT INTEREST

[0002] Portions of the present invention have been made in conj unction with Government funding under contract number N66001 - 13 -C-4047 (US DEPARTMENT OF THE NAVY) , and there are certain rights to the Government.

FIELD OF THE DISCLOSURE

[0003] Embodiments relate to automatically processing low-level computer languages (native machine code) and corresponding execution traces to capture the semantics of binary applications in platform- independent representations and then use those representations to reverse engineer and perform cyber- security analysis of the applications to find hidden malicious code. BACKGROUND

[0004] Assembly language and machine code are low-level, difficult- to-understand burdens for cyber security analysts who reverse engineer binary applications to find hidden malicious code. The problem with reading low-level languages is the complexity of capturing semantics from the code. This results in a time-consuming process for analyzing malware, whereas malicious software can be generated automatically. The imbalance between generating and detecting malevolent software currently puts the cyber security industry at a persistent disadvantage.

[0005] Software development is a complex process. Software errors or 'bugs ' are unavoidable in developing applications. Testing procedure becomes increasingly important to detect the existing and potential bugs. Designing comprehensive test suites, however, is infeasible for any sizable application. Detecting bugs through human inspection of source code is hard. Detecting bugs without source code is even harder due to the complexity and challenge of reasoning about what low-level assembly code and machine code is doing. Automated bug detection techniques currently are limited to mechanical detection of potentially problematic syntax (not semantics) , limited to a single type of bug, and/or limited to heuristic algorithms that produce significant false positives and false negatives.

[0006] What is needed is a method and system to automate reverse engineering to capture and perform static analysis on all runtime code for an executable; get instruction traces without instrumenting and running the target system; automate reasoning and pattern recognition against the semantics of executable binaries ; determine all variables and code branches that are affected by program input; and find feasible application inputs to reach a desired Point-of-Interest (POI) in the executable. Additionally, to find software bugs or vulnerabilities, harden software, test software, and understand and fix software where the original source code is missing. SUMMARY

[0007] An embodiment provides a method performed by at least one computer processing unit for reverse engineering analysis of binary applications the method comprising the steps of inspecting binary files from a target application; translating native instructions of the target application into an intermediate language Power Reverse Engineering Intermediate Language (PREIL) ; transforming and aggregating the PREIL instructions by a Taint Modeling Function (TMF) ; and producing output reports identifying undesirable coding patterns in an entire application space. Embodiments comprise preprocessing the translated native instructions into platform-independent PREIL instructions . In other embodiments pre-processing is computed once. In subsequent embodiments TMF forms higher-level semantic expres sions from PREIL lists . For additional embodiments TMF transforming and aggregating comprises modeling each PREIL instruction as an algebraic expres sion and then aggregating the algebraic expres sion to form TMF expressions . In another embodiment aggregation occurs at multiple levels , comprising instruction, basic block, single path, multiple path, loop , and function levels , capturing relationships between inputs and outputs . For a following embodiment, TMF retains all relevant semantic information such as constraints that have an influence on a desired path, and wherein abstraction is los sles s . In subsequent embodiments preprocessing optionally incorporates additional data from dynamically obtained traces at a point of the traces . Additional embodiments further comprise a taint engine (TE) , wherein the taint engine traces all values and code branches from a designated program input, storing input ancestry at each instruction or branch. In included embodiments analysis is static and optionally uses dynamically obtained traces to fill in gaps in executable control flow understanding. In yet further embodiments aggregation finds directed relations between inputs and outputs from a list of TMF expressions . In related embodiments TMF comprises transforming PREIL instructions and relevant data structures into algebraic expressions and using them in applications comprising constraint generation, mathematical representation, data flow analysis , exploratory bug searches , range and domain analysis , path pruning, and return- oriented programming. For further embodiments pre-proces sing automatically compares resulting PREIL with executing binary, and makes corrections to provide an accurate static representation. In ensuing embodiments introspection comprises obtaining only an initial state of application memory and registers .

[0008] Another embodiment provides a system for reverse engineering analysis of binary applications to find hidden malicious code comprising a processor; memory coupled to the proces sor, wherein the memory includes an analysis module to inspect binary files from a target application ; translate native instructions into an intermediate language Power Reverse Engineering Intermediate Language (PREIL) ; transform and aggregate the PREIL instructions by a Taint Modeling Function (TMF) ; process output of the TMF in a main loop comprising PREIL emulation, Taint analysis , and a dynamic behavior sensor; and produce output reports identifying undesirable coding patterns in the entire application space. For yet further embodiments , TMF is an architecture- independent machine-readable format that captures application control flow, and substantially eliminates semantically irrelevant instructions for efficient automated analysis . For more embodiments , a Taint Engine (TE) pre-calculating relevant data pedigrees , allowing efficient queries on Taint, plus both forward and backward Taint tracing. In continued embodiments Constraint Optimization, Management, Extensions , and Translation System (COMETS) and TMF solve mathematically for feasible code execution paths , identifying all feasible paths from input data to any point of interest in the binary applications . For additional embodiments Constraint Optimization, Management, Extensions , and Translation System (COMETS) solves for a set of input values that cause any particular code branch to be taken, resulting in specific input values that result in execution of all branches needed to reach a point of interest, or else COMETS reports that no input can reach the point of interest. [0009] A yet further embodiment provides a non-transitory computer- readable storage medium including instructions that are configured, when executed by a computing system, to perform a method for reverse engineering analysis of binary applications by reading low-level languages to capture semantics from code for analysis to find hidden malicious code, the method comprising preprocessing binary files from a target application ; translating native instructions into an intermediate language Power Reverse Engineering Intermediate Language (PREIL) ; transforming and aggregating the PREIL instructions by a Taint Modeling Function (TMF) ; producing output reports identifying undesirable coding patterns in the entire application space ; whereby analyses can then be conducted manually or with software tools that support data flow analysis , exploratory bug searches , or constraint generation.

[0010] The features and advantages described herein are not all- inclusive and, in particular, many additional features and advantages will be apparent to one of ordinary skill in the art in view of the drawings , specification, and claims . Moreover, it should be noted that the language used in the specification has been selected principally for readability and instructional purposes and not to limit the scope of the inventive subj ect matter.

BRIEF DESCRIPTION OF THE DRAWINGS

[0011] Figure 1 is a high level view configured in accordance with an embodiment of the invention.

[0012] Figure 2 depicts analysis transformation configured in accordance with an embodiment.

[0013] Figure 3 is a Table 1 : example of PREIL instructions configured in accordance with an embodiment.

[0014] Figure 4 is a Table 2 : PREIL translation of x86 "push eax" configured in accordance with an embodiment. [0015] Figure 5 is a Table 3 : equivalent transformation operation configured in accordance with an embodiment.

[0016] Figure 6 is a Table 4 : modeling native instruction x86 configured in accordance with an embodiment.

[0017] Figure 7 is a Table 5 : aggregation algorithm configured in accordance with an embodiment.

[0018] Figure 8 depiction of single path modelling configured in accordance with an embodiment.

[0019] Figure 9 is a Table 6 : single path aggregation configuration configured in accordance with an embodiment.

[0020] Figure 10 depicts multi-path modelling configured in accordance with an embodiment.

[0021] Figure 1 1 is a Table 7 : multi-path aggregation configured in accordance with an embodiment.

[0022] Figure 12 is a Table 8 : XML version of aggregation of max function configured in accordance with an embodiment.

[0023] Figure 13 depicts a loop and its Taint Modeling Functions (TMFs) configured in accordance with an embodiment.

[0024] Figure 14 is a Table 9 : loop TMF skeleton <tmf> configured in accordance with an embodiment.

[0025] Figure 15 is a Table 10 : recursion TMF skeleton configured in accordance with an embodiment.

[0026] Figure 16 is a constraint generation illustration configured in accordance with an embodiment.

[0027] Figure 17 depicts a data flow analysis of configured in accordance with an embodiment.

[0028] Figure 1 8 depicts a buffer overflow bug search configured in accordance with an embodiment.

[0029] Figure 19 depicts a range and domain analysis of a function configured in accordance with an embodiment. [0030] Figure 20 is an illustration of task-oriented path pruning configured in accordance with an embodiment.

[0031] Figure 21 depicts a VirtualAllocEx called in application configured in accordance with an embodiment.

[0032] These and other features of the present embodiments will be understood better by reading the following detailed description, taken together with the figures herein described. For purposes of clarity, not every component may be labeled in every drawing.

DETAILED DESCRIPTION

[0033] The features and advantages described herein are not all- inclusive and, in particular, many additional features and advantages will be apparent to one of ordinary skill in the art in view of the drawings , specification, and claims . Moreover, it should be noted that the language used in the specification has been selected principally for readability and instructional purposes , and not to limit in any way the scope of the inventive subj ect matter. The invention is susceptible of many embodiments . What follows is illustrative, but not exhaustive, of the scope of the invention.

[0034] Static analysis of binary executables has an ability to analyze software without relying on source code which may be unavailable. Binary code static analysis techniques vary widely from single processes such as disassembly, program slicing, and de-obfuscation to frameworks such as CodeSurfer/x86, Phoenix, and BAP.

[0035] Taint Modeling Function (TMF) , abstracts binary code for software analysis . TMF transforms the binary executables to sets of precise algebraic expres sions in conj unction with the intermediate language Power Reverse Engineering Intermediate Language (PREIL) . PREIL simplifies and dis ambiguates native language. The lossless abstraction of binary codes via algebraic expressions makes it pos sible to automate static analysis tasks such as detecting defective code patterns , generate constraints to find needed inputs for desired paths , and narrowing search space for potential bugs. The expressions are also simple to analyze to understand the target software inside-out via querying TMF expressions in a database. The automated application of TMF balances the current imbalance of generating-versus-detecting malevolent software by speeding up the process of bug finding; alleviating users from that tedious and difficult task.

Taint Modeling Function (TMF)

[0036] Taint Modeling Function (TMF) is a novel technique that models binary code as sets of algebraic expressions. The mathematical model of the binary is compatible with mathematical toolkits such as MATLAB which enable TMF' s predictive power. A TMF model serves as a behavioral model of a target application. The behavioral modeling characteristics of TMF enable it to statically and automatically detect bad behaviors of malicious or defective code hidden in largely benign binary code. TMF is a tool that lifts assembly instructions to an intermediate language.

Power Reverse Engineering Intermediate Language (PREIL)

[0037] PREIL (Power Reverse Engineering Intermediate Language) , an extension to REIL, is used to avoid the profusion and ambiguity of native languages such as x86. PREIL plays an important role in TMF modeling. After an application is translated into PREIL instructions and relevant data structures, TMF transforms them into algebraic expressions and uses them in a wide range of applications such as constraint generation, mathematical representation, data flow analysis, exploratory bug searches, range and domain analysis , path pruning, and return-oriented programming.

[0038] The following sections discuss in detail the process of disassembling binary code, PREIL translation, TMF transformation, and practical applications such as using abstract expressions to find bugs statically and systematically.

[0039] Embodiments comprise the following five components : one, PREIL (Power Reverse Engineering Intermediate Language) and Preprocessing; two, emulated traces from executing PREIL; three, Taint Modeling Function (TMF) - TMF reduces an executable's instructions from PREIL to a minimal algebraic representation of control flow; four, Taint Engine (TE) - TE traces all values and code branches from a designated program input, storing the input ancestry at each instruction or branch; and five, Constraint Optimization, Management, Extensions, and Translation System (COMETS) . COMETS and TMF are used to create constraint solver problems that evaluate execution paths and solve for inputs that follow those paths. COMETS is a front-end to well- known third-party constraint solvers such as STP and z3. COMETS uses TMF to produce constraint problems in a form that the constraint solvers can understand. The formulated constraint problems seek binary- application inputs that cause the binary application to follow a specific execution (control-flow) path and/or reach a specific Point of Interest (POI) within the binary code.

[0040] The following further elaborates advantages of embodiments . First, PREIL extends standard REIL to fill in gaps left by other REIL implementations. PREIL is fully executable. Pre-Processing includes any relevant dynamically-loaded libraries and jump tables (normally invisible to disassemblers) with the static binary to achieve full code coverage before translating the application instructions to PREIL and TMF. Pre-Processing automatically compares the resulting PREIL with the executable binary, and makes corrections to guarantee an accurate static representation. Second, embodiments require only enough introspection to obtain an initial state of application memory and registers. Instruction traces are then easily obtained by emulated execution of the PREIL, eliminating technical challenges and performance impacts of true run-time introspection, and making test iterations with varying input values extremely efficient. Third, TMF is an architecture-independent machine-readable format that captures the application control flow, and eliminates semantically irrelevant instructions through algebraic simplification for efficient automated analysis . Without the simplification of TMF, automated analysis, even of PREIL, becomes computationally intractable. Fourth, calculating input data pedigree is computationally expensive, even with storage of instructions in high-performance non-relation (no-S QL) databases . TE pre-calculates the relevant data pedigrees , and allows efficient queries on Taint, plus both forward and backward Taint tracing. Fifth, COMETS and TMF solve mathematically for feasible code execution paths , efficiently identifying all feasible paths from input data to any POI in the binary. COMETS solves for the set of input values that cause any particular code branch to be taken, resulting in specific input values that result in execution of all branches needed to reach the POI, or else COMETS reports that no input can reach the POI.

[0041] FIG. 1 is a high level view 100 of an embodiment of the invention. Rules 105 are human-readable rules for Analysts 110 where the rules describe the desired reverse engineering and vulnerability analysis to perform against Atom 1 15. Atom 115 consists of the binary executable and supporting binary libraries that make up the binary application and provides input to Analysts 110, Execution Environment 120, and Preproces sing 125. Initial State 130 receives input from Execution Environment 120 , and outputs to Preprocessing 125 and Planner (Path Selector) 135. Preprocessing 125 provides input to PREIL & TMF 140 ; PREIL & TMF 140 provide input to Planner 135 and Static Behavior Sensor (SB S) 145. Static Behavior Sensor 145 identifies syntactic and semantic constructs in the TMF representations indicative of potential bugs and vulnerabilities and provides input to POIs 150. In Main Loop 155, Planner (Path Selector) 135 leads to Input 160 which leads to PREIL Emulation 165 leading to Partial Trace 170. Partial Trace 170 provides input to Dynamic B ehavior Sensor (DB S) 175 and Taint Analysis 180. Taint Analysis 180 provides input to Control. Jumps 185 which leads to Constraint Solver 190 leading to New Inputs 195 ; returning to Planner (Path Selector) 135 then proceeding to Reports 198 for Analysts 110.

[0042] FIG. 2 presents transforming a binary executable to algebraic expressions using TMF 200. TMF is the process of transforming binary code to a set of mathematical functions consisting of algebraic expressions that describe software behaviors. The process of disassembling a target application, and its externally linked libraries , and translating native assembly instructions to PREIL is preprocessing 205. Preprocessing 205 returns data structures and PREIL instructions that form a complete as possible representation model 210 of an entire application. PREIL instructions are then transformed into algebraic expressions which are then written to database 215. Database 215 also holds application structures such as functions, blocks, and loops which are subject to queries that support analyses of the target application. Analyses can then be conducted manually or with software tools that support data flow analysis, exploratory bug searches, or constraint generation. The only prerequisite for TMF transformation is preprocessing. The key task of preprocessing is PREIL translation.

[0043] FIG. 3 is a table, Table 1, of example PREIL instructions 300. Assembly languages tend to have large instruction sets. For example, x86 has more than 300 instructions with most of the instructions performing implicit operations (side effects) in addition to the explicit operation, which make it harder to analyze. PREIL, in contrast, has only 20 instructions, and all operations are explicit. As mentioned, PREIL is the Power-REIL enhancement to REIL, the Reverse Engineering Intermediate Language from the BinNavi manual. PREIL offers improved support for static analysis and instructions that BinNavi does not accurately translate. TMF constructs its algebraic expressions from PREIL instructions. The construction is platform independent because PREIL is platform independent.

[0044] Examples that cover the essentials of PREIL are described in FIG. 3, which is a table, Table 1. Note that each nonempty operand begins with either an "r" (for register), "i" (for integer literal) , or "o" (for instruction offset) followed by a size in bits, e.g. , "r32" for a 32-bit register. Note that PREIL also allows a non-empty operand to begin with "m" (for memory address), but this type of operand is rarely needed. [0045] FIG. 4 is a table, Table 2, illustrating PREIL Translation of x86 "push eax" 400. Since PREIL does not allow side effects, the process of translating native instructions to PREIL instructions exposes the implicit operations in native languages such as x86, PowerPC, and ARM assembly. For instance "push eax" involves pushing register "eax" to the stack after decrementing the stack pointer "esp" by 4 bytes. The decrement operation is implied by the instruction. However, PREIL instructions explicitly include them as shown in Table 2.

[0046] Some x86 instructions have long translations, e.g. , "sub" modifies the carry, parity, adjust, zero, sign, and overflow flags in addition to the subtraction destination. In practice, irrelevant operations (e.g. , writes that cannot be read) may be optimized away.

[0047] The following subsections describe PREIL in greater depth.

Differences from REIL

[0048] Whereas REIL supports only a single memory with fixed endianness, PREIL enables multiple memories for code (e.g. , "unit.bochs" for routines from the Bochs software floating-point engine) and data (e.g. , "data. port" for the processor' s I/O address space) with settings such as "unit.error:setup = <PREIL list>" (for unit initialization instructions), "data. port: address. size = 16" (for a maximum address of 216- 1) , "enum:endian = little big" (to associate "endian. little" with 0 and "endian. big" with 1) , and "data. main:byte. order = endian. little" (or equivalently, "data. main:byte. order = 0"). REIL treats temporary registers the same as machine registers but PREIL restricts their scope to a PREIL list where they can only be written once and must be written before they are read. REIL enables jumps to any REIL instruction but PREIL prevents j umps to earlier instructions in a PREIL list and instructions that are not at the start of other PREIL lists. These restrictions enable processing tools to be faster and simpler.

[0049] REIL has six arithmetic instructions (add, sub, mul, div, mod, and bsh) but PREIL replaces bsh (binary shift) with lsh and rsh to ease interpretation. Both have only 3 bitwise instructions (and, or, and xor) since one' s complement is derived from xor. REIL has 2 conditional instructions (bisz and jcc) and PREIL adds 2 more (ifm and ifr) to efficiently handle localized conditional expressions. While both have 3 data transfer instructions (1dm, stm, and str) and 3 other instructions (undef, unkn, and nop), PREIL extends some of these (e.g., str can modify settings).

[0050] REIL measures sizes in terms of bytes but, for better accuracy, PREIL uses bits. Register operands in REIL must refer to entire registers but, for shorter translations, PREIL operands can refer to a range of bits (e.g., in x86-32, "eax:0,7" for register al, "eax:8,15" for register ah, and "t3:l" for the second lowest bit of temporary register t3). However, to help avoid partially unknown values, the output operand cannot be a range for a temporary register. Bit ranges can also be used in settings (e.g., to simply use al in PREIL operands, set "alias:al" to "eax:0,7"). Another PREIL feature that enables shorter translations than REIL is operand sizing rules that follow the C conventions for unsigned integers.

Instruction Semantics

[0051] "add[ol] [o2] [o3]" writes to the register in operand o3 the sum of the values in literal or register operands ol and o2. Though REIL requires o3 to be large enough to handle potential overflows, PREIL follows the C convention for unsigned conversions.

[0052] "and[ol][o2][o3]" writes to the register in o3 the AND of the literals or registers in ol and o2 (after sizing them to match o3).

[0053] "bisz[ol][][o3]" writes to the register in o3 the logical negation of the literal or register in ol, i.e., it writes 1 if ol = 0 or 0 if ol≠ 0.

[0054] "div[ol][o2][o3]" writes to the register in o3 the result of dividing the literal or register in ol by the literal or register in o2.

[0055] "ifm(oc [o0])[ol][o2][o3]" is abbreviated as "ifm(oc)[ol] [o2] [o3]" if operand oO is empty. If the register in operand oc is nonzero (i.e., true) and ol is nonempty, this is equivalent to "stm[ol][o0][o3]". If the register in oc is zero (i.e., false) and o2 is nonempty, this is equivalent to "stm[o2][o0][o3]". Otherwise, this is equivalent to "nop[][][]". For example, "ifm(r4 eax)[r64 tl][il69][r32 t2]" stores the 8 byte value of tl at the address specified by t2 if eax≠ 0. Otherwise, the 2 byte value 0x0009 is stored at that address.

[0056] "ifr(oc [o0])[ol][o2][o3]" is abbreviated as

"ifr(oc)[ol][o2][o3]" if operand oO is empty. If the register in operand oc is nonzero and ol is nonempty, this is equivalent to "str[ol][o0][o3]". If the register in oc is zero and o2 is nonempty, this is equivalent to "str[o2] [oO] [o3]". Otherwise, this is equivalent to "nop[][][]". For example "ifr(rl PF)[r80 tl][][r80 stO]" copies the 10 byte value of tl to stO if PF is set. Otherwise, stO is not modified.

[0057] "jcc[ol][o2][o3]" jumps to the target address specified by the literal, offset, or register in o3, within the segment specified by the literal or register in o2, if the literal or register in ol is nonzero. If o2 is empty, o3 can be empty (to jump to the end of the current PREIL list), a literal or register (for a target machine address in the current unit), an offset (to skip the given number of PREIL instructions without leaving the current PREIL list), or "rO <label>" (to jump to the first instruction occurring later in the current PREIL list that is of the form "nop[r0 <label>][][]"). If o2 is of the form "rO <unit>", o3 can be of the form "rO <block>" for the target address specified by the "<unit>:<block>:at" setting. This is useful for virtual routines to handle errors, interrupts, floating-point, SSE instructions, and so on.

[0058] "ldm[ol] [o2] [o3]" writes to the register in o3 the contents of memory starting at the address specified by the literal or register in ol within the segment specified by the literal or register in o2 (if o2 is nonempty). The size of o3, which must be a multiple of 8, determines how many bytes are read from memory. The "<data>:byte. order" setting determines the endianness where <data> is "data. main" unless o2 is of the form "rO <data>". This is useful for ports, volatile memory, register banks, and so on.

[0059] "lsh[ol][o2][o3]" writes to the register in o3 the result of left shifting the literal or register in ol by the literal or register in o2. [0060] "mod[ol][o2][o3]" writes to the register in o3 the result of the literal or register in ol modulo the literal or register in o2.

[0061] "mul[ol] [o2] [o3]" writes to the register in o3 the product of the literals or registers in ol and o2.

[0062] "nop[ol][][]" does nothing if ol is empty, sets a jump target if

01 is of the form "[r0 <label>]" where <label> begins with "label.", executes the PREIL list specified by setting "<macro>:code" if ol is of the form "[r0 <macro>]" where <macro> begins with "macro.", or considers ol a comment if it is anything else. A macro may call another macro, but cannot eventually call itself.

[0063] "or[ol] [o2] [o3]" writes to the register in o3 the (inclusive) OR of the literals or registers in ol and o2.

[0064] "rsh[ol] [o2] [o3]" writes to the register in o3 the result of logically right shifting the literal or register in ol by the literal or register in o2, i.e., vacated bits are zero-filled.

[0065] "stm[ol] [o2] [o3]" writes the contents of the literal or register in ol to memory, starting at the address specified by the literal or register in o3, within the segment specified by the literal or register in

02 (if o2 is nonempty). The size of ol, which must be a multiple of 8, determines how many bytes are written to memory. The "<data>:byte. order" setting determines the endianness where <data> is "data. main" unless o2 is of the form "rO <data>".

[0066] "str[ol][][o3]" writes to the register in o3 the contents of the literal or register in ol. The value for ol is truncated or zero-extended to the size of o3 as needed. A setting such as "current. unit" is read when ol is of the form "rO <setting>", and a setting such as "data. main:byte. order" is updated when o3 is of the form "rO <setting>". This is useful for bi-endian architectures.

[0067] "sub[ol][o2][o3]" writes to the register in o3 the result of subtracting the literal or register in o2 from the literal or register in ol.

[0068] "undef[][][o3]" marks the register in o3 as undefined until it is written again. This is useful for confidence measures. [0069] "unkn[] [] []" indicates an unknown operation. This is useful when the PREIL translation is incomplete.

[0070] "xor[o l ] [o2] [o3 ]" writes to the register in o3 the XOR of the literals or registers in o l and o2, i.e., it performs an exclusive or.

Preprocessing

[0071] Preprocessing is the process of disassembling binary code into native assembly instructions and its structures. The disassembly uses the standard IDA (Interactive Disassembler) Pro tool that statically analyzes binary code and breaks it down to functions, basic blocks, and instructions. Preprocessing then converts native instructions to PREIL, and links external libraries to ensure the static analysis will cover as much as possible of the application space. If available, preprocessing also uses dynamic execution traces to rebase addresses, resolve jump tables, load external references , and reconcile differences such as instructions that IDA Pro erroneously marked as data. Note that preprocessing results can be computed once and reused many times.

TMF TRANSFORMATION

[0072] TMF transformation has two steps : ( 1 ) modeling each PREIL instruction as algebraic expressions, and (2) aggregating them to TMF expressions. The aggregation can happen at different levels, from instruction to function level. For embodiments, the aggregation step is necessary to abstract the target application as much as possible while losslessly maintaining its original meaning.

Modeling PREIL Instructions

[0073] Modeling a single PREIL instruction captures the semantics of the instruction algebraically. As shown in FIG. 3 Table 1 , almost every PREIL instruction has one operator and three operands : two input operands and one output operand. The transformation operation varies depending on PREIL operator. For instance, if the PREIL operator is sub, then the transformation operation is subtraction. [0074] FIG. 5 is a table, Table 3, showing the equivalent transformation for each PREIL instruction 500. For example, consider the following:

[0075] sub[r32 esp] [i32 4] [r32 esp] transforms to esp = esp - 4 ( 1 )

[0076] stm[r32 eax] [] [r32 esp] transforms to [esp] = eax (2)

[0077] The square brackets [ and ] indicate pointer dereferencing so [esp] is the top slot on the stack pointed to by stack pointer esp.

[0078] Expression ( 1 ) indicates that the value of esp is decreased by 4. Notice that there are two instances of esp in a single expression. The esp on right hand side is the input esp and the one on the left is the output esp for the updated value. In general, all entities on the right hand side are inputs and all those on left hand side are outputs in the current scope. Expression (2) indicates the memory location pointed to by stack pointer esp obtains value of register eax. In other words, eax is stored on the stack located by stack pointer esp.

Modeling Native Instructions

[0079] FIG. 6 is a table, Table 4, illustrating the modeling of a native instruction 600. A native instruction is translated into several PREIL instructions. The aggregation of the TMF expressions for those PREIL instructions represents the modeling of a native instruction.

[0080] The native instruction "push eax" is translated into two PREIL instructions : "sub [r32 esp] [i32 4] [r32 esp]" and "stm[r32 eax] [] [r32 esp]". These instructions are modeled as "esp = esp - 4" and "[esp] = eax". After replacing esp in (4) by that in (3), we have "[esp-4] = eax". This expression means the value of eax is put on the stack when the stack pointer is decreased by 4. A single expression expresses two operations explicitly. That is the benefit of TMF.

TMF AGGREGATION

[0081] In previous section, we have seen an aggregation at instruction level. The aggregation allows one to see the meaning of an instruction better without any implicit operations. It provides a capability to understand the otherwise cryptic assembly instructions. The aggregation can also be implemented with multiple instructions and at higher levels such as blocks and functions. The aggregation yields a set of expressions that expose the relationships between inputs and outputs in a sequence of instructions.

Aggregation of Sequence of Instructions

[0082] Aggregation of a sequence of instructions has same principle as that of a single instruction. Aggregation of instruction I is a set of expressions expi = {expil,...,expin}. Aggregation of instruction J right before I is another set of expressions expj = {expj 1, ... ,expjm} . The aggregation of both instructions I and j is a new set of expressions expk = {expkl,...,expkn} where some of terms in right-hand side of expressions in expk are left-hand side terms of expj.

[0083] The purpose of aggregation is to find the most directed relations between inputs and outputs from a list of TMF expressions (or TMFs for short).

[0084] Assume we have TMF for a scope f (f could be a block or a function) outi = f(inil,...,inin). g is another scope that includes output of f as part of its inputs outj = g(injl,...,outi,...,injm). Output of an expression could become input of another expression. This process is called aggregation.

[0085] outi = f(inil,...,inin)

[0086] outj = g(inj l,...,outi,...,injm)

[0087] = g(injl,..., f(inil,...,inin),...,injm)

[0088] = gagg(inil,...,inin,injl,...,injm)

[0089] Aggregation results in a set of direct expressions between inputs and outputs in a scope.

Aggregation Algorithm

[0090] FIG.7 is a table, Table 5, that presents aggregation algorithm 700 which starts from a list of PREIL instructions in order. For each instruction, a modeling process occurs that translates a single PREIL to a TMF expression. The TMF expression, in turn, goes through a process to determine its inputs and outputs. The output is a left-hand side term. The inputs are terms that constitute the expression.

[0091] For instance, the expression

[0092] eax = [ebp+0x5] - ebx (6)

[0093] has

[0094] eax as its output (7)

[0095] ebx and [ebp+0x5] are its inputs. (8)

[0096] Note that [ebp+0x5] means dereference of a pointer represented by ebp+0x5. As said in the Aggregation of Sequence of Instructions Section, the output of an expression could become the input of another expression; a process of replacing inputs with outputs happens that transforms the set of TMF expressions into a smaller set whose expressions are more comprehensive and complete. Assume the inputs (8) above are in fact the outputs of previous expressions such as

[0097] ebx = 0x5 (9)

[0098] [ebp+0x5 ] = ecx + edx ( 10)

[0099] Replace input of (6) with outputs of (9) and ( 10), we have the final aggregated expression where eax is output and ecx, edx are inputs :

[00100] eax = ecx + edx - 0x5

LEVELS OF AGGREGATION

[00101] Aggregation can happen at six different levels : instruction, basic block, single path, multiple path, loop and function. No matter at what level, the aggregation still follows the same algorithm described in FIG. 7, Table 5. The instruction level aggregation is discussed in the Aggregation of Sequence of Instructions Section. The rest of the levels will be discussed in next sections.

Basic Block Aggregation

[00102] Basic block is a list of consecutive assembly instructions whose first instruction is the only entry, and last instruction is the only exit. B asic block aggregation starts from the last instruction and goes upward. The inputs of one instruction could be obtained from outputs of instructions that are above it, as described in the Aggregation of Sequence of Instructions Section. The outcome of aggregation of the whole block is a set of expressions which describe the behaviors of the block. The set of expressions has predictive power, i.e., given some inputs, the expressions can predict precisely what outputs should be without executing the instructions. Execution has been replaced by computation. To illustrate the aggregation at this level, let us consider a simple basic block as:

[00103] mov eax, [ebp+0x8] (11)

[00104] sub eax, [ebp+Oxc] (12)

[00105] mov [ebp-0x8], eax (13)

[00106] cmp [ebp-0x8], 0 (14)

[00107] jle 0x40101d (15)

[00108] This block obtains two numbers from two arguments [ebp+0x8] and [ebp+Oxc] (11 and 12). The second number is subtracted from first number and the difference is compared with value 0x0 (12, 13 and 14). If the difference is not positive, jump to address 0x40101d (15), otherwise execute next instruction which is not shown in the sample yet. The modeling of the basic block is done via PREIL and presented as:

[00109] eax = [ebp+0x8] (from 11)

[00110] eax = eax - [ebp+Oxc] = [ebp+0x8] - [ebp+Oxc] (from 12)

[00111] [ebp-0x8] = eax = [ebp+0x8] - [ebp+Oxc] (from 13)

[00112] if [ebp+0x8]-[ebp+0xc]≤ 0x0 then (from 14)

[00113] jump to 0x40101d (from 15)

[00114] The aggregation of the basic block in question now is:

[00115] eax = [ebp+0x8] - [ebp+Oxc] (16)

[00116] [ebp-0x8] = [ebp+0x8] - [ebp+Oxc] (17)

[00117] Summary of the two TMF expressions is: the basic block has two inputs [ebp+0x8], [ebp+Oxc] and two outputs eax, [ebp-0x8]. The relationships between inputs and output are described in (16) and (17). These expressions model the behavior of the block which is finding the difference of two numbers. The difference will dictate what instruction (or block) to execute next, i.e., if the difference is positive or negative. This expression has predictive power where it can tell what the next block should be, given values of the two inputs without executing instructions in the block.

[00118] Basic block aggregation is fundamental in aggregating higher levels. At higher levels, a list of instructions can be divided into a list of basic blocks and the aggregation at the higher levels is the aggregation of aggregated basic blocks. The next aggregation level is the single path aggregation.

Single Path Aggregation

[00119] FIG. 8 describes a three-block path for single path modelling 800. Single path is a list of basic blocks that are executed in sequence (in this case the three blocks 805, 810, and 815). This happens with dynamic execution whose inputs cause the blocks in the path to be executed. The executed path is examined in the aggregation process.

[00120] Aggregation of a path is the aggregation of its consecutive aggregated blocks. Each block is aggregated separately as discussed in the Basic Block Aggregation Section, and the aggregation on these block-level aggregations is called aggregation of a single path. To illustrate the process, select the TMF expressions corresponding to the assembly code in rectangles 820, 825, and 830 in FIG. 8 and aggregate them. First block 805 has eax and [ebp-0x8] as outputs. The condition to have next block 810 executed at this block is [ebp-0x8] < 0 or [ebp+0x8]- [ebp+0xc] < 0. Second block 810 has edx and [ebp-0x4] as outputs. The outputs of first block 805 and inputs of second block 810 have nothing in common, so no aggregation is necessary. The only expression in third block 815 that needs attention is where its output eax is replacing the current value of eax in first block 805 and its input [ebp-0x4] is output of the second expression in the second block 810. Aggregating them altogether as in the algorithm in FIG. 7 Table 5, should yield eax = [ebp+0xc] . Single path aggregation of FIG. 8 is finalized in FIG. 9, Table 6. [00121] FIG. 9, Table 6, depicts finalized single path aggregation 900 of FIG. 8. The path above happens only when [ebp+0x8] - [ebp+0xc] < 0. Once this happens, we can tell that the outcome is eax = [ebp+Oxc] , which is the max value because [ebp+0x8] - [ebp+Oxc] < 0 or [ebp+0x8] < [ebp+Oxc] . From the set of expressions representing the executed path, the execution of path instructions can be replaced by a series of simple computations .

Multi-Path Aggregation

[00122] Statically, one cannot decide which path the execution should take. Only when input data is entered during dynamic run time, will a certain path be executed. TMF however, is able to provide the multi- path aggregation which covers all possible paths from any block. Each path is associated with certain conditions. These conditions , when computed with real input data, will dictate what path the execution would take. That capability is powerful in terms of providing a big picture to an analyst who wants to know the possible choices given different inputs. To illustrate the multi-path aggregation, the same min/max examples as in previous sub-sections are used.

[00123] FIG. 10 depicts Multi-Path Modelling 1000. There are two possible paths based on the outcome of subtraction. If [ebp-0x8] is positive, block 1020 is executed, otherwise block 1010 would be. Blocks 1005 and 1015 are blocks that will be executed no matter what the outcome.

[00124] FIG. 11 , Table 7, 1100 provides a clear cut solution of the max example. If the difference is negative, the max value eax is second number 1105. If the difference is positive, the max is first number 1110. TMF thus proves its capability to abstract the assembly instructions into a set of meaningful algebraic expressions.

Function Aggregation

[00125] Function aggregation is a collection of mutually exclusive aggregated paths. The path to be executed depends on the values of passed-in arguments. The max example in the previous section could be wrapped in a function which has two arguments as two numbers [ebp+0x8] and [ebp+Oxc] and returned value as eax. As with multi-path aggregation, the function aggregation provides a clear cut decision tree of what inputs would lead to what paths and what results. FIG. 11, Table 7 indicates that if [ebp+0x8] - [ebp+Oxc] < 0 or numl - num2 < 0, then the max would be eax = [ebp+Oxc] , i.e., second number is the max.

[00126] FIG. 12, Table 8 shows an XML version of max function aggregation 1200. A TMF XML can have multiple paths. In this example, one path 1205 has [ebp+0x8]> [ebp+0xc] or numl >num2 and other path 1210 has [ebp+0x8]≤[ebp+0xc] or numl<num2. A path can contain several segments which would be discussed in next sub-section. Each segment has a list of algebraic expressions and a list of conditions which are path conditions.

Called Functions

[00127] A function can be called (callee) by other functions (caller). The callees break a caller segment into several sub-segments, where each sub-segment is ended by a call instruction. The callee is expressed in XML as a condition, and callees ' arguments are in expressions. For instance, 'max' function with two arguments [ebp+0x8] (numl ) and [ebp+Oxc] (num2) can be called in XML as follows :

[00128] <exprs>

[00129] <expr>[esp-0x4]=0x8044400</expr>

[00130] <expr>[esp] = [ebp+0x8]</expr>

[00131] <expr>[esp+0x4] = [ebp+Oxc] </expr>

[00132] </exprs>

[00133] <conds>

[00134] <call>max</call>

[00135] </conds>

[00136] Three entities are pushed onto the stack in order before max is called: returned address 0x8044400 at [esp-0x4] , first argument [ebp+0x8] at [esp] and second argument [ebp+Oxc] at [esp+0x4] . All are expressed in node <exprs>.

Loop Aggregation [00137] Loop is complex data structure with a history of research. TMF is able to handle most natural loops using dominance algorithm. Natural loop is defined as loop whose back edge forms smallest set of nodes including back edge and has no predecessors outside the set except for the predecessor of the header. TMF divides loops into two categories : non-nested loops and nested loops.

Non-Nested Loops

[00138] With a non-nested loop, TMF can compute loop variables , loop invariants and loop exit conditions. With exit conditions , TMF constructs inequalities to solve algebraically for the number of iterations to satisfy the conditions. TMF thus does not need to unroll the loop. This feature avoids the most time consuming computation process.

[00139] FIG. 13 depicts a loop and its TMF 1300 illustrating this feature. From algebraic expressions, we can understand the meaning of the loop. The first expression [ebx+eax] = [edi+edx] where eax and edx are set to 0 before the loop, and incremented inside the loop. This expression means the source buffer [edi+edx] , whose index is edx, is copied to destination buffer [ebx+eax] whose index is eax. The loop continues as long as the inequality edx+ 1- esi - [ebp-0x l4] < 0 is satisfied where [ebp-0xl 4] is a local variable and assigned with some constant value before the loop.

[00140] To find out number of iterations it takes to exit the loop, we introduce loop variable n generalized from incremented indices in loop: eax = eax + 1 and edx = edx + 1. The increment with loop variable n now becomes : eax = eax + n and edx = edx + n. The buffer copying process then becomes [ebx+eax+n] = [edi+edx+n] , and the exit condition becomes edx + n - esi - [ebp-0x l4] < 0. This inequality is satisfied as long as n < [ebp-0xl4]+esi-edx. With real values plugged into inequality, we can solve for n. Note that all terms in exit conditions have an original value before loop. For example, let [ebp-0x l4] = 15 , esi=3 and edx=0, then n < 15-3+0= 12, i.e. , it would iterate 12 times to exit the loop above. In other words, instead of unrolling the loop dynamically, we can statically compute all aspects of the loops including how many times the loops would unroll mathematically.

Nested Loops

[00141] Nested loops are loops inside other loops. The dynamic aspects of inner loops and outer loops plus the interactions between them make the static computation mentioned in non-nested loop section above in general impossible. Another generic method is needed to handle nested loops and non-nested loops also.

[00142] TMF treats all loops in nested loops as separate functions where all activities in loops occur inside loop-equivalent functions and the caller just gathers the final outcomes from the loops when they are finished. In other words, the most-outer-loop calls inner-loop- equivalent functions and the functions, in turn, call the most-inner-loop- equivalent function. The XML version of TMF of loop-equivalent function is almost as same as that of a function plus indicator of loop.

[00143] FIG. 14, Table 9, describes an XML version of a loop 1400. Loop always has two segments : one is before and one is after exit conditions. The segment after exit conditions can be empty in case of exit conditions are at the end of loop. The computation of loop starts from the first segment. At the end of first segment, exit conditions are checked. If they are satisfied, computation of loop is done, otherwise continuing to compute the segment after exit conditions. The next round of computation would repeat the same process until the exit conditions are satisfied.

Recursion

[00144] "Recursion is the process of repeating items in a self-similar way". TMF treats recursion as a function calling another function, even though the callee and caller are the same. The recursion is finished when all base cases are satisfied.

[00145] Recursive TMF must have at least two paths : one path has a call to itself and the other path has no call to itself. The latter is the base case. [00146] FIG. 15, Table 10, describes the skeleton of recursion function 1500. The second <path> section describes a path that leads the function to call itself as expressed by <call>itself</call>.

APPLICATIONS

[00147] TMF abstracts application binary to a set of algebraic expressions. The lossless abstraction lifts software understanding to a higher level where human and software can take advantage of meaningful patterns from concrete algebraic representation of the binary code to create better tools in interpreting the binary code without source code.

[00148] Among the tools are constraint generation, data flow analysis , exploratory bug searches, range and domain analysis , path pruning and return-oriented programming.

Constraint Analysis Optimization

[00149] Constraint based techniques have been used to model program analyses. One of the known constraint problems is finding inputs that direct execution path to certain pre-determined paths . To generate constraints for that problem, data flow analysis or taint is used. Taint however is a time consuming and CPU intensive process which requires tracing all executed instructions in a manner that all operations are recorded in detail. The traces are then processed to track the data flow coming from inputs or points of interest along the executed path. A simple over/under taint could cause very large deviation from the correct set of taints, thus renders set of generated constraints under/over-optimized, i.e., more/less constraints than necessary.

[00150] TMF sets of input-output relationships are used to optimize the set of generated constraints by removing irrelevant ones. The irrelevant constraints are ones that have no influence to the desired path. TMF analysis of static data flow could replace taints in most places, and in some case where taints are necessary such as indirect addresses, it could help reduce amount of computation using algebraic expressions. The taintless approach speeds up the process of constraint generation by avoiding taints as much as possible and removing irrelevant constraints. [00151 ] The algorithm of constraint optimization using TMF is as follows . Assume a desired path is selected which is different from executed path. The constraint generation starts from the last identical block of the desired and executed paths . The j ump condition at that last block would be the first constraint problem to solve. There are two types of j umps : conditional j umps such as 'j ump if less than' or unconditional j umps such as calling other function. The j ump in question must be a conditional j ump ; otherwise no constraint is generated, because the path cannot be changed.

[00152] The analysis is made possible by TMF aggregated expressions . As in multi-path aggregation, discus sed in the Multi-Path Aggregation Section, the conditions are analyzed beforehand. Each of the components that constitutes the conditions would be aggregated, and their aggregated values form the optimal constraints for that block. The constraint generation process goes upwards until the needed inputs are found.

[00153] FIG. 16 presents a partial desired path 1600. Circled block 1605 has two potential next blocks . One is block 1610, and the other is block 1615. Block 1610 is where the desired path will go. Block 1615 is where the executed path ends . We look at the block above them which is circled block 1605. This block is magnified in FIG. 16 with broken-lined block 1620. The condition to go to block 1610 is [ebp- Oxc] < 5. Next, we go to the block above the conditioned block 1610 which is block 1605 0xe61080 - another magnified broken-lined-block 1625. The condition of this block is [ebp-Oxc] > 4. Combining these two conditions together, we have 5 > [ebp-Oxc] > 4. Next task would be aggregation of the components of conditions . According to TMF of that block, [ebp-Oxc] = [ebp-0x l 0] + [ebp-0x8 ] + [ebp-0x4] . These are three local variables of that function. Aggregating these local variables to the beginning of the function yields three registers eax, ecx, and edx as inputs . They are three registers that obtain three user inputs from the scanf function. Therefore, to be able to go block 1610 right below circled block 1605, the sum of the three inputs must be 4 or 5. Outside that range, the path will go to the sibling block 1615.

Data Flow Analysis

[00154] As the name Taint Modeling Function implies, TMF expresses complex taint or data flow in application as algebraic expressions.

[00155] FIG 17 presents the control flow graphic 1700 of a function.

[00156] In this graphic, ebx is the first argument of the function, as circled by the first oval 1705. This register involves thoroughly inside the function. As a result, TMF representation also exposes the involvement of this register ebx in mathematical expressions as well.

[00157] The function contains nested loops . The most inner loop is the one discussed in the Non-Nested Loop Section. This loop has only one node. Its task is to copy data from one buffer to another. Second oval 1710 reveals the buffer copying in a loop which is modeled as [ebx+eax+n] = [edi+edx+n] . Register ebx is the pointer of the destination buffer, as seen as a component of [ebx+eax+n] . Register eax is the index of the buffer which is modeled as eax+n. The source buffer is represented by its pointer edi and index edx. The buffer copying is ended when exit condition edx+n-esi < [ebp-0x l4] is satisfied. See the Non-Nested Loop Section for more detail.

[00158] The outer loop also contains a buffer copying process. The buffer pointer is again represented by register ebx as [ebx+eax+m] = 0x2e and [ebx+eax+m+ 1 ] = 0x0. The buffer obtains constant numbers as 0x2e and 0x0 this time. The outer loop is ended when exit conditions [edi+edx+m] ≠ 0 and m > 0. Third oval 1715 contains the native machine code that implements the check for the exit conditions. If the exit conditions are not met, the loop continues.

[00159] TMF can not only expose the relationships between registers and memory locations in the scope that it explores, it also presents the framework that allows one to enter input data to see how a section of codes behaves. This framework is applicable for automatic approaches where the analysis happens just once and can be reused later. The "analyze once and execute many times" capability lifts the limitation of taint analysis in time and space, and thus could explore broader and deeper into application space.

Exploratory Bug Searches

[00160] As mentioned, software development is a complex process. Software errors or 'bugs ' are unavoidable in developing applications. Needless to say, testing procedure becomes increasingly important to detect the existing and potential bugs. Detecting bugs with source code is hard. Detecting bugs in application without source code is even harder due to the complexity and cryptic characteristics of assembly instructions.

[00161] Abstraction of binary codes can be used to simplify the process of understanding binary code and detecting bugs. TMF contributes to that effort by using its algebraic patterns to search for bugs statically in entire application space and therefore achieve very high code coverage. Developers who use TMF to search for bugs just need to write heuristic rules.

[00162] For instance, a buffer overflow bug happens when the buffer is smaller than its received data size. When that data is copied to the buffer, it accidentally overwrites part of the stack which can change the execution direction and cause undesired effects. The heuristic rules to detect buffer overflow are:

[00163] - Find loops in entire application space.

[00164] - In the found loops, focus only on loops that have data copying to a buffer.

[00165] - In these filtered loops, find exit conditions that could become bad, i.e., controlled by user inputs.

[00166] If exit conditions can be controlled by user inputs , then carefully crafted inputs could cause loops to never exit or at least exit after a very large number of iterations which likely overflows the buffers inside the loops.

[00167] FIG. 18 presents a section of binary code 1800 that contains a buffer overflow bug. Following the heuristic strategy mentioned above, a loop is found at address 0x804e523 1805. The next step is to find the buffer copying in this loop. The TMF expressions for this block are displayed in FIG. 13. The expression [ebx+eax] = [edi+edx] has eax and edx as indices of the buffers, and they are incremented inside the loop. The expression is a telltale of data transfer whose source is the buffer pointed to by ebx and the destination is the buffer pointed to by edi. Two of the three rules are satisfied; we need to confirm if the third rule conforms , which is : if the exit condition is controllable by user input. The exit condition is represented by the expression edx+n-esi- [ebp-0x l4] < 0. To check if the condition is bad, one must find if this inequality can be controlled by user inputs or function arguments. There are three terms in the expression which are: edx, esi and [ebp- 0x14] . Function aggregation reveals the origins of these terms : [esp+Oxc] for esi, and [[esp+0x8] + [esp+0xc] ] for [ebp-0xl 4] . These are function arguments which are capable of being changed from the caller, therefore the exit condition could be poisoned on purpose. The loop then has a potential buffer overflow bug.

[00168] If the user can control either [esp+Oxc] or [esp+0x8] or both, then the overflow of the buffer [ebx+eax] is unavoidable. Detecting whether these terms can be controlled by users can be done by a dynamic taint approach.

Range and Domain Analysis

[00169] One of the tools that detects bugs is range and domain analysis . The tool finds the possible ranges and domains that the function in question covers. It allows the developer to find the inputs that expose the corner cases which are usually missed in normal operation. For instance, the thermostat has some ranges which normal operations rarely reach, and therefore would not exercise the codes that handle such cases.

[00170] TMF aggregation yields a set of conditions for multi-path aggregation as seen in the Multi-Path Aggregation Section. TMF also summarizes the computations that happen during execution of the path. Combining these two features, TMF can provide a thorough range and domain analysis .

[00171] FIG. 19 presents a function to be examined by TMF 1900. Multi-path analysis provides a set of paths. Each of them will be analyzed as part of example. The path 1 , 2, 3 , 6, 8 1905 has a set of conflict conditions : [ebp+0x8] > 5 , [ebp+0x8] > 10 and [ebp+0x8] < 5. This path 1905 therefore is pruned, i.e. , the path will be never exercised. The other path 1 ,3 ,4,7, 8 1910 is also pruned because of conflict conditions : [ebp+0x8] ≤ 5 , [ebp+0x8] > 5 and [ebp+0x8] > 10. The other three paths are valid:

[00172] - 1 ,2,5 , 8 1915 with conditions : [ebp+0x8] > 5 and [ebp+0x8] < 10. The output of the function: eax = 0.

[00173] - 1 ,3 ,6, 8 1920 with condition: [ebp+0x8] ≤ 5 and output eax = 1.

[00174] - 1 ,2,3,4,7, 8 1925 with conditions : [ebp+0x8] > 5 and [ebp+0x8] > 10 and output eax = 2.

[00175] Combining these conditions and outputs, TMF can come up with domain: [-∞,∞] and range: { 0, 1 , 2 } .

Path Pruning

[00176] As seen in previous section, domain and range analysis can prune some paths that are never exercised in operation. Such pruning saves time in tasks that involve execution paths. The pruning in the Range and Domain Analysis Section is local to functional scope.

[00177] FIG. 20 shows another path pruning technique, task-oriented pruning 2000, spans the whole application space.

[00178] This type of pruning relies on certain 'hot spots ' such as potential bugs and finds only paths that lead to those places. FIG. 20 shows the red paths 2005 that lead to the destination. The rest of application space is ignored for that task. TMF aggregation statically analyzes binary code and uses heuristic rules to find potential vulnerabilities. Once the 'hot spots ' are found, static path analysis which uses TMF information to find possible paths to the nodes which narrows down scope of dynamic searches.

Return Oriented Programming

[00179] The exploitation such as buffer overflow finds a way to modify the returned address, and therefore could change execution direction to the attacker's benefit. Before data execution prevention (DEP) (executable space protection on Windows) was implemented, certain shellcode which piggybacks on data that overflows the buffer could be deposited onto the stack and executed from there. That simple exploit is no longer available thanks to DEP. A new technique named return- oriented programming (ROP) can bypass DEP by executing chunks of code that are already marked as executable in memory such as code in the application itself and shared linked libraries.

[00180] ROP finds certain instructions in the block that satisfy some constraints, and is ended by return or call instruction. The constraints can be expressed as expressions to be queried using TMF.

[00181] FIG. 21 depicts VirtualAllocEx Called in an Application 2100. This is an example of such constraints that are the parameters of a well- known API that allocates chunks of memory within virtual address space in a process : VirtualAllocEx. This API was found in target application at 0x7c809ae6 2105. The API has five parameters : hProcess, lpAddress , dwSize, flAllocationType and flProtect, and we are interested in dwSize and flAllocationType or [ebp+0xc] and [ebp+0xl 0] accordingly as in FIG. 21. dwSize and flAllocationType determine the size and type of the allocated memory. Memory allocations that are too small or of the wrong type are often the direct cause of bugs and vulnerabilities.

CONCLUSION

[00182] As explained, the Taint Modeling Function (TMF) is a novel approach to abstract binary code for software analysis . TMF transforms the binary executables to sets of precise algebraic expressions thanks to intermediate language PREIL. PREIL is an intermediate language that simplifies and disambiguates native language. The lossless abstraction of binary codes via algebraic expres sions makes it possible to automate static analysis tasks such as detecting defective code patterns , generate constraints to find needed inputs for desired paths , and narrowing search space for potential bugs . The expressions are also simple for human analysts who want to understand the target software inside out via querying TMF expressions in database. The automated applications of TMF can help balance the currently imbalanced of generating versus detecting malevolent software by speeding up the proces s of bug finding, and alleviating human users from that tedious and difficult task.

[00183] The foregoing description of the embodiments of the invention has been presented for the purposes of illustration and description. It is not intended to be exhaustive or to limit the invention to the precise form disclosed. Many modifications and variations are possible in light of this disclosure. It is intended that the scope of the present disclosure be limited not by this detailed description, but rather by the claims appended hereto .

[00184] A number of implementations have been described. Nevertheles s , it will be understood that various modifications may be made without departing from the scope of the disclosure. Although operations are depicted in the drawings in a particular order, this should not be understood as requiring that such operations be performed in the particular order shown or in sequential order, or that all illustrated operations be performed, to achieve desirable results .

[00185] Each and every page of this submission, and all contents thereon, however characterized, identified, or numbered, is considered a substantive part of this application for all purposes , irrespective of form or placement within the application. This specific ation is not intended to be exhaustive or to limit the invention to the precise form disclosed. Many modifications and variations are possible in light of this disclosure. Other and various embodiments will be readily apparent to those skilled in the art, from this description, figures , and the claims that follow. It is intended that the scope of the invention be limited not by this detailed description, but rather by the claims appended hereto.