US 12,277,230 B2
Method and device for symbolic analysis of a software program
William James McCourt, West Lothian (GB); Niall Fitzgibbon, London (GB); Benjamin John Godwood, Chipping Norton (GB); and Paul Compton Hirst, Tiverton (GB)
Assigned to BlackBerry Limited, Waterloo (CA)
Filed by BlackBerry Limited, Waterloo (CA)
Filed on Feb. 4, 2021, as Appl. No. 17/168,079.
Claims priority of application No. 20160281 (EP), filed on Feb. 28, 2020.
Prior Publication US 2021/0271762 A1, Sep. 2, 2021
Int. Cl. G06F 21/57 (2013.01); G06F 21/54 (2013.01)
CPC G06F 21/577 (2013.01) [G06F 21/54 (2013.01)] 15 Claims
OG exemplary drawing
 
1. A method of symbolic analysis of a software program, the method comprising:
constructing, by at least one processor, a control flow graph (CFG), of 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, wherein constructing the CFG comprises symbolically executing the basic blocks of the software program procedure to obtain side-effect free functions representing the basic blocks as symbolic changes of the machine states;
simplifying, by the at least one processor, 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, wherein simplifying the CFG comprises at least one of merging basic blocks through symbolic substitution of the respective functions or replacing back edges within the CFG with explicit loop expressions, wherein simplifying the CFG comprises:
replacing return instructions within the CFG with links to respective nodes having a single exit; and
recursively processing another procedure and replacing a call to the another procedure in the CFG with a function representing a machine state change resulting from the another procedure;
comparing, by the at least one processor, said function to a rule set identifying one or more vulnerabilities based on one or more effects on the machine states; and
preventing, by the at least one processor, deployment of the software program procedure in response to determining a vulnerability within the software program procedure based on the comparing.