Abstract Branch and Bound ( $$\texttt{BaB}$$ BaB ) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of $$\texttt{BaB}$$ BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing $$\texttt{BaB}$$ BaB approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited $$\texttt{BaB}$$ BaB tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary’s position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent $$\texttt{BaB}$$ BaB -based approaches.

Formal verification is a rigorous approach that can provably ensure the quality of neural networks, and to date, Branch and Bound (BaB) is the state-of-the-art that performs verification by splitting the problem as needed and applying off-the-shelf verifiers to sub-problems for improved performance. However, existing BaB may not be efficient, due to its naive way of exploring the space of sub-problems that ignores the importance of different sub-problems. To bridge this gap, we first introduce a notion of “importance” that reflects how likely a counterexample can be found with a sub-problem, and then we devise a novel verification approach, called ABONN, that explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style. The exploration is guided by the “importance” of different sub-problems, so it favors the sub-problems that are more likely to find counterexamples. As soon as it finds a counterexample, it can immediately terminate; even though it cannot find, after visiting all the sub-problems, it can still manage to verify the problem. We evaluate ABONN with 552 verification problems from commonlyused datasets and neural network models, and compare it with the state-of-the-art verifiers as baseline approaches. Experimental evaluation shows that ABONN demonstrates speedups of up to 15.2× on MNIST and 24.7× on CIFAR-10. We further study the influences of hyperparameters to the performance of ABONN, and the effectiveness of our adaptive tree exploration.

The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch-and-bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive "first-come-first-served" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problems and so will not lead to a performance degradation. Specifically, Oliva has two variants, including Oliva^GR, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and Oliva^SA, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR-10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25× in MNIST, and up to 80× in CIFAR-10.

Incremental verification is an emerging neural network verification approach that aims to accelerate the verification of a neural network N* by reusing the existing verification result (called a template ) of a similar neural network N . To date, the state‐of‐the‐art incremental verification approach leverages the problem splitting history produced by branch and bound ( BaB ) in verification of N , to select only a part of the sub‐problems for verification of N* , thus more efficient than verifying N* from scratch. While this approach identifies whether each sub‐problem should be re‐assessed, it neglects the information of how necessary each sub‐problem should be re‐assessed, in the sense that the sub‐problems that are more likely to contain counterexamples should be prioritized, in order to terminate the verification process as soon as a counterexample is detected. To bridge this gap, we first define a counterexample potentiality order over different sub‐problems based on the template, and then we propose Olive, an incremental verification approach that explores the sub‐problems of verifying N* orderly guided by counterexample potentiality. Specifically, Olive has two variants, including Olive g , a greedy strategy that always prefers to exploit the sub‐problems that are more likely to contain counterexamples, and Olive b , a balanced strategy that also explores the sub‐problems that are less likely, in case the template is not sufficiently precise. We experimentally evaluate the efficiency of Olive on 1445 verification problem instances derived from 15 neural networks spanning over two datasets MNIST and CIFAR‐10 . Our evaluation demonstrates significant performance advantages of Olive over state‐of‐the‐art classic verification and incremental approaches. In particular, Olive shows evident superiority on the problem instances that contain counterexamples, and performs as well as Ivan on the certified problem instances.

Machine learning and its promising branch deep learning have shown success in a wide range of application domains. Recently, much effort has been expended on applying deep learning techniques (e.g., graph neural networks) to static vulnerability detection as an alternative to conventional bug detection methods. To obtain the structural information of code, current learning approaches typically abstract a program in the form of graphs (e.g., data-flow graphs, abstract syntax trees), and then train an underlying classification model based on the (sub)graphs of safe and vulnerable code fragments for vulnerability prediction. However, these models are still insufficient for precise bug detection, because the objective of these models is to produce classification results rather than comprehending the semantics of vulnerabilities, e.g., pinpoint bug triggering paths, which are essential for static bug detection.

Code embedding, as an emerging paradigm for source code analysis, has attracted much attention over the past few years. It aims to represent code semantics through distributed vector representations, which can be used to support a variety of program analysis tasks (e.g., code summarization and semantic labeling). However, existing code embedding approaches are intraprocedural, alias-unaware and ignoring the asymmetric transitivity of directed graphs abstracted from source code, thus they are still ineffective in preserving the structural information of code. This paper presents Flow2Vec, a new code embedding approach that precisely preserves interprocedural program dependence (a.k.a value-flows). By approximating the high-order proximity, i.e., the asymmetric transitivity of value-flows, Flow2Vec embeds control-flows and alias-aware data-flows of a program in a low-dimensional vector space. Our value-flow embedding is formulated as matrix multiplication to preserve context-sensitive transitivity through CFL reachability by filtering out infeasible value-flow paths. We have evaluated Flow2Vec using 32 popular open-source projects. Results from our experiments show that Flow2Vec successfully boosts the performance of two recent code embedding approaches codevec and codeseq for two client applications, i.e., code classification and code summarization. For code classification, Flow2Vec improves codevec with an average increase of 21.2%, 20.1% and 20.7% in precision, recall and F1, respectively. For code summarization, Flow2Vec outperforms codeseq by an average of 13.2%, 18.8% and 16.0% in precision, recall and F1, respectively.