BlackBerry Limited
METHOD AND DEVICE FOR SYMBOLIC ANALYSIS OF A SOFTWARE PROGRAM

Abstract:

A method for symbolic analysis of a software program is described. The method comprises constructing a control flow graph (CFG), for a software program procedure, the CFG comprising nodes representing basic blocks reachable within the software program procedure, the basic blocks represented as respective functions from a first machine state on entry to a said basic block to a second machine state on exit from that basic block. The method further describes simplifying the CFG to a single node representing the software program procedure as a function from an input machine state on entry to the software program procedure to an output machine state on exit from the software program procedure, comparing said function to a rule set identifying vulnerabilities based on effects on the machine state; and determining a vulnerability within the software program procedure based on the comparing.