Delays are inevitable in complex distributed environments. Timeout mechanisms are commonly used to handle unexpected failures in distributed systems. However, incorrect timeout handling or implementation errors in timeout mechanisms can lead to system hang-ups or crashes. Such timeout bugs may be crucial and pose a significant threat to the availability and security of distributed systems.In this work, we introduce Chronos, a general testing framework for automatically detecting timeout bugs in distributed systems with deep-priority transient delays. First, we propose general runtime delayed libraries that dynamically inject fine-grained delays in a Distributed System Under Test (DSUT). To effectively trigger delays and constantly explore timeout bugs in deep paths, Chronos harnesses a deep-priority guided fuzzing that dynamically generates high-quality delay sequences in the runtime. Then, Chronos utilizes transient delays to eliminate the time overhead caused by actual delays and accelerate the test process. We implemented and evaluated Chronos on four widely used distributed systems, including ZooKeeper, MySQL-Cluster, HDFS, and Go-Ethereum. Compared with the state-of-the-art techniques, Random, Brute-Force, and Coverage-Guided fault injection, Chronos covers 26.40%, 21.69%, and 15.14% more timeout mechanism logic, respectively. Furthermore, Chronos has detected 27 timeout bugs in these real-world applications, which have been repaired by the corresponding maintainers.
Ethereum's current Gasper consensus mechanism, which combines the Latest Message Driven Greediest Heaviest Observed SubTree (LMD-GHOST) fork choice rule with the probabilistic Casper the Friendly Finality Gadget (FFG) finality overlay, finalizes transactions in 64 to 95 blocks, an approximate 15-minute delay. This finalization latency impacts user experience and exposes the network to short-term chain reorganization risks, potentially enabling transaction censorship or frontrunning by validators without severe penalties. As the ecosystem pursues a rollup-centric roadmap to scale Ethereum into a secure global settlement layer, faster finality allows cross-layer and inter-rollup communication with greater immediacy, reducing capital inefficiencies. Single slot finality (SSF), wherein transactions are finalized within the same slot they are proposed, promises to advance the Ethereum protocol and enable better user experiences by enabling near-instant economic finality. This thesis systematically studies distributed consensus protocols through propose-vote-merge, PBFT-inspired, and graded agreement families - scrutinizing their capacities to enhance or replace LMD-GHOST. The analysis delves into the intricate tradeoffs between safety, liveness, and finality, shedding light on the challenges and opportunities in designing an optimal consensus protocol for Ethereum. It also explores different design decisions and mechanisms by which single slot or fast finality can be enabled, including cumulative finality, subsampling, and application-layer fast finality. Furthermore, this work introduces SSF-enabled and streamlined fast finality constructions based on a single-vote total order broadcast protocol. The insights and recommendations in this thesis provide a solid foundation for the Ethereum community to make informed decisions regarding the future direction of the protocol's consensus.
Yutian Chen, Cong Peng, Yu Dai, Min Luo · 5 authors
Multi-scalar multiplication (MSM) is an important building block in most of elliptic-curve-based zero-knowledge proof systems, such as Groth16 and PLONK. Recently, Lu et al. proposed cuZK, a new parallel MSM algorithm on GPUs. In this paper, we revisit this scheme and present a new GPU-based implementation to further improve the performance of MSM algorithm. First, we propose a novel method for mapping scalars into Pippenger’s bucket indices, largely reducing the number of buckets compared to the original Pippenger algorithm. Second, in the case that memory is sufficient, we develop a new efficient algorithm based on homogeneous coordinates in the bucket accumulation phase. Moreover, our accumulation phase is load-balanced, which means the parallel speedup ratio is almost linear growth as the number of device threads increases. Finally, we also propose a parallel layered reduction algorithm for the bucket aggregation phase, whose time complexity remains at the logarithmic level of the number of buckets. The implementation results over the BLS12-381 curve on the V100 graphics card show that our proposed algorithm achieves up to 1.998x, 1.821x and 1.818x speedup compared to cuZK at scales of 221, 222, and 223, respectively.
Zero-knowledge Proof (ZKP) is widely used in applications like online auctions and electronic voting to ensure privacy. Among ZKP algorithms, Zero-Knowledge Succinct NonInteractive Argument of Knowledge (zk-SNARK) stands out for its efficiency in generating concise proofs and reducing verification costs. However, the generation of zk-SNARK proofs poses challenges due to computation overhead and time requirements, hindering practical applications. Multi-Scalar Multiplication (MSM) is a computationally intensive step in zk-SNARK proof generation and has become a focus for industry acceleration efforts. In this paper, we introduce Barrel State Tracking MSM (BSTMSM), a high-performance FPGA-based MSM hardware accelerator. Unlike traditional approaches, BSTMSM focuses on tracking the state of each barrel rather than the pipeline of point addition (PADD) circuits. This approach eliminates the impact of barrel collisions and improves the utilization rate of PADD circuits by enabling the utilization of the associative law of addition. Furthermore, we have successfully implemented up to double PADD circuits in BSTMSM, leading to remarkable performance enhancements compared to other existing works. For an input size of $2^{20}$, BSTMSM outperforms the ASIC-based work PipeZK by $ 1.53\times$. For an input size of $2^{26}$, BSTMSM achieves performance improvements of $ 2.22\times$ compared to the FPGA-based work HARDCAML and $ 1.24\times$ compared to the GPU-based work GZKP.
The communities of blockchains and distributed ledgers have been stirred up by the introduction of zero-knowledge proofs (ZKPs). Originally designed to solve privacy issues, ZKPs have now evolved into an effective remedy for scalability concerns and are applied in Zcash (internet money like Bitcoin). To enable ZKPs, Rank-1 Constraint Systems (R1CS) offer a verifier for bi-linear equations. To accurately and efficiently represent R1CS, several language tools like Circom, Noir, and Snarky have been proposed to automate the compilation of advanced programs into R1CS. However, due to the flexible nature of R1CS representation, there can be significant differences in the compiled R1CS forms generated from circuit language programs with the same underlying semantics. To address this issue, this paper uses a data-flow-based R1CS paradigm algorithm, which produces a standardized format for different R1CS instances with identical semantics. By using the normalized R1CS format circuits, the complexity of circuits' verification can be reduced. In addition, this paper presents an R1CS normalization algorithm benchmark, and our experimental evaluation demonstrates the effectiveness and correctness of our methods.
Haochen Sun, Tonghe Bai, J. Li, Change Institutions to: University of Waterloo
The recent advancements in deep learning have brought about significant changes in various aspects of people’s lives. Meanwhile, these rapid developments have raised concerns about the legitimacy of the training process of deep neural networks. To protect the intellectual properties of AI developers, directly examining the training process by accessing the model parameters and training data is often prohibited for verifiers. In response to this challenge, we present zero-knowledge deep learning (zkDL), an efficient zero-knowledge proof for deep learning training. To address the long-standing challenge of verifiable computations of non-linearities in deep learning training, we introduce zkReLU, a specialized proof for the ReLU activation and its backpropagation. zkReLU turns the disadvantage of non-arithmetic relations into an advantage, leading to the creation of FAC4DNN, our specialized arithmetic circuit design for modelling neural networks. This design aggregates the proofs over different layers and training steps, without being constrained by their sequential order in the training process. With our new CUDA implementation that achieves full compatibility with the tensor structures and the aggregated proof design, zkDL enables the generation of complete and sound proofs in less than a second per batch update for an 8-layer neural network with 10M parameters and a batch size of 64, while provably ensuring the privacy of data and model parameters. To our best knowledge, we are not aware of any existing work on zero-knowledge proof of deep learning training that is scalable to million-size networks.
Since its inception as one of the Bitcoin's underpinning technologies, the concept of Blockchain has traversed a long way from being merely a secure distributed ledger meant only for storing cryptocurrencies-based financial transactions to implementing innovative and revolutionary distributed systems for multifarious purposes.One of the contemporary and out-of-the-box Blockchain-based projects, namely Hyperledger, promises to make preeminent use of this technology by promoting cross-industry collaboration in developing Blockchain-based solutions, thus, opening a new chapter in distributed computing.However, attributing to its underlying design, leveraging Hyperledger-Fabric (HF) features still lacks an analysis from the perspective of security risks and efficiency concerns pertaining to real-time distributed computing-based systems and applications.In this regard, we investigate the HF architecture, along with various research endeavours undergone by researchers in recent years to combat its security and performance-related challenges.In light of the identified limitations and bottlenecks, we present our conceptual proposal and feasible insights for improving the efficacy of HF-based systems while not compromising their security.
Activation functions are critical components of neural networks, helping the model learn highly-intricate dependencies, trends, and patterns. Non-linear activation functions allow the model to behave as a functional approximator, learning complex decision boundaries and multi-dimensional patterns in the data. Activation functions can be combined with one another to learn better representations with the objective of improving gradient flow, performance metrics reducing training time and computational cost. Recent work on oscillatory activation functions\cite{noel2021growing}\cite{noel2021biologically} showcased their ability to perform competitively on image classification tasks using a compact architecture. Our work proposes the utilization of these oscillatory activation functions for predicting the volume-weighted average of Bitcoin on the G-Research Cryptocurrency Dataset. We utilize a popular LSTM architecture for this task achieving competitive results when compared to popular activation functions formally used.
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio
Abstract Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present $$\textsf {GASOL}^{v2}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GASOL</mml:mi> <mml:mrow> <mml:mi>v</mml:mi> <mml:mn>2</mml:mn> </mml:mrow> </mml:msup> </mml:math> , a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also wrt. memory and storage. $$\textsf {GASOL}^{v2}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GASOL</mml:mi> <mml:mrow> <mml:mi>v</mml:mi> <mml:mn>2</mml:mn> </mml:mrow> </mml:msup> </mml:math> can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler , and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas wrt. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by .
Shikaku is a pencil puzzle consisting of a rectangular grid, with some cells containing a number. The player has to partition the grid into rectangles such that each rectangle contains exactly one number equal to the area of that rectangle. In this paper, we propose two physical zero-knowledge proof protocols for Shikaku using a deck of playing cards, which allow a prover to physically show that he/she knows a solution of the puzzle without revealing it. Most importantly, in our second protocol we develop a general technique to physically verify a rectangle-shaped area with a certain size in a rectangular grid, which can be used to verify other problems with similar constraints.
Abstract Existing models for non-interactive MPC cannot provide full privacy for inputs, because they inherently leak the residual function (i.e., the output of the function on the honest parties’ input together with all possible values of the adversarial inputs). For example, in any non-interactive sealed-bid auction, the last bidder can figure out what was the highest previous bid. We present a new MPC model which avoids this privacy leak. To achieve this, we utilize a blockchain in a novel way, incorporating smart contracts and arbitrary parties that can be incentivized to perform computation (“bounty hunters,” akin to miners). Security is maintained under a monetary assumption about the parties: an honest party can temporarily supply a recoverable collateral of value higher than the computational cost an adversary can expend. We thus construct non-interactive MPC protocols with strong security guarantees (full security, no residual leakage) in the short term. Over time, as the adversary can invest more and more computational resources, the security guarantee decays. Thus, our model, which we call Gage MPC, is suitable for secure computation with limited-time secrecy, such as auctions. A key ingredient in our protocols is a primitive we call “Gage Time Capsules” (GaTC): a time capsule that allows a party to commit to a value that others are able to reveal but only at a designated computational cost. A GaTC allows a party to commit to a value together with a monetary collateral. If the original party properly opens the GaTC, it can recover the collateral. Otherwise, the collateral is used to incentivize bounty hunters to open the GaTC. This primitive is used to ensure completion of Gage MPC protocols on the desired inputs. As a requisite tool (of independent interest), we present a generalization of garbled circuit that are more robust: they can tolerate exposure of extra input labels. This is in contrast to Yao’s garbled circuits, whose secrecy breaks down if even a single extra label is exposed. Finally, we present a proof-of-concept implementation of a special case of our construction, yielding an auction functionality over an Ethereum-like blockchain.
Vladimir Kukharenko, Kirill Ziborov, Rafael Faritovich Sadykov, Ruslan Rezin
The extent of formal verification methods applied in industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain , is rapidly changing the situation. Since the main area of DLSs’ application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is largely determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is also required to ensure that the software implementation of the DLS nodes complies with this protocol. Finally, the verified software implementation of the protocol must run on a fairly reliable operating system. The financial focus of DLS application has also led to the emergence of the so-called smart contracts , which are an important part of the applied implementations of specific business processes based on DLSs. Therefore, the verifiability of smart contracts is also a critical requirement for industrial DLSs. In this paper, we describe an ongoing industrial project between a large Russian airline and three universities – Innopolis University (IU), Moscow Institute of Physics and Technology (MIPT) and Lomonosov Moscow State University (MSU). The main expected project result is a DLS for more flexible refueling of aircrafts, verified at least at the four technological levels described above. After brief project overview, we focus on our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes. The formal specification of the protocol is performed in the TLA+ language and then verified with a specialized TLC tool to verify models based on TLA+ specifications.
Modern computing systems are highly concurrent. Threads run concurrently in shared-memory multi-core systems, and programs run in different servers communicating by sending messages to each other. Concurrent programming is hard because it requires to cope with many possible, unpredictable behaviors of the processes, and the communication media. The article argues that right from the start in 1960's, the main way of dealing with concurrency has been by reduction to sequential reasoning. It traces this history, and illustrates it through several examples, from early ideas based on mutual exclusion (which was initially introduced to access shared physical resources), passing through consensus and concurrent objects (which are immaterial data), until today distributed ledgers. A discussion is also presented, which addresses the limits that this approach encounters, related to fault-tolerance, performance, and inherently concurrent problems.
In this note, we report several solutions to the STARK-Friendly Hash Challenge: a competition with the goal of finding collisions for several hash functions designed specifically for zero-knowledge proofs (ZKP) and multiparty computations (MPC). We managed to find collisions for 3 instances of 91-bit hash functions. The method used is the classic parallel collision search with distinguished points from van Oorshot and Wiener (1994). As this is a general attack on hash functions, it does not exhibit any particular weakness of the chosen hash functions. The crucial part is to optimize the implementations to make the attack cost realistic, and we describe several arithmetic tricks.
This paper introduces the PoSH Consensus protocol, a novel work-in-progress construction for achieving Sybil-resistant Nakamoto-style probabilistic consensus on the contents of a cryptocurrency ledger in a permissionless decentralized network where parties stake their hardware’s computational power towards participation in leader election. PoSH aims to establish an openly mintable cryptocurrency that eliminates the requirement for block rewards and disincentivizes mining pools.
IOTA cryptocurrency is a distributed solution for secure messaging and micropayments between Internet-of Things devices. The authors introduced open source hardware accelerators for Curl hash function and proof-of-work computations to increase the processing rate of IOTA transactions. The structure and operation principle of both accelerators are described. Proposed accelerators have been implemented on FPGA and integrated into ARM-based System-on-Chip. The characteristics of the system have been evaluated. Compared to official software implementation the proposed hardware accelerators demonstrate x2100 speed up on the creation of IOTA transactions.
Decentralised ledgers are a prime application case for consensus protocols. Changing sets of validators have to agree on a set of transactions in an asynchronous network and in the presence of Byzantine behaviour. Major research efforts focus on creating consensus protocols under such conditions, with proof-of-stake (PoS) representing a promising candidate. PoS aims to reduce the waste of energy inherent to proof-of-work (PoW) consensus protocols. However, a significant challenge is to get PoS protocols "right", i.e. ensure that they are secure w.r.t. safety and liveness. The "Correct-by-Construction" (CBC) Casper approach by the Ethereum project employs pen-and-paper proofs to ensure its security. CBC Casper is a framework to define consensus protocols and aims to prove safety without loss of abstractness. Each member of the CBC Casper family of protocols is defined by five parameters. CBC Casper models the protocol by a state of each validator and messages sent by validators. Each validator can transition its state using messages by other validators that include their current consensus value and a justification (i.e. their previous messages). We extend CBC Casper in three ways. First, we summarise the research of CBC Casper and extend the definitions of safety and liveness properties. To this end, we discuss an instance of CBC Casper called Casper The Friendly GHOST (TFG), a consensus protocol using a variant of the GHOST fork-choice rule. Second, we refine the properties of messages and states in CBC Casper and give a definition of blockchain safety for Casper TFG. Third, we formally verify the CBC Casper framework together with our refined message and state properties as well as our blockchain safety definition in the Isabelle/HOL proof assistant.
Reasoning about commutativity between data-structure operations is an important problem with applications including parallelizing compilers, optimistic parallelization and, more recently, Ethereum smart contracts. There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective. We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition. We have implemented our technique in a prototype open-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois through two case studies: (i) We synthesize commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. (ii) We consider an Ethereum smart contract called BlockKing, and show that Servois can detect serious concurrency-related vulnerabilities and guide developers to construct robust and efficient implementations.
A. Nunez Mencias, Donna N. Dillenberger, P. Novotny, Fanni Tóth · 11 authors
Blockchain is a technology that has been available for several years and has already had several generations. Multiple implementations exist. In this paper, we describe how one of them, the Hyperledger Fabric, is used today to demonstrate the wide usage of the technology for multiple markets beyond finance and cryptocurrency. The use cases highlight the relevance of security—due to the type of data and the distributed foundation of blockchain—and of system performance to enable the use cases in production. Security and performance are the base for the architecture of blockchain on the IBM LinuxONE systems. The Secure Service Container prevents tampering, and the cryptocard usage hardens the solution—and the performance optimization in the compiler, cryptoinstructions, and large caches provides the performance. These optimizations have been further extended with the IBM z14 beyond previous IBM Z generations. In this paper, we describe how a cluster topology is used to implement a high-availability service that scales dynamically from small networks to large ones using the hot plug capabilities of the IBM LinuxONE systems.