Biblio

Found 210 results

Filters: Keyword is UIUC  [Clear All Filters]
2017-02-15
Ross Koppel, University of Pennsylvania, Sean W. Smith, Dartmouth College, Jim Blythe, University of Southern California, Vijay Kothari, Dartmouth College.  2015.  Workarounds to Computer Access in Healthcare Organizations: You Want My Password or a Dead Patient? Studies in Health Technology and Informatics Driving Quality Informatics: Fulfilling the Promise . 208

Workarounds to computer access in healthcare are sufficiently common that they often go unnoticed. Clinicians focus on patient care, not cybersecurity. We argue and demonstrate that understanding workarounds to healthcare workers’ computer access requires not only analyses of computer rules, but also interviews and observations with clinicians. In addition, we illustrate the value of shadowing clinicians and conducing focus groups to understand their motivations and tradeoffs for circumvention. Ethnographic investigation of the medical workplace emerges as a critical method of research because in the inevitable conflict between even well-intended people versus the machines, it’s the people who are the more creative, flexible, and motivated. We conducted interviews and observations with hundreds of medical workers and with 19 cybersecurity experts, CIOs, CMIOs, CTO, and IT workers to obtain their perceptions of computer security. We also shadowed clinicians as they worked. We present dozens of ways workers ingeniously circumvent security rules. The clinicians we studied were not “black hat” hackers, but just professionals seeking to accomplish their work despite the security technologies and regulations.
 

Ross Koppel, University of Pennsylvania, Sean W. Smith, Dartmouth College, Jim Blythe, University of Southern California, Vijay Kothari, Dartmouth College.  2015.  Workarounds to Computer Access in Healthcare Organizations: You Want My Password or a Dead Patient? Information Technology and Communications in Health.

Workarounds to computer access in healthcare are sufficiently common that they often go unnoticed. Clinicians focus on patient care, not cybersecurity. We argue and demonstrate that understanding workarounds to healthcare workers’ computer access requires not only analyses of computer rules, but also interviews and observations with clinicians. In addition, we illustrate the value of shadowing clinicians and conducing focus groups to understand their motivations and tradeoffs for circumvention. Ethnographic investigation of the medical workplace emerges as a critical method of research because in the inevitable conflict between even well-intended people versus the machines, it’s the people who are the more creative, flexible, and motivated. We conducted interviews and observations with hundreds of medical workers and with 19 cybersecurity experts, CIOs, CMIOs, CTO, and IT workers to obtain their perceptions of computer security. We also shadowed clinicians as they worked. We present dozens of ways workers ingeniously circumvent security rules. The clinicians we studied were not “black hat” hackers, but just professionals seeking to accomplish their work despite the security technologies and regulations.

Wenxuan Zhou, University of Illinois at Urbana-Champaign, Dong Jin, Illinois Institute of Technology, Jason Croft, University of Illinois at Urbana-Champaign, Matthew Caesar, University of Illinois at Urbana-Champaign, P. Brighten Godfrey, University of Illinois at Urbana-Champaign.  2015.  Enforcing Generalized Consistency Properties in Software-Defined Networks. 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2015).

It is critical to ensure that network policy remains consistent during state transitions. However, existing techniques impose a high cost in update delay, and/or FIB space. We propose the Customizable Consistency Generator (CCG), a fast and generic framework to support customizable consistency policies during network updates. CCG effectively reduces the task of synthesizing an update plan under the constraint of a given consistency policy to a verification problem, by checking whether an update can safely be installed in the network at a particular time, and greedily processing network state transitions to heuristically minimize transition delay. We show a large class of consistency policies are guaranteed by this greedy jeuristic alone; in addition, CCG makes judicious use of existing heavier-weight network update mechanisms to provide guarantees when necessary. As such, CCG nearly achieves the “best of both worlds”: the efficiency of simply passing through updates in most cases, with the consistency guarantees of more heavyweight techniques. Mininet and physical testbed evaluations demonstrate CCG’s capability to achieve various types of consistency, such as path and bandwidth properties, with zero switch memory overhead and up to a 3× delay reduction compared to previous solutions.

2015-11-11
Ning Liu, Illinois Institute of Technology, Adnan Haider, Illinois Institute of Technology, Xian-He Sun, Illinois Institute of Technology, Dong Jin, Illinois Institute of Technology.  2015.  FatTreeSim: Modeling a Large-scale Fat-Tree Network for HPC Systems and Data Centers Using Parallel and Discrete Even Simulation. ACM SIGSIM Conference on Principles of Advanced Discrete Simulation.

Fat-tree topologies have been widely adopted as the communication network in data centers in the past decade. Nowa- days, high-performance computing (HPC) system designers are considering using fat-tree as the interconnection network for the next generation supercomputers. For extreme-scale computing systems like the data centers and supercomput- ers, the performance is highly dependent on the intercon- nection networks. In this paper, we present FatTreeSim, a PDES-based toolkit consisting of a highly scalable fat-tree network model, with the goal of better understanding the de- sign constraints of fat-tree networking architectures in data centers and HPC systems, as well as evaluating the applica- tions running on top of the network. FatTreeSim is designed to model and simulate large-scale fat-tree networks up to millions of nodes with protocol-level fidelity. We have con- ducted extensive experiments to validate and demonstrate the accuracy, scalability and usability of FatTreeSim. On Argonne Leadership Computing Facility’s Blue Gene/Q sys- tem, Mira, FatTreeSim is capable of achieving a peak event rate of 305 M/s for a 524,288-node fat-tree model with a total of 567 billion committed events. The strong scaling experiments use up to 32,768 cores and show a near linear scalability. Comparing with a small-scale physical system in Emulab, FatTreeSim can accurately model the latency in the same fat-tree network with less than 10% error rate for most cases. Finally, we demonstrate FatTreeSim’s usability through a case study in which FatTreeSim serves as the net- work module of the YARNsim system, and the error rates for all test cases are less than 13.7%.

Best Paper Award

Jiaqi Yan, Illinois Institute of Technology, Dong Jin, Illinois Institute of Technology.  2015.  A Virtual Time System for Linux-container-based Emulation of Software-defined Networks. ACM SIGSIM Conference on Principles of Advanced Discrete Simulation.

Realistic and scalable testing systems are critical to evaluate network applications and protocols to ensure successful real system deployments. Container-based network emula- tion is attractive because of the combination of many desired features of network simulators and physical testbeds . The success of Mininet, a popular software- defined networking (SDN) emulation testbed, demonstrates the value of such approach that we can execute unmodified binary code on a large- scale emulated network with lightweight OS-level vir- tualization techniques. However, an ordinary network em- ulator uses the system clock across all the containers even if a container is not being scheduled to run. This leads to the issue of temporal fidelity, especially with high workloads. Virtual time sheds the light on the issue of preserving tem- poral fidelity for large-scale emulation. The key insight is to trade time with system resources via precisely scaling the time of interactions between containers and physical devices by a factor of n, hence, making an emulated network ap- pear to be n times faster from the viewpoints of applications in the container. In this paper, we develop a lightweight Linux-container-based virtual time system and integrate the system to Mininet for fidelity and scalability enhancement. We also design an adaptive time dilation scheduling mod- ule for balancing speed and accuracy. Experimental results demonstrate that (1) with virtual time, Mininet is able to accurately emulate a network n times larger in scale, where n is the scaling factor, with the system behaviors closely match data obtained from a physical testbed; and (2) with the adaptive time dilation scheduling, we reduce the running time by 46% with little accuracy loss. Finally, we present a case study using the virtual-time-enabled Mininet to evalu- ate the limitations of equal-cost multi-path (ECMP) routing in a data center network.

2016-12-01
Huoran Li, Peking University, Xuan Lu, Peking University, Xuanzhe Liu, Peking University, Tao Xie, University of Illinois at Urbana-Champaign, Kaigui Bian, Peking University, Felix Xiaozhu Lin, Purdue University, Qiaozhu Mei, University of Michigan, Feng Feng, Wandoujia Lab.  2015.  Characterizing Smartphone Usage Patterns from Millions of Android Users. 2015 Internet Measurement Conference (IMC 2015).

The prevalence of smart devices has promoted the popularity of mobile applications (a.k.a. apps) in recent years. A number of interesting and important questions remain unanswered, such as why a user likes/dislikes an app, how an app becomes popular or eventually perishes, how a user selects apps to install and interacts with them, how frequently an app is used and how much trac it generates, etc. This paper presents an empirical analysis of app usage behaviors collected from millions of users of Wandoujia, a leading Android app marketplace in China. The dataset covers two types of user behaviors of using over 0.2 million Android apps, including (1) app management activities (i.e., installation, updating, and uninstallation) of over 0.8 million unique users and (2) app network trac from over 2 million unique users. We explore multiple aspects of such behavior data and present interesting patterns of app usage. The results provide many useful implications to the developers, users, and disseminators of mobile apps.

2016-12-12
Maurice Heemels, Geir Dullerud, University of Illinois at Urbana-Champaign, Andrew Teel.  2015.  A Lifting Approach to L2-gain Analysis of Periodic Event-triggered and Switching Sampled-data Control Systems. IEEE International Conference on Decision and Control (CDC 2015).

In this work we are interested in the stability and L2-gain of hybrid systems with linear flow dynamics, periodic time-triggered jumps and nonlinear possibly set-valued jump maps. This class of hybrid systems includes various interesting applications such as periodic event-triggered control. In this paper we also show that sampled-data systems with arbitrarily switching controllers can be captured in this framework by requiring the jump map to be set-valued. We provide novel conditions for the internal stability and L2-gain analysis of these systems adopting a lifting-based approach. In particular, we establish that the internal stability and contractivity in terms of an L2-gain smaller than 1 are equivalent to the internal stability and contractivity of a particular discretetime set-valued nonlinear system. Despite earlier works in this direction, these novel characterisations are the first necessary and sufficient conditions for the stability and the contractivity of this class of hybrid systems. The results are illustrated through multiple new examples.

2016-11-15
Ken Keefre, University of Illinolis at Urbana-Champaing, William H. Sanders, University of Illinois at Urbana-Champaign.  2015.  Reliability Analysis with Dynamic Reliability Block Diagrams in the Mobius Modeling Tool. 9th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS 2015).

Reliability block diagram (RBD) models are a commonly used reliability analysis method. For static RBD models, combinatorial solution techniques are easy and efficient. However, static RBDs are limited in their ability to express varying system state, dependent events, and non-series-parallel topologies. A recent extension to RBDs, called Dynamic Reliability Block Diagrams (DRBD), has eliminated those limitations. This tool paper details the RBD implementation in the M¨obius modeling framework and provides technical details for using RBDs independently or in composition with other M¨obius modeling formalisms. The paper explains how the graphical front-end provides a user-friendly interface for specifying RBD models. The back-end implementation that interfaces with the M¨obius AFI to define and generate executable models that the M¨obius tool uses to evaluate system metrics is also detailed.

2015-12-02
Gul Agha, University of Illinois at Urbana-Champaign.  2014.  Actors Programming for the Mobile Cloud. IEEE 13th International Symposium on Parallel and Distributed Computing,.

Abstract—Actor programming languages provide the kind of inherent parallelism that is needed for building applications in the mobile cloud. This is because the Actor model provides encapsulation (isolation of local state), fair scheduling, location transparency, and locality of reference. These properties facilitate building secure, scalable concurrent systems. Not surprisingly, very large-scale applications such as Facebook chat service and Twitter have been written in actor languages. The paper introduces the basics of the actor model and gives a high-level overview of the problem of coordination in actor systems. It then describes several novel methods for reasoning about concurrent systems that are both effective and scalable.

2014-10-24
Kothari, Vijay, Blythe, Jim, Smith, Sean, Koppel, Ross.  2014.  Agent-based Modeling of User Circumvention of Security. 1st International Workshop on Agents and CyberSecurity. :5:1–5:4.

Security subsystems are often designed with flawed assumptions arising from system designers' faulty mental models. Designers tend to assume that users behave according to some textbook ideal, and to consider each potential exposure/interface in isolation. However, fieldwork continually shows that even well-intentioned users often depart from this ideal and circumvent controls in order to perform daily work tasks, and that "incorrect" user behaviors can create unexpected links between otherwise "independent" interfaces. When it comes to security features and parameters, designers try to find the choices that optimize security utility–-except these flawed assumptions give rise to an incorrect curve, and lead to choices that actually make security worse, in practice. We propose that improving this situation requires giving designers more accurate models of real user behavior and how it influences aggregate system security. Agent-based modeling can be a fruitful first step here. In this paper, we study a particular instance of this problem, propose user-centric techniques designed to strengthen the security of systems while simultaneously improving the usability of them, and propose further directions of inquiry.

2015-11-16
Cuong Pham, University of Illinois at Urbana-Champaign, Zachary J. Estrada, University of Illinois at Urbana-Champaign, Phuong Cao, University of Illinois at Urbana-Champaign, Zbigniew Kalbarczyk, University of Illinois at Urbana-Champaign, Ravishankar K. Iyer, University of Illinois at Urbana-Champaign.  2014.  Building Reliable and Secure Virtual Machines using Architectural Invariants. IEEE Security and Privacy. 12(5):82-85.

Reliability and security tend to be treated separately because they appear orthogonal: reliability focuses on accidental failures, security on intentional attacks. Because of the apparent dissimilarity between the two, tools to detect and recover from different classes of failures and attacks are usually designed and implemented differently. So, integrating support for reliability and security in a single framework is a significant challenge.

Here, we discuss how to address this challenge in the context of cloud computing, for which reliability and security are growing concerns. Because cloud deployments usually consist of commodity hardware and software, efficient monitoring is key to achieving resiliency. Although reliability and security monitoring might use different types of analytics, the same sensing infrastructure can provide inputs to monitoring modules.

We split monitoring into two phases: logging and auditing. Logging captures data or events; it constitutes the framework’s core and is common to all monitors. Auditing analyzes data or events; it’s implemented and operated independently by each monitor. To support a range of auditing policies, logging must capture a complete view, including both actions and states of target systems. It must also provide useful, trustworthy information regarding the captured view.

We applied these principles when designing HyperTap, a hypervisor-level monitoring framework for virtual machines (VMs). Unlike most VM-monitoring techniques, HyperTap employs hardware architectural invariants (hardware invariants, for short) to establish the root of trust for logging. Hardware invariants are properties defined and enforced by a hardware platform (for example, the x86 instruction set architecture). Additionally, HyperTap supports continuous, event-driven VM monitoring, which enables both capturing the system state and responding rapidly to actions of interest.

2015-11-17
Ray Essick, University of Illinois at Urbana-Champaign, Ji-Woong Lee, Pennsylvania State University, Geir Dullerud, University of Illinois at Urbana-Champaign.  2014.  Control of Linear Switched Systems with Receding Horizon Modal Information. IEEE Transactions on Automatic Control. 59(9)

We provide an exact solution to two performance problems—one of disturbance attenuation and one of windowed variance minimization—subject to exponential stability. Considered are switched systems, whose parameters come from a finite set and switch according to a language such as that specified by an automaton. The controllers are path-dependent, having finite memory of past plant parameters and finite foreknowledge of future parameters. Exact, convex synthesis conditions for each performance problem are expressed in terms of nested linear matrix inequalities. The resulting semidefinite programming problem may be solved offline to arrive at a suitable controller. A notion of path-by-path performance is introduced for each performance problem, leading to improved system performance. Non-regular switching languages are considered and the results are extended to these languages. Two simple, physically motivated examples are given to demonstrate the application of these results.

2015-12-02
Jun Moon, University of Illinois at Urbana-Champaign, Tamer Başar, University of Illinois at Urbana-Champaign.  2014.  Control Over Lossy Networks: A Dynamic Game Approach. American Control Conference (ACC 2014).

Abstract— This paper considers a minimax control (H∞) control) problem for linear time-invariant (LTI) systems where the communication loop is subject to a TCP-like packet drop network. The problem is formulated within the zero-sum dynamic game framework. The packet drop network is governed by two independent Bernoulli processes that model control and measurement packet losses. Under this constraint, we obtain a dynamic output feedback minimax controller. For the infinite-horizon case, we provide necessary and sufficient conditions in terms of the packet loss rates and the H disturbance attenuation parameter under which the minimax controller exists and is able to stabilize the closed-loop system in the mean-square sense. In particular, we show that unlike the corresponding LQG case, these conditions are coupled and therefore cannot be determined independently.

2015-11-17
Zhenqi Huang, University of Illinois at Urbana-Champaign, Yu Wang, University of Illinois at Urbana-Champaign, Sayan Mitra, University of Illinois at Urbana-Champaign, Geir Dullerud, University of Illinois at Urbana-Champaign.  2014.  On the Cost of Privacy in Distributed Control Systems. 3rd ACM International Conference on High Confidence Networked Systems (HiCoNS).

Individuals sharing information can improve the cost or performance of a distributed control system. But, sharing may also violate privacy. We develop a general framework for studying the cost of differential privacy in systems where a collection of agents, with coupled dynamics, communicate for sensing their shared environment while pursuing individ- ual preferences. First, we propose a communication strategy that relies on adding carefully chosen random noise to agent states and show that it preserves differential privacy. Of course, the higher the standard deviation of the noise, the higher the cost of privacy. For linear distributed control systems with quadratic cost functions, the standard deviation becomes independent of the number agents and it decays with the maximum eigenvalue of the dynamics matrix. Furthermore, for stable dynamics, the noise to be added is independent of the number of agents as well as the time horizon up to which privacy is desired.

2015-12-02
Bahman Gharesifard, Queen's University, Canada, Tamer Başar, University of Illinois at Urbana-Champaign, Alejandro D. Domínguez-García, University of Illinois at Urbana-Champaign.  2014.  Designing Pricing Strategies for Coordination of Networked Distributed Energy Resources. 19th IFAC World Congress (IFAC 2014).

We study the problem of aggregator’s mechanism design for controlling the amount of active, or reactive, power provided, or consumed, by a group of distributed energy resources (DERs). The aggregator interacts with the wholesale electricity market and through some market-clearing mechanism is incentivized to provide (or consume) a certain amount of active (or reactive) power over some period of time, for which it will be compensated. The objective is for the aggregator to design a pricing strategy for incentivizing DERs to modify their active (or reactive) power consumptions (or productions) so that they collectively provide the amount that the aggregator has agreed to provide. The aggregator and DERs’ strategic decision-making process can be cast as a Stackelberg game, in which aggregator acts as the leader and the DERs are the followers. In previous work [Gharesifard et al., 2013b,a], we have introduced a framework in which each DER uses the pricing information provided by the aggregator and some estimate of the average energy that neighboring DERs can provide to compute a Nash equilibrium solution in a distributed manner. Here, we focus on the interplay between the aggregator’s decision-making process and the DERs’ decision-making process. In particular, we propose a simple feedback-based privacy-preserving pricing control strategy that allows the aggregator to coordinate the DERs so that they collectively provide the amount of active (or reactive) power agreed upon, provided that there is enough capacity available among the DERs. We provide a formal analysis of the stability of the resulting closed-loop system. We also discuss the shortcomings of the proposed pricing strategy, and propose some avenues of future work. We illustrate the proposed strategy via numerical simulations.

2015-11-17
Yu Wang, University of Illinois at Urbana-Champaign, Zhenqi Huang, University of Illinois at Urbana-Champaign, Sayan Mitra, University of Illinois at Urbana-Champaign, Geir Dullerud, University of Illinois at Urbana-Champaign.  2014.  Entropy-minimizing Mechanism for Differential Privacy of Discrete-time Linear Feedback Systems. 53rd IEEE Conference on Decision and Control (CDC 2014).

The concept of differential  privacy stems from the study of private query of datasets.  In  this work, we apply this concept  to metric spaces  to study a  mechanism  that randomizes a deterministic query by adding  mean-zero  noise to keep differential  privacy.

2017-02-10
Jim Blythe, University of Southern California, Ross Koppel, University of Pennsylvania, Vijay Kothari, Dartmouth College, Sean W. Smith, Dartmouth College.  2014.  Ethnography of Computer Security Evasions in Healthcare Settings: Circumvention as the Norm.

Healthcare professionals have unique motivations, goals, perceptions, training, tensions, and behaviors, which guide workflow and often lead to unprecedented workarounds that weaken the efficacy of security policies and mechanisms. Identifying and understanding these factors that contribute to circumvention, as well as the acts of circumvention themselves, is key to designing, implementing, and maintaining security subsystems that achieve security goals in healthcare settings. To this end, we present our research on workarounds to computer security in healthcare settings without compromising the fundamental health goals. We argue and demonstrate that understanding workarounds to computer security, especially in medical settings, requires not only analyses of computer rules and processes, but also interviews and observations with users and security personnel. In addition, we discuss the value of shadowing clinicians and conducting focus groups with them to understand their motivations and tradeoffs for circumvention. Ethnographic investigation of workflow is paramount to achieving security objectives.

Presented at Safety, Security, Privacy and Interoperability of Health Information Technologies (HealthTec 2014), August 19, 2014 in San Diego, CA. See video at URL below.

2015-11-18
Sonia Santiago, Universidad Politécnica de Valencia, Spain, Santiago Escobar, Universidad Politécnica de Valencia, Spain, Catherine Meadows, Naval Research Laboratory, Jose Meseguer, University of Illinois at Urbana-Champaign.  2014.  A Formal Definition of Protocol Indistinguishability and its Verification Using Maude-NPA. 10th International Workshop on Security and Trust Management (STM 2014).

Intuitively, two protocols P1 and P2 are indistinguishable if an attacker cannot tell the difference between interactions with P1 and with P2 . In this paper we: (i) propose an intuitive notion of indistinguishability in Maude-NPA; (ii) formalize such a notion in terms of state unreachability conditions on their synchronous product; (iii) prove theorems showing how —assuming the protocol’s algebraic theory has a finite variant (FV) decomposition – these conditions can be checked by the Maude-NPA tool; and (iv) illustrate our approach with concrete examples. This provides for the first time a framework for automatic analysis of indistinguishability modulo as wide a class of algebraic properties as FV, which includes many associative-commutative theories of interest to cryptographic protocol analysis.

2015-11-16
Gary Wang, University of Illinois at Urbana-Champaign, Zachary J. Estrada, University of Illinois at Urbana-Champaign, Cuong Pham, University of Illinois at Urbana-Champaign, Zbigniew Kalbarczyk, University of Illinois at Urbana-Champaign, Ravishankar K. Iyer, University of Illinois at Urbana-Champaign.  2014.  Hypervisor Introspection: Exploiting Timing Side-Channels against VM Monitoring. 44th International Conference on Dependable Systems and Networks.

Hypervisor activity is designed to be hidden from guest Virtual Machines (VM) as well as external observers. In this paper, we demonstrate that this does not always occur. We present a method by which an external observer can learn sensitive information about hypervisor internals, such as VM scheduling or hypervisor-level monitoring schemes, by observing a VM. We refer to this capability as Hypervisor Introspection (HI).

HI can be viewed as the inverse process of the well-known Virtual Machine Introspection (VMI) technique. VMI is a technique to extract VMs’ internal state from the hypervi- sor, facilitating the implementation of reliability and security monitors[1]. Conversely, HI is a technique that allows VMs to autonomously extract hypervisor information. This capability enables a wide range of attacks, for example, learning a hypervisor’s properties (version, configuration, etc.), defeating hypervisor-level monitoring systems, and compromising the confidentiality of co-resident VMs. This paper focuses on the discovery of a channel to implement HI, and then leveraging that channel for a novel attack against traditional VMI.

In order to perform HI, there must be a method of extracting information from the hypervisor. Since this information is intentionally hidden from a VM, we make use of a side channel. When the hypervisor checks a VM using VMI, VM execution (e.g. network communication between a VM and a remote system) must pause. Therefore, information regarding the hypervisor’s activity can be leaked through this suspension of execution. We call this side channel the VM suspend side channel, illustrated in Fig. 1. As a proof of concept, this paper presents how correlating the results of in-VM micro- benchmarking and out-of-VM reference monitoring can be used to determine when hypervisor-level monitoring tools are vulnerable to attacks.

2015-11-17
Zhenqi Huang, University of Illinois at Urbana-Champaign, Chuchu Fan, University of Illinois at Urbana-Champaign, Alexandru Mereacre, University of Oxford, Sayan Mitra, University of Illinois at Urbana-Champaign, Marta Kwiatkowska, University of Oxford.  2014.  Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. 26th International Conference on Computer Aided Verification (CAV 2014).

Verification algorithms for networks of nonlinear hybrid automata (HA) can aid us understand and control biological processes such as cardiac arrhythmia, formation of memory, and genetic regulation. We present an algorithm for over-approximating reach sets of networks of nonlinear HA which can be used for sound and relatively complete invariant checking. First, it uses automatically computed input-to-state discrepancy functions for the individual automata modules in the network A for constructing a low-dimensional model M. Simulations of both A and M are then used to compute the reach tubes for A. These techniques enable us to handle a challenging verification problem involving a network of cardiac cells, where each cell has four continuous variables and 29 locations. Our prototype tool can check bounded-time invariants for networks with 5 cells (20 continuous variables, 295 locations) typically in less than 15 minutes for up to reasonable time horizons. From the computed reach tubes we can infer biologically relevant properties of the network from a set of initial states.

2016-11-15
2015-12-02
Jun Moon, University of Illinois at Urbana-Champaign, Tamer Başar, University of Illinois at Urbana-Champaign.  2014.  Minimax Control of MIMO Systems Over Multiple TCP-like Lossy Networks. 19th IFAC World Congress (IFAC 2014).

This paper considers a minimax control problem over multiple packet dropping channels. The channel losses are assumed to be Bernoulli processes, and operate under the transmission control protocol (TCP); hence acknowledgments of control and measurement drops are available at each time. Under this setting, we obtain an output feedback minimax controller, which are implicitly dependent on rates of control and measurement losses. For the infinite-horizon case, we first characterize achievable Hdisturbance attenuation levels, and then show that the underlying condition is a function of packet loss rates. We also address the converse part by showing that the condition of the minimum attainable loss rates for closed-loop system stability is a function of H disturbance attenuation parameter. Hence, those conditions are coupled with each other. Finally, we show the limiting behavior of the minimax controller under the disturbance attenuation parameter.

2015-11-23
David Nicol, University of Illinois at Urbana-Champaign, Vikas Mallapura, University of Illinois at Urbana-Champaign.  2014.  Modeling and Analysis of Stepping Stone Attacks. 2014 Winter Simulation Conference.

Computer exploits often involve an attacker being able to compromise a sequence of hosts, creating a chain of "stepping stones" from his source to ultimate target. Stepping stones are usually necessary to access well-protected resources, and also serve to mask the attacker’s location. This paper describes means of constructing models of networks and the access control mechanisms they employ to approach the problem of finding which stepping stone paths are easiest for an attacker to find. While the simplest formulation of the problem can be addressed with deterministic shortest-path algorithms, we argue that consideration of what and how an attacker may (or may not) launch from a compromised host pushes one towards solutions based on Monte Carlo sampling. We describe the sampling algorithm and some preliminary results obtained using it.

2015-11-17
Ray Essick, University of Illinois at Urbana-Champaign, Ji-Woong Lee, Pennsylvania State University, Geir Dullerud, University of Illinois at Urbana-Champaign.  2014.  Path-By-Path Output Regulation of Switched Systems With a Receding Horizon of Modal Knowledge. American Control Conference (ACC).

We address a discrete-time LQG control problem over a fixed performance window and apply a receding-horizon type control strategy, resulting in an exact solution to the problem in terms of semidefinite programming. The systems considered take parameters from a finite set, and switch between them according to an automaton. The controller has a finite preview of future parameters, beyond which only the set of parameters is known. We provide necessary and sufficient convex con- ditions for the existence of a controller which guarantees both exponential stability and finite-horizon performance levels for the system; the performance levels may differ according to the particular parameter sequence within the performance window. A simple, physics-based example is provided to illustrate the main results.