Stabilization, Safety, and Security of Distributed Systems
13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011, Proceedings
Erschienen am 9. Oktober 2011
XIV, 452 Seiten
978-3-642-24550-3 (ISBN)
Beschreibung
This book constitutes the proceedings of the 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS 2011, held in Grenoble, France, in October 2011.
The 29 papers presented were carefully reviewed and selected from 79 submissions. They cover the following areas: ad-hoc, sensor, and peer-to-peer networks; safety and verification; security; self-organizing and autonomic systems; and self-stabilization.
Weitere Details
Weitere Ausgaben
Andere Ausgaben
Xavier Défago | Franck Petit | Vincent Villain
Stabilization, Safety, and Security of Distributed Systems
13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011, Proceedings
Buch
09/2011
1. Auflage
Springer
53,49 €
Versand in 7-9 Tagen
Inhalt
- Title
- Preface
- Conference Organization
- Table of Contents
- Silence Is Golden: Self-stabilizing Protocols Communication-Efficient after Convergence
- Motivation
- Point-to-Point Communication Model
- Local-Broadcast Communication Model
- References
- Computing in Time-Varying Networks
- The K-Observer Problem in Computer Networks
- Introduction
- The K-Observer Problem
- K-Observers of Tree Networks
- K-Observers of Ring Networks
- K-Observers of Large Grid Networks
- Applications
- Concluding Remarks
- References
- Pragmatic Self-stabilization of Atomic Memory in Message-Passing Systems
- Introduction
- Preliminaries
- Overview of the Algorithm
- The Basic Quorum-Based Simulation
- Epochs
- A Bounded Labeling Scheme with Uninitialized Values
- Putting the Pieces Together
- Outline of Correctness Proof
- Discussion
- References
- An Algorithm for Implementing BFT Registers in Distributed Systems with Bounded Churn
- Introduction
- Related Work
- System Model
- Register Specification
- Safe Register Implementation
- A Protocol for Eventually Synchronous System
- Concluding Remarks
- References
- Computing Time Complexity of Population Protocols with Cover Times - The ZebraNet Example
- Introduction
- Model and Notations
- Non Convergence of the Original Protocol
- Modified ZebraNet Protocol 1
- Convergence of MZP1
- Upper Bound to the MZP1 Complexity
- Lower Bound to MZP1 Complexity
- Modified ZebraNet Protocol 2
- Upper Bound to MZP2 Complexity
- Lower Bound to MZP2 Complexity
- Bounded Memory
- Conclusion
- References
- Building Self-stabilizing Overlay Networks with the Transitive Closure Framework
- Introduction
- Our Contributions
- Model
- SKIP+ Graphs
- Transitive Closure Framework
- A Lower Bound
- Bounding the Detector Diameter
- TCF for SKIP+ Graphs
- The DETECT Predicate and REPAIR Subroutine
- Analysis of the Transitive Closure Framework
- The Local Repair Framework
- The Local Repair Program
- Example: JOIN in SKIP+ Graphs
- References
- Active Stabilization
- Introduction
- The Concept of Active Stabilization
- Relation between Different Types of Active and Passive Stabilization
- Relation between Active and Passive Stabilization
- Relation between Active, Fragile Active, and Contained Active Stabilization
- Comparing the Cost of Automated Verification for Active and Passive Stabilization
- Methodology for Designing Active Stabilizing Programs
- Relation between Active Stabilization and Other Stabilization Techniques
- Fault-Contained Stabilization
- Byzantine Self-Stabilization
- Related Work
- Conclusion
- References
- Robot Networks with Homonyms: The Case of Patterns Formation
- Introduction
- Model
- Symmetricity, Regularity and Weber Points
- Polar Coordinate System
- Symmetricity
- Regularity
- Weber Points
- Detection of Regular Configurations
- Preliminaries
- Detection of Even Regularity
- Detection of Odd Regularity
- Formation of a Series of Geometric Patterns: Lower Bound
- Formation of Series of Patterns: Upper Bound
- Intermediate Configurations
- Transitions between Configurations
- Conclusion
- References
- A Non-topological Proof for the Impossibility of k-Set Agreement
- Introduction
- Model of Computation
- Immediate Snapshot Executions
- Impossibility of k-Set Agreement
- An Operational Perspective
- References
- Formal Verification of Consensus Algorithms Tolerating Malicious Faults
- Introduction
- The Heard-of Model for Distributed Algorithms
- A Round-Based Computational Model
- Executing HO Algorithms
- Two Models of Executions
- A Reduction Theorem
- The Consensus Problem
- Representing the Heard-of Model in Isabelle
- Representing Algorithms and Communication Predicates
- Defining Coarse-Grained Executions
- Verifying Concrete Algorithms
- Modeling and Verifying Non-synchronous Algorithms in Isabelle
- Verifying a Synchronous Algorithm
- Related and Future Work
- References
- The Computational Power of Simple Protocols for Self-awareness on Graphs
- Introduction
- Previous Work
- Our Results - Roadmap
- A Formal Model: Mediated Graph Protocols
- Properties of MGPs
- MGPs with Stabilizing Input Graphs
- Composition of MGPs
- Disconnected Graphs
- Deciding Connectivity
- Computing Graph Languages on Disconnected Graphs
- An Exact Characterization: GMGP=LGNSPACE
- Conclusions - Future Research Directions
- References
- Self-stabilizing Labeling and Ranking in Ordered Trees
- Introduction
- Contributions
- Related Work
- Roadmap
- Preliminaries
- Computational Model
- Self-stabilization and Silence
- Composition
- Computing Guide Pairs
- Guide Pairs
- Algorithm GUIDE
- Rank Ordering
- Overview of CRK
- Formal Definition of CRK
- References
- Fault-Tolerant Algorithms for Tick-Generation in Asynchronous Logic: Robust Pulse Generation
- Introduction and Related Work
- Model
- The FATAL Pulse Synchronization Protocol
- References
- The South Zone: Distributed Algorithms for Alliances
- Introduction
- Model and Definitions
- Minimal (f,g)-Alliances
- Srimani and Xu's Algorithm
- Faster Id-Based Deterministic Synchronous Distributed Minimal (f,g)-Alliance Algorithm for f g
- Anonymous Randomized Synchronous Distributed Minimal (f,g)-Alliance Algorithm for f g
- Conclusions and Open Problems
- References
- Social Market: Combining Explicit and Implicit Social Networks
- Introduction
- System Model and Problem Definition
- Social Market
- Background: Gossip-Based Implicit Networks
- Trust-Aware Peer Sampling
- Clustering Trusted Nodes
- Evaluation
- Setting
- Terms of Comparison
- Results
- Related Work
- Conclusions and Future Directions
- References
- TRUMANBOX: Improving Dynamic Malware Analysis by Emulating the Internet
- Introduction
- Related Work
- Contributions
- Roadmap
- Technical Background
- Naming Conventions
- Bridging and (Re-)directing Data
- Extracting Non-altered Header Information
- TrumanBox
- Approach
- Implementation Details
- Extensions to Half Proxy Mode
- Logging
- Evaluation
- Testbed and Evaluation Setting
- Full Emulation Mode
- Half Proxy Mode
- Conclusion
- References
- Rendezvous Tunnel for Anonymous Publishing: Clean Slate and Tor Based Designs
- Introduction
- Settings and Requirements
- RTAP Architecture
- Publication
- Retrieval
- Anonymity Analysis
- Tor Based Solution
- References
- Snake: Control Flow Distributed Software Transactional Memory
- Introduction
- Related Work
- System Overview
- System Model
- Programming Model
- Implementation
- Instrumentation Engine
- Distributed Software Transactional Memory
- Distributed Contention Management
- Global Commitment Protocol
- Experimental Evaluation
- Conclusions
- References
- POLISH: Proactive Co-operative LInk Self-Healing for Wireless Sensor Networks
- Introduction
- Related Work
- Preliminaries
- Notation
- Requirements
- System and Network Assumptions
- Adversarial Model
- The POSH Scheme
- Overview
- Boundary of Security Evaluation in POSH
- The Proposed Scheme
- The Protocol
- The Link State
- Analysis
- Evaluation by Simulation
- Analytical Model
- Secure Connectivity
- Efficiency of POLISH
- Comparison
- Security
- Efficiency of Key Update
- Conclusion
- References
- The Weakest Failure Detector to Implement a Register in Asynchronous Systems with Hybrid Communication
- Introduction
- Atomic Register
- Building an Atomic Register in a Message-Passing System
- Content of the Paper
- A Hybrid Communication System Model
- System Model with Hybrid Communication
- An Atomic Register Cannot Be Built in SM_MPn,m[] when m&1
- A New Failure Detector Class
- Failure Pattern and Failure Detector
- The Failure Detector Class
- The Failure Detector Class M
- M is Sufficient: Building an Atomic Register in SM_MPn,m[M]
- M is Necessary
- M is the Weakest FD for a Register in a Hybrid Communication Model
- Bonnet-Raynal's Extraction Algorithm
- Minimality of M
- M is Strictly Weaker Than When m&n
- On the Implementability of M Despite Asynchrony and Failures
- Conclusion
- References
- Price Stabilization in Networks - What Is an Appropriate Model ?
- Introduction
- Model
- Protocol Design
- Best Bidding Price
- Simulation
- Conclusion
- References
- Dynamic Regular Registers in Systems with Churn
- Introduction
- Related Work
- The Dynamic Regular Register System Model
- The Algorithms
- The Analysis
- Conclusions
- References
- Space-Efficient Fault-Containment in Dynamic Networks
- Introduction
- Related Work
- Model of Computation
- The Transformation
- Upper Layer
- Middle Layer
- Detecting New Edges Near Minor Components
- Analysis
- Final Remarks
- References
- The OCRC Fuel Cell Lab Safety System: A Self-Stabilizing Safety-Critical System
- Introduction
- The OCRC Fuel Cell Lab
- Safety System Design
- Safety System Major Components
- Safety System Stabilization
- Safety System Implementation and Evaluation
- Implementation
- Evaluation
- References
- Relations Linking Failure Detectors Associated with k-Set Agreement in Message-Passing Systems
- Introduction
- Base Computation Model and k-Set Agreement
- Computation Model
- The k-Set Agreement Problem
- The Failure Detectors k, k and Lk
- The Eventual Leadership Failure Detector k
- The Quorum Failure Detector k
- The Loneliness Failure Detector Lk
- On the Implementability of Lk in a Synchronous System
- Relating Lk and k
- The Property Xk
- Building Lk in AMP[Sk,Xk]
- Building Sk,Xk in AMP[Lk]
- Relating Lk and k
- The Failure Detector Lk
- Building Lk in AMP[k]
- Building k in AMP[Lk]
- Conclusion
- References
- Corona: A Stabilizing Deterministic Message-Passing Skip List
- Introduction
- Model, Notation and Definitions
- Necessary Conditions
- Linearization
- Skip List Stabilization
- Skip Graph
- References
- Using Zero Knowledge to Share a Little Knowledge: Bootstrapping Trust in Device Networks
- Introduction
- System Model and the Trust Bootstrap Problem
- Zero Knowledge Approach for Bootstrapping Trust
- Trust Levels: The Architecture
- Setup and Secrets Generation
- Trust Protocols
- Implementation and Analysis
- Protocols Realizations
- Performance Evaluation
- Features and Merits
- Related Work
- Conclusions and Future Work
- References
- Conflict-Free Replicated Data Types
- Introduction
- System Model
- State-Based Object
- Strong Eventual Consistency
- State-Based Convergent Replicated Data Type (CvRDT)
- Op-Based Commutative Replicated Data Type (CmRDT)
- Some Results
- Fault-Tolerance and the CAP Theorem
- CvRDTs and CmRDTs are Equivalent
- SEC is Incomparable to Sequential Consistency
- Example CRDTs
- Integer Vectors and Counters
- U-Set, Map and Log
- Directed Graph CRDT
- Thought Experiment
- Design Alternatives for Arc Removal
- Graph Specification
- Comparison with Previous Work
- Conclusion
- References
- Analysis of DSR Protocol in Event-B
- Introduction
- The Modeling Framework
- Modeling Actions over States
- Model Refinement
- Informal Description of DSR Protocol
- Requirements and Assumptions
- Formal Development
- The Context and Initial Model
- First Refinement : Store and Forward Architecture
- Second Refinement : Routing Update
- Third Refinement : Route Discovery Protocol
- Fourth Refinement : Continue Route Discovery Protocol
- Fifth Refinement : Sequence Number
- Proof Statistics
- Discussion and Conclusion
- References
- Self-Stabilizing De Bruijn Networks
- Introduction
- Related Work
- The Linearized De Bruijn Network
- Routing Algorithm
- Self-Stabilization
- Linear Probing
- Convergence of Linearization with Linear Probing
- Join and Leave
- Conclusion
- References
- Brief Announcement: A Conjecture on Traceability, and a New Class of Traceable Networks
- Introduction
- The Unique Path Length Conjecture
- References
- Brief Announcement: A Stabilizing Algorithm for Finding Two Edge-Disjoint Paths in Arbitrary Graphs
- References
- Brief Announcement: Towards Interoperability Standards and Services for Autonomic Systems
- Introduction
- Interoperability Service Interfaces
- A Management Description Language
- Conflict Detection
- Brief Announcement: Distributed Self-organizing Event Space Partitioning for Content-Based Publish/Subscribe Systems
- References
- Brief Announcement: A Note on Replication of Documents
- Main Result
- Discussion
- References
- Brief Announcement: A Stable and Robust Membership Protocol
- Overview of the Membership Protocol
- References
- Brief Announcement: Sorting on Skip Chains
- Introduction
- Formal Statement of the Problem
- Overview of the Solution
- References
- Brief Announcement: A Concurrent Partial Snapshot Algorithm for Large-Scale and Dynamic Distributed Systems
- References
- Brief Announcement: Fault-Tolerant Object Location in Large Compute Clusters
- References
- Brief Announcement: Faster Gossiping in Bidirectional Radio Networks with Large Labels
- Introduction
- Deterministic Gossiping in Bi-directional Networks with Large Labels
- Gossiping in Bidirectional Networks with Large Labels
- References
- Author Index
