Many decision-making scenarios, e.g., public policy, healthcare, business, and disaster response, require accommodating the preferences of multiple stakeholders. We offer the first formal treatment of reasoning with multi-stakeholder qualitative preferences in a setting where stakeholders express their preferences in a qualitative preference language, e.g., CP-net, CI-net, TCP-net, CP-Theory. We introduce a query language for expressing queries against such preferences over sets of outcomes that satisfy specified criteria, e.g., ψ1PAψ2 (read loosely as the set of outcomes satisfying ψ1 that are preferred over outcomes satisfying ψ2 by a set of stakeholders A). Motivated by practical application scenarios, we introduce and analyze several alternative semantics for such queries, and examine their interrelationships. We provide a provably correct algorithm for answering multi-stakeholder qualitative preference queries using model checking in alternation-free μ-calculus. We present experimental results that demonstrate the feasibility of our approach.

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

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

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

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

We present a framework for reasoning with preferences in the context of Goal-Oriented Requirements Engineering (GORE). Our choice of preference language, conditional importance networks (CI-nets), is motivated by the occurrence in requirements engineering of qualitative preferences and tradeoffs involving sets of items; such preferences are expressed more naturally in CI-nets than in other representations. Building on our past experience with CI-nets, we are improving the scalability and usability of CI-nets for specifying and analyzing requirements preferences. We discuss our ongoing work and long-term plans, including efforts to develop more efficient methods to identify conflicting preferences among possible requirements, guide negotiation of resolutions to such conflicts, and improve traceability and comprehension of requirements preferences.

In many applications such as service-oriented computing, users often prefer some compositions over the others based on their preferences over non-functional attributes such as security and cost. After a composition is deployed, apart from changes in the functional requirements, service-oriented architectures often have to deal with changes in the user preferences over the non-functional attributes and/or repository of available components. We formulate the problem of adaptation as iterative substitution of appropriate components in a composition, and provide two algorithms that produce a sequence of increasingly preferred adaptations with time: a fast algorithm that searches for preferred adaptations by improving the valuation of the relatively more important attributes, and another that is computationally more intensive but guaranteed to produce at least one preferred adaptation, if one exists.

Spread of infections (diseases, ideas, etc.) in a networkcan be modeled as the evolution of states of nodes ina graph as a function of the states of their neighbors.Given an initial configuration of a network in which asubset of the nodes have been infected, and an infectionpropagation function that specifies how the states ofthe nodes evolve over time, we show how to use modelchecking to identify, verify, and evaluate the effectivenessof intervention policies for containing the propagationof infection over such networks.

For a Web service composition to satisfy a user's needs, it must not only provide the desired functionality, but also have nonfunctional properties (e.g., reliability, availability, cost) that are acceptable to the user. In the recent past, several techniques have been developed and deployed to identify a composite service that conforms to the functional requirements and is also optimal with respect to the user-defined preferences over non-functional properties. However, these composition techniques are limited to using one formalism for specifying the required functionality, in short, the existing techniques cannot identify optimal (w.r.t. non-functional properties) composite services that are required to satisfy functional requirements described in multiple formalisms. We have previously proposed a meta-framework for service composition that involves decomposing the required functionality into a boolean combination of atomic requirements, which are expressed using different formalisms. This meta-framework supports the use of multiple formalisms and their corresponding composition algorithms within a single scenario. In this paper, we integrate support for unconditional preferences over nonfunctional requirements into this composition meta-framework. We show that for a large class of problems, local selection of preferred service(s) can yield the most preferred composite service that satisfies the desired functional requirements.

In goal-oriented requirements engineering, a goal model graphically represents relationships between the required goals (functional requirements), tasks (realizations of goals), and optional goals (non-functional properties) involved in designing a system. It may, however, be impossible to find a design that fulfills all required goals and all optional goals. In such cases, it is useful to find designs that provide the required functionality while satisfying the most preferred set of optional goals under the goal model's constraints. We present an approach that considers expressive qualitative preferences over optional goals, as these can model interacting and/or mutually exclusive subgoals. Our framework employs a model checking-based method for reasoning with qualitative preferences to identify the most preferred alternative(s). We evaluate our approach using existing goal models from the literature.

Dominance testing, the problem of determining whether an outcome is preferred over another, is of fundamental importance in many applications. Hence, there is a need for algorithms and tools for dominance testing. CP-nets and TCP-nets are some of the widely studied languages for representing and reasoning with preferences. We reduce dominance testing in TCP-nets to reachability analysis in a graph of outcomes. We provide an encoding of TCP-nets in the form of a Kripke structure for CTL. We show how to compute dominance using NuSMV, a model checker for CTL. We present results of experiments that demonstrate the feasibility of our approach to dominance testing.