Venkatesh-Prasad Ranganath

A breezy guide to using Python's built-in support for logging. The guide covers general concepts relevant to logging, logging APIs in Python and how to use them, and good practices, gotchas, and performance considerations associated with these APIs.

As security of mobile apps is crucial to modern-day living, there is a growing need to help developers build apps with provable security guarantees that apps do not leak sensitive user information or cannot be exploited to perform actions without the user's consent. The current prevalent approach to mobile app security curatively addresses vulnerabilities after apps have been developed. This approach has downsides in terms of time, resources, user inconvenience, and information loss.

As… Show more

As security of mobile apps is crucial to modern-day living, there is a growing need to help developers build apps with provable security guarantees that apps do not leak sensitive user information or cannot be exploited to perform actions without the user's consent. The current prevalent approach to mobile app security curatively addresses vulnerabilities after apps have been developed. This approach has downsides in terms of time, resources, user inconvenience, and information loss.

As an alternative, we propose a design-based mobile app development methodology called SeMA to prevent the creation of vulnerabilities in mobile apps. SeMA enables app designers and developers to iteratively reason about the security of an app by using its storyboard, an existing and prevalent design artifact. A proof of concept realization of SeMA using Android Studio tooling is able to prevent 49 known vulnerabilities that plague Android apps. Show less

UX designers use storyboards to visually capture a user experience (UX) of an app. Lately, story-boarding is used by Android app development to conceptualize and design apps.

Recently, security has become an integral part of an Android app’s UX because mobile apps are used to perform critical activities such as banking, communication, etc. Therefore, it is imperative for app creators to ensure the security of their users.

In this context, storyboarding tools offer limited… Show more

UX designers use storyboards to visually capture a user experience (UX) of an app. Lately, story-boarding is used by Android app development to conceptualize and design apps.

Recently, security has become an integral part of an Android app’s UX because mobile apps are used to perform critical activities such as banking, communication, etc. Therefore, it is imperative for app creators to ensure the security of their users.

In this context, storyboarding tools offer limited capabilities to capture and reason about security requirements of an app. Consequently, security cannot be baked into the app at design time. This allows vulnerabilities that stem from design flaws to creep into apps. To address this concern, we propose a storyboard based design methodology that will enable specification and verification of security properties of an Android app at design time. Show less

In recent years, various efforts have designed and developed benchmark suites to evaluate the efficacy of vulnerability detection tools in Android apps. The choice of benchmark suites used in tool evaluations is often based on availability and popularity of suites instead of on the characteristics and relevance of benchmark suites relative to real world native Android apps. One of the reasons for such choice is the lack of information about characteristics and relevance of benchmarks suites… Show more

In recent years, various efforts have designed and developed benchmark suites to evaluate the efficacy of vulnerability detection tools in Android apps. The choice of benchmark suites used in tool evaluations is often based on availability and popularity of suites instead of on the characteristics and relevance of benchmark suites relative to real world native Android apps. One of the reasons for such choice is the lack of information about characteristics and relevance of benchmarks suites relative to real world apps.

In this paper, we report the findings from our effort aimed at addressing this gap. We empirically evaluated three Android specific benchmark suites – DroidBench, Ghera, and IccBench. For each suite,we report how well do these benchmark suites represent real world apps in terms of API usage: 1)coverage – how often are the APIs used in a benchmark suite used in a sample of real world native Android apps? and 2) gap – which of the APIs used in a sample of real world native Android apps arenot used in any benchmark suite? Based on pairwise comparison, we also report how these suites fare relative to each other in terms of API usage.

The findings in this paper can help 1) Android security analysis tool developers choose benchmark suites that are best suited to evaluate their tools (informed by coverage and pairwise comparison) and2) Android specific benchmark creators improve API usage based representativeness of suites (informed by gaps). Show less

Increasing interest to secure Android ecosystem has spawned numerous efforts to assist app developers in building secure apps. These efforts have developed tools and techniques capable of detecting vulnerabilities and malicious behaviors in apps. However, there has been no evaluation of the effective- ness of these tools and techniques to detect known vulnerabilities. Absence of such evaluations poses as a hurdle when app developers try to choose security analysis tools to secure their… Show more

Increasing interest to secure Android ecosystem has spawned numerous efforts to assist app developers in building secure apps. These efforts have developed tools and techniques capable of detecting vulnerabilities and malicious behaviors in apps. However, there has been no evaluation of the effective- ness of these tools and techniques to detect known vulnerabilities. Absence of such evaluations poses as a hurdle when app developers try to choose security analysis tools to secure their apps.

In this regard, we evaluated the effectiveness of vulnerability (and malicious behavior) detection tools for Android apps. We considered 64 security analysis tools and empirically evaluated 19 of them -- 14 vulnerability detection tools and 5 malicious behavior detection tools -- against 42 known vulnerabilities captured by benchmarks in Ghera repository. Of the many observations from the evaluation, the key observation is existing security analysis tools for Android apps are very limited in their ability to detect known vulnerabilities: all of the evaluated vulnerability detection tools together could only detect 30 of the 42 known vulnerabilities.

Clearly, serious effort is required if security analysis tools are to help developers build secure apps. We hope the observations from this evaluation will help app developers choose appropriate security analysis tools and persuade tool developers and researchers to identify and address limitations in their tools and techniques. We also hope this evaluation will catalyze or spark a conversation in the Android security analysis community to require more rigorous and explicit evaluation of security analysis tools and techniques.

[Pre-print: https://arxiv.org/abs/1806.09059] Show less

Given the cost of HPC clusters, making best use of them is crucial to improve infrastructure ROI. Likewise, reducing failed HPC jobs and related waste in terms of user wait times is crucial to improve HPC user productivity (aka human ROI). While most efforts (e.g.,debugging HPC programs) explore technical aspects to improve ROI of HPC clusters, we hypothesize non-technical (human) aspects are worth exploring to make non-trivial ROI gains; specifically, understanding non-technical aspects and… Show more

Given the cost of HPC clusters, making best use of them is crucial to improve infrastructure ROI. Likewise, reducing failed HPC jobs and related waste in terms of user wait times is crucial to improve HPC user productivity (aka human ROI). While most efforts (e.g.,debugging HPC programs) explore technical aspects to improve ROI of HPC clusters, we hypothesize non-technical (human) aspects are worth exploring to make non-trivial ROI gains; specifically, understanding non-technical aspects and how they contribute to the failure of HPC jobs.

In this regard, we conducted a case study in the context of Beocat cluster at Kansas State University. The purpose of the study was to learn the reasons why users terminate jobs and to quantify wasted computations in such jobs in terms of system utilization and user wait time. The data from the case study helped identify interesting and actionable reasons why users terminate HPC jobs. It also helped confirm that user terminated jobs may be associated with non-trivial amount of wasted computation, which if reduced can help improve the ROI of HPC clusters. Show less

Lately more and more people are getting their up-to-date news bits from social media platforms such as Twitter and Facebook. These platforms add immediacy and transparency to information sharing. They also customize information for each user. Consequently, people prefer these platforms to seek and share information. Given this appeal of social media platforms along with the ubiquity of powerful mobile devices and the advances in information processing technology, if and how can social media… Show more

Lately more and more people are getting their up-to-date news bits from social media platforms such as Twitter and Facebook. These platforms add immediacy and transparency to information sharing. They also customize information for each user. Consequently, people prefer these platforms to seek and share information. Given this appeal of social media platforms along with the ubiquity of powerful mobile devices and the advances in information processing technology, if and how can social media like platform help in dealing with disasters? Specifically, how can such a platform enable people to automatically be part of pertinent local network, share observations about disasters, provide personalized contextual recommendations to folks in disasters, and possibly improve situational awareness of responders? If such a platform is to be realized, then what challenges need to be addressed? Show less

Security of mobile apps affects the security of their users. This has fueled the development of techniques to automatically detect vulnerabilities in mobile apps and help developers secure their apps; specifically, in the context of Android platform due to openness and ubiquitousness of the platform. Despite a slew of research efforts in this space, there is no comprehensive repository of up-to-date and lean benchmarks that contain most of the known Android app vulnerabilities and… Show more

Security of mobile apps affects the security of their users. This has fueled the development of techniques to automatically detect vulnerabilities in mobile apps and help developers secure their apps; specifically, in the context of Android platform due to openness and ubiquitousness of the platform. Despite a slew of research efforts in this space, there is no comprehensive repository of up-to-date and lean benchmarks that contain most of the known Android app vulnerabilities and, consequently, can be used to rigorously evaluate both existing and new vulnerability detection techniques and help developers learn about Android app vulnerabilities. In this paper, we describe Ghera, an open source repository of benchmarks that capture 25 known vulnerabilities in Android apps (as pairs of exploited/benign and exploiting/malicious apps). We also present desirable characteristics of vulnerability benchmarks and repositories that we uncovered while creating Ghera.

https://bitbucket.org/secure-it-i/android-app-vulnerability-benchmarks/ Show less

Chapter in a book titled "Perspectives on Data Science for Software Engineering".

Chapter in a book titled "Perspectives on Data Science for Software Engineering".

This paper proposes a set of communication patterns to enable the construction of medical systems by composing devices and apps in Integrated Clinical Environments (ICE). These patterns abstract away the details of communication tasks, reduce engineering overhead, and ease compositional reasoning of the system. The proposed patterns have been successfully implemented on top of two distinct platforms (i.e., RTI Connext and Vert.x) to allow for experimentation.

A Medical Application Platform (MAP) enables multi-vendor heterogeneous medical devices to be integrated via network infrastructure and provides an application hosting facility that supports a wide range of clinical applications for data fusion, decision support, multi-device safety interlocks, workflow automations, and closed-loop control of actuating medical devices. The assurance of MAP components and systems is distributed across a broad group of stakeholders including medical device… Show more

A Medical Application Platform (MAP) enables multi-vendor heterogeneous medical devices to be integrated via network infrastructure and provides an application hosting facility that supports a wide range of clinical applications for data fusion, decision support, multi-device safety interlocks, workflow automations, and closed-loop control of actuating medical devices. The assurance of MAP components and systems is distributed across a broad group of stakeholders including medical device manufacturers, platform infrastructure providers, application vendors, third-party certification organizations, and regulatory agencies. Realization of the MAP vision requires that all stakeholders involved in developing, testing, certifying, regulating, purchasing, and using medical devices and applications operate and cooperate within a well-defined ecosphere. This paper presents a high-level overview of the organization of such an ecosphere. We focus on identifying stakeholder roles, responsibilities, artifacts, and interactions, we also indicate the contributions of each of these to the development and safety/security assurance of MAP-based systems. Show less

Although Machine Learning (ML) based approaches have shown promise for Android malware detection, a set of critical challenges remain unaddressed. Some of those challenges arise in relation to proper evaluation of the detection approach while others are related to the design decisions of the same. In this paper, we systematically study the impact of these challenges as a set of research questions (i.e., hypotheses). We design an experimentation framework where we can reliably vary several… Show more

Although Machine Learning (ML) based approaches have shown promise for Android malware detection, a set of critical challenges remain unaddressed. Some of those challenges arise in relation to proper evaluation of the detection approach while others are related to the design decisions of the same. In this paper, we systematically study the impact of these challenges as a set of research questions (i.e., hypotheses). We design an experimentation framework where we can reliably vary several parameters while evaluating ML-based Android malware detection approaches. The results from the experiments are then used to answer the research questions. Meanwhile, we also demonstrate the impact of some challenges on some existing ML-based approaches. The large (market-scale) dataset (benign and malicious apps) we use in the above experiments represents the real-world Android app security analysis scale. We envision this study to encourage the practice of employing a better evaluation strategy and better designs of future ML-based approaches for Android malware detection. Show less

Both researchers and industry vendors are exploring the concept of systems of interoperable medical devices and health information systems that support safety and enhance clinical functionality. The Integrated Clinical Environment (ICE) has been proposed as an architecture for such systems, and several research and commercial implementations are being developed. Central to ICE concept of safe and flexible plug-and-play interoperability is the notion of an ICE Device Model (DM), which is… Show more

Both researchers and industry vendors are exploring the concept of systems of interoperable medical devices and health information systems that support safety and enhance clinical functionality. The Integrated Clinical Environment (ICE) has been proposed as an architecture for such systems, and several research and commercial implementations are being developed. Central to ICE concept of safe and flexible plug-and-play interoperability is the notion of an ICE Device Model (DM), which is intended to be a machine-readable meta-data description of a device's capabilities as exposed in standardized form over its network interface. In this paper, we present an overview of the stakeholders and high level goals of the ICE DM as necessary for supporting safe and flexible plug-and-play interoperability. These goals provide the foundation for further refinement by research and industry teams to specific safety and implementation requirements for the ICE DM concept. Show less

When composing a system from components, we need to ensure that the components are compatible. This is commonly achieved by components interacting only via published and well-defined interfaces. Even so, it is possible for client components to learn about and depend on unpublished yet observable behaviors of components. To identify and support these situations, compatibility testing should uncover such observable behaviors.

As a solution, we propose a patterns-based approach to… Show more

When composing a system from components, we need to ensure that the components are compatible. This is commonly achieved by components interacting only via published and well-defined interfaces. Even so, it is possible for client components to learn about and depend on unpublished yet observable behaviors of components. To identify and support these situations, compatibility testing should uncover such observable behaviors.

As a solution, we propose a patterns-based approach to test compatibility between programs in terms of their observable behaviors. The approach compares traces of behaviors observed at identical published interfaces of programs and detects incompatibilities stemming from both the presence of previously unobserved behaviors and the absence of previously observed behaviors. The traces are compared by transforming them into sets of structural and binary linear temporal patterns.

During Windows 8 development cycle, we applied this approach to test compatibility between USB 2.0 and USB 3.0 bus drivers. Upon testing 14 USB 2.0 devices that were functioning without errors with both USB bus drivers, we uncovered 25 previously unknown incompatibilities between the bus drivers. Show less

Reliability of software depends not only on intrinsic factors such as its code properties, but also on extrinsic factors—that is, the properties of the environment it operates in. In an empirical study of more than 200,000 Windows users, we found that the reliability of individual applications is related to whether and which other applications are in-stalled: While games and file-sharing applications tend to decrease the reliability of other applications, security applications tend to increase… Show more

Reliability of software depends not only on intrinsic factors such as its code properties, but also on extrinsic factors—that is, the properties of the environment it operates in. In an empirical study of more than 200,000 Windows users, we found that the reliability of individual applications is related to whether and which other applications are in-stalled: While games and file-sharing applications tend to decrease the reliability of other applications, security applications tend to increase it. Furthermore, application reliability is related to the usage profiles of these applications; generally, the more an application is used, the more likely it is to have negative impact on reliability of others. As a conse-quence, software testers must be careful to investigate and control these factors. Show less

In this paper, we propose a data transformation pattern to transform sequential data into a set of binary/categorical features and numerical features to enable data analysis. These features capture both structural and temporal information inherent in sequential data.

Libraries usually impose constraints on how clients should use them. Often these constraints are not well-documented. In this paper, we address the problem of recovering such constraints automatically, a problem referred to as specification mining. Given some client programs that use a given library, we identify constraints on the library usage that are (almost) satisfied by the given set of clients.

The class of rules we target for mining combines simple binary temporal operators with… Show more

Libraries usually impose constraints on how clients should use them. Often these constraints are not well-documented. In this paper, we address the problem of recovering such constraints automatically, a problem referred to as specification mining. Given some client programs that use a given library, we identify constraints on the library usage that are (almost) satisfied by the given set of clients.

The class of rules we target for mining combines simple binary temporal operators with state predicates (composed of equality constraints) and quantification. This is a simple yet expressive subclass of temporal properties (LTL formulae) that allows us to capture many common API usage rules. We focus on recovering rules from execution traces and apply classical data mining concepts to be robust against bugs (API usage rule violations) in clients. We present new algorithms for mining rules from execution traces. We show how a propositional rule mining algorithm can be generalized to treat quantification and state predicates in a unified way. Our approach enables the miner to be complete (i.e. , mine all rules within the targeted class that are satisfied by the given traces) while avoiding an exponential blowup.

We have implemented these algorithms and used them to mine API usage rules for several Windows APIs. Our experiments show the efficiency and effectiveness of our approach. Show less

We are interested in identifying and enforcing the isolation requirements of a concurrent program, i.e., concurrency control that ensures that the program meets its specification. The thesis of this paper is that this can be done systematically starting from a sequential proof, i.e., a proof of correctness of the program in the absence of concurrent interleavings. We illustrate our thesis by presenting a solution to the problem of making a sequential library thread-safe for concurrent clients… Show more

We are interested in identifying and enforcing the isolation requirements of a concurrent program, i.e., concurrency control that ensures that the program meets its specification. The thesis of this paper is that this can be done systematically starting from a sequential proof, i.e., a proof of correctness of the program in the absence of concurrent interleavings. We illustrate our thesis by presenting a solution to the problem of making a sequential library thread-safe for concurrent clients. We consider a sequential library annotated with assertions along with a proof that these assertions hold in a sequential execution. We show how we can use the proof to derive concurrency control that ensures that any execution of the library methods, when invoked by concurrent clients, satisfies the same assertions. We also present an extension to guarantee that the library methods are linearizable or atomic. Show less

We are interested in identifying and enforcing the isolation requirements of a concurrent program, i.e., concurrency control that ensures that the program meets its specification. The thesis of this paper is that this can be done systematically starting from a sequential proof, i.e., a proof of correctness of the program in the absence of concurrent interleavings. We illustrate our thesis by presenting a solution to the problem of making a sequential library thread-safe for concurrent clients… Show more

We are interested in identifying and enforcing the isolation requirements of a concurrent program, i.e., concurrency control that ensures that the program meets its specification. The thesis of this paper is that this can be done systematically starting from a sequential proof, i.e., a proof of correctness of the program in the absence of concurrent interleavings. We illustrate our thesis by presenting a solution to the problem of making a sequential library thread-safe for concurrent clients. We consider a sequential library annotated with assertions along with a proof that these assertions hold in a sequential execution. We show how we can use the proof to derive concurrency control that ensures that any execution of the library methods, when invoked by concurrent clients, satisfies the same assertions. We also present an extension to guarantee that the library is linearizable with respect to its sequential specification. Show less

In this paper, we focus on concurrent programs that use locks to achieve isolation of data accessed by critical sections of code. We present ISOLATOR, an algorithm that guarantees isolation for well-behaved threads of a program that obey a locking discipline even in the presence of ill-behaved threads that disobey the locking discipline. ISOLATOR uses code instrumentation, data replication, and virtual memory protection to detect isolation violations and delays ill-behaved threads to ensure… Show more

In this paper, we focus on concurrent programs that use locks to achieve isolation of data accessed by critical sections of code. We present ISOLATOR, an algorithm that guarantees isolation for well-behaved threads of a program that obey a locking discipline even in the presence of ill-behaved threads that disobey the locking discipline. ISOLATOR uses code instrumentation, data replication, and virtual memory protection to detect isolation violations and delays ill-behaved threads to ensure isolation. Our instrumentation scheme requires access only to the code of well-behaved threads. We have evaluated ISOLATOR on several benchmark programs and found that ISOLATOR can ensure isolation with reasonable runtime overheads. In addition, we present three general desiderata - safety, isolation, and permissiveness - for any scheme that attempts to ensure isolation, and formally prove that ISOLATOR satisfies all of these desiderata. Show less

Libraries usually impose constraints on how clients should use them. Often these constraints are not well-documented. In this paper, we address the problem of recovering such constraints automatically, a problem referred to as specification mining. Given some client programs that use a given library, we identify constraints on the library usage that are (almost) satisfied by the given set of clients.The class of rules we target for mining combines simple binary temporal operators with state… Show more

Libraries usually impose constraints on how clients should use them. Often these constraints are not well-documented. In this paper, we address the problem of recovering such constraints automatically, a problem referred to as specification mining. Given some client programs that use a given library, we identify constraints on the library usage that are (almost) satisfied by the given set of clients.The class of rules we target for mining combines simple binary temporal operators with state predicates (involving equality constraints) and quantification. This is a simple yet expressive subclass of temporal properties that allows us to capture many common API usage rules. We focus on recovering rules from execution traces and apply classical data mining concepts to be robust against bugs (API usage rule violations) in clients. We present new algorithms for mining rules from execution traces. We show how a propositional rule mining algorithm can be generalized to treat quantification and state predicates in a unified way. Our approach enables the miner to be complete — mine all rules within the targeted class that are satisfied by the given traces — while avoiding an exponential blowup.We have implemented these algorithms and used them to mine API usage rules for several Windows APIs. Our experiments show the efficiency and effectiveness of our approach. Show less

Component-oriented programming enables the development of easily deployable and manageable applications while datacenters sup- ports easy deployment and management of applications (via provisioning). So, why not consider component-oriented programming as the paradigm to program datacenter applications?

Concurrent programs are hard to design, develop, and debug. It is widely accepted that we lack good abstractions to design and reason about concurrent programs, and good tools to debug concurrent programs. Recent technology trends, such as the increasing prevalence of multicore processors, make concur rent programming more important than ever. Non-determinism arises in concurrent programs when the order in which threads can execute is unconstrained. While executions of concurrent programs on… Show more

Concurrent programs are hard to design, develop, and debug. It is widely accepted that we lack good abstractions to design and reason about concurrent programs, and good tools to debug concurrent programs. Recent technology trends, such as the increasing prevalence of multicore processors, make concur rent programming more important than ever. Non-determinism arises in concurrent programs when the order in which threads can execute is unconstrained. While executions of concurrent programs on multiprocessors inherently exhibit non-determinism, the executions on uniprocessors exhibit non-determinism due to the choices of the thread scheduler in the underlying O/S. Undesired non-determinism is a major cause of errors in concurrent programs. Nevertheless, we believe that non-determinism can be safely, permissively, and automatically controlled to tolerate runtime errors in concurrent programs and to provide various desirable semantic guarantees. In this position paper, we sketch some recent work we have done in this direction and outline our longer term goals along the same direction.

Controlling Nondeterminism for Semantic Guarantees. Available from: https://www.researchgate.net/publication/253709573_Controlling_Nondeterminism_for_Semantic_Guarantees [accessed Jul 4, 2017]. Show less

The notion of control dependence underlies many program analysis and transformation techniques. Despite being widely used, existing definitions and approaches to calculating control dependence are difficult to apply directly to modern program structures because these make substantial use of exception processing and increasingly support reactive systems designed to run indefinitely.

This article revisits foundational issues surrounding control dependence, and develops definitions and… Show more

The notion of control dependence underlies many program analysis and transformation techniques. Despite being widely used, existing definitions and approaches to calculating control dependence are difficult to apply directly to modern program structures because these make substantial use of exception processing and increasingly support reactive systems designed to run indefinitely.

This article revisits foundational issues surrounding control dependence, and develops definitions and algorithms for computing several variations of control dependence that can be directly applied to modern program structures. To provide a foundation for slicing reactive systems, the article proposes a notion of slicing correctness based on weak bisimulation, and proves that some of these new definitions of control dependence generate slices that conform to this notion of correctness. This new framework of control dependence definitions, with corresponding correctness results, is even able to support programs with irreducible control flow graphs. Finally, a variety of properties show that the new definitions conservatively extend classic definitions. These new definitions and algorithms form the basis of the Indus Java slicer, a publicly available program slicer that has been implemented for full Java.
Show less

In our previous work, we developed partial order reduction techniques that now form the core reduction strategies of several popular Java model checking frameworks including Bogor and JPF. These techniques work by dynamically collecting independence information needed to drive POR. In this paper, we consider several additional variants of partial order reductions and how independence information needed to drive these reductions can be calculated statically via a collection of Java analyses… Show more

In our previous work, we developed partial order reduction techniques that now form the core reduction strategies of several popular Java model checking frameworks including Bogor and JPF. These techniques work by dynamically collecting independence information needed to drive POR. In this paper, we consider several additional variants of partial order reductions and how independence information needed to drive these reductions can be calculated statically via a collection of Java analyses techniques including points-to, escape analysis, and smart call-graph construction. As part of this investigation, we also give a stateful implementation of Flanagan and Godefroid's dynamic POR framework capable of handling cyclic systems. We show that (a) the performance of these variants compares favorably in many cases to existing state-of-the-art techniques and (b) the variants suggest opportunities for further optimizations. In addition, our results give an alternative implementation strategy in which the gathering of dependence information can be lifted out of the model checking engine and performed in a separate static analysis phase. Show less

Program slicing is a program analysis and transformation technique that has been successfully used in a wide range of applications including program comprehension, debugging, maintenance, testing, and verification. However, there are only few fully featured implementations of program slicing that are available for industrial applications or academic research. In particular, very little tool support exists for slicing programs written in modern object-oriented languages such as Java, C#, or C++.… Show more

Program slicing is a program analysis and transformation technique that has been successfully used in a wide range of applications including program comprehension, debugging, maintenance, testing, and verification. However, there are only few fully featured implementations of program slicing that are available for industrial applications or academic research. In particular, very little tool support exists for slicing programs written in modern object-oriented languages such as Java, C#, or C++. In this paper, we present Indus—a robust framework for analyzing and slicing concurrent Java programs, and Kaveri—a feature-rich Eclipse-based GUI front end for Indus slicing. For Indus, we describe the underlying tool architecture, analysis components, and program dependence capabilities required for slicing. In addition, we present a collection of advanced features useful for effective slicing of Java programs including calling-context sensitive slicing, scoped slicing, control slicing, and chopping. For Kaveri, we discuss the design goals and basic capabilities of the graphical facilities integrated into a Java development environment to present the slicing information. This paper is an extended version of a tool demonstration paper presented at the International Conference on Fundamental Aspects of Software Engineering (FASE 2005). Thus, the paper highlights tool capabilities and engineering issues and refers the reader to other papers for technical details. Show less

Program slicing is a program analysis and transformation technique that has been successfully applied in a wide range of applications including program comprehension, debugging, maintenance, testing, and verification. However, there are only a few full-featured implementations of program slicing that are available for industrial applications or academic research. In particular, very little tool support exists for slicing programs written in modern object-oriented languages such as Java, C#, or… Show more

Program slicing is a program analysis and transformation technique that has been successfully applied in a wide range of applications including program comprehension, debugging, maintenance, testing, and verification. However, there are only a few full-featured implementations of program slicing that are available for industrial applications or academic research. In particular, very little tool support exists for slicing programs written in modern object-oriented languages such as Java, C#, or C++. This talk presents an overview of Indus1 - a robust framework for analysis and slicing of concurrent Java programs, and Kaveri - a feature-rich Eclipse-based GUI for Indus slicing. For Indus, we describe the underlying tool architecture, analysis components, and program dependence capabilities required for slicing. In addition, we present a collection of advanced features useful for effective slicing of Java programs including calling-context sensitive slicing, scoped slicing, control slicing, and chopping. For Kaveri, we discuss the design goals and basic capabilities of a graphical presentation of slicing information that is integrated into a Java development environment. We will also briefly overview the Indus scripting framework that allows developers easy access to a variety of information collected by the underlying Indus program analysis framework. Show less

In this paper, we present our experience in automating the XML schema driven serialization approach within the Apache Axis 1 and Axis 2 SOAP frameworks. We have generalized our previous template based approach to serialization (7) as a generic XML schema driven serialization approach and realized the generic approach via two stylistically different and non-intrusive implementation strategies. We illustrate the benefits of our approach - performance improvements of up to 89% with low memory… Show more

In this paper, we present our experience in automating the XML schema driven serialization approach within the Apache Axis 1 and Axis 2 SOAP frameworks. We have generalized our previous template based approach to serialization (7) as a generic XML schema driven serialization approach and realized the generic approach via two stylistically different and non-intrusive implementation strategies. We illustrate the benefits of our approach - performance improvements of up to 89% with low memory overhead - by empirically comparing it with the Java Bean based approaches employed in Apache Axis 1 and Axis 2. Show less

Model checking techniques have proven effective for checking a number of non-trivial concurrent object-oriented software systems. However, due to the high computational and memory costs, a variety of model reduction techniques are needed to overcome current limitations on applicability and scalability. Conventional wisdom holds that static program slicing can be an effective model reduction technique, yet anecdotal evidence is mixed, and there has been no work that has systematically studied… Show more

Model checking techniques have proven effective for checking a number of non-trivial concurrent object-oriented software systems. However, due to the high computational and memory costs, a variety of model reduction techniques are needed to overcome current limitations on applicability and scalability. Conventional wisdom holds that static program slicing can be an effective model reduction technique, yet anecdotal evidence is mixed, and there has been no work that has systematically studied the costs/benefits of slicing for model reduction in the context of model checking source code for realistic systems. In this paper, we present an overview of the sophisticated Indus program slicer that is capable of handling full Java and is readily applicable to interesting off-the- shelf concurrent Java programs. Using the Indus program slicer as part of the next generation of the Bandera model checking framework, we experimentally demonstrate significant benefits from using slicing as a fully automatic model reduction technique. Our experimental results consider a number of Java systems with varying structural properties, the effects of combining slicing with other well-known model reduction techniques such as partial order reductions, and the effects of slicing for different classes of properties. Our conclusions are that slicing concurrent object-oriented source code provides significant reductions that are orthogonal to a number of other reduction techniques, and that slicing should always be applied due to its automation and low computational costs. Show less

This dissertation presents a collection of scalable and accurate approaches to tackle the above situation. Primarily, the approaches are focused on discovering dependences (relations) between various parts of the software/program and leveraging the dependences to improve maintenance and development tasks via program slicing (comprehension) and verification.

This paper provides the following contributions to the study of middleware optimization techniques for product line architectures in real-time systems. First, we identify different dimensions of generality in standards based middleware implementations. Second, we describe how specialization approaches used in other domains including OS, compiler and programming languages can be applied to address middleware generality challenges. Third, we present preliminary results from the application of our… Show more

This paper provides the following contributions to the study of middleware optimization techniques for product line architectures in real-time systems. First, we identify different dimensions of generality in standards based middleware implementations. Second, we describe how specialization approaches used in other domains including OS, compiler and programming languages can be applied to address middleware generality challenges. Third, we present preliminary results from the application of our specialization techniques. Our results illustrate that specialization techniques represent a promising approach for minimizing time/space overheads in middleware. Show less

The notion of control dependence underlies many program analysis and transformation techniques. Despite wide applications, existing definitions and approaches for calculating control dependence are difficult to apply seamlessly to modern program structures. Such program structures make substantial use of exception processing and increasingly support reactive systems designed to run indefinitely.

This paper revisits foundational issues surrounding control dependence and slicing… Show more

The notion of control dependence underlies many program analysis and transformation techniques. Despite wide applications, existing definitions and approaches for calculating control dependence are difficult to apply seamlessly to modern program structures. Such program structures make substantial use of exception processing and increasingly support reactive systems designed to run indefinitely.

This paper revisits foundational issues surrounding control dependence and slicing. It develops definitions and algorithms for computing control dependence that can be directly applied to modern program structures. A variety of properties show that the new definitions conservatively extend classic definitions. In the context of slicing reactive systems, the paper proposes a notion of slicing correctness based on weak bisimulation and proves that the definition of control dependence generates slices that conform to this notion of correctness. The new definitions and algorithms for control dependence form the basis of a publicly available program slicer that has been implemented for full Java.
Show less

Component middleware frameworks such as the CORBA Component Model (CCM) and Enterprise Java Beans (EJB) are increasingly being applied to address challenges involved in building large-scale distributed systems. We seek to provide foundations and tools for model-driven development of such systems in which architectural models serve as highly leveragable abstractions that form a substrate into which a variety of forms of essential behavioral properties are woven. Our vision emphasizes a… Show more

Component middleware frameworks such as the CORBA Component Model (CCM) and Enterprise Java Beans (EJB) are increasingly being applied to address challenges involved in building large-scale distributed systems. We seek to provide foundations and tools for model-driven development of such systems in which architectural models serve as highly leveragable abstractions that form a substrate into which a variety of forms of essential behavioral properties are woven. Our vision emphasizes a synergistic integration of analysis and analysis clients at multiple levels of abstraction in a system including both the architectural model (component interfaces and connections) level and the source code (component implementation) level. Dependence and flow properties have proven to be useful behavioral abstractions that can be leveraged in a variety of ways at both the architectural model level and code level. However, previous works provide no mechanism for connecting architectural-level dependences to code-level dependences, e. g., for the purpose of guaranteeing soundness of model-level specifications by checking that dependences present in implementations conform to model-level specifications – a task that is especially challenging when working with sophisticated component frameworks like CCM. In this paper, we propose a layered approach to enriching component interfaces specifi-cations to include a variety of forms dependence and flow information. We have implemented conformance checks between layers of component specifications using a flexible Java dependence analysis framework, and we report on our experiences applying the framework to a collection of CCM component specifications and implementations. Show less

This tool paper describes a modular program slicer for Java built using the Indus program analysis framework along with it's Eclipse-based user interface called Kaveri. Indus provides a library of classes that enables users to quickly assemble a highly customized non-system dependence graph based inter-procedural program slicer capable of slicing concurrent Java programs. Kaveri is an Eclipse plugin that relies on the above library to deliver program slicing to the eclipse platform. Apart from… Show more

This tool paper describes a modular program slicer for Java built using the Indus program analysis framework along with it's Eclipse-based user interface called Kaveri. Indus provides a library of classes that enables users to quickly assemble a highly customized non-system dependence graph based inter-procedural program slicer capable of slicing concurrent Java programs. Kaveri is an Eclipse plugin that relies on the above library to deliver program slicing to the eclipse platform. Apart from the basic feature for generating program slices from within eclipse along with an intuitive UI to view the slice, the plugin also provides the capability for chasing various dependences in the application to understand the slice. Show less

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems.

In this paper… Show more

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems.

In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on (a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lock-acquisition and release in a program (building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time over existing approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL−X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers.
Show less

Large distributed systems, including real-time embedded systems, are increasingly being built using sophisticated middleware frameworks. Communication in such systems is often realized using in terms of asynchronous events whose propagation is implemented by an underlying publish/subscribe service that hooks components into a generic event communication channel. Event correlation—a mechanism for monitoring and filtering events—has been introduced in some of these systems as an effective… Show more

Large distributed systems, including real-time embedded systems, are increasingly being built using sophisticated middleware frameworks. Communication in such systems is often realized using in terms of asynchronous events whose propagation is implemented by an underlying publish/subscribe service that hooks components into a generic event communication channel. Event correlation—a mechanism for monitoring and filtering events—has been introduced in some of these systems as an effective technique for reducing network traffic and computation time. Unfortunately, even though event correlation is used heavily in frameworks such as ACE/TAO’s real-time event-channel and in mission critical contexts such as Boeing’s Bold Stroke avionics middleware, the industry standard CORBA Component Model (CCM) does not include a specification of event correlation. While previous proposals for event correlation usually offer sophisticated facilities to detect combinations in the stream of incoming events, they have not been constructed to fit within the CCM type system, and they offer relatively little support for transforming and rearranging filtered events into meaningful output events. In this paper, we present the design rationale, syntax, and semantics for a new and highly flexible model for event correlation that is designed for integration into the CCM type system. Our model has been integrated and tested in the Cadena development and analysis framework, which has been designed to support development of mission-control applications in the Boeing Bold Stroke framework. Show less

This tool paper gives an overview of Cadena – an integrated environment for building and modeling systems built using the CORBA Component Model (CCM). Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition system semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM… Show more

This tool paper gives an overview of Cadena – an integrated environment for building and modeling systems built using the CORBA Component Model (CCM). Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition system semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM IDL, component assembly information, and Cadena specifications, and producing CORBA stubs and skeletons implemented in Java. Cadena has been applied to build applications in Boeing’s Bold Stroke framework for avionics mission-control systems. Cadena is implemented in IBM’s Eclipse open-source IDE and is freely available. Show less

The Simple Object Access Protocol (SOAP) is a dominant enabling technology in the field of web services. Web services demand high performance, security and extensibility. SOAP, being based on Extensible Markup Language (XML), inherits not only the advantages of XML, but its relatively poor performance. This makes SOAP a poor choice for many high-performance web services. In this paper, we present a new approach to implementing the SOAP protocol using caching on the SOAP server. This approach… Show more

The Simple Object Access Protocol (SOAP) is a dominant enabling technology in the field of web services. Web services demand high performance, security and extensibility. SOAP, being based on Extensible Markup Language (XML), inherits not only the advantages of XML, but its relatively poor performance. This makes SOAP a poor choice for many high-performance web services. In this paper, we present a new approach to implementing the SOAP protocol using caching on the SOAP server. This approach has significant performance advantages over current approaches while maintaining complete protocol compliance. We demonstrate its practicality by implementing a demonstration system under Linux, giving speedups of over 250% in our sample applications. Show less

Simple Object Access Protocol (SOAP) is a dominant enabling technology in the field of web services. Web services demand high performance, security and extensibility. SOAP, being based on Extensible Markup Language (XML), inherits not only the advantages of XML, but its relatively poor performance. This makes SOAP a poor choice for many high-performance web services. In this paper, we present new approaches to leverage multiple levels of caching and template-based customized response generation… Show more

Simple Object Access Protocol (SOAP) is a dominant enabling technology in the field of web services. Web services demand high performance, security and extensibility. SOAP, being based on Extensible Markup Language (XML), inherits not only the advantages of XML, but its relatively poor performance. This makes SOAP a poor choice for many high-performance web services. In this paper, we present new approaches to leverage multiple levels of caching and template-based customized response generation in a SOAP server to improve performance while maintaining complete protocol compliance. We demonstrate its practicality by implementing a demonstration system under Linux that provided speedups of over 600 % for sample applications. Show less

In this paper, we show how previous work on escape analysis can be adapted and extended to yield a static analysis that is efficient yet effective for reducing the number of interference dependence edges considered while slicing concurrent Java programs. The key idea is to statically detect situations where run-time heap objects are reachable from a single thread and use it to prune spurious interference dependence edges. We also show how this analysis can be extended to reduce the number of… Show more

In this paper, we show how previous work on escape analysis can be adapted and extended to yield a static analysis that is efficient yet effective for reducing the number of interference dependence edges considered while slicing concurrent Java programs. The key idea is to statically detect situations where run-time heap objects are reachable from a single thread and use it to prune spurious interference dependence edges. We also show how this analysis can be extended to reduce the number of ready dependence edges – dependences that capture indefinite delay due to Java synchronization constructs.

The analysis we describe has been implemented in the Bandera [9] slicer which is being applied to reduce the size of software models for model-checking. Using this implementation, we give experimental results that demonstrate the effectiveness of our approach. We believe leveraging escape information in the manner we describe is a crucial element in scaling slicing techniques to larger concurrent object-oriented programs. Show less

Firewalls, and packet classification in general, are be coming more and more significant as data rates soar and hackers become increasingly sophisticated - and more forceful. In this paper, we present a new packet classification approach that uses set theory to classify packets. This approach has significant theoretical ad vantages over current approaches. We demonstrate its practicality by implementing a firewall subsystem in Linux which approaches the performance of today's naive… Show more

Firewalls, and packet classification in general, are be coming more and more significant as data rates soar and hackers become increasingly sophisticated - and more forceful. In this paper, we present a new packet classification approach that uses set theory to classify packets. This approach has significant theoretical ad vantages over current approaches. We demonstrate its practicality by implementing a firewall subsystem in Linux which approaches the performance of today's naive packet-filtering implementations. Show less

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution. To form an effective basis for development of such systems, we believe that support for reasoning about correctness properties of… Show more

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution. To form an effective basis for development of such systems, we believe that support for reasoning about correctness properties of component-based designs is essential.In this paper, we present Cadena -- an integrated environment for building and modeling CCM systems. Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition system semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM IDL, component assembly information, and Cadena specifications, and producing CORBA stubs and skeletons implemented in Java. We are applying Cadena to avionics applications built using Boeing 's Bold Stroke framework. Show less

To support the trend toward component-based systems, the Cadena project aims to provide an Eclipse-based development environment that includes support for design, behavior modeling, formal reasoning, and automated code synthesis for systems built using the CORBA Component Model. In this paper, we describe the basic functionality of the Cadena tool, and summarize how it is currently being evaluated by industrial partners for use in developing high-assurance avionics applications.

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety-critical and mission-critical domains, component-based development is beginning to take hold as a mechanism for in-corporating non-functional aspects such as real-time, quality-of-service, and distribution.

At present, Java is a predominant language in the software industry and it is expanding it’s influence into areas of safety critical systems. The ever growing complexity of software along with the high assurance required by safety critical systems has prompted the software researchers to explore various forms of verification provided by model checking as it has been successfully used in electronic hardware industry.

Research has shown that model checking is a feasible option if the size… Show more

At present, Java is a predominant language in the software industry and it is expanding it’s influence into areas of safety critical systems. The ever growing complexity of software along with the high assurance required by safety critical systems has prompted the software researchers to explore various forms of verification provided by model checking as it has been successfully used in electronic hardware industry.

Research has shown that model checking is a feasible option if the size of the generated model is finite and small. To this end, static analysis techniques like slicing have been used to extract parts of the system relevant to the property being verified. Even so, these techniques are forced to take a conservative approach as rich features (encapsulation and dynamic dispatch) provided by OO languages such as Java and C++ make it hard to statically capture the dynamism of the given software system.

The contributions of this thesis address these issues. Object Flow Analysis (OFA) provides an approximation of the set of objects an expression can evaluate to at runtime in a Java program. The analysis has been implemented using Bandera Flow Analysis (BFA), which is a constraint-based style flow analysis framework implemented as part this thesis. The information from OFA has been used in the Slicer module in Bandera to reduce the size of the generated slice. It has also been found that use of allocation sites to partition the summary sets can help improve the precision of OFA in the presence of fields and arrays.

In summary, we have demonstrated that the information available from OFA enables the reduction of the state space of the generated model, and hence, improves the speed of model checking of Java programs. Show less