Complexity vulnerability analysis using symbolic execution. (6th February 2020)

• Record Type: Journal Article
• Authors: Luckow, Kasper; Kersten, Rody; Pasareanu, Corina
• Other Names: Schieferdecker Ina guestEditor.; Memon Atif guestEditor.; Washizaki Hironori guestEditor.
• Is Part Of: Software testing, verification & reliability. Volume 30:Number 7/8(2020)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2020-02-06
• Subjects: complexity analysis -- guided exploration -- machine learning -- symbolic execution; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1716
• Languages: English
• ISSNs: 0960-0833

Abstract

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. Abstract : We describe analysis techniques based on symbolic execution that use guided exploration to compute bounds on the worst‐case complexity of programs and to generate test values that can exercise the worst case behavior. The techniques have found vulnerabilities in realistic software that are due to algorithmic complexity.