Identifying computer program security access control violations using static analysis

A computer-implemented method, comprising:

• generating, by a device operatively coupled to a processor, a mathematical model of a computer program product, wherein the mathematical model defines data flows through nodes of the computer program product that reach a secure node corresponding to a secure resource;
• and
• evaluating, by the device, a security protocol of the computer program product using static program analysis of the mathematical model to determine whether any of the data flows provide a path to the secure node that does not proceed through security nodes in an order corresponding to the security protocol, wherein the security nodes are included in the nodes of the computer program product, wherein the security nodes comprise an authorization node that checks an authorization of an entity to access the secure resource and an authentication node that checks an authentication of the entity, and wherein the order comprises flow through the authentication node prior to flow through the authorization node, wherein the using the static program analysis comprises evaluating the data flows as an interprocedural control-flow graph reachability problem using an interprocedural, finite, distributive, subset (IFDS) algorithm.