Visible to the public Biblio

Found 267 results

Book Chapter
Javier Camara, David Garlan, Gabriel Moreno, Bradley Schmerl.  2016.  Evaluating Trade-offs of Human Involvement in Self-adaptive Systems. Managing Trade-offs in Adaptable Software Architectures.

Software systems are increasingly called upon to autonomously manage their goals in changing contexts and environments, and under evolving requirements. In some circumstances, autonomous systems cannot be fully-automated but instead cooperate with human operators to maintain and adapt themselves. Furthermore, there are times when a choice should be made between doing a manual or automated repair. Involving operators in self-adaptation should itself be adaptive, and consider aspects such as the training, attention, and ability of operators. Not only do these aspects change from person to person, but they may change with the same person. These aspects make the choice of whether to involve humans non-obvious. Self-adaptive systems should trade-off whether to involve operators, taking these aspects into consideration along with other business qualities it is attempting to achieve. In this chapter, we identify the various roles that operators can perform in cooperating with self-adapting systems. We focus on humans as effectors-doing tasks which are difficult or infeasible to automate. We describe how we modified our self-adaptive framework, Rainbow, to involve operators in this way, which involved choosing suitable human models and integrating them into the existing utility trade-off decision models of Rainbow. We use probabilistic modeling and quantitative verification to analyze the trade-offs of involving humans in adaptation, and complement our study with experiments to show how different business preferences and modalities of human involvement may result in different outcomes.

Conference Paper
Thomas Glazier, Javier Camara, Bradley Schmerl, David Garlan.  2015.  Analyzing Resilience Properties of Different Topologies of Collective Adaptive Systems. Proceedings of the 3rd FoCAS Workshop on the Fundamentals of Collective Adaptive Systems.

Modern software systems are often compositions of entities that increasingly use self-adaptive capabilities to improve their behavior to achieve systemic quality goals. Self adaptive managers for each component system attempt to provide locally optimal results, but if they cooperated and potentially coordinated their efforts it might be possible to obtain more globally optimal results. The emergent properties that result from such composition and cooperation of self-adaptive systems are not well understood, difficult to reason about, and present a key challenge in the evolution of modern software systems. For example, the effects of coordination patterns and protocols on emergent properties, such as the resiliency of the collectives, need to be understood when designing these systems. In this paper we propose that probabilistic model checking of stochastic multiplayer games (SMG) provides a promising approach to analyze, understand, and reason about emergent properties in collectives of adaptive systems (CAS). Probabilistic Model Checking of SMGs is a technique particularly suited to analyzing emergent properties in CAS since SMG models capture: (i) the uncertainty and variability intrinsic to a CAS and its execution environment in the form of probabilistic and nondeterministic choices, and (ii) the competitive/cooperative aspects of the interplay among the constituent systems of the CAS. Analysis of SMGs allows us to reason about things like the worst case scenarios, which constitutes a new contribution to understanding emergent properties in CAS. We investigate the use of SMGs to show how they can be useful in analyzing the impact of communication topology for collections of fully cooperative systems defending against an external attack.

Dawid Gawel, Maciej Kosarzecki, Poorvi L. Vora, Hua Wu, Filip Zagórski.  2016.  Apollo - End-to-End Verifiable Internet Voting with Recovery from Vote Manipulation. E-VOTE-ID.

We present security vulnerabilities in the remote voting system Helios. We propose Apollo, a modified version of Helios, which addresses these vulnerabilities and could improve the feasibility of internet voting.

In particular, we note that Apollo does not possess Helios' major known vulnerability, where a dishonest voting terminal can change the vote after it obtains the voter's credential. With Apollo-lite, votes not authorized by the voter are detected by the public and prevented from being included in the tally.

The full version of Apollo enables a voter to prove that her vote was changed. We also describe a very simple protocol for the voter to interact with any devices she employs to check on the voting system, to enable frequent and easy auditing of encryptions and checking of the bulletin board.
 

Bradley Schmerl, Jeffrey Gennari, Alireza Sadeghi, Hamid Bagheri, Sam Malek, Javier Camara, David Garlan.  2016.  Architecture Modeling and Analysis of Security in Android Systems. 10th European Conference on Software Architecture (ECSA 2016).

Software architecture modeling is important for analyzing system quality attributes, particularly security. However, such analyses often assume that the architecture is completely known in advance. In many modern domains, especially those that use plugin-based frameworks, it is not possible to have such a complete model because the software system continuously changes. The Android mobile operating system is one such framework, where users can install and uninstall apps at run time. We need ways to model and analyze such architectures that strike a balance between supporting the dynamism of the underlying platforms and enabling analysis, particularly throughout a system’s lifetime. In this paper, we describe a formal architecture style that captures the modifiable architectures of Android systems, and that supports security analysis as a system evolves. We illustrate the use of the style with two security analyses: a predicatebased approach defined over architectural structure that can detect some common security vulnerabilities, and inter-app permission leakage determined by model checking. We also show how the evolving architecture of an Android device can be obtained by analysis of the apps on a device, and provide some performance evaluation that indicates that the architecture can be amenable for use throughout the system’s lifetime. 

Nirav Ajmeri, Hui Guo, Pradeep K. Murukannaiah, Munindar P. Singh.  2017.  Arnor: Modeling Social Intelligence via Norms to Engineer Privacy-Aware Personal Agents. :1–9.

We seek to address the challenge of engineering socially intelligent personal agents that are privacy-aware. We propose Arnor, a method, including a metamodel based on social constructs. Arnor incorporates social norms and goes beyond existing agent-oriented software engineering (AOSE) methods by systematically capturing how a personal agent’s actions influence the social experience it delivers. We conduct two empirical studies to evaluate Arnor. First, via a multiphase developer study, we show that Arnor simplifies application development. Second, via simulation experiments, we show that Arnor provides improved privacy-preserving social experience to end users than personal agents engineered using a traditional AOSE method.

Forget, Alain, Komanduri, Saranga, Acquisti, Alessandro, Christin, Nicolas, Cranor, Lorrie, Telang, Rahul.  2014.  Building the Security Behavior Observatory: An Infrastructure for Long-term Monitoring of Client Machines. IEEE Symposium and Bootcamp on the Science of Security (HotSoS) 2014.

We present an architecture for the Security Behavior Observatory
(SBO), a client-server infrastructure designed to
collect a wide array of data on user and computer behavior
from hundreds of participants over several years. The SBO
infrastructure had to be carefully designed to fulfill several
requirements. First, the SBO must scale with the desired
length, breadth, and depth of data collection. Second, we
must take extraordinary care to ensure the security of the
collected data, which will inevitably include intimate participant
behavioral data. Third, the SBO must serve our
research interests, which will inevitably change as collected
data is analyzed and interpreted. This short paper summarizes
some of our design and implementation benefits and
discusses a few hurdles and trade-offs to consider when designing
such a data collection system.

Darya Melicher(Kurilova), Yangqingwei Shi, Alex Potanin, Jonathan Aldrich.  2017.  A Capability-Based Module System for Authority Control. European Conference on Object-Oriented Programming (ECOOP).

The principle of least authority states that each component of the system should be given authority to access only the information and resources that it needs for its operation. This principle is fundamental to the secure design of software systems, as it helps to limit an application’s attack surface and to isolate vulnerabilities and faults. Unfortunately, current programming languages do not provide adequate help in controlling the authority of application modules, an issue that is particularly acute in the case of untrusted third-party extensions. In this paper, we present a language design that facilitates controlling the authority granted to each application module. The key technical novelty of our approach is that modules are firstclass, statically typed capabilities. First-class modules are essentially objects, and so we formalize our module system by translation into an object calculus and prove that the core calculus is typesafe and authority-safe. Unlike prior formalizations, our work defines authority non-transitively, allowing engineers to reason about software designs that use wrappers to provide an attenuated version of a more powerful capability. Our approach allows developers to determine a module’s authority by examining the capabilities passed as module arguments when the module is created, or delegated to the module later during execution. The type system facilitates this by identifying which objects provide capabilities to sensitive resources, and by enabling security architects to examine the capabilities passed into and out of a module based only on the module’s interface, without needing to examine the module’s implementation code. An implementation of the module system and illustrative examples in the Wyvern programming language suggest that our approach can be a practical way to control module authority.

Burcham, Morgan, Al-Zyoud, Mahran, Carver, Jeffrey C., Alsaleh, Mohammed, Du, Hongying, Gilani, Fida, Jiang, Jun, Rahman, Akond, Kafalı, Özgür, Al-Shaer, Ehab et al..  2017.  Characterizing Scientific Reporting in Security Literature: An Analysis of ACM CCS and IEEE S&P Papers. Proceedings of the Hot Topics in Science of Security: Symposium and Bootcamp. :13–23.

Scientific advancement is fueled by solid fundamental research, followed by replication, meta-analysis, and theory building. To support such advancement, researchers and government agencies have been working towards a "science of security". As in other sciences, security science requires high-quality fundamental research addressing important problems and reporting approaches that capture the information necessary for replication, meta-analysis, and theory building. The goal of this paper is to aid security researchers in establishing a baseline of the state of scientific reporting in security through an analysis of indicators of scientific research as reported in top security conferences, specifically the 2015 ACM CCS and 2016 IEEE S&P proceedings. To conduct this analysis, we employed a series of rubrics to analyze the completeness of information reported in papers relative to the type of evaluation used (e.g. empirical study, proof, discussion). Our findings indicated some important information is often missing from papers, including explicit documentation of research objectives and the threats to validity. Our findings show a relatively small number of replications reported in the literature. We hope that this initial analysis will serve as a baseline against which we can measure the advancement of the science of security.

Nirav Ajmeri, Jiaming Jiang, Rada Y. Chirkova, Jon Doyle, Munindar P. Singh.  2016.  Coco: Runtime Reasoning about Conflicting Commitments. Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI). :1–7.

To interact effectively, agents must enter into commitments. What should an agent do when these commitments conflict? We describe Coco, an approach for reasoning about which specific commitments apply to specific parties in light of general types of commitments, specific circumstances, and dominance relations among specific commitments. Coco adapts answer-set programming to identify a maximalsetofnondominatedcommitments. It provides a modeling language and tool geared to support practical applications.

[Anonymous].  2017.  COCONUT: Seamless Scale-out of Network Elements. EuroSys.

A key use of software-defined networking is to enable scale-out of network data plane elements. Naively scaling networking elements, however, can cause incorrect security responses. For example, we show that an IDS system which operates correctly as a single network element can erroneously and permanently block hosts when it is replicated. Similarly, a scaled-out firewall can incorrectly block hosts.

In this paper, we provide a system, COCONUT, for seamless scale-out of network forwarding elements; that is, an SDN application programmer can program to what functionally appears to be a single forwarding element, but which may be replicated behind the scenes. To do this, we identify the key property for seamless scale out, weak causality, and guarantee it through a practical and scalable implementation of vector clocks in the data plane. We formally prove that COCONUT enables seamless scale out of networking elements, i.e., the user-perceived behavior of any COCONUT element implemented with a distributed set of concurrent replicas is provably indistinguishable from its singleton implementation. Finally, we build a prototype of COCONUT and experimentally demonstrate its correct behavior. We also show that its abstraction enables a more efficient implementation of seamless scale-out compared to a naive baseline.

This work was funded by the SoS lablet at the University of Illinois at Urbana-Champaign.

Authors: Soudeh Ghorbani, P. Brighten Godfrey (UIUC)
Munindar P. Singh.  2022.  Consent as a Foundation for Responsible Autonomy. Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI). 36
This paper focuses on a dynamic aspect of responsible autonomy, namely, to make intelligent agents be responsible at run time. That is, it considers settings where decision making by agents impinges upon the outcomes perceived by other agents. For an agent to act responsibly, it must accommodate the desires and other attitudes of its users and, through other agents, of their users. The contribution of this paper is twofold. First, it provides a conceptual analysis of consent, its benefits and misuses, and how understanding consent can help achieve responsible autonomy. Second, it outlines challenges for AI (in particular, for agents and multiagent systems) that merit investigation to form as a basis for modeling consent in multiagent systems and applying consent to achieve responsible autonomy.
Blue Sky Track
Michael Coblenz, Robert Seacord, Brad Myers, Joshua Sunshine, Jonathan Aldrich.  2015.  A Course-Based Usability Analysis of Cilk Plus and OpenMP. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC) .

Cilk Plus and OpenMP are parallel language ex-tensions for the C and C++ programming languages. The CPLEX Study Group of the ISO/IEC C Standards Committee is developing a proposal for a parallel programming extension to C that combines ideas from Cilk Plus and OpenMP. We conducted a preliminary comparison of Cilk Plus and OpenMP in a master's level course on security to evaluate the design tradeoffs in the usability and security of these two approaches. The eventual goal is to inform decision making within the committee. We found several usability problems worthy of further investigation based on student performance, including declaring and using reductions, multi-line compiler directives, and the understandability of task assignment to threads.

Amit K. Chopra, Munindar P. Singh.  2015.  Cupid: Commitments in Relational Algebra. Proceedings of the 23rd Conference on Artificial Intelligence (AAAI). :1–8.

We propose Cupid, a language for specifying commitments that supports their information-centric aspects, and offers crucial benefits.  One, Cupid is first-order, enabling a systematic treatment of commitment instances.  Two, Cupid supports features needed for real-world scenarios such as deadlines, nested commitments, and complex event expressions for capturing the lifecycle of commitment instances.  Three, Cupid maps to relational database queries and thus provides a set-based semantics for retrieving commitment instances in states such as being violated,discharged, and so on.  We prove that Cupid queries are safe.  Four,to aid commitment modelers, we propose the notion of well-identified commitments, and finitely violable and finitely expirable commitments.  We give syntactic restrictions for obtaining such commitments.

Amit K. Chopra, Munindar P. Singh.  2016.  Custard: Computing Norm States over Information Stores. Proceedings of the International Conference on Autonomous Agents and MultiAgent Systems (AAMAS). :1–10.

Norms provide a way to model the social architecture of a sociotechnical system (STS) and are thus crucial for understanding how such a system supports secure collaboration between principals,that is, autonomous parties such as humans and organizations. Accordingly, an important challenge is to compute the state of a norm instance at runtime in a sociotechnical system.

Custard addresses this challenge by providing a relational syntax for schemas of important norm types along with their canonical lifecycles and providing a mapping from each schema to queries that compute instances of the schema in different lifecycle stages.  In essence, Custard supports a norm-based abstraction layer over underlying information stores such as databases and event logs. Specifically, it supports deadlines; complex events, including those based on aggregation; and norms that reference other norms.

We prove important correctness properties for Custard, including stability (once an event has occurred, it has occurred forever) and safety (a query returns a finite set of tuples).  Our compiler generates SQL queries from Custard specifications.  Writing out such SQL queries by hand is tedious and error-prone even for simple norms, thus demonstrating Custard's practical benefits.

Du Li, Alex Potanin, Jonathan Aldrich.  2015.  Delegation vs Inheritance for Typestate Analysis. European Conference on Object-Oriented Programming, Formal Techniques for Java-like Programs track.

For several decades, inheritance and delegation have been widely adopted for code reuse in object-oriented languages. Though extensive research has explored the expressiveness of these techniques, little is known about how the choice between them affects formal reasoning. In this paper, we explore this question by describing two core languages that are identical except for the use of inheritance and delegation, respectively. We add support for formal reasoning about typestate to both languages, and evaluate the complexity of the formal semantics and compare the example specifications. Our study suggests that our variant of delegation can substantially simplify typestate reasoning, while inheritance makes code more succinct in the case where open recursion is used.

Yu Wang, University of Illinois at Urbana-Champaign, Matthew Hale, University of Illinois at Urbana-Champaign, Magnus Egerstedt, University of Illinois at Urbana-Champaign, Geir Dullerud, University of Illinois at Urbana-Champaign.  2017.  Differentially Private Objective Functions in Distributed Cloud-based Optimization. 20th World Congress of the International Federations of Automatic Control (IFAC 2017 World Congress).

Abstract—In this work, we study the problem of keeping the objective functions of individual agents "-differentially private in cloud-based distributed optimization, where agents are subject to global constraints and seek to minimize local objective functions. The communication architecture between agents is cloud-based – instead of communicating directly with each other, they oordinate by sharing states through a trusted cloud computer. In this problem, the difficulty is twofold: the objective functions are used repeatedly in every iteration, and the influence of  erturbing them extends to other agents and lasts over time. To solve the problem, we analyze the propagation of perturbations on objective functions over time, and derive an upper bound on them. With the upper bound, we design a noise-adding mechanism that randomizes the cloudbased distributed optimization algorithm to keep the individual objective functions "-differentially private. In addition, we study the trade-off between the privacy of objective functions and the performance of the new cloud-based distributed optimization algorithm with noise. We present simulation results to numerically verify the theoretical results presented.

Yutaka Tsutano, Shakthi Bachala, Witawas Srisa-an, Gregg Rothermel, Jackson Dinh.  2017.  An Efficient, Robust, and Scalable Approach for Analyzing Interacting Android Apps. 39th International Conference on Software Engineering.

When multiple apps on an Android platform interact, faults and security vulnerabilities can occur. Software engineers need to be able to analyze interacting apps to detect such problems. Current approaches for performing such analyses, however, do not scale to the numbers of apps that may need to be considered, and thus, are impractical for application to realworld scenarios. In this paper, we introduce JITANA, a program analysis framework designed to analyze multiple Android apps simultaneously. By using a classloader-based approach instead of a compiler-based approach such as SOOT, JITANA is able to simultaneously analyze large numbers of interacting apps, perform on-demand analysis of large libraries, and effectively analyze dynamically generated code. Empirical studies of JITANA show that it is substantially more efficient than a state-of-theart approach, and that it can effectively and efficiently analyze complex apps including Facebook, Pokemon Go, and Pandora ´ that the state-of-the-art approach cannot handle.

Zack Coker, Michael Maass, Tianyuan Ding, Claire Le Goues, Joshua Sunshine.  2015.  Evaluating the Flexibility of the Java Sandbox. ACSAC Annual Computer Security Applications Conference.

The ubiquitously-installed Java Runtime Environment (JRE) provides a complex, flexible set of mechanisms that support the execution of untrusted code inside a secure sandbox. However, many recent exploits have successfully escaped the sandbox, allowing attackers to infect numerous Java hosts. We hypothesize that the Java security model affords developers more flexibility than they need or use in practice, and thus its complexity compromises security without improving practical functionality. We describe an empirical study of the ways benign open-source Java applications use and interact with the Java security manager. We found that developers regularly misunderstand or misuse Java security mechanisms, that benign programs do not use all of the vast flexibility afforded by the Java security model, and that there are clear differences between the ways benign and exploit programs interact with the security manager. We validate these results by deriving two restrictions on application behavior that restrict (1) security manager modifications and (2) privilege escalation. We demonstrate that enforcing these rules at runtime stop a representative proportion of modern Java 7 exploits without breaking backwards compatibility with benign applications. These practical rules should be enforced in the JRE to fortify the Java sandbox.

Morgan Evans, Jaspreet Bhatia, Sudarshan Wadkar, Travis Breaux.  2017.  An Evaluation of Constituency-based Hyponymy Extraction from Privacy Policies . 25th IEEE International Requirements Engineering Conference.

Requirements analysts can model regulated data practices to identify and reason about risks of noncompliance. If terminology is inconsistent or ambiguous, however, these models and their conclusions will be unreliable. To study this problem, we investigated an approach to automatically construct an information type ontology by identifying information type hyponymy in privacy policies using Tregex patterns. Tregex is a utility to match regular expressions against constituency parse trees, which are hierarchical expressions of natural language clauses, including noun and verb phrases. We discovered the Tregex patterns by applying content analysis to 30 privacy policies from six domains (shopping, telecommunication, social networks, employment, health, and news.) From this dataset, three semantic and four lexical categories of hyponymy emerged based on category completeness and wordorder. Among these, we identified and empirically evaluated 72 Tregex patterns to automate the extraction of hyponyms from privacy policies. The patterns match information type hyponyms with an average precision of 0.72 and recall of 0.74. 

Jiaming Jiang, Nirav Ajmeri, Rada Y. Chirkova, Jon Doyle, Munindar P. Singh.  2016.  Expressing and Reasoning about Conflicting Norms in Cybersecurity: Poster. Proceedings of the International Symposium and Bootcamp on the Science of Security (HotSoS). :1–2.

Secure collaboration requires the collaborating parties to apply the
right policies for their interaction.  We adopt a notion of
conditional, directed norms as a way to capture the standards of
correctness for a collaboration.  How can we handle conflicting norms?
We describe an approach based on knowledge of what norm dominates what
norm in what situation.  Our approach adapts answer-set programming to
compute stable sets of norms with respect to their computed conflicts
and dominance.  It assesses agent compliance with respect to those
stable sets.  We demonstrate our approach on a healthcare scenario.

Amit K. Chopra, Munindar P. Singh.  2016.  From Social Machines to Social Protocols: Software Engineering Foundations for Sociotechnical Systems. Proceedings of the 25th International World Wide Web Conference.

The overarching vision of social machines is to facilitate social processes by having computers provide administrative support. We conceive of a social machine as a sociotechnical system (STS): a software-supported system in which autonomous principals such as humans and organizations interact to exchange information and services.  Existing approaches for social machines emphasize the technical aspects and inadequately support the meanings of social processes, leaving them informally realized in human interactions. We posit that a fundamental rethinking is needed to incorporate accountability, essential for addressing the openness of the Web and the autonomy of its principals.

We introduce Interaction-Oriented Software Engineering (IOSE) as a paradigm expressly suited to capturing the social basis of STSs. Motivated by promoting openness and autonomy, IOSE focuses not on implementation but on social protocols, specifying how social relationships, characterizing the accountability of the concerned parties, progress as they interact.  Motivated by providing computational support, IOSE adopts the accountability representation to capture the meaning of a social machine's states and transitions.

We demonstrate IOSE via examples drawn from healthcare.  We reinterpret the classical software engineering (SE) principles for the STS setting and show how IOSE is better suited than traditional software engineering for supporting social processes.  The contribution of this paper is a new paradigm for STSs, evaluated via conceptual analysis.

Akond Rahman, Effat Farhana, Chris Parnin, Laurie Williams.  2020.  Gang of Eight: A Defect Taxonomy for Infrastructure as Code Scripts. International Conference of Softare Engineering (ICSE).

Defects in infrastructure as code (IaC) scripts can have serious
consequences, for example, creating large-scale system outages. A
taxonomy of IaC defects can be useful for understanding the nature
of defects, and identifying activities needed to fix and prevent
defects in IaC scripts. The goal of this paper is to help practitioners
improve the quality of infrastructure as code (IaC) scripts by developing
a defect taxonomy for IaC scripts through qualitative analysis.
We develop a taxonomy of IaC defects by applying qualitative analysis
on 1,448 defect-related commits collected from open source
software (OSS) repositories of the Openstack organization. We conduct
a survey with 66 practitioners to assess if they agree with the
identified defect categories included in our taxonomy. We quantify
the frequency of identified defect categories by analyzing 80,425
commits collected from 291 OSS repositories spanning across 2005
to 2019.


Our defect taxonomy for IaC consists of eight categories, including
a category specific to IaC called idempotency (i.e., defects that
lead to incorrect system provisioning when the same IaC script is
executed multiple times). We observe the surveyed 66 practitioners
to agree most with idempotency. The most frequent defect category
is configuration data i.e., providing erroneous configuration data
in IaC scripts. Our taxonomy and the quantified frequency of the
defect categories may help in advancing the science of IaC script
quality.

Michael Coblenz, Whitney Nelson, Jonathan Aldrich, Brad Myers, Joshua Sunshine.  2017.  Glacier: Transitive Class Immutability for Java. 39th International Conference on Software Engineering.

Though immutability has been long-proposed as a way to prevent bugs in software, little is known about how to make immutability support in programming languages effective for software engineers. We designed a new formalism that extends Java to support transitive class immutability, the form of immutability for which there is the strongest empirical support, and implemented that formalism in a tool called Glacier. We applied Glacier successfully to two real-world systems. We also compared Glacier to Java’s final in a user study of twenty participants. We found that even after being given instructions on how to express immutability with final, participants who used final were unable to express immutability correctly, whereas almost all participants who used Glacier succeeded. We also asked participants to make specific changes to immutable classes and found that participants who used final all incorrectly mutated immutable state, whereas almost all of the participants who used Glacier succeeded. Glacier represents a promising approach to enforcing immutability in Java and provides a model for enforcement in other languages.