Summary We describe techniques based on symbolic execution for finding software vulnerabilities that are due to algorithmic complexity. Such vulnerabilities allow an attacker to mount denial‐of‐service attacks to deny service to benign users or to otherwise disable a software system. The techniques use an efficient guided symbolic execution of a program to compute bounds on the worst‐case complexity (for increasing input sizes) and to generate test values that trigger the worst‐case behaviours. The resulting bounds are fitted to a function to obtain a prediction of the worst‐case program behaviour at any input size. Scalability is achieved by using path policies that guide the symbolic execution towards worst‐case paths. The policies are learned from the worst‐case results obtained with exhaustive exploration at small input sizes and are applied to guide exploration at larger input sizes, where unguided exhaustive exploration is not possible. To achieve precision in the analysis, the path policies take into account the history of choices made along the path when deciding which branch to execute next. Furthermore, the computation is contextpreserving, meaning that the decision for each branch depends on the history computed with respect to the enclosing method. We further report preliminary results on a complementary technique that uses machine learning for building the path policies that guide the search. The techniques are implemented in open‐source projects that build on the Symbolic Pathfinder tool for analysing Java programs. Experimental evaluation shows that the techniques can find vulnerabilities in complex Java programs and can outperform previous symbolic approaches.

Hybrid testing approaches that involve fuzz testing and symbolic execution have shown promising results in achieving high code coverage, uncovering subtle errors and vulnerabilities in a variety of software applications. In this paper we describe Badger - a new hybrid approach for complexity analysis, with the goal of discovering vulnerabilities which occur when the worst-case time or space complexity of an application is significantly higher than the average case.

Grey-box fuzzing is a random testing technique that has been shown to be effective at finding security vulnerabilities in software. The technique leverages program instrumentation to gather information about the program with the goal of increasing the code coverage during fuzzing, which makes gray-box fuzzers extremely efficient vulnerability detection tools. One such tool is AFL, a grey-box fuzzer for C programs that has been used successfully to find security vulnerabilities and other critical defects in countless software products. We present Kelinci, a tool that interfaces AFL with instrumented Java programs. The tool does not require modifications to AFL and is easily parallelizable. Applying AFL-type fuzzing to Java programs opens up the possibility of testing Java based applications using this powerful technique. We show the effectiveness of Kelinci by applying it on the image processing library Apache Commons Imaging, in which it identified a bug within one hour.

We propose a technique based on symbolic execution for analyzing the algorithmic complexity of programs. The technique uses an efficient guided analysis to compute bounds on the worst-case complexity (for increasing input sizes) and to generate test values that trigger the worst-case behaviors. The resulting bounds are fitted to a function to obtain a prediction of the worst-case program behavior at any input sizes. Comparing these predictions to the programmers' expectations or to theoretical asymptotic bounds can reveal vulnerabilities or confirm that a program behaves as expected. To achieve scalability we use path policies to guide the symbolic execution towards worst-case paths. The policies are learned from the worst-case results obtained with exhaustive exploration at small input sizes and are applied to guide exploration at larger input sizes, where un-guided exhaustive exploration is no longer possible. To achieve precision we use path policies that take into account the history of choices made along the path when deciding which branch to execute next in the program. Furthermore, the history computation is context-preserving, meaning that the decision for each branch depends on the history computed with respect to the enclosing method. We implemented the technique in the Symbolic PathFinder tool. We show experimentally that it can find vulnerabilities in complex Java programs and can outperform established symbolic techniques.

Heap and data structures represent one of the biggest challenges when applying model checking to the analysis of software programs: in order to verify (unbounded) safety of a program, it is typically necessary to formulate quantified inductive invariants that state properties about an unbounded number of heap locations. Methods like Craig interpolation, which are commonly used to infer invariants in model checking, are often ineffective when a heap is involved. To address this challenge, we introduce a set of new proof and program transformation rules for verifying object-oriented programs with the help of space invariants, which (implicitly) give rise to quantified invariants. Leveraging advances in Horn solving, we show how space invariants can be derived fully automatically, and how the framework can be used to effectively verify safety of Java programs.

SUMMARY For real‐time and embedded systems, limiting the consumption of time and memory resources is often an important part of the requirements. Being able to predict bounds on the consumption of such resources during the development process of the code can be of great value. In this paper, we focus mainly on memory‐related bounds. Recent research results have advanced the state of the art of resource consumption analysis. In this paper, we present a toolset that makes it possible to apply these research results in practice for (real‐time) systems enabling JAVA developers to analyse symbolic loop bounds, symbolic bounds on heap size and both symbolic and numeric bounds on stack size. We describe which theoretical additions were needed in order to achieve this. We give an overview of the capabilities of the RESANA (Radboud University Nijmegen, The Netherlands) toolset that is the result of this effort. The toolset can not only perform generally applicable analyses, but it also contains a part of the analysis that is dedicated to the developers' (real‐time) virtual machine, such that the results apply directly to the actual development environment that is used in practice. Copyright © 2013 John Wiley & Sons, Ltd.