Software testing techniques like symbolic execution face significant challenges with path explosion. Asymptotic Path Complexity (APC) quantifies this path explosion complexity, but existing APC methods do not work for interprocedural functions in general. Our new algorithm, APC-IP, efficiently computes APC for a wider range of functions, including interprocedural ones, improving over previous methods in both speed and scope. We implement APC-IP atop the existing software Metrinome, and test it against a benchmark of C functions, comparing it to existing and baseline approaches as well as comparing it to the path explosion of the symbolic execution engine Klee. The results show that APC-IP not only aligns with previous APC values but also excels in performance, scalability, and handling complex source code. It also provides a complexity prediction of the number of paths explored by Klee, extending the APC metric's applicability and surpassing previous implementations.

Undergraduate computer science programs have increasingly adopted introductory sequences with multiple entry points in order to accommodate students arriving with varying degrees of prior experience. This paper examines student experiences at the critical stage when multiple introductory tracks merge: the convergence course. We find that students from all tracks arrive with similar levels of enthusiasm and positive attitudes towards collaborative learning. By the end of the convergence course, group differences in self-efficacy and a sense of belonging in the CS community have begun to ease. Importantly, students with the least pre-college CS experience enjoy the most significant gains in self-efficacy. However, curricular techniques intended to integrate these student populations appear insufficient alone to close the achievement gap between these groups, suggesting that alternate approaches may be necessary to supplement.

We describe our work on the relationship between the asymptotic path complexity of a program, time-to-completion, subjective complexity, correctness performance, and levels of brain (de)activation in select Brodmann areas of the brain, as measured by fMRI, while a human subject attempts to understand the source code of a program. Asymptotic path complexity gives an asymptotic upper bound on how quickly the number of paths through a program grows with increasing execution depth. (De)activation levels in the studied Brodmann areas of the brain are known to correlate with different specific types of cognitive effort. We add the asymptotic path complexity metric to an existing fMRI-code-comprehension data set that compares common code metrics to cognitive effort. Our results show that, according to Kendall rank correlation, asymptotic path complexity has (1) better correlation than all other metrics with code comprehension task completion time, (2) better correlation than all other metrics with subjective participant complexity, (3) better correlation than all other metrics for brain areas responsible for semantic processing, (4) correlations comparable to lines of code and Halstead complexity, and better correlation than (McCabe’s) cyclomatic complexity and dependency degree for participant response correctness and for (de)activation levels in brain areas responsible for rational thought and extracting signal from noise, and, finally, (5) worse correlation than all metrics (except McCabe’s cyclomatic complexity) for brain areas responsible for motion plandisse, language and audio processing, and additional forms of semantic processing. Overall, our results indicate that path complexity is a useful metric for measuring many aspects of code comprehension effort.

Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.

Model counting procedures for data structures are crucial for advancing the field of automated quantitative program analysis. We present a tool for Model Counting for Bounded Array Theory (MCBAT). MCBAT works on quantified integer array constraints in which all arrays have a finite length. We employ reductions from the theory of arrays to uninterpreted functions and linear integer arithmetic (LIA). Once reduced to LIA, we leverage Barvinok's polynomial time integer lattice point enumeration algorithm. Finally, we present a case study demonstrating applicability to automated quantitative program analysis. MCBAT is available for immediate use as a Docker image and the source code is freely available in our Github repository.

We present an automated technique for synthesizing adaptive attacks to extract information from program functions that leak secret data through a side channel. We synthesize attack steps dynamically and consider noisy program environments. Our approach consists of an offline profiling phase using symbolic execution, witness generation, and profiling to construct a noise model. During our online attack synthesis phase, we use weighted model counting and numeric optimization to automatically synthesize attack inputs. We experimentally evaluate the effectiveness of our approach on DARPA benchmark programs created for testing side-channel analysis techniques.

Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint within the bound. We present a parameterized model counting constraint solver for string and numeric constraints. We first construct a multi-track deterministic finite state automaton that accepts all solutions to the given constraint. We limit the numeric constraints to linear integer arithmetic, and for non-regular string constraints we over-approximate the solution set. Counting the number of accepting paths in the generated automaton solves the model counting problem. Our approach is parameterized in the sense that, we do not assume a finite domain size during automata construction, resulting in a potentially infinite set of solutions, and our model counting approach works for arbitrarily large bounds. We experimentally demonstrate the effectiveness of our approach on a large set of string and numeric constraints extracted from software applications. We experimentally compare our tool to five existing model counting constraint solvers for string and numeric constraints and demonstrate that our tool is as efficient and as or more precise than other solvers. Moreover, our tool can handle mixed constraints with string and integer variables that no other tool can.

We present symbolic analysis techniques for detecting vulnerabilities that are due to adaptive side-channel attacks, and synthesizing inputs that exploit the identified vulnerabilities. We start with a symbolic attack model that encodes succinctly all the side-channel attacks that an adversary can make. Using symbolic execution over this model, we generate a set of mathematical constraints, where each constraint characterizes the set of secret values that lead to the same sequence of side-channel measurements. We then compute the optimal attack, i.e, the attack that yields maximum leakage over the secret, by solving an optimization problem over the computed constraints. We use information-theoretic concepts such as channel capacity and Shannon entropy to quantify the leakage over multiple runs in the attack, where the measurements over the side channels form the observations that an adversary can use to try to infer the secret. We also propose greedy heuristics that generate the attack by exploring a portion of the symbolic attack model in each step. We implemented the techniques in Symbolic PathFinder and applied them to Java programs encoding web services, string manipulations and cryptographic functions, demonstrating how to synthesize optimal side-channel attacks.

We present an automated approach for detecting and quantifying side channels in Java programs, which uses symbolic execution, string analysis and model counting to compute information leakage for a single run of a program. We further extend this approach to compute information leakage for multiple runs for a type of side channels called segmented oracles, where the attacker is able to explore each segment of a secret (for example each character of a password) independently. We present an efficient technique for segmented oracles that computes information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. Our implementation uses the symbolic execution tool Symbolic PathFinder (SPF), SMT solver Z3, and two model counting constraint solvers LattE and ABC. Although LattE has been used before for analyzing numeric constraints, in this paper, we present an approach for using LattE for analyzing string constraints. We also extend the string constraint solver ABC for analysis of both numeric and string constraints, and we integrate ABC in SPF, enabling quantitative symbolic string analysis.

Recent automated software testing techniques concentrate on achieving path coverage. We present a complexity measure that provides an upper bound for the number of paths in a program, and hence, can be used for assessing the difficulty of achieving path coverage for a given method. We define the path complexity of a program as a function that takes a depth bound as input and returns the number of paths in the control flow graph that are within that bound. We show how to automatically compute the path complexity function in closed form, and the asymptotic path complexity which identifies the dominant term in the path complexity function. Our results demonstrate that path complexity can be computed efficiently, and it is a better complexity measure for path coverage compared to cyclomatic complexity and NPATH complexity.