The shift to cloud-based APIs has made application security critically depend on understanding and reasoning about policies that regulate access to cloud resources.We present stratified predicate abstraction, a new approach that summarizes complex security policies into a compact set of positive and declarative statements that precisely state who has access to a resource.We have implemented stratified abstraction and deployed it as the engine powering AWS's IAM Access Analyzer service, and hence, demonstrate how formal methods and SMT can be used for security policy explanation.

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.

In this paper we describe symbolic side-channel analysis techniques for detecting and quantifying information leakage, given in terms of Shannon and min-entropy. Measuring the precise leakage is challenging due to the randomness and noise often present in program executions and side-channel observations. We account for this noise by introducing additional (symbolic) program inputs which are interpreted probabilistically, using symbolic execution with parametrized model counting. We also explore a sampling approach for increased scalability. In contrast to typical Monte Carlo techniques, our approach works by sampling symbolic paths, representing multiple concrete paths, and uses pruning to accelerate computation and guarantee convergence to the optimal results. A key novelty of our approach is to provide bounds on the leakage that are provably under- and over-approximating the exact leakage. We implemented the techniques in the Symbolic PathFinder tool and demonstrate them on Java programs.

Cloud computing provides on-demand access to IT resources via the Internet. Permissions for these resources are defined by expressive access control policies. This paper presents a formalization of the Amazon Web Services (AWS) policy language and a corresponding analysis tool, called ZELKOVA, for verifying policy properties. ZELKOVA encodes the semantics of policies into SMT, compares behaviors, and verifies properties. It provides users a sound mechanism to detect misconfigurations of their policies. ZELKOVA solves a PSPACE-complete problem and is invoked many millions of times daily.

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.

Summary We present HVMTP, a time predictable and portable Java virtual machine (JVM) implementation with applications in resource‐constrained, hard real‐time embedded systems, which implements all levels of the safety critical Java (SCJ) specification. Time predictability is achieved by a combination of time‐predictable algorithms, exploiting the programming model of the SCJ profile and harnessing static knowledge of the hosted SCJ system. This paper presents HVMTPin terms of its design and capabilities and demonstrates how a complete timing model of the JVM represented as a network of timed automata can be obtained using the tool TETASARTSJVM. The timing model readily integrates with the rest of the TETASARTS tool set for temporal verification of SCJ systems. We will also show how a complete timing scheme in terms of safe worst‐case execution times and best‐case execution times of the Java bytecodes can be derived from the model. Furthermore, we take a first look at how to support the new Java 8 language feature of Lambda expressions in a SCJ context – we look in particular at how theinvokedynamicbytecode can be implemented in a time‐predictable way and integrated in HVMTP. Copyright © 2016 John Wiley & Sons, Ltd.

Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.