Visible to the public Biblio

Filters: Keyword is Distributed Systems  [Clear All Filters]
2019-12-09
Sel, Daniel, Zhang, Kaiwen, Jacobsen, Hans-Arno.  2018.  Towards Solving the Data Availability Problem for Sharded Ethereum. Proceedings of the 2Nd Workshop on Scalable and Resilient Infrastructures for Distributed Ledgers. :25–30.
The success and growing popularity of blockchain technology has lead to a significant increase in load on popular permissionless blockchains such as Ethereum. With the current design, these blockchain systems do not scale with additional nodes since every node executes every transaction. Further efforts are therefore necessary to develop scalable permissionless blockchain systems. In this paper, we provide an aggregated overview of the current research on the Ethereum blockchain towards solving the scalability challenge. We focus on the concept of sharding, which aims to break the restriction of every participant being required to execute every transaction and store the entire state. This concept however introduces new complexities in the form of stateless clients, which leads to a new challenge: how to guarantee that critical data is published and stays available for as long as it is relevant. We present an approach towards solving the data availability problem (DAP) that leverages synergy effects by reusing the validators from Casper. We then propose two distinct approaches for reliable collation proposal, state transition, and state verification in shard chains. One approach is based on verification by committees of Casper validators that execute transactions in proposed blocks using witness data provided by executors. The other approach relies on a proof of execution provided by the executor proposing the block and a challenge game, where other executors verify the proof. Both concepts rely on executors for long-term storage of shard chain state.
2019-11-26
Tenorio-Fornés, Antonio, Hassan, Samer, Pavón, Juan.  2018.  Open Peer-to-Peer Systems over Blockchain and IPFS: An Agent Oriented Framework. Proceedings of the 1st Workshop on Cryptocurrencies and Blockchains for Distributed Systems. :19-24.

In recent years, the increasing concerns around the centralized cloud web services (e.g. privacy, governance, surveillance, security) have triggered the emergence of new distributed technologies, such as IPFS or the Blockchain. These innovations have tackled technical challenges that were unresolved until their appearance. Existing models of peer-to-peer systems need a revision to cover the spectrum of potential systems that can be now implemented as peer-to-peer systems. This work presents a framework to build these systems. It uses an agent-oriented approach in an open environment where agents have only partial information of the system data. The proposal covers data access, data discovery and data trust in peer-to-peer systems where different actors may interact. Moreover, the framework proposes a distributed architecture for these open systems, and provides guidelines to decide in which cases Blockchain technology may be required, or when other technologies may be sufficient.

2019-11-19
Dijkhuis, Sander, van Wijk, Remco, Dorhout, Hidde, Bharosa, Nitesh.  2018.  When Willeke Can Get Rid of Paperwork: A Lean Infrastructure for Qualified Information Exchange Based on Trusted Identities. Proceedings of the 19th Annual International Conference on Digital Government Research: Governance in the Data Age. :89:1-89:10.

As a frequent participant in eSociety, Willeke is often preoccupied with paperwork because there is no easy to use, affordable way to act as a qualified person in the digital world. Confidential interactions take place over insecure channels like e-mail and post. This situation poses risks and costs for service providers, civilians and governments, while goals regarding confidentiality and privacy are not always met. The objective of this paper is to demonstrate an alternative architecture in which identifying persons, exchanging information, authorizing external parties and signing documents will become more user-friendly and secure. As a starting point, each person has their personal data space, provided by a qualified trust service provider that also issues a high level of assurance electronic ID. Three main building blocks are required: (1) secure exchange between the personal data space of each person, (2) coordination functionalities provided by a token based infrastructure, and (3) governance over this infrastructure. Following the design science research approach, we developed prototypes of the building blocks that we will pilot in practice. Policy makers and practitioners that want to enable Willeke to get rid of her paperwork can find guidance throughout this paper and are welcome to join the pilots in the Netherlands.

2019-11-12
Padon, Oded.  2018.  Deductive Verification of Distributed Protocols in First-Order Logic. 2018 Formal Methods in Computer Aided Design (FMCAD). :1-1.

Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.

2019-10-30
Demoulin, Henri Maxime, Vaidya, Tavish, Pedisich, Isaac, DiMaiolo, Bob, Qian, Jingyu, Shah, Chirag, Zhang, Yuankai, Chen, Ang, Haeberlen, Andreas, Loo, Boon Thau et al..  2018.  DeDoS: Defusing DoS with Dispersion Oriented Software. Proceedings of the 34th Annual Computer Security Applications Conference. :712-722.

This paper presents DeDoS, a novel platform for mitigating asymmetric DoS attacks. These attacks are particularly challenging since even attackers with limited resources can exhaust the resources of well-provisioned servers. DeDoS offers a framework to deploy code in a highly modular fashion. If part of the application stack is experiencing a DoS attack, DeDoS can massively replicate only the affected component, potentially across many machines. This allows scaling of the impacted resource separately from the rest of the application stack, so that resources can be precisely added where needed to combat the attack. Our evaluation results show that DeDoS incurs reasonable overheads in normal operations, and that it significantly outperforms standard replication techniques when defending against a range of asymmetric attacks.

2019-09-26
Pant, S., Kumar, V..  2018.  BitTrusty: A BitCoin Incentivized Peer-to-Peer File Sharing System. 2018 IEEE 3rd International Conference on Computing, Communication and Security (ICCCS). :148-155.

Among the various challenges faced by the P2P file sharing systems like BitTorrent, the most common attack on the basic foundation of such systems is: Free-riding. Generally, free-riders are the users in the file sharing network who avoid contributing any resources but tend to consume the resources unethically from the P2P network whereas white-washers are more specific category of free-riders that voluntarily leave the system in a frequent fashion and appearing again and again with different identities to escape from the penal actions imposed by the network. BitTorrent being a collaborative distributed platform requires techniques for discouraging and punishing such user behavior. In this paper, we propose that ``Instead of punishing, we may focus more on rewarding the honest peers''. This approach could be presented as an alternative to other mechanisms of rewarding the peers like tit-for-tat [10], reciprocity based etc., built for the BitTorrent platform. The prime objective of BitTrusty is: providing incentives to the cooperative peers by rewarding in terms of cryptocoins based on blockchain. We have anticipated three ways of achieving the above defined objective. We are further investigating on how to integrate these two technologies of distributed systems viz. P2P file sharing systems and blockchain, and with this new paradigm, interesting research areas can be further developed, both in the field of P2P cryptocurrency networks and also when these networks are combined with other distributed scenarios.

2019-09-23
Whittaker, Michael, Teodoropol, Cristina, Alvaro, Peter, Hellerstein, Joseph M..  2018.  Debugging Distributed Systems with Why-Across-Time Provenance. Proceedings of the ACM Symposium on Cloud Computing. :333–346.
Systematically reasoning about the fine-grained causes of events in a real-world distributed system is challenging. Causality, from the distributed systems literature, can be used to compute the causal history of an arbitrary event in a distributed system, but the event's causal history is an over-approximation of the true causes. Data provenance, from the database literature, precisely describes why a particular tuple appears in the output of a relational query, but data provenance is limited to the domain of static relational databases. In this paper, we present wat-provenance: a novel form of provenance that provides the benefits of causality and data provenance. Given an arbitrary state machine, wat-provenance describes why the state machine produces a particular output when given a particular input. This enables system developers to reason about the causes of events in real-world distributed systems. We observe that automatically extracting the wat-provenance of a state machine is often infeasible. Fortunately, many distributed systems components have simple interfaces from which a developer can directly specify wat-provenance using a technique we call wat-provenance specifications. Leveraging the theoretical foundations of wat-provenance, we implement a prototype distributed debugging framework called Watermelon.
2019-05-01
Chen, Yudong, Su, Lili, Xu, Jiaming.  2018.  Distributed Statistical Machine Learning in Adversarial Settings: Byzantine Gradient Descent. Abstracts of the 2018 ACM International Conference on Measurement and Modeling of Computer Systems. :96-96.

We consider the distributed statistical learning problem over decentralized systems that are prone to adversarial attacks. This setup arises in many practical applications, including Google's Federated Learning. Formally, we focus on a decentralized system that consists of a parameter server and m working machines; each working machine keeps N/m data samples, where N is the total number of samples. In each iteration, up to q of the m working machines suffer Byzantine faults – a faulty machine in the given iteration behaves arbitrarily badly against the system and has complete knowledge of the system. Additionally, the sets of faulty machines may be different across iterations. Our goal is to design robust algorithms such that the system can learn the underlying true parameter, which is of dimension d, despite the interruption of the Byzantine attacks. In this paper, based on the geometric median of means of the gradients, we propose a simple variant of the classical gradient descent method. We show that our method can tolerate q Byzantine failures up to 2(1+$ε$)q łe m for an arbitrarily small but fixed constant $ε$0. The parameter estimate converges in O(łog N) rounds with an estimation error on the order of max $\surd$dq/N, \textasciitilde$\surd$d/N , which is larger than the minimax-optimal error rate $\surd$d/N in the centralized and failure-free setting by at most a factor of $\surd$q . The total computational complexity of our algorithm is of O((Nd/m) log N) at each working machine and O(md + kd log 3 N) at the central server, and the total communication cost is of O(m d log N). We further provide an application of our general results to the linear regression problem. A key challenge arises in the above problem is that Byzantine failures create arbitrary and unspecified dependency among the iterations and the aggregated gradients. To handle this issue in the analysis, we prove that the aggregated gradient, as a function of model parameter, converges uniformly to the true gradient function.

2019-02-14
Schuette, J., Brost, G. S..  2018.  LUCON: Data Flow Control for Message-Based IoT Systems. 2018 17th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/ 12th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :289-299.
Today's emerging Industrial Internet of Things (IIoT) scenarios are characterized by the exchange of data between services across enterprises. Traditional access and usage control mechanisms are only able to determine if data may be used by a subject, but lack an understanding of how it may be used. The ability to control the way how data is processed is however crucial for enterprises to guarantee (and provide evidence of) compliant processing of critical data, as well as for users who need to control if their private data may be analyzed or linked with additional information - a major concern in IoT applications processing personal information. In this paper, we introduce LUCON, a data-centric security policy framework for distributed systems that considers data flows by controlling how messages may be routed across services and how they are combined and processed. LUCON policies prevent information leaks, bind data usage to obligations, and enforce data flows across services. Policy enforcement is based on a dynamic taint analysis at runtime and an upfront static verification of message routes against policies. We discuss the semantics of these two complementing enforcement models and illustrate how LUCON policies are compiled from a simple policy language into a first-order logic representation. We demonstrate the practical application of LUCON in a real-world IoT middleware and discuss its integration into Apache Camel. Finally, we evaluate the runtime impact of LUCON and discuss performance and scalability aspects.
2018-08-23
Crooks, Natacha, Pu, Youer, Alvisi, Lorenzo, Clement, Allen.  2017.  Seeing is Believing: A Client-Centric Specification of Database Isolation. Proceedings of the ACM Symposium on Principles of Distributed Computing. :73–82.

This paper introduces the first state-based formalization of isolation guarantees. Our approach is premised on a simple observation: applications view storage systems as black-boxes that transition through a series of states, a subset of which are observed by applications. Defining isolation guarantees in terms of these states frees definitions from implementation-specific assumptions. It makes immediately clear what anomalies, if any, applications can expect to observe, thus bridging the gap that exists today between how isolation guarantees are defined and how they are perceived. The clarity that results from definitions based on client-observable states brings forth several benefits. First, it allows us to easily compare the guarantees of distinct, but semantically close, isolation guarantees. We find that several well-known guarantees, previously thought to be distinct, are in fact equivalent, and that many previously incomparable flavors of snapshot isolation can be organized in a clean hierarchy. Second, freeing definitions from implementation-specific artefacts can suggest more efficient implementations of the same isolation guarantee. We show how a client-centric implementation of parallel snapshot isolation can be more resilient to slowdown cascades, a common phenomenon in large-scale datacenters.

2017-12-20
Schulz, A., Kotson, M., Meiners, C., Meunier, T., O’Gwynn, D., Trepagnier, P., Weller-Fahy, D..  2017.  Active Dependency Mapping: A Data-Driven Approach to Mapping Dependencies in Distributed Systems. 2017 IEEE International Conference on Information Reuse and Integration (IRI). :84–91.

We introduce Active Dependency Mapping (ADM), a method for establishing dependency relations among a set of interdependent services. The approach is to artificially degrade network performance to infer which assets on the network support a particular process. Artificial degradation of the network environment could be transparent to users; run continuously it could identify dependencies that are rare or occur only at certain timescales. A useful byproduct of this dependency analysis is a quantitative assessment of the resilience and robustness of the system. This technique is intriguing for hardening both enterprise networks and cyber physical systems. We present a proof-of-concept experiment executed on a real-world set of interrelated software services. We assess the efficacy of the approach, discuss current limitations, and suggest options for future development of ADM.

2017-12-12
Rezaeibagha, F., Mu, Y..  2017.  Access Control Policy Combination from Similarity Analysis for Secure Privacy-Preserved EHR Systems. 2017 IEEE Trustcom/BigDataSE/ICESS. :386–393.

In distributed systems, there is often a need to combine the heterogeneous access control policies to offer more comprehensive services to users in the local or national level. A large scale healthcare system is usually distributed in a computer network and might require sophisticated access control policies to protect the system. Therefore, the need for integrating the electronic healthcare systems might be important to provide a comprehensive care for patients while preserving patients' privacy and data security. However, there are major impediments in healthcare systems concerning not well-defined and flexible access control policy implementations, hindering the progress towards secure integrated systems. In this paper, we introduce an access control policy combination framework for EHR systems that preserves patients' privacy and ensures data security. We achieve our goal through an access control mechanism which handles multiple access control policies through a similarity analysis phase. In that phase, we evaluate different XACML policies to decide whether or not a policy combination is applicable. We have provided a case study to show the applicability of our proposed approach based on XACML. Our study results can be applied to the electronic health record (EHR) access control policy, which fosters interoperability and scalability among healthcare providers while preserving patients' privacy and data security. 

2017-12-04
Hwang, T..  2017.  NSF GENI cloud enabled architecture for distributed scientific computing. 2017 IEEE Aerospace Conference. :1–8.

GENI (Global Environment for Network Innovations) is a National Science Foundation (NSF) funded program which provides a virtual laboratory for networking and distributed systems research and education. It is well suited for exploring networks at a scale, thereby promoting innovations in network science, security, services and applications. GENI allows researchers obtain compute resources from locations around the United States, connect compute resources using 100G Internet2 L2 service, install custom software or even custom operating systems on these compute resources, control how network switches in their experiment handle traffic flows, and run their own L3 and above protocols. GENI architecture incorporates cloud federation. With the federation, cloud resources can be federated and/or community of clouds can be formed. The heart of federation is user identity and an ability to “advertise” cloud resources into community including compute, storage, and networking. GENI administrators can carve out what resources are available to the community and hence a portion of GENI resources are reserved for internal consumption. GENI architecture also provides “stitching” of compute and storage resources researchers request. This provides L2 network domain over Internet2's 100G network. And researchers can run their Software Defined Networking (SDN) controllers on the provisioned L2 network domain for a complete control of networking traffic. This capability is useful for large science data transfer (bypassing security devices for high throughput). Renaissance Computing Institute (RENCI), a research institute in the state of North Carolina, has developed ORCA (Open Resource Control Architecture), a GENI control framework. ORCA is a distributed resource orchestration system to serve science experiments. ORCA provides compute resources as virtual machines and as well as baremetals. ORCA based GENI ra- k was designed to serve both High Throughput Computing (HTC) and High Performance Computing (HPC) type of computes. Although, GENI is primarily used in various universities and research entities today, GENI architecture can be leveraged in the commercial, aerospace and government settings. This paper will go over the architecture of GENI and discuss the GENI architecture for scientific computing experiments.

2017-11-13
Patti, E., Syrri, A. L. A., Jahn, M., Mancarella, P., Acquaviva, A., Macii, E..  2016.  Distributed Software Infrastructure for General Purpose Services in Smart Grid. IEEE Transactions on Smart Grid. 7:1156–1163.

In this paper, the design of an event-driven middleware for general purpose services in smart grid (SG) is presented. The main purpose is to provide a peer-to-peer distributed software infrastructure to allow the access of new multiple and authorized actors to SGs information in order to provide new services. To achieve this, the proposed middleware has been designed to be: 1) event-based; 2) reliable; 3) secure from malicious information and communication technology attacks; and 4) to enable hardware independent interoperability between heterogeneous technologies. To demonstrate practical deployment, a numerical case study applied to the whole U.K. distribution network is presented, and the capabilities of the proposed infrastructure are discussed.

2017-11-03
Dennis, R., Owenson, G., Aziz, B..  2016.  A Temporal Blockchain: A Formal Analysis. 2016 International Conference on Collaboration Technologies and Systems (CTS). :430–437.

This paper presents a possible solution to a fundamental limitation facing all blockchain-based systems; scalability. We propose a temporal rolling blockchain which solves the problem of its current exponential growth, instead replacing it with a constant fixed-size blockchain. We conduct a thorough analysis of related work and present a formal analysis of the new rolling blockchain, comparing the results to a traditional blockchain model to demonstrate that the deletion of data from the blockchain does not impact on the security of the proposed blockchain model before concluding our work and presenting future work to be conducted.

2017-09-26
Gleissenthall, Klaus v., Bjørner, Nikolaj, Rybalchenko, Andrey.  2016.  Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. :599–613.

Parallel and distributed systems rely on intricate protocols to manage shared resources and synchronize, i.e., to manage how many processes are in a particular state. Effective verification of such systems requires universally quantification to reason about parameterized state and cardinalities tracking sets of processes, messages, failures to adequately capture protocol logic. In this paper we present Tool, an automatic invariant synthesis method that integrates cardinality-based reasoning and universal quantification. The resulting increase of expressiveness allows Tool to verify, for the first time, a representative collection of intricate parameterized protocols.

Woos, Doug, Wilcox, James R., Anton, Steve, Tatlock, Zachary, Ernst, Michael D., Anderson, Thomas.  2016.  Planning for Change in a Formal Verification of the Raft Consensus Protocol. Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. :154–165.

We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an end-to-end guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks. The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariant-strengthening patterns into custom induction principles, proves higher-order lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.

2017-05-22
Sheff, Isaac, Magrino, Tom, Liu, Jed, Myers, Andrew C., van Renesse, Robbert.  2016.  Safe Serializable Secure Scheduling: Transactions and the Trade-Off Between Security and Consistency. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :229–241.

Modern applications often operate on data in multiple administrative domains. In this federated setting, participants may not fully trust each other. These distributed applications use transactions as a core mechanism for ensuring reliability and consistency with persistent data. However, the coordination mechanisms needed for transactions can both leak confidential information and allow unauthorized influence. By implementing a simple attack, we show these side channels can be exploited. However, our focus is on preventing such attacks. We explore secure scheduling of atomic, serializable transactions in a federated setting. While we prove that no protocol can guarantee security and liveness in all settings, we establish conditions for sets of transactions that can safely complete under secure scheduling. Based on these conditions, we introduce \textbackslashti\staged commit\, a secure scheduling protocol for federated transactions. This protocol avoids insecure information channels by dividing transactions into distinct stages. We implement a compiler that statically checks code to ensure it meets our conditions, and a system that schedules these transactions using the staged commit protocol. Experiments on this implementation demonstrate that realistic federated transactions can be scheduled securely, atomically, and efficiently.

2017-05-18
Giang, Nam K., Lea, Rodger, Blackstock, Michael, Leung, Victor C. M..  2016.  On Building Smart City IoT Applications: A Coordination-based Perspective. Proceedings of the 2Nd International Workshop on Smart. :7:1–7:6.

In the Internet of Things (IoT), Internet-connected things provide an influx of data and resources that offer unlimited possibility for applications and services. Smart City IoT systems refer to the things that are distributed over wide physical areas covering a whole city. While the new breed of data and resources looks promising, building applications in such large scale IoT systems is a difficult task due to the distributed and dynamic natures of entities involved, such as sensing, actuating devices, people and computing resources. In this paper, we explore the process of developing Smart City IoT applications from a coordination-based perspective. We show that a distributed coordination model that oversees such a large group of distributed components is necessary in building Smart City IoT applications. In particular, we propose Adaptive Distributed Dataflow, a novel Dataflow-based programming model that focuses on coordinating city-scale distributed systems that are highly heterogeneous and dynamic.

2017-05-16
Mendizabal, Odorico M., Dotti, Fernando Luís, Pedone, Fernando.  2016.  Analysis of Checkpointing Overhead in Parallel State Machine Replication. Proceedings of the 31st Annual ACM Symposium on Applied Computing. :534–537.

State machine replication (SMR) is a well-established technique to fault-tolerant systems. In part, this is explained by the simplicity of the approach and its strong consistency guarantees. Recently, several proposals have suggested parallelizing the execution of state machine replicas to achieve high throughput. Concurrent execution of commands has many implications, including the recovery of replicas from failures. Conventional checkpointing techniques, for example, must be revisited in parallelized models. In this paper, we review parallel variations of state machine replication and discuss how checkpointing procedures apply to these models. Moreover, we evaluate the impact caused by checkpointing techniques on recovery through simulations.

2015-05-06
Nitti, M., Girau, R., Atzori, L..  2014.  Trustworthiness Management in the Social Internet of Things. Knowledge and Data Engineering, IEEE Transactions on. 26:1253-1266.

The integration of social networking concepts into the Internet of things has led to the Social Internet of Things (SIoT) paradigm, according to which objects are capable of establishing social relationships in an autonomous way with respect to their owners with the benefits of improving the network scalability in information/service discovery. Within this scenario, we focus on the problem of understanding how the information provided by members of the social IoT has to be processed so as to build a reliable system on the basis of the behavior of the objects. We define two models for trustworthiness management starting from the solutions proposed for P2P and social networks. In the subjective model each node computes the trustworthiness of its friends on the basis of its own experience and on the opinion of the friends in common with the potential service providers. In the objective model, the information about each node is distributed and stored making use of a distributed hash table structure so that any node can make use of the same information. Simulations show how the proposed models can effectively isolate almost any malicious nodes in the network at the expenses of an increase in the network traffic for feedback exchange.