# US 10,122,749 B2 · Systems and methods for analyzing software using queries > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 10,122,749 B2 - Document ID: US10122749B2 - Status: Granted - Kind: B2 - Application number: 15/249,284 - Filed: 2016-08-26 - Published: 2017-11-16 - Granted: 2018-11-06 - Earliest claimed: 2016-05-12 - Assignees: Synopsys, Inc. - Applicants: Synopsys, Inc. - Inventors: Guodong Li; John Steven - Web page: https://patentgrep.com/patent/US10122749B2 ## CPC - G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)} - G06F 8/75: Structural analysis for program understanding - G06F 11/3604: Analysis of software for verifying properties of programs (testing of software G06F11/3668) - G06F 11/3668: Testing of software - G06F 16/90332: {Natural language query formulation or dialogue systems} - G06F 21/562: {Static detection} - G06F 21/577: {Assessing vulnerabilities and evaluating computer system security} - H04L 63/1425: {Traffic logging, e.g. anomaly detection} - H04L 63/1433: {Vulnerability analysis} - G06F 2221/033: Test or assess software - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) - H04L: TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION (arrangements common to telegraphic and telephonic communication H04M) ## Abstract Systems and methods for software verification. In some embodiments, a first statement is identified, from a discovery query written in a query language, the first statement comprising a side-effect construct with at least a first parameter and a second parameter, wherein: the first parameter of the side-effect construct comprises at least one second statement specifying one or more actions to be performed; and the second parameter of the side-effect construct comprises at least one condition specified based on a syntactic pattern. Source code of a software application may be analyzed to determine whether the at least one condition is satisfied, wherein determining whether the at least one condition is satisfied comprises determining whether the source code comprises a program element that matches the syntactic pattern. ## Claims ### Claim 1 A computer-implemented method for performing static analysis to detect security vulnerabilities in a software application developed using a software framework, comprising operations of: identifying, by at least one computer processor, from a discovery query written in a query language, a framework model representing the software framework and a first statement comprising a side-effect construct with at least a first parameter and a second parameter, wherein: the first parameter of the side-effect construct comprises at least one second statement specifying one or more actions to be performed; and the second parameter of the side-effect construct comprises at least one condition specified based on a syntactic pattern; removing, by the at least one computer processor, information from a representation of code of a software application, based on at least one of the framework model, the first statement, the at least one second statement, and the syntactic pattern; analyzing, by the at least one computer processor, the representation of the code of the software application to determine whether the at least one condition is satisfied, wherein determining whether the at least one condition is satisfied comprises determining whether the code comprises a program element that matches the syntactic pattern; and in response to determining, by the at least one computer processor, that the code comprises the program element that matches the syntactic pattern: storing, by the at least one computer processor, the program element in a variable; performing, by the at least one computer processor, the one or more actions specified by the discovery query, based on the framework model and the program element stored in the variable; constructing, by the at least one computer processor, based on the one or more actions specified by the discovery query, at least part of an application architecture model for the software application; determining, by the at least one computer processor, based on the at least part of the application architecture model, whether the code of the software application satisfies one or more properties of interest; and in response to a determination that the code of the software application satisfies the one or more properties of interest: transforming, by the at least one computer processor, the code of the software application that satisfies the one or more properties of interest, wherein the transforming comprises substituting a new program element in place of the program element that matches the syntactic pattern. ### Claim 2 (depends on 1) The method of claim 1, wherein: the application architecture model comprises a plurality of component models; and the one or more actions specified by the discovery query are performed to generate at least one component model of the plurality of component models. ### Claim 3 (depends on 1) The method of claim 1, wherein: the framework model comprises a first module; and the first module comprises the discovery query. ### Claim 4 (depends on 3) The method of claim 3, wherein: the framework model further comprises a second module and a third module; the first module is imported into the framework model via the second module; and the second module is imported into the framework model via the third module. ### Claim 5 (depends on 4) The method of claim 4, wherein: the framework model further comprises a fourth module; and the fourth module is imported into the framework model via the second module. ### Claim 6 (depends on 1) The method of claim 1, wherein: the discovery query is a first discovery query; the framework model further comprises a second discovery query written in the query language; the application architecture model comprises a plurality of component models; and the second discovery query comprises a noun for accessing a component model of the plurality of component models, wherein the noun is defined in a library, wherein the library is associated with the software framework. ### Claim 7 (depends on 6) The method of claim 6, wherein: the second discovery query further comprises a verb for querying the noun; and an implementation of the verb is defined in the library. ### Claim 8 (depends on 1) The method of claim 1, further comprising: identifying, from a property query written in the query language, a first statement of the property query, a second statement of the property query, and a third statement of the property query, wherein: the first statement of the property query comprises the syntactic pattern; the second statement of the property query comprises at least one property indicative of a specific security vulnerability or type of security vulnerability; and the third statement of the property query comprises an additional one or more actions to be performed; analyzing the code of the software application to determine whether the code comprises at least one program element that matches the syntactic pattern of the first statement; in response to determining that the code comprises at least one program element that matches the syntactic pattern of the first statement: storing at least one portion of the at least one program element in at least one second variable; and evaluating the at least one property based at least in part on the at least one portion of the program element stored in the at least one second variable; in response to determining that the at least one property is satisfied, performing the additional one or more actions of the third statement of the property query. ### Claim 9 (depends on 8) The method of claim 8, wherein: the at least one portion of the program elements is a first portion of the at least one program element; and the one or more actions of the third statement are performed based on the second portion of the at least one program element. ### Claim 10 (depends on 9) The method of claim 9, further comprising: replacing, by the at least one processor, the second portion of the at least one program element with a modified program element. ### Claim 11 A system comprising: a memory; and at least one processor coupled to the memory, the at least one processor configured to perform operations comprising: for a software application developed using a software framework: identifying, from a discovery query written in a query language, a framework model representing the software framework and a first statement comprising a side-effect construct with at least a first parameter and a second parameter, wherein: the first parameter of the side-effect construct comprises at least one second statement specifying one or more actions to be performed; and the second parameter of the side-effect construct comprises at least one condition specified based on a syntactic pattern; removing information from a representation of code of a software application, based on at least one of the framework model, the first statement, the at least one second statement, and the syntactic pattern; analyzing the representation of the code of the software application to determine whether the at least one condition is satisfied, wherein determining whether the at least one condition is satisfied comprises determining whether the code comprises a program element that matches the syntactic pattern; and in response to determining that the code comprises the program element that matches the syntactic pattern: storing the program element in a variable; performing the one or more actions specified by the discovery query, based on the framework model and the program element stored in the variable; constructing, based on the one or more actions specified by the discovery query, at least part of an application architecture model for the software application; determining, based on the at least part of the application architecture model, whether the code of the software application satisfies one or more properties of interest; and in response to a determination that the code of the software application satisfies the one or more properties of interest: transforming, by the at least one computer processor, the code of the software application that satisfies the one or more properties of interest, wherein the transforming comprises substituting a new program element in place of the program element that matches the syntactic pattern. ### Claim 12 (depends on 11) The system of claim 11, wherein: the application architecture model comprises a plurality of component models; and the one or more actions specified by the discovery query are performed to generate at least one component model of the plurality of component models. ### Claim 13 (depends on 11) The system of claim 11, wherein: the framework model comprises a first module; and the first module comprises the discovery query. ### Claim 14 (depends on 13) The system of claim 13, wherein: the framework model further comprises a second module and a third module; the first module is imported into the framework model via the second module; and the second module is imported into the framework model via the third module. ### Claim 15 (depends on 14) The system of claim 14, wherein: the framework model further comprises a fourth module; and the fourth module is imported into the framework model via the second module. ### Claim 16 (depends on 11) The system of claim 11, wherein: the discovery query is a first discovery query; the framework model further comprises a second discovery query written in the query language; the application architecture model comprises a plurality of component models; and the second discovery query comprises a noun for accessing a component model of the plurality of component models, wherein the noun is defined in a library that is associated with the software framework. ### Claim 17 (depends on 16) The system of claim 16, wherein: the second discovery query further comprises a verb for querying the noun; and an implementation of the verb is defined in the library. ### Claim 18 At least one non-transitory computer-readable storage medium having stored thereon instructions which, when executed, program at least one processor to perform operations comprising: for a software application developed using a software framework: identifying, from a discovery query written in a query language, a framework model representing the software framework and a first statement comprising a side-effect construct with at least a first parameter and a second parameter, wherein: the first parameter of the side-effect construct comprises at least one second statement specifying one or more actions to be performed; and the second parameter of the side-effect construct comprises at least one condition specified based on a syntactic pattern; removing information from a representation of code of a software application, based on at least one of the framework model, the first statement, the at least one second statement, and the syntactic pattern; analyzing the representation of the code of the software application to determine whether the at least one condition is satisfied, wherein determining whether the at least one condition is satisfied comprises determining whether the code comprises a program element that matches the syntactic pattern; and in response to determining that the code comprises the program element that matches the syntactic pattern: storing the program element in a variable; performing the one or more actions specified by the discovery query, based on the framework model and the program element stored in the variable; constructing, based on the one or more actions specified by the discovery query, at least part of an application architecture model for the software application; determining, based on the at least part of the application architecture model, whether the code of the software application satisfies one or more properties of interest; and in response to a determination that the code of the software application satisfies the one or more properties of interest: transforming, by the at least one computer processor, the code of the software application that satisfies the one or more properties of interest, wherein the transforming comprises substituting a new program element in place of the program element that matches the syntactic pattern. ### Claim 19 (depends on 18) The at least one non-transitory computer-readable storage medium of claim 18, wherein: the application architecture model comprises a plurality of component models; and the one or more actions specified by the discovery query are performed to generate at least one component model of the plurality of component models. ### Claim 20 (depends on 18) The at least one non-transitory computer-readable storage medium of claim 18, wherein: the framework model comprises a first module; and the first module comprises the discovery query.