Isolation increases upfront costs of provisioning containers. This is due to unnecessary software and data in container images. While several static and dynamic analysis methods for pruning unnecessary software are known, less attention has been paid to pruning unnecessary data. In this paper, we address the problem of determining and reducing unused data within a containerized application. Current data lineage methods can be used to detect data files that are never accessed in any of the observed runs, but this leads to a pessimistic amount of debloating. It is our observation that while an application may access a data file, it often accesses only a small portion of it over all its runs. Based on this observation, we present an approach and a tool Kondo, which aims to identify the set of all possible offsets that could be accessed within the data files over all executions of the application. Kondo works by fuzzing the parameter inputs to the application, and running it on the fuzzed inputs, with vastly fewer runs than brute force execution over all possible parameter valuations. Our evaluation on realistic benchmarks shows that Kondo is able to achieve 63% reduction in data file sizes and 98% recall against the set of all required offsets, on average.

Two-player games are a fruitful way to represent and reason about several important synthesis tasks. These tasks include controller synthesis (where one asks for a controller for a given plant such that the controlled plant satisfies a given temporal specification), program repair (setting values of variables to avoid exceptions), and synchronization synthesis (adding lock/unlock statements in multi-threaded programs to satisfy safety assertions). In all these applications, a solution directly corresponds to a winning strategy for one of the players in the induced game. In turn, logically-specified games offer a powerful way to model these tasks for large or infinite-state systems. Much of the techniques proposed for solving such games typically rely on abstraction-refinement or template-based solutions. In this paper, we show how to apply classical fixpoint algorithms, that have hitherto been used in explicit, finite-state, settings, to a symbolic logical setting. We implement our techniques in a tool called GENSys-LTL and show that they are not only effective in synthesizing valid controllers for a variety of challenging benchmarks from the literature, but often compute maximal winning regions and maximally-permissive controllers. We achieve 46.38X speed-up over the state of the art and also scale well for non-trivial LTL specifications.

For cloud native microservice monitoring and incident detection, companies and developers tend to largely focus only on generating logs, metrics, and traces at the application layer. However, in order to enable precise fault localization, it is necessary to access and correlate logs pertaining to a single end-user request across non-application layers as well, such as the load balancer at the front and the database at the back end. In this paper, we propose an observability library and an observability platform that addresses this problem and generates alerts that precisely point to fault locations. Logs at multiple layers are tagged with a common request identifier that helps in performing correlation. The observability platform is architected such that it lends itself to extensions to catch multiple types of errors and issues. The proposed observability platform has been tested on five open source benchmarks. The results confirm that our tool can be used deterministically and precisely to detect elusive issues.

In this work we describe a novel approach for modeling, analysis and verification of database-accessing applications that use the ORM (Object Relational Mapping) paradigm. Rather than directly analyze ORM code to check specific properties, our approach infers a general-purpose relational algebra summary of each controller in the application. This summary can then be fed into any off-the-shelf relational algebra solver to check for properties or specifications given by a developer. The summaries can also aid program understanding, and may have other applications. We have implemented our approach as a prototype tool that works for 'Spring' based MVC applications. A preliminary evaluation reveals that the approach is efficient, and gives good results while checking a set of properties given by human subjects.

When microservices are written from scratch, APIs are usually made stateless. However, when an existing monolith application is decomposed into microservices, it may not be possible to make all the APIs stateless. Therefore, objects transferred via APIs may contain pointers. Consequently, data transfer via an API i.e., from a client address space to a server address space, reconstruction at the server, and returning to the client become non-trivial operations.Conventionally, data transfer between microservices is done using JSON, which serializes pointers to values that they point to. Once the data in JSON reaches the server, deserialization creates objects of the original types on the server. However, deserialization is unable to return the same objects passed by the client because serialization leads to loss of pointer information. We propose to apply pointer swizzling to solve this problem. Pointer swizzling modifies the definition of the class by introducing ID of the object and by replacing all pointers with IDs of the objects it refers. These IDs help to maintain correct reference in the server. After the server API operates on the objects, the server returns new objects of the same types to the client. These new objects need to be plugged back in the client address space i.e., pointers to the old objects in the client need to now point to the corresponding new objects. This plugging back is non-trivial because we do not know how the old objects map to the new objects. We propose creating memory maps at runtime to overcome this challenge.

Abstract Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This paper addresses the problem of precise data flow analysis for such systems. To obtain good precision, data flow analysis needs to somehow skip execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at run time. Existing data flow analysis techniques do elide a subset of such infeasible paths, but have the restriction that they admit only finite abstract analysis domains. In this paper we propose a generalization of these approaches to admit infinite abstract analysis domains, as such domains are commonly used in practice to obtain high precision. We have implemented our approach, and have analyzed its performance on a set of 14 benchmarks. On these benchmarks our tool obtains significantly higher precision compared to a baseline approach that does not elide any infeasible paths and to another baseline that elides infeasible paths but admits only finite abstract domains.

The synthesis of maximally-permissive controllers in infinite-state systems has many practical applications. Such controllers directly correspond to maximal winning strategies in logically specified infinite-state two-player games. In this paper, we introduce a tool called GenSys which is a fixed-point engine for computing maximal winning strategies for players in infinite-state safety games. A key feature of GenSys is that it leverages the capabilities of existing off-the-shelf solvers to implement its fixed point engine. GenSys outperforms state-of-the-art tools in this space by a significant margin. Our tool has solved some of the challenging problems in this space, is scalable, and also synthesizes compact controllers. These controllers are comparatively small in size and easier to comprehend. GenSys is freely available for use and is available under an open-source license.

Verifying whether a procedure is observationally pure (that is, it always returns the same result for the same input argument) is challenging when the procedure uses mutable (private) global variables, e.g., for memoization, and when the procedure is recursive. We present a deductive verification approach for this problem. Our approach encodes the procedure’s code as a logical formula, with recursive calls being modeled using a mathematical function symbol assuming that the procedure is observationally pure . Then, a theorem prover is invoked to check whether this logical formula agrees with the function symbol referred to above in terms of input-output behavior for all arguments. We prove the soundness of this approach. We then present a conservative approximation of the first approach that reduces the verification problem to one of checking whether a quantifier-free formula is satisfiable and prove the soundness of the second approach. We evaluate our approach on a set of realistic examples, using the Boogie intermediate language and theorem prover. Our evaluation shows that the invariants are easy to construct manually, and that our approach is effective at verifying observationally pure procedures.

Object sensitivity analysis is a well-known form of context-sensitive points-to analysis. This analysis is parameterized by a bound on the names of symbolic objects associated with each allocation site. In this paper, we propose a novel approach based on object sensitivity analysis that takes as input a set of client queries, and tries to answer them using an initial round of inexpensive object sensitivity analysis that uses a low object-name length bound at all allocation sites. For the queries that are answered unsatisfactorily, the approach then pin points "bad" points-to facts, which are the ones that are responsible for the imprecision. It then employs a form of program slicing to identify allocation sites that are potentially causing these bad points-to facts to be generated. The approach then runs object sensitivity analysis once again, this time using longer names for just these allocation sites, with the objective of resolving the imprecision in this round. We describe our approach formally, prove its completeness, and describe a Datalog-based implementation of it on top of the Petablox framework. Our evaluation of our approach on a set of large Java benchmarks, using two separate clients, reveals that our approach is more precise than the baseline object sensitivity approach, by around 29% for one of the clients and by around 19% for the other client. Our approach is also more precise on most large benchmarks than a recently proposed approach that uses SAT solvers to identify allocation sites to refine.

A common need of refactorings that involve object allocations is to determine precisely the program points at which objects allocated at a given allocation site become fully initialized. In this paper we formalize the notion of full initialization points (FIPs) of allocation sites, and present a static analysis to determine precisely these program points. While this analysis can benefit several allocation-site refactorings, to demonstrate its usefulness we select two specific refactorings in this paper - object sharing refactoring and immutability refactoring. By introducing code to cache and share objects at the FIPs suggested by our analysis, object-sharing refactoring was able to obtain a mean memory savings of 11.4% on a set of real Java benchmarks. Immutability refactoring guided by our analysis achieved a mean runtime speedup of 1.6X compared to performing the same refactoring using a baseline approach.

Web applications are difficult to analyze using code-based tools because data-flow and control-flow through the application occurs via both server-side code and client-side pages. Client-side pages are typically specified in a scripting language that is different from the main server-side language; moreover, the pages are generated dynamically from the scripts. To address these issues we propose a static-analysis approach that automatically constructs a ``model'' of each page in a given application. A page model is a code fragment in the same language as the server-side code, which faithfully over-approximates the possible elements of the page as well as the control-flows and data-flows due to these elements. The server-side code in conjunction with the page models then becomes a standard (non-web) program, thus amenable to analysis using standard code-based tools. We have implemented our approach in the context of J2EE applications. We demonstrate the versatility and usefulness of our approach by applying three standard analysis tools on the resultant programs from our approach: a concolic-execution based model checker (JPF), a dynamic fault localization tool (Zoltar), and a static slicer (Wala).

We address the task of mapping a given textual domain model with the source code of an application which is in the same domain but was developed independently of the domain model. The key novelty of our approach is to use mathematical optimization to find a mapping between the elements in the two sides that maximizes the instances of clusters of related elements on each side being mapped to clusters of similarly related elements on the other side. We describe experiments wherein we apply our approach to the task of matching two real, open-source applications to corresponding industry-standard domain models. In comparison with previous approaches that leverage relationships, but are formulated as heuristics rather than as a principled optimization problem, our approach gives up to 40% higher precision given a desired level of recall.

Programs that process data that reside in files are widely used in varied domains, such as banking, healthcare, and web-traffic analysis. Precise static analysis of these programs in the context of software transformation and verification tasks is a challenging problem. Our key insight is that static analysis of file-processing programs can be made more useful if knowledge of the input file formats of these programs is made available to the analysis. We instantiate this idea to solve two practical problems - specializing the code of a program to a given “restricted” input file format, and verifying if a program “conforms” to a given input file format. We then discuss an implementation of our approach, and also empirical results on a set of real and realistic programs. The results are very encouraging in the terms of both scalability as well as precision of the approach.

Context sensitive inter-procedural dataflow analysis is a precise approach for static analysis of programs. It is very expensive in its full form. We propose a prefix approximation for context sensitive analysis, wherein a prefix of the full context stack is used to tag dataflow facts. Our technique, which is in contrast with suffix approximation that has been widely used in the literature, is designed to be more scalable when applied to programs with modular structure. We describe an instantiation of our technique in the setting of the classical call-strings approach for inter-procedural analysis. We analyzed several large enterprise programs using an implementation of our technique, and compared it with the fully context sensitive, context insensitive, as well as suffix-approximated variants of the call-strings approach. The precision of our technique was in general less than that of suffix approximation when measured on entire programs. However, the precision that it offered for outer-level procedures, which typically contain key business logic, was better, and its performance was much better.

Creation of large numbers of co-existing long-lived isomorphic objects increases the memory footprint of applications significantly. In this paper we propose a dynamic-analysis based approach that detects allocation sites that create large numbers of long-lived isomorphic objects, estimates quantitatively the memory savings to be obtained by sharing isomorphic objects created at these sites, and also checks whether certain necessary conditions for safely employing object sharing hold. We have implemented our approach as a tool, and have conducted experiments on several real-life Java benchmarks. The results from our experiments indicate that in real benchmarks a significant amount of heap memory, ranging up to 37% in some benchmarks, can be saved by employing object sharing. We have also validated the precision of estimates from our tool by comparing these with actual savings obtained upon introducing object-sharing at selected sites in the real benchmarks.

Null dereferences are a bane of programming in languages such as Java. In this paper we propose a sound, demand-driven, inter-procedurally context-sensitive dataflow analysis technique to verify a given dereference as safe or potentially unsafe. Our analysis uses an abstract lattice of formulas to find a pre-condition at the entry of the program such that a null-dereference can occur only if the initial state of the program satisfies this pre-condition. We use a simplified domain of formulas, abstracting out integer arithmetic, as well as unbounded access paths due to recursive data structures. For the sake of precision we model aliasing relationships explicitly in our abstract lattice, enable strong updates, and use a limited notion of path sensitivity. For the sake of scalability we prune formulas continually as they get propagated, reducing to true conjuncts that are less likely to be useful in validating or invalidating the formula. We have implemented our approach, and present an evaluation of it on a set of ten real Java programs. Our results show that the set of design features we have incorporated enable the analysis to (a) explore long, inter-procedural paths to verify each dereference, with (b) reasonable accuracy, and (c) very quick response time per dereference, making it suitable for use in desktop development environments.

A number of companies are trying to migrate large monolithic software systems to Service Oriented Architectures. A common approach to do this is to first identify and describe desired services (i.e., create a model), and then to locate portions of code within the existing system that implement the described services. In this paper we describe a detailed case study we undertook to match a model to an open-source business application. We describe the systematic methodology we used, the results of the exercise, as well as several observations that throw light on the nature of this problem. We also suggest and validate heuristics that are likely to be useful in partially automating the process of matching service descriptions to implementations.

We present an algorithm for reverse engineering object-oriented (OO) data models from programs written in weakly-typed languages like Cobol. These models, similar to UML class diagrams, can facilitate a variety of program maintenance and migration activities. Our algorithm is based on a semantic analysis of the program's code, and we provide a bisimulation-based formalization of what it means for an OO data model to be correct for a program.

Procedure extraction is an important program transformation that can be used to make programs easier to understand and maintain, to facilitate code reuse, and to convert “monolithic” code to modular or object-oriented code. Procedure extraction involves the following steps:

Replication is often used in many distributed systems to provide a higher level of performance, reliability and availability. Lazy replica update protocols, which propagate updates to replicas through independent transactions after the original transaction commits, have become popular with database vendors due to their superior performance characteristics. However, if lazy protocols are used indiscriminately, they can result in non-serializable executions. In this paper, we propose two new lazy update protocols that guarantee serializability but impose a much weaker requirement on data placement than earlier protocols. Further, many naturally occurring distributed systems, like distributed data warehouses, satisfy this requirement. We also extend our lazy update protocols to eliminate all requirements on data placement. The extension is a hybrid protocol that propagates as many updates as possible in a lazy fashion. We implemented our protocols on the Datablitz database system product developed at Bell Labs. We also conducted an extensive performance study which shows that our protocols outperform existing protocols over a wide range of workloads.