Biblio

In this paper we explore the differential perceptions of cybersecurity professionals and general users regarding access rules and passwords. We conducted a preliminary survey involving 28 participants: 15 cybersecurity professionasl and 13 general users. We present our preliminary findings and explain how such survey data might be used to improve security in practice. We focus on user fatigue with access rules and passwords.

We present a technique for bounded invariant verification of nonlinear networked dynamical systems with delayed interconnections. The underlying problem in precise boundedtime verification lies with computing bounds on the sensitivity of trajectories (or solutions) to changes in initial states and inputs of the system. For large networks, computing this sensitivity
with precision guarantees is challenging. We introduce the notion of input-to-state (IS) discrepancy of each module or subsystem in a larger nonlinear networked dynamical system. The IS discrepancy bounds the distance between two solutions or trajectories of a module in terms of their initial states and their inputs. Given the IS discrepancy functions of the modules, we show that it is possible to effectively construct a reduced (low dimensional) time-delayed dynamical system, such that the trajectory of this reduced model precisely bounds the distance between the trajectories of the complete network with changed initial states. Using the above results we develop a sound and relatively complete algorithm for bounded invariant verification of networked dynamical systems consisting of nonlinear modules interacting through possibly delayed signals. Finally, we introduce a local version of IS discrepancy and show that it is possible to compute them using only the Lipschitz constant and the Jacobian of the dynamic function of the modules.
 

The successful operations of modern power grids are highly dependent on a reliable and ecient underlying communication network. Researchers and utilities have started to explore the opportunities and challenges of applying the emerging software-de ned networking (SDN) technology to enhance eciency and resilience of the Smart Grid. This trend calls for a simulation-based platform that provides sufcient exibility and controllability for evaluating network application designs, and facilitating the transitions from inhouse research ideas to real productions. In this paper, we present DSSnet, a hybrid testing platform that combines a power distribution system simulator with an SDN emulator to support high delity analysis of communication network applications and their impacts on the power systems. Our contributions lay in the design of a virtual time system with the tight controllability on the execution of the emulation system, i.e., pausing and resuming any speci ed container processes in the perception of their own virtual clocks, with little overhead scaling to 500 emulated hosts with an average of 70 ms overhead; and also lay in the ecient synchronization of the two sub-systems based on the virtual time. We evaluate the system performance of DSSnet, and also demonstrate the usability through a case study by evaluating a load shifting algorithm.

While there have been various studies identifying and classifying Android malware, there is limited discussion of the broader class of apps that fall in a gray area. Mobile grayware is distinct from PC grayware due to differences in operating system properties. Due to mobile grayware’s subjective nature, it is difficult to identify mobile grayware via program analysis alone. Instead, we hypothesize enhancing analysis with text analytics can effectively reduce human effort when triaging grayware. In this paper, we design and implement heuristics for seven main categories of grayware.We then use these heuristics to simulate grayware triage on a large set of apps from Google Play. We then present the results of our empirical study, demonstrating a clear problem of grayware. In doing so, we show how even relatively simple heuristics can quickly triage apps that take advantage of users in an undesirable way.
 

In recent years, online programming and software engineering education via information technology has gained a lot of popularity. Typically, popular courses often have hundreds or thousands of students but only a few course sta members. Tool automation is needed to maintain the quality of education. In this paper, we envision that the capability of quantifying behavioral similarity between programs is helpful for teaching and learning programming and software engineering, and propose three metrics that approximate the computation of behavioral similarity. Speci cally, we leverage random testing and dynamic symbolic execution (DSE) to generate test inputs, and run programs on these test inputs to compute metric values of the behavioral similarity. We evaluate our metrics on three real-world data sets from the Pex4Fun platform (which so far has accumulated more than 1.7 million game-play interactions). The results show that our metrics provide highly accurate approximation to the behavioral similarity. We also demonstrate a number of practical applications of our metrics including hint generation, progress indication, and automatic grading.

Anonymous messaging platforms like Whisper and Yik Yak allow users to spread messages over a network (e.g., a social network) without revealing message authorship to other users. The spread of messages on these platforms can be modeled by a diffusion process over a graph. Recent advances in network analysis have revealed that such diffusion processes are vulnerable to author deanonymization by adversaries with access to metadata, such as timing information. In this work, we ask the fundamental question of how to propagate anonymous messages over a graph to make it difficult for adversaries to infer the source. In particular, we study the performance of a message propagation protocol called adaptive diffusion introduced in (Fanti et al., 2015). We prove that when the adversary has access to metadata at a fraction of corrupted graph nodes, adaptive diffusion achieves asymptotically optimal source-hiding and significantly outperforms standard diffusion. We further demonstrate empirically that adaptive diffusion hides the source effectively on real social networks.
 

Anonymous messaging applications have recently gained popularity as a means for sharing opinions without fear of judgment or repercussion. These messages propagate anonymously over a network, typically de ned by social connections or physical proximity. However, recent advances in rumor source detection show that the source of such an anonymous message can be inferred by certain statistical inference attacks. Adaptive di usion was recently proposed as a solution that achieves optimal source obfuscation over regular trees. However, in real social networks, the degrees difer from node to node, and adaptive di usion can be signicantly sub-optimal. This gap increases as the degrees become more irregular.

In order to quantify this gap, we model the underlying network as coming from standard branching processes with i.i.d. degree distributions. Building upon the analysis techniques from branching processes, we give an analytical characterization of the dependence of the probability of detection achieved by adaptive di usion on the degree distribution. Further, this analysis provides a key insight: passing a rumor to a friend who has many friends makes the source more ambiguous. This leads to a new family of protocols that we call Preferential Attachment Adaptive Di usion (PAAD). When messages are propagated according to PAAD, we give both the MAP estimator for nding the source and also an analysis of the probability of detection achieved by this adversary. The analytical results are not directly comparable, since the adversary's observed information has a di erent distribution under adaptive di usion than under PAAD. Instead, we present results from numerical experiments that suggest that PAAD achieves a lower probability of detection, at the cost of increased communication for coordination.

SDN’s logically centralized control provides an insertion point for programming the network. While it is generally agreed that higherlevel abstractions are needed to make that programming easy, there is little consensus on what are the “right” abstractions. Indeed, as SDN moves beyond its initial specialized deployments to broader use cases, it is likely that network control applications will require diverse abstractions that evolve over time. To this end, we champion a perspective that SDN control fundamentally revolves around data representation. We discard any application-specific structure that might be outgrown by new demands. Instead, we adopt a plain data representation of the entire network — network topology, forwarding, and control applications — and seek a universal data language that allows application programmers to transform the primitive representation into any high-level representations presented to applications or network operators. Driven by this insight, we present a system, Ravel, that implements an entire SDN network control infrastructure within a standard SQL database. In Ravel, network abstractions take the form of user-defined SQL views expressed by SQL queries that can be added on the fly. A key challenge in realizing this approach is to orchestrate multiple simultaneous abstractions that collectively affect the same underlying data. To achieve this, Ravel enhances the database with novel data integration mechanisms that merge the multiple views into a coherent forwarding behavior. Moreover, Ravel is exposed to applications through the one simple, familiar and highly interoperable SQL interface. While this is an ambitious long-term goal, our prototype built on the PostgreSQL database exhibits promising performance even for large scale networks.

The emerging software-defined networking (SDN) technology decouples the control plane from the data plane in a computer network with open and standardized interfaces, and hence opens up the network designers’ options and ability to innovate. The wide adoption of SDN in industry has motivated the development of large-scale, high-fidelity testbeds for evaluation of systems that incorporate SDN. In this article, we develop a framework to support OpenFlow-based SDN simulation and distributed emulation, by leveraging our prior work on a hybrid network testbed with a parallel network simulator and a virtual-machine-based emulation system. We show how to exploit typical SDN controller behaviors to handle performance issues caused by the centralized controller in parallel discrete-event simulation. In particular, we develop an asynchronous synchronization algorithm for passive SDN controllers and design a two-level architecture for active SDN controllers. We evaluate the system performance, showing good scalability. Finally, we present a case study, using the testbed, to evaluate network verification applications in an SDN-based data center network. CCS Concepts: Networks→Network simulations; Computing methodologies→Simulation

The Pi Calculus is a popular formalism for modeling distributed computation. Session Types extend the Pi Calculus with a static, inferable type system. Dependent Types allow for a more precise characterization of the behavior of programs, but in their full generality are not inferable. In this paper, we present LiquidPi an approach that combines the dependent type inferencing of Liquid Types with Honda’s Session Types to give a more precise automatically derived description of the behavior of distributed programs. These types can be used to describe/enforce safety properties of distributed systems. We present a type system parametric over an underlying functional language with Pi Calculus connectives and give an inference algorithm for it by means of efficient external solvers and a set of dependent qualifier templates.

In this paper, we consider a minimax control problem for linear time-invariant (LTI) systems over unreliable communication channels. This can be viewed as an extension of the H^∞ optimal control problem, where the transmission from the plant output sensors to the controller, and from the controller to the plant are over sporadically failing channels. We consider two different scenarios for unreliable communication. The first one is where the communication channel provides perfect acknowledgments of successful transmissions of control packets through a clean reverse channel, that is the TCP (Transmission Control Protocol). Under this setting, we obtain a class of output feedback minimax controllers; we identify a set of explicit threshold-type existence conditions in terms of the H^∞ disturbance attenuation parameter and the packet loss rates that guarantee stability and performance of the closed-loop system. The second scenario is one where there is no acknowledgment of successful transmissions of control packets, that is the UDP (User Datagram Protocol). We consider a special case of this problem where there is no measurement noise in the transmission from the sensors. For this problem, we obtain a class of corresponding minimax controllers by characterizing a set of (different) existence conditions. We also discuss stability and performance of the closed-loop system. We provide simulations to illustrate the results in all cases.

Critical infrastructures, such as power grids and transportation systems, are increasingly using open networks for operation. The use of open networks poses many challenges for control systems.  The  classical  design  of  control systems  takes  into  account  modeling uncertainties  as  well  as  physical  disturbances,  providing  a  multitude  of control design methods such as robust control, adaptive control, and stochastic control. With the growing level of integration of control systems with new information technologies, modern control systems face uncertainties not only from the physical world but also from the cybercomponents of the system.  The vulnerabilities of the software deployed in the new control system infra- structure will expose the control system to many potential Game-Theoretic Methods for Robustness, Security, and Resilience of Cyberphysical Control Systems risks and threats from attackers. Exploitation of these vulnerabilities can lead to severe damage as has been reported in various news outlets [1], [2]. More recently, it has been reported in [3] and [4] that a computer worm, Stuxnet, was spread to target Siemens supervisory control and data acquisition (SCADA) systems that are configured to control and monitor specific industrial processes.

We analyze the stability properties of a susceptible-infected-susceptible diffusion model over directed networks. Similar to the majority of infection spread dynamics, this model exhibits a threshold phenomenon. When the curing rates in the network are high, the all-healthy state is globally asymptotically stable (GAS). Otherwise, an endemic state arises and the entire network could become infected. Using notions from positive systems theory, we prove that the endemic state is GAS in strongly connected networks. When the graph is weakly connected, we provide conditions for the existence, uniqueness, and global asymptotic stability of weak and strong endemic states. Several simulations demonstrate our results.

In this paper, we formulate a three-player three-stage Colonel Blotto game, in which two players fight against a common adversary. We assume that the game is one of complete information, that is, the players have complete and consistent information on the underlying model of the game; further, each player observes the actions taken by all players up to the previous stage.  The setting  under  consideration is similar  to the one considered in our recent  work [1], but with a different  information structure  during  the  second  stage  of the  game;  this  leads  to  a  significantly different  solution.

In the first stage, players can add additional battlefields. In the second stage, the players (except the adversary) are allowed to transfer resources among  each  other  if it  improves their  expected payoffs, and simultaneously, the adversary decides  on the amount  of resource it allocates  to the battle with each player subject to its resource constraint. At the third stage, the players and the adversary fight against each other with updated resource levels and battlefields. We compute the subgame-perfect Nash equilibrium for this game. Further, we show that when playing according to the equilibrium, there are parameter regions  in which (i) there  is a net  positive transfer, (ii)  there  is absolutely no transfer, (iii) the  adversary fights  with  only  one player, and  (iv)  adding  battlefields is beneficial to a player. In doing so, we also exhibit a counter-intuitive property of Nash equilibrium in games: extra information to a player in the game does not necessarily lead to a better performance for that player.  The result finds application in resource allocation problems for securing cyber-physical systems.

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 H^∞ disturbance 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.

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.