Methods for concurrent vulnerability detection based on code concurrency property graphs

A concurrency vulnerability detection method based on a code concurrency property graph (CCPG), wherein the method adopts a vulnerability detection tool CONCODEQL, and comprises:

• S1, initializing a code property graph (CPG) and identifying one or more critical nodes based on a source code to be tested, including:
• initializing the CCPG and identifying one or more critical nodes within a concurrent program of the CCPG based on the source code to be tested, the CPG, and a value flow graph (VFG);
• S2, constructing one or more concurrency relationships by traversing the CCPG, including:
• traversing the initialized CCPG, constructing a thread-aware context, and sequentially performing flow-sensitive happens-before analysis, inter-procedural lock-set analysis, and enhanced concurrent pointer analysis based on the thread-aware context, and constructing the one or more concurrency relationships for the one or more critical nodes in the CCPG;
• performing thread-aware analysis and thread-aware, flow-sensitive analysis;
• wherein the performing the thread-aware analysis includes:
• defining the thread-aware context for a critical node as one or more paths from a main entry node to the critical node that collectively encompass all ancestor threads and a current thread;
• denoting a thread-aware context along a specific path as c=[n1, n2, . . . , nm], wherein each element denotes a concurrency behavior node, all thread-aware contexts of a critical node ni are denoted as a two-dimensional matrix
• C
• =
• [
• c
• 1
• i
• ,
• c
• 2
• i
• ,
• …
• ,
• c
• k
• i
• ]
• ,
• and k denotes a count of feasible execution paths from the main entry node to the critical node;
• the flow-sensitive happens-before analysis includes:
• constructing one or more happens-before edges based on the thread-aware context to determine an execution order between a first node ni and a second node nj;
• for the first node ni, constructing a fork set for each thread-aware context of the first node ni;
• defining the fork set as
• fs
• k
• i
• =
• {
• n
• ∈
• c
• k
• i
• ❘
• λ
• ⁡
• (
• n
• )
• =
• Fork
• ⁢
• (
• t
• )
• ⋀
• JOIN
• ⁢
• (
• t
• )
• ∉
• c
• k
• i
• }
• ,
• wherein the fork set consists of one or more FORK nodes whose corresponding threads have not yet been joined within the thread-aware context, the CONCODEQL checks whether fork sets of the first node ni and the second node n have any overlap, an overlap between the fork sets of the first node ni and the second node nj indicates that the first node ni and the second node nj execute concurrently, and a hp relationship between the first node ni and the second node nj is determined using following formula:
• h
• ⁢
• p
• ⁡
• (
• n
• i
• ,
• n
• j
• )
• =
• {
• 0
• ,
• Λ
• k
• 1
• ∈
• [
• 1
• ,
• k
• i
• ]
• ;
• k
• 2
• ∈
• [
• 1
• ,
• k
• j
• ]
• ⁢
• fs
• k
• 1
• i
• ⋂
• fs
• k
• 2
• j
• ==
• ∅
• 1
• ,
• otherwise
• performing the inter-procedural lock-set analysis includes:
• analyzing the happens-before relationship is insufficient to determine whether the first node ni and the second node nj are capable of concurrent execution, because the first node ni and the second node nj are capable of being protected by locks;
• for the first node ni and the second node nj, performing the inter-procedural lock-set analysis is performed to determine whether the first node ni and the second node nj are protected by a same lock;
• for the first node ni, the CONCODEQL constructs a lock set for each thread-aware context of the first node ni;
• wherein the lock set
• ls
• k
• i
• =
• {
• n
• ∈
• c
• k
• i
• ❘
• λ
• ⁡
• (
• n
• )
• =
• acquire_lock
• ⁢
• (
• l
• )
• ⋀
• release_lock
• ⁢
• (
• l
• )
• ∉
• c
• k
• i
• }
• .
• the lock set consists of one or more lock-acquisition nodes whose corresponding locks have not yet been released within the thread-aware context;
• the CONCODEQL determines whether the first node ni and the second node nj are protected by a same lock by checking whether lock sets of the first node ni and the second node nj have any overlap;
• a psl relationship between the first node ni and the second node nj is determined using following formula:
• psl
• ⁡
• (
• n
• i
• ,
• n
• j
• )
• =
• {
• 0
• ,
• Λ
• k
• 1
• ∈
• [
• 1
• ,
• k
• i
• ]
• ;
• k
• 2
• ∈
• [
• 1
• ,
• k
• j
• ]
• ⁢
• ls
• k
• 1
• i
• ⋂
• ls
• k
• 2
• j
• ==
• ∅
• 1
• ,
• otherwise
• performing the enhanced concurrent pointer analysis, wherein the enhanced concurrent pointer analysis includes global variable analysis and struct analysis;
• the global variable analysis denotes a precise analysis of global variables, designed by analyzing the CCPG and the VFG, including:
• identifying all global variable declarations by traversing the CCPG, thereby obtaining a global variable set;
• reconstructing connections between global variables and local variables, and determining one or more global variable aliases through flow-sensitive pointer analysis;
• the struct analysis includes:
• for an access node of a struct, simply obtaining a specific attribute accessed by the access node through the CPG using a regular expression-based determination, wherein the CONCODEQL analyzes the CCPG and the VFG, and adjusting a denotation of the struct in the flow-sensitive pointer analysis to the specific attribute;
• the thread-aware, flow-sensitive analysis includes:
• traversing the CCPG, and constructing the thread-aware context for each critical node;
• wherein the CONCODEQL obtains the all main entry nodes from the CCPG and initializes the thread-aware contexts of the main entry nodes as empty;
• during a main loop, if a current node with a current thread-aware context is accessed, the CONCODEQL directly terminates the loop;
• otherwise, the CONCODEQL traverses the CCPG along a thread-lifecycle edge and control-flow edge, if a current node n is a FORK node that creates a new thread, a thread-aware context of an entry node n′ of the new thread is initialized to each thread-aware context previously added to the current node n, and the new thread is created;
• if the current node n is not a FORK node, the CONCODEQL traversal proceeds along the control-flow edge, and the thread-aware context of the current node n is propagated to a successor node;
• the thread-aware context for each critical node is utilized for the flow-sensitive happens-before analysis and the inter-procedural lock-set analysis;
• the CONCODEQL traversing any pair of threads and checks whether memory access nodes of the thread pair execute concurrently based on the thread-aware context of each critical node, including:
• if the first node ni and the second node nj simultaneously satisfy that:
• 1) the first node ni and the second node nj access a same memory location;
• 2) the first node ni and the second node nj execute concurrently;
• 3) the first node ni and the second node n are not protected by a same lock, the CONCODEQL adding an HP edge between the first node ni and the second node nj;
• wherein an updated CCP is generated when the loop terminates;
• S3, detecting a concurrency vulnerability based on a domain-specific language, including:
• designing one or more query interfaces of the domain-specific language for different types of concurrency vulnerabilities, performing queries on the CCPG to conduct concurrency vulnerability detection, and outputting detected concurrency vulnerabilities as a vulnerability report.