Software bloat has negative implications for security, reliability, and performance. To counter bloat, we proposeTrimmer, a static analysis-based system for pruning unused functionality.Trimmerremoves code that is unused with respect to user-provided command-line arguments and application-specific configuration files.Trimmeruses concrete memory tracking and a custom inter-procedural constant propagation analysis that facilitates dead code elimination. Our system supports both context-sensitive and context-insensitive constant propagation. We show that context-sensitive constant propagation is important for effective software pruning in most applications. We introducesparse constant propagationthat performs constant propagation only for configuration-hosting variables and show that it performs better (higher code size reductions) compared to constant propagation for all program variables. Overall, our results show thatTrimmerreduces binary sizes for real-world programs with reasonable analysis times. Across 20 evaluated programs, we observe a mean binary size reduction of 22.7 percent and a maximum reduction of 62.7 percent. For 5 programs, we observe performance speedups ranging from 5 to 53 percent. Moreover, we show that winnowing software applications can reduce the program attack surface by removing code that contains exploitable vulnerabilities. We find that debloating usingTrimmerremoves CVEs in 4 applications.

We present the design and evaluation of a 3.5-year embedded sensing deployment at the Mithræum of Circus Maximus, a UNESCO-protected underground archaeological site in Rome (Italy). Unique to our work is the use of energy harvesting through thermal and kinetic energy sources. The extreme scarcity and erratic availability of energy, however, pose great challenges in system software, embedded hardware, and energy management. We tackle them by testing, for the first time in a multi-year deployment, existing solutions in intermittent computing, low-power hardware, and energy harvesting. Through three major design iterations, we find that these solutions operate as isolated silos and lack integration into a complete system, performing suboptimally. In contrast, we demonstrate the efficient performance of a hardware/software co-design featuring accurate energy management and capturing the coupling between energy sources and sensed quantities. Installing a battery-operated system alongside also allows us to perform a comparative study of energy harvesting in a demanding setting. Albeit the latter reduces energy availability and thus lowers the data yield to about 22% of that provided by batteries, our system provides a comparable level of insight into environmental conditions and structural health of the site. Further, unlike existing energy-harvesting deployments that are limited to a few months of operation in the best cases, our system runs with zero maintenance since almost 2 years, including 3 months of site inaccessibility due to a COVID19 lockdown.

Intermittently powered embedded devices ensure forward progress of programs through state checkpointing in non-volatile memory. Checkpointing is, however, expensive in energy and adds to the execution times. To minimize this overhead, we present DICE, a system that renders differential checkpointing profitable on these devices. DICE is unique because it is a software-only technique and efficient because it only operates in volatile main memory to evaluate the differential. DICE may be integrated with reactive (Hibernus) or proactive (MementOS, HarvOS) checkpointing systems, and arbitrary code can be enabled with DICE using automatic code-instrumentation requiring no additional programmer effort. By reducing the cost of checkpoints, DICE cuts the peak energy demand of these devices, allowing operation with energy buffers that are one-eighth of the size originally required, thus leading to benefits such as smaller device footprints and faster recharging to operational voltage level. The impact on final performance is striking: with DICE, Hibernus requires one order of magnitude fewer checkpoints and one order of magnitude shorter time to complete a workload in real-world settings.

Transiently powered computers (TPCs) form the foundation of the battery-less Internet of Things, using energy harvesting and small capacitors to power their operation. This kind of power supply is characterized by extreme variations in supply voltage, as capacitors charge when harvesting energy and discharge when computing. We experimentally find that these variations cause marked fluctuations in clock speed and power consumption . Such a deceptively minor observation is overlooked in existing literature. Systems are thus designed and parameterized in overly conservative ways, missing on a number of optimizations. We rather demonstrate that it is possible to accurately model and concretely capitalize on these fluctuations. We derive an energy model as a function of supply voltage and prove its use in two settings. First, we develop EPIC, a compile-time energy analysis tool. We use it to substitute for the constant power assumption in existing analysis techniques, giving programmers accurate information on worst-case energy consumption of programs. When using EPIC with existing TPC system support, run-time energy efficiency drastically improves, eventually leading up to a 350% speedup in the time to complete a fixed workload. Further, when using EPIC with existing debugging tools, it avoids unnecessary program changes that hurt energy efficiency. Next, we extend the MSPsim emulator and explore its use in parameterizing a different TPC system support. The improvements in energy efficiency yield up to more than 1000% time speedup to complete a fixed workload.

Embedded devices running on ambient energy perform computations intermittently, depending upon energy availability. System support ensures forward progress of programs through state checkpointing in non-volatile memory. Checkpointing is, however, expensive in energy and adds to execution times. To reduce this overhead, we present DICE, a system design that efficiently achieves differential checkpointing in intermittent computing. Distinctive traits of DICE are its software-only nature and its ability to only operate in volatile main memory to determine differentials. DICE works with arbitrary programs using automatic code instrumentation, thus requiring no programmer intervention, and can be integrated with both reactive (Hibernus) or proactive (MementOS, HarvOS) checkpointing systems. By reducing the cost of checkpoints, performance markedly improves. For example, using DICE, Hibernus requires one order of magnitude shorter time to complete a fixed workload in real-world settings.

Transiently-powered computers (TPCs) lay the basis for a battery-less Internet of Things, using energy harvesting and small capacitors to power their operation. This power supply is characterized by extreme variations in supply voltage, as capacitors charge when harvesting energy and discharge when computing. We experimentally find that these variations cause marked fluctuations in clock speed and power consumption, which determine energy efficiency. We demonstrate that it is possible to accurately model and concretely capitalize on these fluctuations. We derive an energy model as a function of supply voltage and develop EPIC, a compile-time energy analysis tool. We use EPIC to substitute for the constant power assumption in existing analysis techniques, giving programmers accurate information on worst-case energy consumption of programs. When using EPIC with existing TPC system support, run-time energy efficiency drastically improves, eventually leading up to a 350% speedup in the time to complete a fixed workload. Further, when using EPIC with existing debugging tools, programmers avoid unnecessary program changes that hurt energy efficiency.

The resource-constrained devices of the battery-less Internet of Things are powered off energy harvesting and compute intermittently, as energy is available. Forward progress of programs is ensured by creating persistent state. Mixed-volatile platforms are thus an asset, as they map slices of the address space onto non-volatile memory. However, these platforms also possibly introduce intermittence bugs, where intermittent and continuous executions differ.

Energy harvesting enables battery-less sensing applications, but causes executions to become intermittent as a result of erratic energy provisioning. Intermittent executions pose challenges to peripheral consistency that threaten to leave peripheral-bound workloads in failed states or to impede forward progress of programs. Intermittent synchronous peripheral operations are supported in existing literature for specific kinds of peripherals. Asynchronous peripheral operations enable reactive concurrency in application implementations, which increases reactivity and improves energy consumption, but lack dedicated support in intermittent settings. We present Karma, the first general abstraction and system design to support both synchronous and asynchronous operations in an intermittent setting. Karma employs a novel combination of peripheral roll-forward and computation roll-back to a rendezvous point guaranteeing consistency. It remains transparent to application programmers and peripheral driver, which favours portability. Our evaluation, based on three applications running on prototype hardware and using diverse energy sources, indicates that intermittent asynchronous peripheral support provided by Karma boosts data throughput by 83% compared to existing literature.

Generation of complex heap structures is required for many software testing and verification techniques, which are used to enhance software reliability. It enables them to work for programs dependent on such structures. Generating all the valid structures within a size bound is time-consuming, and it is hard to predict an input size completely generatable within a time bound. This is due to the depth-first traversal of the candidate space. However, an efficient breadth-first traversal requires a compact state encoding to store candidates for exploration in the next level. In this paper, we present present a novel state encoding technique that stores an incomplete representation of state that can be recovered during search. We build upon the Korat algorithm-demonstrated to effectively generate tests and find bugs for many software programs-and present iKorat, an incremental algorithm for breadth-first exploration of the search space. Our encoding enables a more efficient implementation of iterative deepening that avoids redundant work. Standard iterative deepening algorithms allow a breadth-first search when the underlying algorithm is depth-first by repeating the work of earlier iterations. iKorat, however, uses information from smaller sizes to avoid redundant work for larger sizes. It also enables a new technique for parallelizing Korat by communicating candidates using our encoding. piKorat generates structures of larger sizes in parallel as soon as incremental information is available from smaller sizes. Our evaluation shows that iKorat-based iterative deepening is more efficient than Korat and that piKorat naturally extends the technique for parallel generation of complex structures.

We propose a set of differential techniques to allow transientlypowered embedded devices reduce the amount of data written on non-volatile memory during checkpoints used to cross times of energy unavailability. These techniques track modifications in the application state to isolate data from the slice of the previous checkpoint that remains unaltered. At the following checkpoint, our approach may thus only update the parts it detects as modified. This allows us to shift part of the energy budget from checkpointing overhead to useful computations, yielding better overall energy efficiency.

Parallel and distributed computing have enabled development of much more scalable software. However, developing concurrent software requires the programmer to be aware of nondeterminism, data races, and deadlocks. MPI (message passing interface) is a popular standard for writing message-oriented distributed applications. Some messages in MPI systems can be processed by one of the many machines and in many possible orders. This non-determinism can affect the result of an MPI application. The alternate results may or may not be correct. To verify MPI applications, we need to check all these possible orderings and use an application specific oracle to decide if these orderings give correct output. MPJ Express is an open source Java implementation of the MPI standard. Model checking of MPI Java programs is a challenging task due to their parallel nature. We developed a Java based model of MPJ Express, where processes are modeled as threads, and which can run unmodified MPI Java programs on a single system. This model enabled us to adapt the Java PathFinder explicit state software model checker (JPF) using a custom listener to verify our model running real MPI Java programs. The evaluation of our approach shows that model checking reveals incorrect system behavior that results in very intricate message orderings.

Distributed applications, in particular web applications, often depend on a centralized database. The results of database operations depend on the state of database at that time and often also on the order of execution of operations performed by concurrent clients. Verification of such applications requires modeling all these possible orders so that the user can determine which are incorrect orderings and can prevent them with transactions or business logic. However, straightforward exploration leads to state space explosion. Partial order reduction prunes orderings that are equivalent to other orderings already explored. We present a novel technique of Effective Partial Order Reduction (EPOR) for model checking software of Java applications sharing database state. EPOR improves upon prior work by performing a more precise analysis and supports many more operations. The key idea behind EPOR is that monitoring the effect of database operations inside database implementation gives a more precise view of operation dependencies than what can be achieved from an external view. Like prior work, EPOR also relies on Java Pathfinder model checker for model checking Java application. However, unlike prior work, there is additional instrumentation inside the database that enables our precise analysis and allows supporting more constructs. Our results improve upon prior work by achieving significant reduction in number of states explored and thus enables more effective model checking of database applications with concurrent operations.

Stored procedures in database management systems are often used to implement complex business logic. Correctness of these procedures is critical for correct working of the system. However, testing them remains difficult due to many possible states of data and database constraints. This leads to mostly manual testing. Newer tools offer automated execution for unit testing of stored procedures but the test cases are still written manually.

Development of concurrent software requires the programmer to be aware of non-determinism, data races, and deadlocks. MPI (message passing interface) is a popular standard for writing message oriented distributed applications. Some messages in MPI systems can be processed by one of the many machines and in many possible orders. This non-determinism can affect the result of an MPI application. The alternate results may or may not be correct. To verify MPI applications, we need to check all these possible orderings and use an application specific oracle to decide if these orderings give correct output. MPJ Express is an open source Java implementation of the MPI standard. We developed a Java based model of MPJ Express, where processes are modeled as threads, and which can run unmodified MPI Java programs on a single system. This enabled us to adapt the Java PathFinder explicit state software model checker (JPF) using a custom listener to verify our model running real MPI Java programs. We evaluated our approach using small examples where model checking revealed message orders that would result in incorrect system behavior.

We propose incremental checkpointing techniques enabling transiently powered devices to retain computational state across multiple activation cycles. As opposed to the existing approaches, which checkpoint complete program state, the proposed techniques keep track of modified RAM locations to incrementally update the retained state in secondary memory, significantly reducing checkpointing overhead both in terms of time and energy.

Scaling software analysis techniques based on source-code, such as symbolic execution and data flow analyses, remains a challenging problem for systematically checking software systems. In this work, we aim to efficiently apply symbolic execution in increments based on versions of code. Our technique is based entirely on dynamic analysis and patches completely automated test suites based on the code changes. Our key insight is that we can eliminate constraint solving for unchanged code by checking constraints using the test suite of a previous version. Checking constraints is orders of magnitude faster than solving them. This is in contrast to previous techniques that rely on inexact static analysis or cache of previously solved constraints. Our technique identifies ranges of paths, each bounded by two concrete tests from the previous test suite. Exploring these path ranges covers all paths affected by code changes up to a given depth bound. Our experiments show that incremental symbolic execution based on dynamic analysis is an order of magnitude faster than running complete standard symbolic execution on the new version of code.

We present a novel approach for parallel analysis of models written in Alloy, a declarative extension of first-order logic based on relations. The Alloy language is supported by the fully automatic Alloy Analyzer, which translates models into propositional formulas and uses off-the-shelf SAT technology to solve them. Our key insight is that the underlying constraint satisfaction problem can be split into subproblems of lesser complexity by using ranges of candidate solutions, which partition the space of all candidate solutions. Conceptually, we define a total ordering among the candidate solutions, split this space of candidates into ranges, and let independent SAT searches take place within these ranges' endpoints. Our tool, Ranger, embodies our insight. Experimental evaluation shows that Ranger provides substantial speedups (in several cases, superlinear ones) for a variety of hard-to-solve Alloy models, and that adding more hardware reduces analysis costs almost linearly.

Constraint-based testing is a methodology for finding bugs in code, which has been successfully used for testing real systems. A key element of the methodology is generation of test inputs from input constraints, i.e., properties of desired inputs, which is performed by solving the constraints. We present a novel approach to optimize input generation from imperative constraints, i.e., constraints written as predicates in an imperative language. A well known technique for solving such constraints is execution-driven monitoring, where the given predicate is executed on candidate inputs to filter and prune invalid inputs, and generate valid ones. Our insight is that a lightweight static data-flow analysis of the given imperative constraint can enable more efficient solving. This paper describes an approach that embodies our insight and evaluates it using a suite of well-studied subject constraints. The experimental results show our approach provides substantial speedup over previous work.

This paper introduces a novel approach to scale symbolic execution --- a program analysis technique for systematic exploration of bounded execution paths---for test input generation. While the foundations of symbolic execution were developed over three decades ago, recent years have seen a real resurgence of the technique, specifically for systematic bug finding. However, scaling symbolic execution remains a primary technical challenge due to the inherent complexity of the path-based exploration that lies at core of the technique.

Developers have used data structure repair over the last few decades as an effective means to recover on-the-fly from errors in program state. Traditional repair techniques were based on dedicated repair routines, whereas more recent techniques have used invariants that describe desired structural properties as the basis for repair. All repair techniques are designed with one primary goal: run-time error recovery. However, the actions that any such technique performs to repair an erroneous program state are meant to produce the effect of the actions of a (hypothetical) correct program. The key insight in this paper is that repair actions on the program state can guide debugging of code (when the erroneous program execution is due to a fault in the program and not an external event).This paper presents an approach that abstracts concrete repair actions that a routine performs to repair an erroneous state into a sequence of program statements that perform the same actions using variables visible in the scope of the faulty code. Thus, appending the generated statements to the original code is akin to performing the repair from within the program. Our implementation uses the Juzi data structure repair tool as an enabling technology. Experimental results using a library data structure as well as two applications demonstrate the effectiveness of our approach in enabling repair of faulty code.

Constraint solving lies at the heart of several specification-based approaches to automated testing. Korat is a previously developed algorithm for solving constraints in Java programs. Given a Java predicate that represents the desired constraints and a bound on the input size, Korat systematically explores the bounded input space of the predicate and enumerates inputs that satisfy the constraint. Korat search is largely sequential: it considers one candidate input in each iteration and it prunes the search space based on the candidates considered. This paper presents PKorat, a new parallel algorithm that parallelizes the Korat search. PKorat explores the same state space as Korat but considers several candidates in each iteration. These candidates are distributed among parallel workers resulting in an efficient parallel version of Korat. Experimental results using complex structural constraints from a variety of subject programs show significant speedups over the traditional Korat search.

Several static analysis techniques, e.g., symbolic execution or scope-bounded checking, as well as dynamic analysis techniques, e.g., specification-based testing, use constraint solvers as an enabling technology. To analyze code that manipulates structurally complex data, the underlying solver must support structural constraints. Solving such constraints can be expensive due to the large number of aliasing possibilities that the solver must consider. This paper presents a novel technique to selectively reduce the number of test cases to be generated. Our technique applies across a class of structural constraint solvers. Experimental results show that the technique enables an order of magnitude reduction in the number of test cases to be considered.