UIUC – University of Illinois at Urbana-Champaign

These publications were done for the Lablet activities at this school, and were listed in the Quarterly Reports back to the government. Please direct any comments to research (at) securedatabank.net if there are any questions or concerns regarding these publications.

UIUC - University of Illinois at Urbana-Champaign
Topic: Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Title: Proving Abstractions of Dynamical Systems through Numerical Simulations
Author(s): Sayan Mitra
Hard Problem: Scalability and Composability, Metrics
Abstract: ACM Library
Sayan Mitra. 2014. Proving abstractions of dynamical systems through numerical simulations. InProceedings of the 2014 Symposium and Bootcamp on the Science of Security (HotSoS '14). ACM, New York, NY, USA, , Article 12 , 9 pages. DOI=10.1145/2600176.2600188 http://doi.acm.org/10.1145/2600176.2600188

A key question that arises in rigorous analysis of cyberphysical systems under attack involves establishing whether or not the attacked system deviates significantly from the ideal allowed behavior. This is the problem of deciding whether or not the ideal system is an abstraction of the attacked system. A quantitative variation of this question can capture how much the attacked system deviates from the ideal. Thus, algorithms for deciding abstraction relations can help measure the effect of attacks on cyberphysical systems and to develop attack detection strategies. In this paper, we present a decision procedure for proving that one nonlinear dynamical system is a quantitative abstraction of another. Directly computing the reach sets of these nonlinear systems are undecidable in general and reach set over-approximations do not give a direct way for proving abstraction. Our procedure uses (possibly inaccurate) numerical simulations and a model annotation to compute tight approximations of the observable behaviors of the system and then uses these approximations to decide on abstraction. We show that the procedure is sound and that it is guaranteed to terminate under reasonable robustness assumptions. (ID#:14-2558)
URL: http://dl.acm.org/citation.cfm?id=2600188
Publication Location: Hot Topics in Science of Security (HOTSOS) 2014


UIUC - University of Illinois at Urbana-Champaign
Topic: Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Title: Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells
Author(s): Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Kwiatkowska
Hard Problem: Scalability and Composability, Metrics
Abstract: Available from Springer via link listed below.. (ID#:14-2559)
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_25#
Publication Location: Computer Aided Verification (CAV 2014)


UIUC - University of Illinois at Urbana-Champaign
Topic: Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems
Title: Decentralized Control of Switched Nested Systems with l2-induced Norm Performance
Author(s): Anshuman Mishra, Cedric Langbort, and Geir Dullerud
Hard Problem: Scalability and Composability, Metrics

Abstract: Abstract not available (ID#:14-2560)

URL: URL not available
Similar paper with same authors and same topic: "Optimal decentralized control of a stochastically switched system..." Link
Publication Location: Proceedings of the American Control Conference (ACC) 2014

Topic: Data Driven Security Models and Analysis
Title: An Experiment Using Factor Graph for Early Attack Detection
Author(s): P. Cao, K.-W. Chung, A. Slagell, Z. Kalbarczyk, R. Iyer
Hard Problem: Metrics, Resilient Architectures, Human Behavior
Abstract: Not Found (ID#:14-2561)
URL: Not found
Similar paper with same authors and same topic : "Preemptive Intrusion Detection" by P. Cao, K.-W. Chung, A. Slagell, Z. Kalbarczyk, R. Iyer Link
Publication Location: Workshop on Learning from Authoritative Security Experiment Results (LASER) 2014

UIUC - University of Illinois at Urbana-Champaign
Topic: A Hypothesis Testing Framework for Network Security
Title: Towards Correct Network Virtualization
Author(s): Soudeh Ghorbani and Brighten Godfrey
Hard Problem: Scalability and Composability, Policy-Governed Secure Collaboration, Metrics, Resilient Architectures
Abstract: ACM Digital Library
In SDN, the underlying infrastructure is usually abstracted for applications that can treat the network as a logical or virtual entity. Commonly, the ``mappings" between virtual abstractions and their actual physical implementations are not one-to-one, e.g., a single "big switch" abstract object might be implemented using a distributed set of physical devices. A key question is, what abstractions could be mapped to multiple physical elements while faithfully preserving their native semantics? E.g., can an application developer always expect her abstract "big switch" to act exactly as a physical big switch, despite being implemented using multiple physical switches in reality?
We show that the answer to that question is "no" for existing virtual-to-physical mapping techniques: behavior can differ between the virtual "big switch" and the physical network, providing incorrect application-level behavior. We also show that that those incorrect behaviors occur despite the fact that the most pervasive and commonly-used correctness invariants, such as per-packet consistency, are preserved throughout. These examples demonstrate that for practical notions of correctness, new systems and a new analytical framework are needed. We take the first steps by defining end-to-end correctness, a correctness condition that focuses on applications only, and outline a research vision to obtain virtualization systems with correct virtual to physical mappings (ID#:14-2562)
URL: http://dl.acm.org/citation.cfm?id=2620754
Publication Location: ACM Workshop on Hot Topics in Software Defined Networks (HotSDN), August 2014

UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Agent-Based Modeling of User Circumvention of Security
Author(s): V. Kothari, J. Blythe, S.W. Smith, and R. Koppel
Hard Problem: Human Behavior
Collaborating: In collaboration with Dartmouth University
Abstract: ACM Digital Library
Vijay Kothari, Jim Blythe, Sean Smith, and Ross Koppel. 2014. Agent-based modeling of user circumvention of security. In Proceedings of the 1st International Workshop on Agents and CyberSecurity (ACySE '14). ACM, New York, NY, USA, , Article 5 , 4 pages. DOI=10.1145/2602945.2602948 http://doi.acm.org/10.1145/2602945.2602948
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. (ID#:14-2563)
URL: http://dl.acm.org/citation.cfm?id=2602948
Publication Location: 1st International Workshop on Agents and CyberSecurity. ACM. May 2014

UIUC - University of Illinois at Urbana-Champaign
Topic: Theoretical Foundations of Threat Assessment by Inverse Optimal Control
Title: Equilibrium configurations of a Kirchhoff elastic rod under quasi-static manipulation
Author(s): Timothy Bretl and Zoe McCarthy
Abstract: Available from Springer via link listed below.. (ID#:14-2564)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-36279-8_5
ACM Library link for "Quasi-static manipulation of a Kirchhoff elastic rod based on a geometric analysis of equilibrium configurations : http://dl.acm.org/citation.cfm?id=2568347
Publication Location: Workshop on Algorithmic Foundations of Robotics 12

UIUC - University of Illinois at Urbana-Champaign
Title: Mechanics and manipulation of planar elastic kinematic chains
Topic: Science of Human Circumvention of Security
Author(s): Zoe McCarthy and Timothy Bretl
Abstract: McCarthy, Z.; Bretl, T., "Mechanics and manipulation of planar elastic kinematic chains," Robotics and Automation (ICRA), 2012 IEEE International Conference on , vol., no., pp.2798,2805, 14-18 May 2012
doi: 10.1109/ICRA.2012.6224693
In this paper, we study quasi-static manipulation of a planar kinematic chain with a fixed base in which each joint is a linearly-elastic torsional spring. The shape of this chain when in static equilibrium can be represented as the solution to a discrete-time optimal control problem, with boundary conditions that vary with the position and orientation of the last link. We prove that the set of all solutions to this problem is a smooth manifold that can be parameterized by a single chart. For manipulation planning, we show several advantages of working in this chart instead of in the space of boundary conditions, particularly in the context of a sampling-based planning algorithm. Examples are provided in simulation. (ID#:14-2565)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6224693&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6224693
Publication Location: IEEE International Conference on Robotics and Automation, 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Experiments in quasi-static manipulation of a planar elastic rod
Author(s): D. Matthews and Timothy Bretl
Abstract: Matthews, D.; Bretl, T., "Experiments in quasi-static manipulation of a planar
elastic rod," Intelligent Robots and Systems (IROS), 2012 IEEE/RSJ International Conference on , vol., no., pp.5420,5427, 7-12 Oct. 2012
doi: 10.1109/IROS.2012.6385876
In this paper, we introduce and experimentally validate a sampling-based planning algorithm for quasi-static manipulation of a planar elastic rod. Our algorithm is an immediate consequence of deriving a global coordinate chart of finite dimension that suffices to describe all possible configurations of the rod that can be placed in static equilibrium by fixing the position and orientation of each end. Hardware experiments confirm this derivation in the case where the "rod" is a thin, flexible strip of metal that has a fixed base and that is held at the other end by an industrial robot. We show an example in which a path of the robot that was planned by our algorithm causes the metal strip to move between given start and goal configurations while remaining in quasi-static equilibrium. (ID#:14-2566)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6385876&url=http%3A%2F
%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6385876
Publication Location: IEEE/RSJ International Conference on Intelligent Robots and Systems, 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: A brain-machine interface to navigate mobile robots along human-like paths amidst obstacles
Author(s): A. Akce, J. Norton, and T. Bretl
Abstract: Akce, A; Norton, J.; Bretl, T., "A brain-machine interface to navigate mobile robots along human-like paths amidst obstacles," Intelligent Robots and Systems (IROS), 2012 IEEE/RSJ International Conference on , vol., no., pp.4084,4089, 7-12 Oct. 2012
doi: 10.1109/IROS.2012.6386024
This paper presents an interface that allows a human user to specify a desired path for a mobile robot in a planar workspace with noisy binary inputs that are obtained at low bit-rates through an electroencephalograph (EEG). We represent desired paths as geodesics with respect to a cost function that is defined so that each path-homotopy class contains exactly one (local) geodesic. We apply max-margin structured learning to recover a cost function that is consistent with observations of human walking paths. We derive an optimal feedback communication protocol to select a local geodesic-equivalently, a path-homotopy class-using a sequence of noisy bits. We validate our approach with experiments that quantify both how well our learned cost function characterizes human walking data and how well human subjects perform with the resulting interface in navigating a simulated robot with EEG. (ID#:14-2567)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6386024&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6386024
Publication Location: IEEE/RSJ International Conference on Intelligent Robots and Systems, 2012



UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Quasi-Static Manipulation of a Kirchhoff Elastic Rod based on a Geometric Analysis of Equilibrium Configurations
Author(s): T. Bretl and Z. McCarthy
Abstract: Timothy Bretl and Zoe Mccarthy. 2014. Quasi-static manipulation of a Kirchhoff elastic rod based on a geometric analysis of equilibrium configurations. Int. J. Rob. Res. 33, 1 (January 2014), 48-68. DOI=10.1177/0278364912473169 http://dx.doi.org/10.1177/0278364912473169
Consider a thin, flexible wire of fixed length that is held at each end by a robotic gripper. Any curve traced by this wire when in static equilibrium is a local solution to a geometric optimal control problem, with boundary conditions that vary with the position and orientation of each gripper. We prove that the set of all local solutions to this problem over all possible boundary conditions is a smooth manifold of finite dimension that can be parameterized by a single chart. We show that this chart makes it easy to implement a sampling-based algorithm for quasi-static manipulation planning. We characterize the performance of such an algorithm with experiments in simulation. (ID#:14-2568)
URL: http://dl.acm.org/citation.cfm?id=2568347
Publication Location: International Journal of Robotics Research, 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Mechanics and Quasi-Static Manipulation of Planar Elastic Kinematic Chains
Author(s): T. Bretl and Z. McCarthy
Abstract: Bretl, T.; McCarthy, Z., "Mechanics and Quasi-Static Manipulation of Planar Elastic Kinematic Chains," Robotics, IEEE Transactions on , vol.29, no.1, pp.1,14, Feb. 2013 DOI: 10.1109/TRO.2012.2218911
In this paper, we study quasi-static manipulation of a planar kinematic chain with a fixed base in which each joint is a linearly elastic torsional spring. The shape of this chain when in static equilibrium can be represented as the solution to a discrete-time optimal control problem, with boundary conditions that vary with the position and orientation of the last link. We prove that the set of all solutions to this problem is a smooth three-manifold that can be parameterized by a single chart. Empirical results in simulation show that straight-line paths in this chart are uniformly more likely to be feasible (as a function of distance) than straight-line paths in the space of boundary conditions. These results, which are consistent with an analysis of visibility properties, suggest that the chart we derive is a better choice of space in which to apply a sampling-based algorithm for manipulation planning. We describe such an algorithm and show that it is easy to implement. (ID#:14-2569)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6327684
Publication Location: IEEE Transactions on Robotics, 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security
Title: Inverse optimal control for deterministic continuous-time nonlinear systems
Author(s): M. Johnson, N. Aghasadeghi, and T. Bretl
Abstract: Johnson, M.; Aghasadeghi, N.; Bretl, T., "Inverse optimal control for deterministic continuous-time nonlinear systems," Decision and Control (CDC), 2013 IEEE 52nd Annual Conference on , vol., no., pp.2906,2913, 10-13 Dec. 2013
doi: 10.1109/CDC.2013.6760325
Inverse optimal control is the problem of computing a cost function with respect to which observed state and input trajectories are optimal. We present a new method of inverse optimal control based on minimizing the extent to which observed trajectories violate first-order necessary conditions for optimality. We consider continuous-time deterministic optimal control systems with a cost function that is a linear combination of known basis functions. We compare our approach with three prior methods of inverse optimal control. We demonstrate the performance of these methods by performing simulation experiments using a collection of nominal system models. We compare the robustness of these methods by analysing how they perform under perturbations to the system. To this purpose, we consider two scenarios: one in which we exactly know the set of basis functions in the cost function, and another in which the true cost function contains an unknown perturbation. Results from simulation experiments show that our new method is more computationally efficient than prior methods, performs similarly to prior approaches under large perturbations to the system, and better learns the true cost function under small perturbations. (ID#:14-2570)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6760325&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6760325
Publication Location: IEEE International Conference on Robotics and Automation, 2013

UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: A Dynamic Game-Theoretic Approach to Resilient Control System Design for Cascading Failures
Author(s): Quanyan Zhu and Tamer Basar
Abstract: Quanyan Zhu and Tamer Basar. 2012. A dynamic game-theoretic approach to resilient control system design for cascading failures. In Proceedings of the 1st international conference on High Confidence Networked Systems (HiCoNS '12). ACM, New York, NY, USA, 41-46. DOI=10.1145/2185505.2185512 http://doi.acm.org/10.1145/2185505.2185512 The migration of many current critical infrastructures, such as power grids and transportations systems, into open public networks has posed many challenges in control systems. Modern control systems face uncertainties not only from the physical world but also from the cyber space. In this paper, we propose a hybrid game-theoretic approach to investigate the coupling between cyber security policy and robust control design. We study in detail the case of cascading failures in industrial control systems and provide a set of coupled optimality criteria in the linear-quadratic case. This approach can be further extended to more general cases of parallel cascading failures. (ID#:14-2571)
URL: http://dl.acm.org/citation.cfm?id=2185512&dl=ACM&coll=DL&CFID=551960065&CFTOKEN=77203732
Publication Location: Conference on High Confidence Networked Systems (HiCoNS) at CPSWeek 2012



UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Game-Theoretic Methods for Distributed Management of Energy Resources in the Smart Grid
Author(s): Quanyan Zhu and Tamer Basar
Abstract: Quanyan Zhu; Jiangmeng Zhang; Sauer, P.W.; Dominguez-Garcia, A; Basar, T., "A game-theoretic framework for control of distributed renewable-based energy resources in smart grids," American Control Conference (ACC), 2012 , vol., no., pp.3623,3628, 27-29 June 2012
doi: 10.1109/ACC.2012.6315275
Renewable energy plays an important role in distributed energy resources in smart grid systems. Deployment and integration of renewable energy resources require an intelligent management to optimize their usage in the current power grid. In this paper, we establish a game-theoretic framework for modeling the strategic behavior of buses that are connected to renewable energy resources and study the equilibrium distributed power generation at each bus. Our framework takes a cross-layer approach, taking into account the economic factors as well as system stability issues at each bus. We propose an iterative algorithm to compute Nash equilibrium solutions based on a sequence of linearized games. Simulations and numerical examples are used to illustrate the algorithm and corroborate the results. (ID#:14-2572)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6315275&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6315275
Publication Location: Annual CMU Electricity Conference 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Agent-based cyber control strategy design for resilient control systems: Concepts, architecture and methodologies
Author(s): C. Rieger, Quanyan Zhu and Tamer Basar
Abstract: Rieger, C.; Quanyan Zhu; Basar, T., "Agent-based cyber control strategy design for resilient control systems: Concepts, architecture and methodologies," Resilient Control Systems (ISRCS), 2012 5th International Symposium on , vol., no., pp.40,47, 14-16 Aug. 2012
doi: 10.1109/ISRCS.2012.6309291
The implementation of automated regulatory control has been around since the middle of the last century through analog means. It has allowed engineers to operate the plant more consistently by focusing on overall operations and settings instead of individual monitoring of local instruments (inside and outside of a control room). A similar approach is proposed for cyber security, where current border-protection designs have been inherited from information technology developments that lack consideration of the high-reliability, high consequence nature of industrial control systems. Instead of an independent development, however, an integrated approach is taken to develop a holistic understanding of performance. This performance takes shape inside a multi-agent design, which provides a notional context to model highly decentralized and complex industrial process control systems, the nervous system of critical infrastructure. The resulting strategy will provide a framework for researching solutions to security and unrecognized interdependency concerns with industrial control systems. (ID#:14-2573)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6309291&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Ftp%3D%26arnumber%3D6309291
Publication Location: Resilient Control Systems 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Dependable demand response management in smart grid: A Stackelberg game approach
Author(s): S. Maharjan, Quanyan Zhu, Y. Zhang, S. Gjessing, and Tamer Basar
Abstract: Maharjan, S.; Quanyan Zhu; Yan Zhang; Gjessing, S.; Basar, T., "Dependable Demand Response Management in the Smart Grid: A Stackelberg Game Approach," Smart Grid, IEEE Transactions on , vol.4, no.1, pp.120,132, March 2013
doi: 10.1109/TSG.2012.2223766
Demand Response Management (DRM) is a key component in the smart grid to effectively reduce power generation costs and user bills. However, it has been an open issue to address the DRM problem in a network of multiple utility companies and consumers where every entity is concerned about maximizing its own benefit. In this paper, we propose a Stackelberg game between utility companies and end-users to maximize the revenue of each utility company and the payoff of each user. We derive analytical results for the Stackelberg equilibrium of the game and prove that a unique solution exists. We develop a distributed algorithm which converges to the equilibrium with only local information available for both utility companies and end-users. Though DRM helps to facilitate the reliability of power supply, the smart grid can be succeptible to privacy and security issues because of communication links between the utility companies and the consumers. We study the impact of an attacker who can manipulate the price information from the utility companies. We also propose a scheme based on the concept of shared reserve power to improve the grid reliability and ensure its dependability. (ID#:14-2574)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6464552
Publication Location: IEEE Trans. on Smart Grid, Special Issue on Smart Grid Communication Systems: Reliability, Dependability & Performance, 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Resilience in consensus dynamics via competitive interconnections
Author(s): Bahman Gharesifard and Tamer Basar
Abstract: We show that competitive engagements within the agents of a network can result in resilience in consensus dynamics with respect to the presence of an adversary. We first show that interconnections with an adversary, with linear dynamics, can make the consensus dynamics diverge, or drive its evolution to a state different from the average. We then introduce a second network, interconnected with the original network via an engagement topology. This network has no information about the adversary and each agent in it has only access to partial information about the state of the other network. We introduce a dynamics on the coupled network which corresponds to a saddle-point dynamics of a certain zero-sum game and is distributed over each network, as well as the engagement topology. We show that, by appropriately choosing a design parameter corresponding to the competition between these two networks, the coupled dynamics can be made resilient with respect to the presence of the adversary. Our technical approach combines notions of graph theory and stable perturbations of nonsymmetric matrices. We demonstrate our results on an example of kinematic-based flocking in presence of an adversary. (ID#:14-2575)
URL: http://www.ifac-papersonline.net/Detailed/56775.html
Publication Location: IFAC Workshop on Distributed Estimation and Control in Networked Systems 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: SODEXO: A system framework for deployment and exploitation of deceptive honeybots in social networks
Author(s): Q. Zhu, A. Clark, R.Poovendran, T. Basar
Abstract: As social networking sites such as Facebook and Twitter are becoming increasingly popular, a growing number of malicious attacks, such as phishing and malware, are exploiting them. Among these attacks, social botnets have sophisticated infrastructure that leverages compromised users accounts, known as bots, to automate the creation of new social networking accounts for spamming and malware propagation. Traditional defense mechanisms are often passive and reactive to non-zero-day attacks. In this paper, we adopt a proactive approach for enhancing security in social networks by infiltrating botnets with honeybots. We propose an integrated system named SODEXO which can be interfaced with social networking sites for creating deceptive honeybots and leveraging them for gaining information from botnets. We establish a Stackelberg game framework to capture strategic interactions between honeybots and botnets, and use quantitative methods to understand the tradeoffs of honeybots for their deployment and exploitation in social networks. We design a protection and alert system that integrates both microscopic and macroscopic models of honeybots and optimally determines the security strategies for honeybots. We corroborate the proposed mechanism with extensive simulations and comparisons with passive defenses. (ID#:14-2576)
URL: http://arxiv.org/abs/1207.5844
Publication Location: IEEE International Conference on Computer Communications (INFOCOM) 2013


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Deceptive routing in relay networks
Author(s): A. Clark, Q. Zhu, R. Poovendran, T. Basar
Abstract: Available from Springer via link listed below.. (ID#:14-2577)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-34266-0_10
Publication Location: Conference on Decision and Game Theory for Security (GameSec) 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Game--theoretic analysis of node capture and cloning attack with multiple attackers in wireless sensor networks
Author(s): Q. Zhu, L. Bushnell, T. Basar
Abstract: Quanyan Zhu; Bushnell, L.; Basar, T., "Game-theoretic analysis of node capture and cloning attack with multiple attackers in wireless sensor networks," Decision and Control (CDC), 2012 IEEE 51st Annual Conference on , vol., no., pp.3404,3411, 10-13 Dec. 2012
doi: 10.1109/CDC.2012.6426481
Wireless sensor networks are subject to attacks such as node capture and cloning, where an attacker physically captures sensor nodes, replicates the nodes, which are deployed into the network, and proceeds to take over the network. In this paper, we develop models for such an attack when there are multiple attackers in a network, and formulate multi-player games to model the noncooperative strategic behavior between the attackers and the network. We consider two cases: a static case where the attackers' node capture rates are time-invariant and the network's clone detection/revocation rate is a linear function of the state, and a dynamic case where the rates are general functions of time. We characterize Nash equilibrium solutions for both cases and derive equilibrium strategies for the players. In the static case, we study both the single-attacker and the multi-attacker games within an optimization framework, provide conditions for the existence of Nash equilibria and characterize them in closed forms. In the dynamic case, we study the underlying multi-person differential game under an open-loop information structure and provide a set of conditions to characterize the open-loop Nash equilibrium. We show the equivalence of the Nash equilibrium for the multi-person game to the saddle-point equilibrium between the network and the attackers as a team. We illustrate our results with numerical examples. (ID#:14-2578)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6426481
Publication Location: IEEE Conference on Decision and Control (CDC) 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Deceptive routing games
Author(s): Q. Zhu, A. Clark, R. Poovendran, T. Basar
Abstract: Quanyan Zhu; Clark, A; Poovendran, R.; Basar, T., "Deceptive routing games," Decision and Control (CDC), 2012 IEEE 51st Annual Conference on , vol., no., pp.2704,2711, 10-13 Dec. 2012
doi: 10.1109/CDC.2012.6426515
The use of a shared medium leaves wireless networks, including mobile ad hoc and sensor networks, vulnerable to jamming attacks. In this paper, we introduce a jamming defense mechanism for multiple-path routing networks based on maintaining deceptive flows, consisting of fake packets, between a source and a destination. An adversary observing a deceptive flow will expend energy on disrupting the fake packets, allowing the real data packets to arrive at the destination unharmed. We model this deceptive flow-based defense within a multi-stage stochastic game framework between the network nodes, which choose a routing path and flow rates for the real and fake data, and an adversary, which chooses which fraction of each flow to target at each hop. We develop an efficient, distributed procedure for computing the optimal routing at each hop and the optimal flow allocation at the destination. Furthermore, by studying the equilibria of the game, we quantify the benefit arising from deception, as reflected in an increase in the valid throughput. Our results are demonstrated via a simulation study. (ID#:14-2579)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6426515&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F6416474%2F6425800%2F06426515.pdf%3Farnumbe...
Publication Location: IEEE Conference on Decision and Control (CDC) 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: GUIDEX: A game-theoretic Incentive-Based mechanism for intrusion detection networks
Author(s): Q. Zhu, C. Fung, R. Boutaba, T. Basar
Abstract: Quanyan Zhu; Fung, C.; Boutaba, R.; Basar, T., "GUIDEX: A Game-Theoretic Incentive-Based Mechanism for Intrusion Detection Networks," Selected Areas in Communications, IEEE Journal on , vol.30, no.11, pp.2220,2230, December 2012
doi: 10.1109/JSAC.2012.121214
Traditional intrusion detection systems (IDSs) work in isolation and can be easily compromised by unknown threats. An intrusion detection network (IDN) is a collaborative IDS network intended to overcome this weakness by allowing IDS peers to share detection knowledge and experience, and hence improve the overall accuracy of intrusion assessment. In this work, we design an IDN system, called GUIDEX, using game-theoretic modeling and trust management for peers to collaborate truthfully and actively. We first describe the system architecture and its individual components, and then establish a game-theoretic framework for the resource management component of GUIDEX. We establish the existence and uniqueness of a Nash equilibrium under which peers can communicate in a reciprocal incentive compatible manner. Based on the duality of the problem, we develop an iterative algorithm that converges geometrically to the equilibrium. Our numerical experiments and discrete event simulation demonstrate the convergence to the Nash equilibrium and the security features of GUIDEX against free riders, dishonest insiders and DoS attacks. (ID#:14-2580)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6354280&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F49%2F6354264%2F06354280.pdf%3Farnumber%3D6...
Publication Location: IEEE Journal on Selected Areas in Communications (JSAC) Special Issue on Economics of Communication Networks & Systems


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: An Impact-Aware Defense against Stuxnet
Author(s): A. Clark, Q. Zhu, R. Poovendran and T. Basar
Abstract: Clark, A; Quanyan Zhu; Poovendran, R.; Basar, T., "An impact-aware defense against Stuxnet," American Control Conference (ACC), 2013 , vol., no., pp.4140,4147, 17-19 June 2013
doi: 10.1109/ACC.2013.6580475
The Stuxnet worm is a sophisticated malware designed to sabotage industrial control systems (ICSs). It exploits vulnerabilities in removable drives, local area communication networks, and programmable logic controllers (PLCs) to penetrate the process control network (PCN) and the control system network (CSN). Stuxnet was successful in penetrating the control system network and sabotaging industrial control processes since the targeted control systems lacked security mechanisms for verifying message integrity and source authentication. In this work, we propose a novel proactive defense system framework, in which commands from the system operator to the PLC are authenticated using a randomized set of cryptographic keys. The framework leverages cryptographic analysis and control-and game-theoretic methods to quantify the impact of malicious commands on the performance of the physical plant. We derive the worst-case optimal randomization strategy as a saddle-point equilibrium of a game between an adversary attempting to insert commands and the system operator, and show that the proposed scheme can achieve arbitrarily low adversary success probability for a sufficiently large number of keys. We evaluate our proposed scheme, using a linear-quadratic regulator (LQR) as a case study, through theoretical and numerical analysis. (ID#:14-2581)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6580475&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6580475
Publication Location: American Control Conference (ACC) 2013



UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Price-based distributed control for networked plug-in electric vehicles
Author(s): B. Gharesifard, T. Basar, and A.D. Dominguez-Garcia
Abstract: Gharesifard, B.; Basar, T.; Dominguez-Garcia, AD., "Price-based distributed control for networked plug-in electric vehicles," American Control Conference (ACC), 2013 , vol., no., pp.5086,5091, 17-19 June 2013 doi: 10.1109/ACC.2013.6580628
We introduce a framework for controlling the charging and discharging processes of plug-in electric vehicles (PEVs) via pricing strategies. Our framework consists of a hierarchical decision-making setting with two layers, which we refer to as aggregator layer and retail market layer. In the aggregator layer, there is a set of aggregators that are requested (and will be compensated for) to provide certain amount of energy over a period of time. In the retail market layer, the aggregator offers some price for the energy that PEVs may provide; the objective is to choose a pricing strategy to incentivize the PEVs so as they collectively provide the amount of energy that the aggregator has been asked for. The focus of this paper is on the decision-making process that takes places in the retail market layer, where we assume that each individual PEV is a price-anticipating decision-maker. We cast this decision-making process as a game, and provide conditions on the pricing strategy of the aggregator under which this game has a unique Nash equilibrium. We propose a distributed consensus-based iterative algorithm through which the PEVs can seek for this Nash equilibrium. Numerical simulations are included to illustrate our results. (ID#:14-2582)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6580628
Publication Location: American Control Conference (ACC) 2013


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Toward a theory of multi-resolution games
Author(s): Q. Zhu and T. Basar
Abstract: University of Illinois at Urbana-Champaign
Modern critical infrastructures are highly integrated systems composed of many complex interactions between different system modules or agents including cyber and physical components as well as human factors. Their growing complexity demands novel techniques (ID#:14-2583)
URL: https://wiki.engr.illinois.edu/download/attachments/229421613/ZhuBasar_SIAM2013.pdf?version=1&modificationDate=1383488188000
Publication Location: 2013 SIAM Conference on Control and Its Applications (CT13)


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Resilient distributed control of multi-agent cyber-physical systems
Author(s): Q. Zhu, L. Bushnell, T. Basar
Abstract: Available from Springer via link listed below. (ID#:14-2584)
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-01159-2_16
Publication Location: CISS Workshop on Cyber-Physical Systems 2013


**Title: A price-based approach to control of networked distributed energy resources
** Price-Based Distributed Control for Networked Plug-in Electric Vehicles (alternate title)
Author(s): B. Gharesifard, T. Basar, and A. D. Dominguez-Garcia
Abstract: no abstract found (ID#:14-2585)
URL: http://energy.ece.illinois.edu/aledan/publications_files/ACC_2013.pdf
Publication Location: Special Issue on Cyber-Physical-Systems, IEEE Transactions on Automatic Control


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Resilient Control of Cyber-Physical Systems against Denial-of-Service Attacks
Author(s): Y. Yuan, Q. Zhu, F. Sun, Q. Wang, and T. Basar
Abstract: Yuan Yuan; Quanyan Zhu; Fuchun Sun; Qinyi Wang; Basar, T., "Resilient control of cyber-physical systems against Denial-of-Service attacks," Resilient Control Systems (ISRCS), 2013 6th International Symposium on , vol., no., pp.54,59, 13-15 Aug. 2013
doi: 10.1109/ISRCS.2013.6623750
The integration of control systems with modern information technologies has posed potential security threats for critical infrastructures. The communication channels of the control system are vulnerable to malicious jamming and Denial-of-Service (DoS) attacks, which lead to severe time-delays and degradation of control performances. In this paper, we design resilient controllers for cyber-physical control systems under DoS attacks. We establish a coupled design framework which incorporates the cyber configuration policy of Intrusion Detection Systems (IDSs) and the robust control of dynamical system. We propose design algorithms based on value iteration methods and linear matrix inequalities for computing the optimal cyber security policy and control laws. We illustrate the design principle with an example from power systems. The results are corroborated by numerical examples and simulations. (ID#:14-2586)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6623750&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6601033%2F6623739%2F06623750.pdf%3Farnumber%3D6623750
Publication Location: International Symposium on Resilient Control Systems (ISRCS 2013)


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Hierarchical Architectures of Resilient Control Systems: Concepts, Metrics and Design Principles
Author(s): Q. Zhu, D. Wei, K. Ji, C. Rieger, and T. Basar
Abstract: Security of control systems is becoming a pivotal concern in critical national infrastructures such as the power grid and nuclear plants. In this paper, we adopt a hierarchical viewpoint to these security issues, addressing security concerns at each level and emphasizing a holistic cross-layer philosophy for developing security solutions. We propose a bottom-up framework that establishes a model from the physical and control levels to the supervisory level, incorporating concerns from network and communication levels. We show that the game-theoretical approach can yield cross-layer security strategy solutions to the cyber-physical systems. (ID#:14-2587)

URL: See: "A Hierarchical Security Architecture for Cyber-Physical Systems"
Publication Location: Special Issue of the IEEE Transactions on Cybernetics: "Resilient Control Architectures and Systems"


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Distributed optimization by myopic strategic interactions and the price of heterogeneity
Author(s): B. Gharesifard, B. Touri, T. Basar, and C. Langbort
Abstract: Gharesifard, B.; Touri, B.; Basar, T.; Langbort, C., "Distributed optimization by myopic strategic interactions and the price of heterogeneity," Decision and Control (CDC), 2013 IEEE 52nd Annual Conference on , vol., no., pp.1174,1179, 10-13 Dec. 2013
doi: 10.1109/CDC.2013.6760041
This paper is concerned with the tradeoffs between low-cost heterogenous designs and optimality. We study a class of constrained myopic strategic games on networks which approximate the solutions to a constrained quadratic optimization problem; the Nash equilibria of these games can be found using best-response dynamical systems, which only use local information. The notion of price of heterogeneity captures the quality of our approximations. This notion relies on the structure and the strength of the interconnections between agents. We study the stability properties of these dynamical systems and demonstrate their complex characteristics, including abundance of equilibria on graphs with high sparsity and heterogeneity. We also introduce the novel notions of social equivalence and social dominance, and show some of their interesting implications, including their correspondence to consensus. Finally, using a classical result of Hirsch [1], we fully characterize the stability of these dynamical systems for the case of star graphs with asymmetric interactions. Various examples illustrate our results. (ID#:14-2588)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6760041&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6760041
Publication Location: IEEE Conference on Decision and Control (CDC), December 2013


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Game-theoretic methods for robustness, security and resilience of cyber-physical control systems: Games-in-games principle for optimal cross-layer resilient control systems
Author(s): Q. Zhu and T. Basar
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Not IEEE Modern critical infrastructures are highly integrated systems composed of many complex interactions between different system modules or agents including cyber and physical components as well as human factors. Their growing complexity demands novel design techniques for scalable and efficient control and computations for providing system security and resilience. This dissertation develops new game-theoretic frameworks for addressing security and resilience problems residing at multiple layers of the cyber-physical systems including robust and resilient control, secure network routing and management of information security and smart grid energy systems. Hybrid distributed reinforcement learning algorithms are developed as practical modeling tools for defense systems with different levels of rationality and intelligence at different times. The learning algorithms enable online computations of defense strategies, such as routing decisions and configuration policies, for nonzero-sum security games with incomplete information. In addition, games-in-games frameworks are proposed for system-wide modeling of complex hierarchical systems, where games played at different levels interact through their outcomes, action spaces, and costs. This concept is applied to robust and resilient control of power systems in which a zero-sum differential game for physical robust control design is nested in and coupled with a zero-sum stochastic game for security policy design. At the networking layer of the system, multi-hop secure routing games also exhibit the games-in-games structure, and their equilibrium solutions are characterized by backward induction solving a sequence of nested games. This approach leads to a distributed secure routing protocol that enables the resilience of network routing and self-recovery mechanisms in face of adversarial attacks. Finally, in order to address emerging energy management issues of the smart grid, we establish a fundamental game-theoretic framework for analyzing system equilibrium under distributed generations, renewable energy sources and active participation of utility users. Furthermore, we develop a novel game framework and its equilibrium solution, named mirror Stackelberg equilibrium, for modeling the demand response management in the smart grid. This approach enables quantitative study of the value of demand response brought by emerging smart grid technologies as compared to the current supply-side economic dispatch model. It facilitates fundamental understanding of pricing, energy policies and infrastructural investment decision in future highly interconnected and interdependent energy systems. Examples from power systems, cognitive radio communication networks, and the smart grid are used as driving examples for illustrating new solution concepts, distributed algorithms and analytical techniques presented in this dissertation. (ID#:14-2589)
URL: http://oatd.org/oatd/record?record=handle%5C:2142%5C%2F45479
Publication Location: IEEE Control Systems Magazine



UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: A three-stage Colonel Blotto game with applications to cyberphysical security
Author(s): A. Gupta, G. Schwartz C. Langbort, S. Sastry, and T. Basar
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Gupta, A; Schwartz, G.; Langbort, C.; Sastry, S.S.; Basar, T., "A three-stage Colonel Blotto game with applications to cyberphysical security," American Control Conference (ACC), 2014 , vol., no., pp.3820,3825, 4-6 June 2014 doi: 10.1109/ACC.2014.6859164
We consider a three-step three-player complete information Colonel Blotto game in this paper, in which the first two players fight against a common adversary. Each player is endowed with a certain amount of resources at the beginning of the game, and the number of battlefields on which a player and the adversary fights is specified. The first two players are allowed to form a coalition if it improves their payoffs. In the first stage, the first two players may add battlefields and incur costs. In the second stage, the first two players may transfer resources among each other. The adversary observes this transfer, and decides on the allocation of its resources to the two battles with the players. At the third step, the adversary and the other two players fight on the updated number of battlefields and receive payoffs. We characterize the subgame-perfect Nash equilibrium (SPNE) of the game in various parameter regions. In particular, we show that there are certain parameter regions in which if the players act according to the SPNE strategies, then (i) one of the first two players add battlefields and transfer resources to the other player (a coalition is formed), (ii) there is no addition of battlefields and no transfer of resources (no coalition is formed). We discuss the implications of the results on resource allocation for securing cyberphysical systems. (ID#:14-2590)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6859164&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6849600%2F6858556%2F06859164.pdf%3Farnumber%3D6859164
Publication Location: 2014 American Control Conference (ACC) 2014


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Stability properties of infected networks with low curing rates
Author(s): A. Khanafer, T. Basar, and B. Gharesifard
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Khanafer, A; Basar, T.; Gharesifard, B., "Stability properties of infected networks with low curing rates," American Control Conference (ACC), 2014 , vol., no., pp.3579,3584, 4-6 June 2014 doi: 10.1109/ACC.2014.6859418
In this work, we analyze the stability properties of a recently proposed dynamical system that describes the evolution of the probability of infection in a network. We show that this model can be viewed as a concave game among the nodes. This characterization allows us to provide a simple condition, that can be checked in a distributed fashion, for stabilizing the origin. When the curing rates at the nodes are low, a residual infection stays within the network. Using properties of Hurwitz Mertzel matrices, we show that the residual epidemic state is locally exponentially stable. We also demonstrate that this state is globally asymptotically stable. Furthermore, we investigate the problem of stabilizing the network when the curing rates of a limited number of nodes can be controlled. In particular, we characterize the number of controllers required for a class of undirected graphs. Several simulations demonstrate our results. (ID#:14-2591)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6859418&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6859418
Publication Location: 2014 American Control Conference (ACC) 2014


UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Control over lossy networks: A dynamic game approach
Author(s): J. Moon and T. Basar
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: Jun Moon; Basar, T., "Control over TCP-like lossy networks: A dynamic game approach," American Control Conference (ACC), 2013 , vol., no., pp.1578,1583, 17-19 June 2013 doi: 10.1109/ACC.2013.6580060
This paper considers H optimal control of LTI systems where the loop is closed over TCP-like lossy networks. Following a game theoretic formulation of the problem, we first obtain an explicit Hcontroller. We then analyze the infinite-horizon behavior of the H controller. In particular, we provide necessary and sufficient conditions in terms of the packet drop probability and the H disturbance attenuation parameter under which the optimal controller is unique and stabilizes the closed-loop system in the mean-square sense. It is also shown that these conditions are coupled; therefore, they cannot be determined independently. A numerical example is presented to illustrate the main results. (ID#:14-2592)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6580060&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6580060
Publication Location: 2014 American Control Conference (ACC) 2014

UIUC - University of Illinois at Urbana-Champaign
Topic: Toward a Theory of Resilience in Systems: A Game-Theoretic Approach
Title: Actors Programming for the Mobile Cloud
Author(s): Gul Agha
Hard Problem: Resilient Architecture, Policy-Governed Secure Collaboration
Abstract: From UCLA; different title, same content; no abstract available (ID#:14-2593)
URL: http://www.cs.ucla.edu/~palsberg/course/cs239/papers/karmani-agha.pdf
Publication Location: International Symposium on Parallel and Distributed Computing 2014

UIUC - University of Illinois at Urbana-Champaign
Topic: The Science of Summarizing Systems: Generating Security Properties Using Data Mining and Formal Analysis
Title: Using Control-Flow Techniques in a Security Context: A Survey on Common Prototypes and Their Common Weakness
Author(s): Seeger, M.M
Abstract: Seeger, M.M., "Using Control-Flow Techniques in a Security Context: A Survey on Common Prototypes and Their Common Weakness," Network Computing and Information Security (NCIS), 2011 International Conference on , vol.2, no., pp.133,137, 14-15 May 2011
doi: 10.1109/NCIS.2011.126
Practical approaches using control-flow techniques in order to detect changes in the control-flow of a program have been subject of many scientific works. This work focuses on three common tools making use of control- and data-flow analysis in order to detect alternations and reveals their common weakness in terms of the ability to react directly to a dynamic change in control-flow. With a general focus on static analysis of binaries or source code, detection of dynamic changes in the executive flow cannot be detected. In order to emphasize this shortcoming of static analysis, we present an approach for dynamically changing a program's control-flow and validate it by depicting a proof of concept. (ID#:14-2594)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=5948809&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D5948809
Publication Location: Network Computing and Information Security (NCIS), 2011

UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Parameterized concurrent multi-party session types
Author(s): Minas Charalambides, Peter Dinges, and Gul Agha
Abstract: From arXiv: Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful in verifying some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is inexpressible in previously proposed session type systems. This paper describes System-A, a new typing language which overcomes many of the expressiveness limitations of prior work. System-A explicitly supports asynchrony and parallelism, as well as multiple forms of parameterization. We define System-A and show how it can be used for the static verification of a large class of asynchronous communication protocols. (ID#:14-2595)
URL: http://arxiv.org/pdf/1208.4632.pdf
Publication Location: International Workshop on Foundations of Coordination Languages and Self Adaptation 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Why Do Scala Developers Mix the Actor Model with Other Concurrency Models
Author(s): Samira Tasharo , Peter Dinges, and Ralph Johnson
Abstract: Samira Tasharofi, Peter Dinges, and Ralph E. Johnson. 2013. Why do scala developers mix the actor model with other concurrency models?. In Proceedings of the 27th European conference on Object-Oriented Programming (ECOOP'13), Giuseppe Castagna (Ed.). Springer-Verlag, Berlin, Heidelberg, 302-326. DOI=10.1007/978-3-642-39038-8_13 http://dx.doi.org/10.1007/978-3-642-39038-8_13
Mixing the actor model with other concurrency models in a single program can break the actor abstraction. This increases the chance of creating deadlocks and data races--two mistakes that are hard to make with actors. Furthermore, it prevents the use of many advanced testing, modeling, and verification tools for actors, as these require pure actor programs. This study is the first to point out the phenomenon of mixing concurrency models by Scala developers and to systematically identify the factors leading to it. We studied 15 large, mature, and actively maintained actor programs written in Scala and found that 80% of them mix the actor model with another concurrency model. Consequently, a large part of real-world actor programs does not use actors to their fullest advantage. Inspection of the programs and discussion with the developers reveal two reasons for mixing that can be influenced by researchers and library-builders: weaknesses in the actor library implementations, and shortcomings of the actor model itself. (ID#:14-2596)
URL: http://dl.acm.org/citation.cfm?id=2525001
Publication Location: ECOOP 2013 - Object-Oriented Programming


UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Automated inference of atomic sets for safe concurrent execution
Author(s): Peter Dinges, Minas Charalambides, and Gul Agha
Abstract: Peter Dinges, Minas Charalambides, and Gul Agha. 2013. Automated inference of atomic sets for safe concurrent execution. In Proceedings of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE '13). ACM, New York, NY, USA, 1-8. DOI=10.1145/2462029.2462030 http://doi.acm.org/10.1145/2462029.2462030
Atomic sets are a synchronization mechanism in which the programmer specifies the groups of data that must be accessed as a unit. The compiler can check this specification for consistency, detect deadlocks, and automatically add the primitives to prevent interleaved access. Atomic sets relieve the programmer from the burden of recognizing and pruning execution paths which lead to interleaved access, thereby reducing the potential for data races. However, manually converting programs from lock-based synchronization to atomic sets requires reasoning about the program's concurrency structure, which can be a challenge even for small programs. Our analysis eliminates the challenge by automating the reasoning. Our implementation of the analysis allowed us to derive the atomic sets for large code bases such as the Java collections framework in a matter of minutes. The analysis is based on execution traces; assuming all traces reflect intended behavior, our analysis enables safe concurrency by preventing unobserved interleavings which may harbor latentHeisenbugs (ID#:14-2597)
URL: http://dl.acm.org/citation.cfm?id=2462030
Publication Location: Workshop on Program Analysis for Software Tools and Engineering 2013


UIUC - University of Illinois at Urbana-Champaign
Topic: Scalable Methods for Security Against Distributed Attacks
Title: Performance Evaluation of Sensor Networks by Statistical Modeling and Euclidean Model Checking
Author(s): YoungMin Kwon and Gul Agha
Abstract: Youngmin Kwon and Gul Agha. 2013. Performance evaluation of sensor networks by statistical modeling and euclidean model checking. ACM Trans. Sen. Netw. 9, 4, Article 39 (July 2013), 38 pages. DOI=10.1145/2489253.2489256 http://doi.acm.org/10.1145/2489253.2489256
Modeling and evaluating the performance of large-scale wireless sensor networks (WSNs) is a challenging problem. The traditional method for representing the global state of a system as a cross product of the states of individual nodes in the system results in a state space whose size is exponential in the number of nodes. We propose an alternative way of representing the global state of a system: namely, as a probability mass function (pmf) which represents the fraction of nodes in different states. A pmf corresponds to a point in a Euclidean space of possible pmf values, and the evolution of the state of a system is represented by trajectories in this Euclidean space. We propose a novel performance evaluation method that examines all pmf trajectories in a dense Euclidean space by exploring only finite relevant portions of the space. We call our method Euclidean model checking. Euclidean model checking is useful both in the design phase--where it can help determine system parameters based on a specification--and in the evaluation phase--where it can help verify performance properties of a system. We illustrate the utility of Euclidean model checking by using it to design a time difference of arrival (TDoA) distance measurement protocol and to evaluate the protocol's implementation on a 90-node WSN. To facilitate such performance evaluations, we provide a Markov model estimation method based on applying a standard statistical estimation technique to samples resulting from the execution of a system. (ID#:14-2599)
URL: http://dl.acm.org/citation.cfm?id=2489256
Publication Location: ACM Transactions on Sensor Networks

UIUC - University of Illinois at Urbana-Champaign
Topic: Beyond Reachability Properties
Title: A Formal Definition of Protocol Indistinguishability and its Verification on Maude-NPA
Author(s): S. Escobar, C. Meadows, J. Meseguer, and S. Santiago
Abstract: not available: Possible broken lnk. (ID#:14-2600)
URL: http://users.dsic.upv.es/~sescobar/papers-security.html
Publication Location: UIUC Technical Report

UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Differentially Private Iterative Synchronous Consensus
Author(s): Zhenqi Huang, Sayan Mitra, Geir Dullerud
Abstract: Zhenqi Huang, Sayan Mitra, and Geir Dullerud. 2012. Differentially private iterative synchronous consensus. In Proceedings of the 2012 ACM workshop on Privacy in the electronic society (WPES '12). ACM, New York, NY, USA, 81-90. DOI=10.1145/2381966.2381978 http://doi.acm.org/10.1145/2381966.2381978
The iterative consensus problem requires a set of processes or agents with different initial values, to interact and update their states to eventually converge to a common value. Protocols solving iterative consensus serve as building blocks in a variety of systems where distributed coordination is required for load balancing, data aggregation, sensor fusion, filtering, and synchronization. In this paper, we introduce the private iterative consensus problem where agents are required to converge while protecting the privacy of their initial values from honest but curious adversaries. Protecting the initial states, in many applications, suffice to protect all subsequent states of the individual participants.
We adapt the notion of differential privacy in this setting of iterative computation. Next, we present (i) a server-based and (ii) a completely distributed randomized mechanism for solving differentially private iterative consensus with adversaries who can observe the messages as well as the internal states of the server and a subset of the clients. Our analysis establishes the tradeoff between privacy and the accuracy: for given e, b >0, the e-differentially private mechanism for N agents, is guaranteed to convergence to a value withinO(/1/e bN) of the average of the initial values, with probability at least (1-b). (ID#:14-2601)
URL: http://dl.acm.org/citation.cfm?id=2381978
Publication Location: Workshop on Privacy in the Electronic Society (WPES), collocated with of 19th ACM Conference on Computer and Communications Security (CCS) 2012


UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Using Run-Time Checking to Provide Safety and Progress for Distributed Cyber-Physical Systems
Author(s): Stanley Bak, Fardin Abdi, Zhenqi Huang and Marco Caccamo
Abstract: Bak, S.; Abad, F.AT.; Zhenqi Huang; Caccamo, M., "Using run-time checking to provide safety and progress for distributed cyber-physical systems," Embedded and Real-Time Computing Systems and Applications (RTCSA), 2013 IEEE 19th International Conference on , vol., no., pp.287,296, 19-21 Aug. 2013
doi: 10.1109/RTCSA.2013.6732229
Cyber-physical systems (CPS) may interact and manipulate objects in the physical world, and therefore ideally would have formal guarantees about their behavior. Performing static-time proofs of safety invariants, however, may be intractable for systems with distributed physical-world interactions. This is further complicated when realistic communication models are considered, for which there may not be bounds on message delays, or even that messages will eventually reach their destination. In this work, we address the challenge of proving safety and progress in distributed CPS communicating over an unreliable communication layer. This is done in two parts. First, we show that system safety can be verified by partially relying upon run-time checks, and that dropping messages if the run-time checks fail will maintain safety. Second, we use a notion of compatible action chains to guarantee system progress, despite unbounded message delays. We demonstrate the effectiveness of our approach on a multi-agent vehicle flocking system, and show that the overhead of the proposed run-time checks is not overbearing. (ID#:14-2602)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6732229&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel7%2F6720220%2F6732192%2F06732229.pdf%3Farnumber%3D6732229
Publication Location: IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2013)


UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Classification of Cyber-physical System Adversaries
Author(s): R. Essick, J.-W. Lee, and G.E. Dullerud
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Essick, R.; Lee, J.; Dullerud, G.E., "Control of Linear Switched Systems With Receding Horizon Modal Information," Automatic Control, IEEE Transactions on , vol.59, no.9, pp.2340,2352, Sept. 2014
doi: 10.1109/TAC.2014.2321251
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.(ID#:14-2603)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6808501&url=http%3A%2F%2Fieeexplore.ieee.org%2Fstamp%2Fstamp.jsp%3Ftp%3D%26arnumber%3D6808501
Publication Location: IEEE Transactions on Automatic Control, 2014


UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Path-By-Path Output Regulation of Switched Systems With a Receding Horizon of Modal Knowledge
Author(s): R. Essick, J.-W. Lee, and G.E. Dullerud
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Essick, R.; Ji-Woong Lee; Dullerud, G., "Path-by-path output regulation of switched systems with a receding horizon of modal knowledge," American Control Conference (ACC), 2014 , vol., no., pp.2650,2655, 4-6 June 2014
doi: 10.1109/ACC.2014.6859318
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 conditions 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. (ID#:14-2604)
URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6859318&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6859318
Publication Location: proceedings of the American Control Conference (ACC), 2014


UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: Proofs from Simulations and Modular Annotations
Author(s): Zhenqi Huang and Sayan Mitra
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Zhenqi Huang and Sayan Mitra. 2014. Proofs from simulations and modular annotations. InProceedings of the 17th international conference on Hybrid systems: computation and control(HSCC '14). ACM, New York, NY, USA, 183-192. DOI=10.1145/2562059.2562126 http://doi.acm.org/10.1145/2562059.2562126
We present a modular technique for simulation-based bounded verification for nonlinear dynamical systems. We introduce the notion of input-to-state discrepancy of each subsystem Ai in a larger nonlinear dynamical system A which bounds the distance between two (possibly diverging) trajectories of Ai in terms of their initial states and inputs. Using the IS discrepancy functions, we construct a low dimensional deterministic dynamical system M(d). For any two trajectories of A starting d distance apart, we show that one of them bloated by a factor determined by the trajectory of M contains the other. Further, by choosing appropriately small d's the overapproximations computed by the above method can be made arbitrarily precise. Using the above results we develop a sound and relatively complete algorithm for bounded safety verification of nonlinear ODEs. Our preliminary experiments with a prototype implementation of the algorithm show that the approach can be effective for verification of nonlinear models. (ID#:14-2605)
URL: http://dl.acm.org/citation.cfm?id=2562126
Publication Location: International Conference on Hybrid Systems: Computation and Control (HSCC 2014)


UIUC - University of Illinois at Urbana-Champaign
Topic: Classification of Cyber-Physical System Adversaries
Title: On Price of Privacy in Distributed Control Systems
Author(s): Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir Dullerud
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development and Deployment
Abstract: Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir E. Dullerud. 2014. On the cost of differential privacy in distributed control systems. In Proceedings of the 3rd international conference on High confidence networked systems (HiCoNS '14). ACM, New York, NY, USA, 105-114. DOI=10.1145/2566468.2566474 http://doi.acm.org/10.1145/2566468.2566474
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 individual 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. Finally, we show that the cost of e-differential privacy up to time T, for a linear stable system with N agents, is upper bounded by O(T3/ Ne2). (ID#:14-2606)
URL: http://dl.acm.org/citation.cfm?id=2566468.2566474
Publication Location: ACM International Conference on High Confidence Networked Systems (HiCoNS) 2014

UIUC - University of Illinois at Urbana-Champaign
Topic: End-to-end Analysis of Side Channels
Title: Website Detection Using Remote Traffic Analysis
Author(s): Xun Gong, Nikita Borisov, Negar Kiyavash, Nabil Schear
Hard Problem: Security-Metrics-Driven Evaluation, Design, Development, and Deployment
Abstract: Xun Gong, Nikita Borisov, Negar Kiyavash, and Nabil Schear. 2012. Website detection using remote traffic analysis. In Proceedings of the 12th international conference on Privacy Enhancing Technologies (PETS'12), Simone Fischer-Hubner and Matthew Wright (Eds.). Springer-Verlag, Berlin, Heidelberg, 58-78. DOI=10.1007/978-3-642-31680-7_4 http://dx.doi.org/10.1007/978-3-642-31680-7_4
Recent work in traffic analysis has shown that traffic patterns leaked through side channels can be used to recover important semantic information. For instance, attackers can find out which website, or which page on a website, a user is accessing simply by monitoring the packet size distribution. We show that traffic analysis is even a greater threat to privacy than previously thought by introducing a new attack that can be carried out remotely. In particular, we show that, to perform traffic analysis, adversaries do not need to directly observe the traffic patterns. Instead, they can gain sufficient information by sending probes from a far-off vantage point that exploits a queuing side channel in routers.
To demonstrate the threat of such remote traffic analysis, we study a remote website detection attack that wo rks against home broadband users. Because the remotely observed traffic patterns are more noisy than those obtained using previous schemes based on direct local traffic monitoring, we take a dynamic time warping (DTW) based approach to detecting fingerprints from the same website. As a new twist on website fingerprinting, we consider a website detection attack, where the attacker aims to find out whether a user browses a particular web site, and its privacy implications. We show experimentally that, although the success of the attack is highly variable, depending on the target site, for some sites very low error rates. We also show how such website detection can be used to deanonymize message board users. (ID#:14-2607)
URL: http://dl.acm.org/citation.cfm?id=2359021
Publication Location: 12th Privacy Enhancing Technologies Symposium (PETS) 2012

UIUC - University of Illinois at Urbana-Champaign
Topic: Attack-Tolerant Systems
Title: An Algorithmic Approach to Error Localization and Partial Recomputation for Low-Overhead Fault Tolerance on Parallel Systems
Author(s): Joseph Sloan, Greg Bronevetsky, and Rakesh Kumar
Abstract: Sloan, J.; Kumar, R.; Bronevetsky, G., "An algorithmic approach to error localization and partial recomputation for low-overhead fault tolerance," Dependable Systems and Networks (DSN), 2013 43rd Annual IEEE/IFIP International Conference on , vol., no., pp.1,12, 24-27 June 2013 doi: 10.1109/DSN.2013.6575309
The increasing size and complexity of massively parallel systems (e.g. HPC systems) is making it increasingly likely that individual circuits will produce erroneous results. For this reason, novel fault tolerance approaches are increasingly needed. Prior fault tolerance approaches often rely on checkpoint-rollback based schemes. Unfortunately, such schemes are primarily limited to rare error event scenarios as the overheads of such schemes become prohibitive if faults are common. In this paper, we propose a novel approach for algorithmic correction of faulty application outputs. The key insight for this approach is that even under high error scenarios, even if the result of an algorithm is erroneous, most of it is correct. Instead of simply rolling back to the most recent checkpoint and repeating the entire segment of computation, our novel resilience approach uses algorithmic error localization and partial recomputation to efficiently correct the corrupted results. We evaluate our approach in the specific algorithmic scenario of linear algebra operations, focusing on matrix-vector multiplication (MVM) and iterative linear solvers. We develop a novel technique for localizing errors in MVM and show how to achieve partial recomputation within this algorithm, and demonstrate that this approach both improves the performance of the Conjugate Gradient solver in high error scenarios by 3x-4x and increases the probability that it completes successfully by up to 60% with parallel experiments up to 100 nodes. (ID#:14-2608)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6575309
Publication Location: IEEE/IFIP International Conference on Dependable Systems and Networks, DSN, 2013

UIUC - University of Illinois at Urbana-Champaign
Topic: From Measurements to Security Science - Data-Driven Approach
Title: Adapting Bro into SCADA: building a specification-based intrusion detection system for the DNP3 protocol
Author(s): H. Lin, A. Slagell, C. Di Martino, Z. Kalbarczyk, and R. Iyer
Abstract: When SCADA systems are exposed to public networks, attackers can more easily penetrate the control systems that operate electrical power grids, water plants, and other critical infrastructures. To detect such attacks, SCADA systems require an intrusion detection technique that can understand the information carried by their usually proprietary network protocols.
To achieve that goal, we propose to attach to SCADA systems a specification-based intrusion detection framework based on Bro [7][8], a runtime network traffic analyzer. We have built a parser in Bro to support DNP3, a network protocol widely used in SCADA systems that operate electrical power grids. This built-in parser provides a clear view of all network events related to SCADA systems. Consequently, security policies to analyze SCADA-specific semantics related to the network events can be accurately defined. As a proof of concept, we specify a protocol validation policy to verify that the semantics of the data extracted from network packets conform to protocol definitions. We performed an experimental evaluation to study the processing capabilities of the proposed intrusion detection framework .(ID#:14-2609)
URL: http://dl.acm.org/citation.cfm?id=2459982
Publication Location: Annual Cyber Security and Information Intelligence Research Workshop (CSIIRW 2012)


UIUC - University of Illinois at Urbana-Champaign
Topic: From Measurements to Security Science - Data-Driven Approach
Title: Semantic Security Analysis of SCADA Networks to Detect Malicious Control Commands in Power Grids
Author(s): H. Lin, A. Slagell, Z. Kalbarczyk, P. Sauer, R. Iyer
Abstract: Hui Lin, Adam Slagell, Zbigniew Kalbarczyk, Peter W. Sauer, and Ravishankar K. Iyer. 2013. Semantic security analysis of SCADA networks to detect malicious control commands in power grids. In Proceedings of the first ACM workshop on Smart energy grid security (SEGS '13). ACM, New York, NY, USA, 29-34. DOI=10.1145/2516930.2516947 http://doi.acm.org/10.1145/2516930.2516947
In the current generation of SCADA (Supervisory Control And Data Acquisition) systems used in power grids, a sophisticated attacker can exploit system vulnerabilities and use a legitimate maliciously crafted command to cause a wide range of system changes that traditional contingency analysis does not consider and remedial action schemes cannot handle. To detect such malicious commands, we propose a semantic analysis framework based on a distributed network of intrusion detection systems (IDSes). The framework combines system knowledge of both cyber and physical infrastructure in power grid to help IDS to estimate execution consequences of control commands, thus to reveal attacker's malicious intentions. We evaluated the approach on the IEEE 30-bus system. Our experiments demonstrate that: (i) by opening 3 transmission lines, an attacker can avoid detection by the traditional contingency analysis and instantly put the tested 30-bus system into an insecure state and (ii) the semantic analysis provides reliable detection of malicious commands with a small amount of analysis time. (ID#:14-2610)
URL: http://dl.acm.org/citation.cfm?id=2516947
Publication Location: IEEE Int'l Conference on Smart Grid Communications, SmartGridComm 2013

UIUC - University of Illinois at Urbana-Champaign
Topic: Protocol Verification: Beyond Reachability Properties
Title: Asymmetric unification: A new unification paradigm for cryptographic protocol analysis
Author(s): Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos'e Meseguer, Paliath Narendran, Sonia Santiago and Ralf Sasse
Abstract: Available from Springer via link listed below.. (ID#:14-2611)
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-38574-2_16
Publication Location: Intl. Conf. On Automated Deduction (CADE 2013)


UIUC - University of Illinois at Urbana-Champaign
Topic: Protocol Verification: Mathematical Foundations & Analysis Techniques for Protocol Indistinguishability
Title: Sequential Protocol Compositon in Maude-NPA
Author(s): Santiago Escobar, Catherine Meadows, Jose Meseguer and Sonia Santiago
Hard Problem: Scalability and Composability
Abstract: Santiago Escobar, Catherine Meadows, Jos\&\#233; Meseguer, and Sonia Santiago. 2010. Sequential protocol composition in maude-NPA. In Proceedings of the 15th European conference on Research in computer security (ESORICS'10), Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou (Eds.). Springer-Verlag, Berlin, Heidelberg, 303-318.
Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified separately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification. Moreover, we show that, by a simple protocol transformation, we are able to analyze and verify this dynamic composition in the current Maude-NPA tool. We prove soundness and completeness of the protocol transformation with respect to the extended operational semantics, and illustrate our results on some examples. (ID#:14-2612)
URL: http://dl.acm.org/citation.cfm?id=1888906
Publication Location: Computer Security - ESORICS 2010


UIUC - University of Illinois at Urbana-Champaign
Topic: Protocol Verification: Mathematical Foundations & Analysis Techniques for Protocol Indistinguishability
Title: A Rewriting- based forward semantics for Maude-NPA
Author(s): Santiago Escobar, Catherine Meadows, Jose Meseguer and Sonia Santiago
Hard Problem: Scalability and Composability
Abstract: The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It tries to find secrecy or authentication attacks by searching backwards from an insecure attack state pattern that may contain logical variables, in such a way that logical variables become properly instantiated in order to find an initial state. The execution mechanism for this logical reachability is narrowing modulo an equational theory. Although Maude-NPA also possesses a forwards semantics naturally derivable from the backwards semantics, it is not suitable for state space exploration or protocol simulation.
In this paper we define an executable forwards semantics for Maude-NPA, instead of its usual backwards one, and restrict it to the case of concrete states, that is, to terms without logical variables. This case corresponds to standard rewriting modulo an equational theory. We prove soundness and completeness of the backwards narrowing-based semantics with respect to the rewriting-based forwards semantics. We show its effectiveness as an analysis method that complements the backwards analysis with new prototyping, simulation, and explicit-state model checking features by providing some experimental results. (ID#:14-2613)
URL: http://dl.acm.org/citation.cfm?id=2600186&dl=ACM&coll=DL&CFID=552978724&CFTOKEN=96539078
Publication Location: In Proceedings HotSoS '14

UIUC - University of Illinois at Urbana-Champaign
Topic: Science of Human Circumvention of Security (SHuCS)
Title: Circumvention of Security: Good Users Do Bad Things
Author(s): J. Blythe, R. Koppel, and S.W. Smith
Hard Problem: Human Behavior
Abstract: Blythe, J.; Koppel, R.; Smith, S.W., "Circumvention of Security: Good Users Do Bad Things," Security & Privacy, IEEE , vol.11, no.5, pp.80,83, Sept.-Oct. 2013 doi: 10.1109/MSP.2013.110
Conventional wisdom is that the textbook view describes reality, and only bad people (not good people trying to get their jobs done) break the rules. And yet it doesn't, and good people circumvent. (ID#:14-2614)
URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6630017
Publication Location: IEEE Security and Privacy 2013

UIUC - University of Illinois at Urbana-Champaign
Topic: Quantitative Security Metrics for Cyber-Human Systems
Title: Simulation debugging and visualization in the Mobius modeling framework
Author(s): Buchanan, Craig
Hard Problem: Metrics
Abstract: Available from Springer via link listed below.. (ID#:14-2615)
URL: http://link.springer.com/chapter/10.1007/978-3-319-10696-0_18
Publication Location: M.S. Thesis, ECE Dept., Univ. of Illinois

UIUC - University of Illinois at Urbana-Champaign
Topic: No Topic Listed
Title: VeriFlow: Verifying Network-Wide Invariants in Real Time
Author(s): Ahmed Khurshid, Kelvin Zou, Wenxuan Zhou, Matthew Caesar, P. Brighten Godfrey
Abstract: Networks are complex and prone to bugs. Existing tools that check configuration files and data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise.

Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a preliminary design, VeriFlow, which suggests that this goal is achievable. VeriFlow is a layer between a software-defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted. Based on an implementation using a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion. (ID#:14-2616)
URL: http://dl.acm.org/citation.cfm?id=2342452
Publication Location: ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (HotSDN), August 2012

UIUC - University of Illinois at Urbana-Champaign
Topic: Data Driven Security Models and Analysis
Title: An Experiment Using Factor Graph for Early Attack Detection
Author(s): P. Cao, K-W. Chung, A. Slagell, Z. Kalbarcyk, R. Iyer
Hard Problem: Metrics, Resilient Architectures, Human Behavior
Abstract: Not Found (ID#:14-2617)
URL: Not found
See: : "Preemptive Intrusion Detection" by P. Cao, K-W. Chung, A. Slagell, Z. Kalbarczyk, R. Iyer at http://dl.acm.org/citation.cfm?id=2600177

Note:

Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to SoS.Project (at) SecureDataBank.net for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.