Algorithmic Complexity Vulnerabilities (ACV) are a class of vulnerabilities that enable Denial of Service Attacks. ACVs stem from asymmetric consumption of resources due to complex loop termination logic, recursion, and/or resource intensive library APIs. Completely automated detection of ACVs is intractable and it calls for tools that assist human analysts.

Build systems are crucial for software system development, however there is a lack of tool support to help with their high maintenance overhead. GNU Autotools are widely used in the open source community, but users face various challenges from its hard to comprehend nature and staging of multiple code generation steps, often leading to low quality and error-prone build code. In this paper, we present a platform, AutoHaven, to provide a foundation for developers to create analysis tools to help them understand, maintain, and migrate their GNU Autotools build systems. Internally it uses approximate parsing and symbolic analysis of the build logic. We illustrate the use of the platform with two tools: ACSense helps developers to better understand their build systems and ACSniff detects build smells to improve build code quality. Our evaluation shows that AutoHaven can support most GNU Autotools build systems and can detect build smells in the wild.

Immutability analysis is important to software testing, verification and validation (V&V) because it can be used to identify independently testable functions without side-effects. Existing tools for immutability analysis are largely academic prototypes that have not been rigorously tested for accuracy or have not been maintained and are unable to analyze programs written in later versions of Java. In this paper, we re-implement two prominent approaches to inferring the immutability of an object: one that leverages a points-to analysis and another that uses a type-system. In addition to supporting Java 8 source programs, our re-implementations support the analysis of compiled Java bytecode. In order to evaluate the relative accuracy, we create a benchmark that rigorously tests the accuracy boundaries of the respective approaches. We report results of experiments on analyzing the benchmark with the two approaches and compare their scalability to real world applications. Our results from the benchmark reveal that points-to based approach is more accurate than the type inference based approach in certain cases. However, experiments with real world applications show that the points-to based approach does not scale well to very large applications and a type inference based approach may offer a scalable alternative.

Detecting zero-day sophisticated malware is like searching for a needle in the haystack, not knowing what the needle looks like. This paper describes Android Malicious Flow Visualization Toolbox that empowers a human analyst to detect such malware. Detecting sophisticated malware requires systematic exploration of the code to identify potentially malignant code, conceiving plausible malware hypotheses, and gathering evidence from the code to prove or refute each hypothesis. We describe interactive visualizations of program artifacts to understand and analyze complex Android semantics used by an app. The toolbox incorporates visualization capabilities that work together cohesively, and provides a mechanism to easily add new capabilities. We present case studies of detecting Android malware with confidentiality and integrity breaches. We report the accuracy and efficiency achieved by our team of analysts by using the toolbox, while auditing 77 sophisticated Android apps provided by Defense Advanced Research Projects Agency (DARPA). Toolbox URL·: https://kcsl.github.io/AMFVT/.

The goal of path-sensitive analysis (PSA) is to achieve accuracy by accounting precisely for the execution behavior along each path of a control flow graph (CFG). A practical adoption of PSA is hampered by two roadblocks: (a) the exponential growth of the number of CFG paths, and (b) the exponential complexity of a path feasibility check. We introduce projected control graph (PCG) as an optimal mathematical abstraction to address these roadblocks.The PCG follows from the simple observation that for any given analysis problem, the number of distinct relevant execution behaviors may be much smaller than the number of CFG paths. The PCG is a projection of the CFG to retain only the relevant execution behaviors and elide duplicate paths with identical execution behavior. A mathematical definition of PCG and an efficient algorithm to transform CFG to PCG are presented. We present an empirical study for three major versions of the Linux kernel to assess the practical benefit of using the optimal mathematical abstraction. As a measure of the efficiency gain, the study reports the reduction from CFG to PCG graphs for all relevant functions for pairing Lock and Unlock on all feasible execution paths. We built a tool to compute these graphs for 66,609 Lock instances. The CFG and PCG graphs with their source correspondence are posted on a website. We used these PCG graphs in a classroom project to audit the results of Lock and Unlock pairing done by the Linux Driver Verification (LDV) tool, the top-rated formal verification tool for the Linux kernel. Our audit has revealed complex Linux bugs missed by LDV.

Invisible Control Flow (ICF) results from dynamic binding and asynchronous processing. For modern software replete with ICF, the ability to analyze and resolve ICF is crucial for verifying software. A fully automated analysis to resolve ICF suffers from imprecision and high computational complexity. As a practical alternative, we present a novel solution of interactive human-machine collaboration to resolve ICF. Our approach is comprised of interactive program analysis and comprehension to systematically capture and link the clues crucial for resolving ICF. We present the tool support we have developed using the query language and visualization capabilities of the Atlas Platform. We illustrate the approach using examples where resolving ICF is crucial to verify software and show a complex bug in the Linux kernel discovered by resolving ICF.

Algorithmic Complexity (AC) vulnerabilities can be exploited to cause a denial of service attack. Specifically, an adversary can design an input to trigger excessive (space/time) resource consumption. It is not possible to build a fully automated tool to detect AC vulnerabilities. Since it is an open-ended problem, a human-in-loop exploration is required to find the program loops that could have AC vulnerabilities. Ascertaining whether an arbitrary loop has an AC vulnerability is itself difficult, which is equivalent to the halting problem. This paper is about a pragmatic engineering approach to detect AC vulnerabilities. It presents a statically-informed dynamic (SID) analysis and two tools that provide critical capabilities for detecting AC vulnerabilities. The first is a static analysis tool for exploring the software to find loops as the potential candidates for AC vulnerabilities. The second is a dynamic analysis tool that can try many different inputs to evaluate the selected loops for excessive resource consumption. The two tools are built and integrated together using the interactive software analysis, transformation, and visualization capabilities provided by the Atlas platform. The paper describes two use cases for the tools, one to detect AC vulnerabilities in Java bytecode and another for students in an undergraduate algorithm class to perform experiments to learn different aspects of algorithmic complexity Tool and Demo Video: https://ensoftcorp.github.io/SID.

This paper presents a demo of our Security Toolbox to detect novel malware in Android apps. This Toolbox is developed through our recent research project funded by the DARPA Automated Program Analysis for Cybersecurity (APAC) project. The adversarial challenge ("Red") teams in the DARPA APAC program are tasked with designing sophisticated malware to test the bounds of malware detection technology being developed by the research and development ("Blue") teams. Our research group, a Blue team in the DARPA APAC program, proposed a "human-in-the-loop program analysis" approach to detect malware given the source or Java bytecode for an Android app. Our malware detection apparatus consists of two components: a general-purpose program analysis platform called Atlas, and a Security Toolbox built on the Atlas platform. This paper describes the major design goals, the Toolbox components to achieve the goals, and the workflow for auditing Android apps. The accompanying video illustrates features of the Toolbox through a live audit.

Automated static analysis tools are widely used in identifying software anomalies, such as memory leak, unsafe thread synchronization and malicious behaviors in smartphone applications. Such anomaly-prone scenarios can be bifurcated into: “ordinary” (analysis requires relatively simple automation) and “complex” (analysis poses extraordinary automation challenges). While automated static analysis tools can resolve ordinary scenarios with high accuracy, automating the analysis of complex scenarios can be very challenging and, at times, infeasible. Even when feasible the cost for full automation can be exorbitant: either in implementing the automation or in sifting through the large number of erroneous results manually. Instead, we appeal for a “Human-in-the-loop” approach called “Amplified Reasoning Technique” (ART). While some of the existing approaches do involve human in the analysis process, the roles played by man and machine are mainly segregated. Whereas, ART puts man and machine in a “loop” in an interactive and visualization-based fashion. This paper makes an attempt to convince its readers to make their analysis of software anomalies ART-based by presenting real-world case studies of complex anomalies and how an ART based approach can be very effective in resolving them. The case studies highlight the desired characteristics of an ART based tool and the type of role it plays in amplifying human intelligence.

Expressed sequence tags, abbreviated as ESTs, are DNA molecules experimentally derived from expressed portions of genes. Clustering of ESTs is essential for gene recognition and for understanding important genetic variations such as those resulting in diseases. We present the algorithmic foundations and implementation of PaCE, a parallel software system we developed for large-scale EST clustering. The novel features of our approach include 1) design of space-efficient algorithms to limit the space required to linear in the size of the input data set, 2) a combination of algorithmic techniques to reduce the total work without sacrificing the quality of EST clustering, and 3) use of parallel processing to reduce runtime and facilitate clustering of large data sets. Using a combination of these techniques, we report the clustering of 327,632 rat ESTs in 47 minutes, and 420,694 Triticum aestivum ESTs in 3 hours and 15 minutes, using a 60-processor IBM xSeries cluster. These problems are well beyond the capabilities of state-of-the-art sequential software. We also present thorough experimental evaluation of our software including quality assessment using benchmark Arabidopsis EST data.

Expressed sequence tags, ESTs, are DNA molecules experimentally derived from expressed portions of genes. Clustering of ESTs is essential for gene recognition and understanding important genetic variations such as those resulting in diseases. In this paper, we present the design and development of a parallel software system for EST clustering. To our knowledge, this is the first such effort to address the problem of EST clustering in parallel. The novel features of our approach include 1) design of space efficient algorithms to keep the space requirement linear in the size of the input data set, 2) a combination of algorithmic techniques to reduce the total work without sacrificing the quality of EST clustering, and 3) use of parallel processing to reduce the run-time and facilitate the clustering of large datasets. Using a combination of these techniques, we report the clustering of 81,414 Arabidopsis ESTs in under 2.5 minutes on a 64-processor IBM SP, a problem that is estimated to take 9 hours of run-time with a state-of-the-art software, provided the memory required to run the software can be made available.

A performance evaluation metric called CMP scalability is introduced This metric is useful in analyzing performance of a parallel algorithm as the number of processors grows but the memory size per processor is fixed. The CMP scalability metric is derived for the parallel Matrix Multiplication (MM). Gauss Jordan Elimination (GJE), and Fast Fourier Transform (FFT). These examples show that the CMP scalability metric and the isoefficiency metric really address different aspects of scalability and could lead to very different conclusions. According to the CMP scalability analysis FFT is more scalable than GJE. Interestingly, conclusions drawn from the isoefficiency analysis are quite the opposite. The CMP scalability metric, and so also the isoefficiency metric, is a function indicating the asymptotic behavior as the number of processors becomes large. However, the CMP analysis can also help to analyze the performance of an algorithm on a given architecture with a limited number of processors. We present such an analysis of the three algorithms on a 16K processor MasPar MP-1 machine.

An iterative learning algorithm called PRLAB is described for the discrete bidirectional associative memory (BAM). Guaranteed recall of all training pairs is ensured by PRLAB. The proposed algorithm is significant in many ways. Unlike many existing iterative learning algorithms, PRLAB is not based on the gradient descent technique. It is a novel adaptation from the well-known relaxation method for solving a system of linear inequalities. The algorithm is very fast. Learning 200 random patterns in a 200-200 BAM takes only 20 epochs on the average. PRLAB is highly insensitive to learning parameters and the initial configuration of a BAM. It also offers high scalability for large applications by providing the same high performance when the number of training patterns are increased in proportion to the size of the BAM. An extensive performance analysis of the new learning algorithm is included.

The problem of calculating the combinatorial power of certain SW-banyan networks is related to a problem of enumerating certain matrices. Examples of two- and three-stage networks are used to demonstrate the technique. In each case, a polynomial-time algorithm is found to solve the problem. The results are presented for each case and certain asymptotic behavior is noted.>

This paper closely examines the performance analysis for unbuffered multipath multistage interconnection networks. A critical discussion of commonly used analysis is provided to identify a basic flaw in the model. A new analysis based on the grouping of alternate links is proposed as an alternative to rectify the error. The results based on the new analysis and extensive simulation are presented for three representative networks. The simulation study strongly supports the results of the new analysis.

The design of the Gamma network is analyzed in terms of block structure. The analysis reveals the asymmetry of its duplicate links, and an alternate design in the form of the Kappa network is proposed. Its novel feature is the symmetry of duplicate links at the block level. This symmetry results in a simple control algorithm and enhanced fault tolerance. The relationship between the Kappa network and other existing fault-tolerant networks is briefly discussed.>