Biblio

Peer-assisted content distribution networks (CDNs)have emerged to improve performance and reduce deployment costs of traditional, infrastructure-based content delivery networks. This is done by employing peer-to-peer data transfers to supplement the resources of the network infrastructure. However, these hybrid systems are vulnerable to accounting attacks in which the peers, or caches, collude with clients in order to report that content was transferred when it was not. This is a particular issue in systems that incentivize cache participation, because malicious caches may collect rewards from the content publishers operating the CDN without doing any useful work. In this paper, we introduce CAPnet, the first technique that lets untrusted caches join a peer-assisted CDN while providing a bound on the effectiveness of accounting attacks. At its heart is a lightweight cache accountability puzzle that clients must solve before caches are given credit. This puzzle requires colocating the data a client has requested, so its solution confirms that the content has actually been retrieved. We analyze the security and overhead of our scheme in realistic scenarios. The results show that a modest client machine using a single core can solve puzzles at a rate sufficient to simultaneously watch dozens of 1080p videos. The technique is designed to be even more scalable on the server side. In our experiments, one core of a single low-end machine is able to generate puzzles for 4.26 Tbps of bandwidth - enabling 870,000 clients to concurrently view the same 1080p video. This demonstrates that our scheme can ensure cache accountability without degrading system productivity.

In this paper, we describe an abstraction-based method for synthesizing a state-based switching control for stabilizing a family of dynamical systems. Given a set of dynamical systems and a set of polyhedral switching surfaces, the algorithm synthesizes a strategy that assigns to every surface the linear dynamics to switch to at the surface. Our algorithm constructs a finite game graph that consists of the switching surfaces as the existential nodes and the choices of the dynamics as the universal nodes. In addition, the edges capture quantitative information about the evolution of the distance of the state from the equilibrium point along the executions. A switching strategy for the family of dynamical systems is extracted by finding a strategy on the game graph which results in plays having a bounded weight. Such a strategy is obtained by reducing the problem to the strategy synthesis for an energy game, which is a well-studied problem in the literature. We have implemented our algorithm for polyhedral inclusion dynamics and linear dynamics. We illustrate our algorithm on examples from these two classes of systems.

We consider the problem of translating a deterministic \textbackslashemph\simulation model\ (like Matlab-Simunk, Modelica or Ptolemy models) into a \textbackslashemphěrification model\ expressed by a network of hybrid automata. The goal is to verify safety using reachability analysis on the verification model. Simulation models typically use transitions with urgent semantics, which must be taken as soon as possible. Urgent transitions also make it possible to decompose systems that would otherwise need to be modeled with a monolithic hybrid automaton. In this paper, we include urgent transitions in our verification models and propose a suitable adaptation of our reachability algorithm. However, the simulation model, due to its imperfections, may be unsafe even though the corresponding hybrid automata are safe. Conversely, set-based reachability may not be able to show safety of an ideal formal model, since complex dynamics necessarily entail overapproximations. Taken as a whole, the formal modeling and verification process can both falsely claim safety and fail to show safety of the concrete system. We address this inconsistency by relaxing the model as follows. The standard semantics of hybrid automata is a mathematical idealization, where reactions are considered to be instantaneous and physical measurements infinitely precise. We propose semantics that relax these assumptions, where guard conditions are sampled in discrete time and admit measurement errors. The relaxed semantics can be translated to an equivalent relaxed model in standard semantics. The relaxed model is realistic in the sense that it can be implemented on hardware fast and precise enough, and in a way that safety is preserved. Finally, we show that overapproximative reachability analysis can show safety of relaxed models, which is not the case in general.

In the modern retailing industry, many enterprise resource planning (ERP) systems are considered legacy software systems that have become too expensive to replace and too costly to re-engineer. Countering the need to maintain and extend the business value of these systems is the need to do so in the simplest, cheapest, and least risky manner available. There are a number of approaches used by software engineers to mitigate the negative impact of evolving a legacy systems, including leveraging service-oriented architecture to automate manual tasks previously performed by humans. A relatively recent approach in software engineering focuses upon implementing self-managing attributes, or “autonomic” behavior in software applications and systems of applications in order to reduce or eliminate the need for human monitoring and intervention. Entire systems can be autonomic or they can be hybrid systems that implement one or more autonomic components to communicate with external systems. In this paper, we describe a commercial development project in which a legacy multi-channel commerce enterprise resource planning system was extended with service-oriented architecture an autonomic control loop design to communicate with an external third-party security screening provider. The goal was to reduce the cost of the human labor necessary to screen an ever-increasing volume of orders and to reduce the potential for human error in the screening process. The solution automated what was previously an inefficient, incomplete, and potentially error-prone manual process by inserting a new autonomic software component into the existing order fulfillment workflow.

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

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.

Design and testing of pacemaker is challenging because of the need to capture the interaction between the physical processes (e.g. voltage signal in cardiac tissue) and the embedded software (e.g. a pacemaker). At the same time, there is a growing need for design and certification methodologies that can provide quality assurance for the embedded software. We describe recent progress in simulation-based techniques that are capable of ensuring guaranteed coverage. Our methods employ discrep- ancy functions, which impose bounds on system dynamics, and proceed through iteratively constructing over-approximations of the reachable set of states. We are able to prove time bounded safety or produce counterexamples. We illustrate the techniques by analyzing a family of pacemaker designs against time duration requirements and synthesize safe parameter ranges. We conclude by outlining the potential uses of this technology to improve the safety of medical device designs.