Model-based Systems Engineering (MBSE) has been widely utilized to formalize system artifacts and facilitate their development throughout the entire lifecycle. During complex system development, MBSE models need to be frequently exchanged across stakeholders. Concerns about data security and tampering using traditional data exchange approaches obstruct the construction of a reliable marketplace for digital assets. The emerging Distributed Ledger Technology (DLT), represented by blockchain, provides a novel solution for this purpose owing to its unique advantages such as tamper-resistant and decentralization. In this paper, we integrate MBSE approaches with DLT aiming to create a decentralized marketplace to facilitate the exchange of digital engineering assets (DEAs). We first define DEAs from perspectives of digital engineering objects, development processes and system architectures. Based on this definition, the Graph-Object-Property-Point-Role-Relationship (GOPPRR) approach is used to formalize the DEAs. Then we propose a framework of a decentralized DEAs marketplace and specify the requirements, based on which we select a Directed Acyclic Graph (DAG) structured DLT solution. As a proof-of-concept, a prototype of the proposed DEAs marketplace is developed and a case study is conducted to verify its feasibility. The experiment results demonstrate that the proposed marketplace facilitates free DEAs exchange with a high level of security, efficiency and decentralization.
Open access
2 source records
Systems Engineering Methodologies and Applications
Ethereum Research team has proposed a family of Casper blockchain consensus protocols for Ethereum 2.0. It has been shown in the literature that Casper Friendly Finality Gadget (Casper FFG) for Ethereum 2.0's beacon network cannot achieve liveness property in partially synchronous networks such as the Internet environment. The ``Correct-by-Construction'' family of Casper blockchain consensus protocols (CBC Casper) has been proposed as a finality gadget for the future release of Ethereum 2.0 blockchain. Unfortunately, neither constructive finality rule nor satisfactory liveness property has been obtained for CBC Casper, and it is commonly believed that CBC Casper could not achieve liveness property in asynchronous networks. This paper provides the first probabilistic CBC Casper protocol that achieves liveness property against $t=\lfloor \frac{n-1}{3}\rfloor$ Byzantine participants in complete asynchronous networks. The seminal work by Fisher, Lynch, and Paterson (FLP) shows that there does not exist a deterministic BFT protocol in complete asynchronous networks against a single failure. Existing BFT protocols for complete asynchronous networks are all probabilistic which are based either on individual coin-flipping or on common coin-flipping. This paper proposes the first secure and deterministic leaderless blockchain BFT protocol XP against $t=\lfloor \frac{n-1}{3}\rfloor$ Byzantine participants in complete asynchronous networks. This result does not contradict with FLP's impossibility results since XP leverages the total order properties of candidate blocks in blockchains (similar properties may not hold for general BFT application scenarios).
Ethereum Research team has proposed a family of Casper blockchain consensus protocols for Ethereum 2.0. It has been shown in the literature that Casper Friendly Finality Gadget (Casper FFG) for Ethereum 2.0's beacon network cannot achieve liveness property in partially synchronous networks such as the Internet environment. The "Correct-by-Construction" family of Casper blockchain consensus protocols (CBC Casper) has been proposed as a finality gadget for the future release of Ethereum 2.0 blockchain. Unfortunately, neither constructive finality rule nor satisfactory liveness property has been obtained for CBC Casper, and it is commonly believed that CBC Casper could not achieve liveness property in asynchronous networks. This paper provides the first probabilistic CBC Casper protocol that achieves liveness property against (n-1)/3 Byzantine participants in complete asynchronous networks.
Inspired by Bitcoin, many different kinds of cryptocurrencies based on blockchain technology have turned up on the market. Due to the special structure of the blockchain, it has been deemed impossible to directly trade between traditional currencies and cryptocurrencies or between different types of cryptocurrencies. Generally, trading between different currencies is conducted through a centralized third-party platform. However, it has the problem of a single point of failure, which is vulnerable to attacks and thus affects the security of the transactions. In this paper, we propose a distributed cryptocurrency trading scheme to solve the problem of centralized exchanges, which can achieve secure trading between different types of cryptocurrencies. Our scheme is implemented with smart contracts on an Ethereum blockchain and deployed on an Ethereum test network. In addition to implementing transactions between individual users, our scheme also allows transactions among multiple users. The experimental result proves that the cost of our scheme is acceptable.
Yackolley Amoussou-Guenou, Bruno Biais, Maria Potop-Butucaru, Sara Tucci-Piergiovanni
We analyze from the game theory point of view Consensus-based blockchains when participants exhibit rational or Byzantine behavior. Our work is the first to model the Byzantine-consensus based blockchains as a committee coordination game. Our first contribution is to offer a game-theoretical methodology to analyze equilibrium interactions between Byzantine and rational committee members in Consensus-based blockchains.Byzantine participants seek to inflict maximum damage to the system, while rational participants best-respond to maximize their expected net gains. Our second contribution is to derive conditions under which consensus properties are satisfied or not in equilibrium. When the number of votes required for a decision is lower than the proportion of Byzantine participants, invalid blocks are accepted in equilibrium. When the number of votes needed is large, equilibrium can involve coordination failures, in which no block is ever accepted. However, when the cost of accepting invalid blocks is large, there exists an equilibrium in which blocks are accepted if and only if they are valid.
Smart contracts are the artifact of the blockchain that provide immutable and verifiable specifications of physical transactions. Solidity is a domain-specific programming language with the purpose of defining smart contracts. It aims at reducing the transaction costs occasioned by the execution of contracts on the distributed ledgers such as the Ethereum. However, Solidity contracts need to adhere safety and security requirements that require formal verification and certification. This paper proposes a method to meet such requirements by translating Solidity contracts to Event-B models, supporting certification. To that purpose, we define a restrained Solidity subset and a transfer function which translates Solidity contracts to Event-B models. Then we take advantage of Event-B method capabilities to refine models at different levels of abstraction to verify Solidity contracts' properties. And we can verify the generated proof obligations of the Event-B model with the help of the Rodin platform.
Exhibition of malicious behavior during blockchain consensus, threats against reputation systems, and high TX latency are significant issues for blockchain-based IoT systems. Hence, to mitigate such challenges we propose "Pledge", a unique Proof-of-Honesty based consensus protocol. Initial experimentation shows that Pledge is economical with low computations and communications complexity and low latency in transaction confirmation.
Victor Ermolaev, Indrek Klangberg, Yash Madhwal, Silver Vapper · 6 authors
In modern and interconnected world, information is accumulatively stored digitally, making the process of exchanging, gathering and querying the information much easier. Continuously, it has introduced new challenges about how to ensure its consistency and reliability due to the sheer volume of data. A blockchain-based information system can provide an incorruptible record of history, enabling better auditing and data management practices. The paper describes how to combine an Exonum blockchain and a Neo4j graph database into a system that can provide a verifiable audit trail of data integrity and its modifications for information stored in a graph database.
Blockchain has become a promising technology in distributed systems in recent years, but scalability remains a major problem. The traditional approach to scalability, namely sharding, does not solve the problem easily because the process of interleaving blocks stored in different shards to create a unified master ledger introduces overhead. This paper examines two techniques for interleaving the shards of permissioned blockchains, which we refer to as strong temporal coupling and weak temporal coupling. We implement these techniques in a prototype system with a Bitcoin-like transaction structure, using the EPaxos consensus protocol for transaction ordering. Our experimental results show that strong coupling can achieve lower latency as compared to weak coupling but same level of peak throughput. However, strong coupling requires all shards to grow at the same rate, and cannot tolerate any shard failure. In contrast, the higher latency of weak coupling is because of the consensus strategy it uses to order the blocks. However, if shard failure occurs, weak coupling can still make progress without stalling the whole system.
Maya Leshkowitz, Olivia Benattasse, Oded Wertheim, Ori Rottenstreich
A dominant part in blockchain networks is reaching an agreement on block transactions and their impact on the network state. We follow a common scenario where a node is selected to propose a block and its implied state updates. The proposal is then validated by other nodes that examine the block impact on the state. Typically, all validators execute the complete block and provide an indication based on comparing the results of their execution to the updated state in the proposal. With the increase in the number of participants in blockchain networks, we suggest a time-efficient block validation through splitting it into multiple disjoint tasks. This can be challenging due to possible dependencies between the block transactions. We describe the additional information the leader has to provide to enable that. Moreover, we describe a unique proof for the block partition computed by the leader such that when validated in part by the different committees guarantees the correctness of the execution by the leader. We compare the approach to traditional solutions based on real data of the Ethereum blockchain.
Correct-by-Construction Casper (CBC Casper) is an Ethereum candidate consensus protocol undergoing active design and development. We present a formalization of CBC Casper using the Coq proof assistant that includes a model of the consensus protocol and proofs of safety and non-triviality protocol properties. We leverage Coq's type classes to model CBC Casper at various levels of abstraction. In doing so, we 1) illuminate the assumptions that each protocol property depends on, and 2) reformulate the protocol in general, mathematical terms. We highlight two advantages of our approach: 1) from a proof engineering perspective, it enables a clean separation of concerns between theory and implementation; 2) from a protocol engineering perspective, it provides a rigorous, foundational understanding of the protocol conducive to finding and proving stronger properties. We detail one such new property: strong non-triviality.
This paper introduces a new approach to reduce end-to-end costs in large-scale replicated systems built under a Byzantine fault model. Specifically, our approach transforms a given replicated state machine (RSM) to another RSM where nodes incur lower costs by delegating state machine execution: an untrusted prover produces succinct cryptographic proofs of correct state transitions along with state changes, which nodes in the transformed RSM verify and apply respectively.To realize our approach, we build Piperine, a system that makes the proof machinery profitable in the context of RSMs. Specifically, Piperine reduces the costs of both proving and verifying the correctness of state machine execution while retaining liveness-a distinctive requirement in the context of RSMs. Our experimental evaluation demonstrates that, for a payment service, employing Piperine is more profitable than naive reexecution of transactions as long as there are > 104nodes. When we apply Piperine to ERC-20 transactions in Ethereum (a real-world RSM with up to 105nodes), it reduces per-transaction costs by 5.4× and network costs by 2.7×.
Blockchains are distributed secure ledgers to which transactions are issued continuously and each block of transactions is tightly coupled to its predecessors. Permissioned blockchains place special emphasis on transactions throughput. In this paper we present FireLedger, which leverages the iterative nature of blockchains in order to improve their throughput in optimistic execution scenarios. FireLedger trades latency for throughput in the sense that in FireLedger the last f + 1 blocks of each node's blockchain are considered tentative, i.e., they may be rescinded in case one of the last f + 1 blocks proposers was Byzantine. Yet, when optimistic assumptions are met, a new block is decided in each communication step, which consists of a proposer that sends only its proposal and all other participants are sending a single bit each. In our performance study FireLedger obtained 20% -- 600% better throughput than state of the art protocols like HotStuff and BFT-SMaRt, depending on the configuration.
Sean Bowe, Alessandro Chiesa, Matthew Green, Ian Miers · 6 authors
Ledger-based systems that support rich applications often suffer from two limitations. First, validating a transaction requires re-executing the state transition that it attests to. Second, transactions not only reveal which application had a state transition but also reveal the application's internal state.We design, implement, and evaluate ZEXE, a ledger-based system where users can execute offline computations and subsequently produce transactions, attesting to the correctness of these computations, that satisfy two main properties. First, transactions hide all information about the offline computations. Second, transactions can be validated in constant time by anyone, regardless of the offline computation.The core of ZEXE is a construction for a new cryptographic primitive that we introduce, decentralized private computation (DPC) schemes. In order to achieve an efficient implementation of our construction, we leverage tools in the area of cryptographic proofs, including succinct zero knowledge proofs and recursive proof composition. Overall, transactions in ZEXE are 968 bytes regardless of the offline computation, and generating them takes less than 1min plus a time that grows with the offline computation.We demonstrate how to use ZEXE to realize privacy-preserving analogues of popular applications: private user-defined assets and private decentralized exchanges for these assets.
The world is being transformed by the onset of new high speed 5G Technologies that open the possibility of IoT networks at scale. This demands delivery guarantees and coordinated distributed communications that are resistant to damage and can self-heal under adversity. The speed of change is increasing with increased automation, artificial intelligence, information from multiple sources, integrated systems of systems and emerging quantum technologies. Current distributed consensus checking mechanisms are computationally intensive and fail to scale along with these changes because of the complexity of proof of work calculations or the unnecessary need to bind in domain specific elements such as cryptocurrencies. Furthermore, these mechanisms are brittle in that small changes in messages can cause restarts or failure of integrity checks, or they introduce domain specific elements (e.g. monetary design that has little to do with integrity). We propose distributed ledgers as a pure technology coupled with a strong proof protocol for exchanges, called "Proof of Integrity" without any need for cryptocurrencies or other domain specific elements. Proof of Integrity provides distributed data guarantees and operational continuity through adversity or breakdowns while creating a reliable and trustworthy layer for the application specificity of domain specific elements.
Mehrdad Kiamari, Bhaskar Krishnamachari, Muhammad Naveed, Seokgu Yun
We present a Byzantine Fault Tolerant (BFT) distributed ledger protocol that is aimed at making mobile devices first-class citizens in the consensus process by having them communicate through online brokers. The protocol is provably safe and live. We show that it is capable of a throughput on the order of several thousand transactions per second per shard, and sub-second confirmation latency.
Michael P. Frank, Christopher Cordi, Kasimir Gabert, Carollan Helinski · 8 authors
Simple but mission-critical internet-based applications that require extremely high reliability and availability could potentially benefit from running on robust public programmable blockchain platforms such as Ethereum. Unfortunately, program code running on such blockchains is ordinarily publicly viewable, rendering these platforms unsuitable for applications requiring strict privacy of application code, data, and results. However, might it be possible to encode an application's business logic and data for these platforms in such a way that it becomes impossible for unauthorized parties to infer any meaningful information whatsoever about the semantics of the data, and the operations being performed on that data? In this report, we describe GABLE (Garbled Autonomous Bots Leveraging Ethereum), a system concept developed at Sandia that achieves this security goal in a limited, but still useful range of circumstances. GABLE, uses simple but effective algorithms to permit secure private execution of garbled state machines (and more efficient garbled circuits) on public computing resources. We give an example working implementation for garbled state machines, written using the Python and Solidity programming languages, and outline how our methods can be extended to support a more powerful garbled universal circuit model of computation. The capability embodied by the GABLE, system has significant potential applications, a few of which we discuss in this report.
Mainstream applications typically require a trusted authority where application clients will connect to obtain a service. In the blockchain decentralized environment, this trusted authority or the leader changes frequently and is selected randomly depending on the protocol. Such procedures may take an unacceptable amount of time or resources to establish the leader causing overheads, latency or processing issues if mainstream applications are to adopt the blockchain. Focusing on these issues, we present Right-of-Stake (RoS), a novel approach in a synchronous blockchain network to deterministically elect a leader or block proposer out of a group of participants, each with different stakes. This procedure is completed in a guaranteed equitable manner while removing the need for Proof-of-Work's (PoW) aggressive-resource computations or Proof-of-Stake's (PoS) inter-node negotiations. Besides, through the use of zero-knowledge range proofs, RoS has a distinct advantage of being able to hide the identity of future leaders until the point when the leader surfaces to propose the block. We also simulate RoS and show that it can recover from Denial-of-Service attacks which have been a point of contention in arguments against deterministic leader election protocols. We view RoS as a possible consensus replacement for blockchains that require an improved leader election process when deployed for mainstream applications.
IoT-blockchain applications have advantages of managing massive IoT devices, achieving advanced data security, and data credibility. However, there are still some challenges when deploying IoT applications on blockchain systems due to limited storage, power, and computing capability of IoT devices. Applying current consensus protocols to IoT applications may be vulnerable to Sybil node attacks or suffer from high-computational cost and low scalability. In this paper, we propose G-PBFT (Geographic-PBFT), a new location-based and scalable consensus protocol designed for IoT-blockchain applications. The principle of G-PBFT is based on the fact that most IoT-blockchain applications rely on fixed IoT devices for data collection and processing. Fixed IoT devices have more computational power than other mobile IoT devices, e.g., mobile phones and sensors, and are less likely to become malicious nodes. G-PBFT exploits geographic information of fixed IoT devices to reach consensus, thus avoiding Sybil attacks. In G-PBFT, we select those fixed, loyal, and capable nodes as endorsers, reducing the overhead for validating and recording transactions. As a result, G-PBFT achieves high consensus efficiency and low traffic intensity. Moreover, G-PBFT uses a new era switch mechanism to handle the dynamics of the IoT network. To evaluate our protocol, we conduct extensive experiments to compare the performance of G-PBFT against existing consensus protocol with over 200 participating nodes in a blockchain system. Experimental results demonstrate that G-PBFT significantly reduces consensus time, network overhead, and is scalable for IoT applications.
Zachary Painter, Pradeep Kumar Gayam, Victor Cook, Damian Dechev
Popular blockchains such as Bitcoin or Ethereum provide a transaction isolation level of READ-COMMITTED. This provides difficulties when state changes many times per block interval. Hash-Mark-Set (HMS) alleviates this problem by enabling READ-UNCOMMITTED transactions for state variables. However, the current HMS implementation relies on a sequential algorithm and is susceptible to redundant calculations. As modern processors rely more heavily on parallel algorithms to leverage multiple cores for speedup, sequential algorithms see less benefit from hardware improvements. This paper proposes a lock-free HMS to make use of thread-safe techniques and other optimizations to improve the performance of the HMS algorithm and reduce the latency of read-uncommitted state variable accesses. In our experiments, the proposed algorithm experiences an average 6.4× increase in performance up to 128 go-routines, and a maximum 11.1× increase.
The articles in this special section focus on distributed ledger technologies (DLT). DLT, of which blockchain is a popular example, are increasingly becoming a popular means to maintain transactional integrity and achieve consensus among competing parties in many modern distributed data exchanges. Indeed, a Gartner survey estimates that by 2020, DLT and blockchain will support the global movement and tracking of $2 trillion of goods and services annually. Unlike centralized files and databases, distributed ledgers rely on peering nodes to record, share, and synchronize transactions and data in their individually maintained local ledgers. In the case of blockchain, information is organized into blocks that are securely and transparently chained together. These blocks become immutable global knowledge among all peers using consensus algorithms to achieve data synchronization. The “append-only, globally accepted” transactions supported by blockchain technologies have given rise to both opportunities and challenges compared to traditional data storage systems. One of the challenges faced by current information sharing systems, and a key concept that makes DLT appealing is the support for the creation of large scale systems from nodes and components that do not trust each other. Being able to reach consensus and share a commonly verifiable ledger is a very powerful primitive, which is already being considered for data sharing applications in energy, pharmaceuticals, and many other domains.
The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or CLI for .Net programs): the use of the stack for saving the jump addresses instead of having it explicit in the code of the jumping instructions. Static analyzers need the complete control flow graph (CFG) of the EVM program in order to be able to represent all its execution paths. This report addresses the problem of obtaining a precise and complete stack-sensitive CFG by means of a static analysis, cloning the blocks that might be executed using different states of the execution stack. The soundness of the analysis presented is proved.
Marten Sigwart, Philipp Frauenthaler, Christof Spanring, Michael Sober · 5 authors
Today, several solutions for cross-blockchain asset transfers exist. However, these solutions are either tailored to specific assets or neglect finality guarantees that prevent assets from getting lost in transit. In this paper, we present a cross-blockchain asset transfer protocol that supports arbitrary assets and adheres to finality requirements. The ability to freely transfer assets between blockchains may increase transaction throughput and provide developers with more flexibility by allowing them to design digital assets that leverage the capacities and capabilities of multiple blockchains.
Proof-of-work cryptocurrencies are heavily criticized for the alleged inefficiency of their mining mechanism. However, critics fail to distinguish between the resources that are used to secure the blockchain and those that are wasted. In this paper, we introduce a simple mining model and use this model to analyze the consensus protocol's efficiency, while accounting for the heterogeneity of the miners involved. We categorize the resources allocated by the miners as either useful or wasteful, and then use this to introduce a new measure of efficiency. We then demonstrate how this value depends on a set of potential miners and the variation of their marginal costs. Using this model, we then consider the existence of botnets and show how one could affect the security of the network. This analysis indicates that botnets can significantly change the mining landscape and, under certain circumstances, may lead to a dissipation ratio greater than one.