Super-instructions are a crucial optimization method for interpreters, as they combine multiple basic instructions into single specialized operations. The optimization technique reduces dispatch overhead and enables further optimizations in the synthesized operation code for a super-instruction. However, due to combinatorial explosion, identifying super-instructions is a complex selection problem. This paper presents a novel approach for the automated synthesis of super-instructions using a combination of offline dictionary-based compression algorithms and greedy heuristics. Our method addresses the common issue of overlap between super-instructions, which previous approaches often overlook. Additionally, we introduce a meta-compiler for the Ethereum Virtual Machine (EVM) that automatically generates a new interpreter incorporating the super-instructions. The super-instructions generated with our approach result in an 8.45% speedup for the interpreter component of the EVM.
Decompilation of binary code has arisen as a highly-important application in the space of Ethereum VM (EVM) smart contracts. Major new decompilers appear nearly every year and attain popularity, for a multitude of reverse-engineering or tool-building purposes. Technically, the problem is fundamental: it consists of recovering high-level control flow from a highly-optimized continuation-passing-style (CPS) representation. Architecturally, decompilers can be built using either static analysis or symbolic execution techniques. We present Shrnkr, a static-analysis-based decompiler succeeding the state-of-the-art Elipmoc decompiler. Shrnkr manages to achieve drastic improvements relative to the state of the art, in all significant dimensions: scalability, completeness, precision. Chief among the techniques employed is a new variant of static analysis context: shrinking context sensitivity. Shrinking context sensitivity performs deep cuts in the static analysis context, eagerly “forgetting” control-flow history, in order to leave room for further precise reasoning. We compare Shrnkr to state-of-the-art decompilers, both static-analysis- and symbolic-execution-based. In a standard benchmark set, Shrnkr scales to over 99.5% of contracts (compared to ∼95% for Elipmoc), covers (i.e., reaches and manages to decompile) 67% more code than Heimdall-rs, and reduces key imprecision metrics by over 65%, compared again to Elipmoc.
Xudong Zhu, Haoqi He, Zhengbang Yang, Yi Deng · 6 authors
Zero-knowledge proof (ZKP) is a cryptographic primitive that enables a prover to convince a verifier that a statement is true, without revealing any other information beyond the correctness of the statement itself. Due to its powerful capabilities, its most practical type, called zero-knowledge Succinct Non-interactive ARgument of Knowledge (zkSNARK), has been widely deployed in various privacypreserving applications such as cryptocurrencies and verifiable computation. Although state-of-the-art zkSNARKs are highly efficient for the verifier, the computational overhead for the prover is still orders of magnitude too high to warrant use in many applications. This overhead arises from several time-consuming operations, including large-scale matrix-vector multiplication (MUL), number-theoretic transform (NTT), and especially the multi-scalar multiplication (MSM) which constitutes the largest proportion. Therefore, further efficiency improvements are needed.In this paper, we focus on comprehensive optimization of running time and storage space required by the MSM algorithm on GPUs. Specifically, we propose a novel, modular and adaptive parameter configuration technique—elastic MSM to enable us to adjust the scale of MSM according to our own wishes by performing a corresponding amount of preprocessing. This technique enables us to fully unleash the potential of various efficient parallel MSM algorithms. We have implemented and tested elastic MSM over three prevailing parallel Pippenger algorithms on GPUs. Across various preprocessing space limitations (across various MSM scales), our constructions achieve up to about 1.90×, 1.08× and 1.36× (2.58×, 1.39× and 1.91×) speedup versus three state-of-the-art parallel Pippenger algorithms on GPUs, respectively.From another perspective, elastic MSM could also be regarded as a preprocessing technique over the well-known Pippenger algorithm, which is modular and could be used to accelerate almost all the most advanced parallel Pippenger algorithms on GPUs. Meanwhile, elastic MSM provides an adaptive trade-off between the running time and the extra storage space needed by parallel Pippenger algorithms on GPUs. This is the first preprocessing technique to retain the improved MSM computation brought by preprocessing under varying storage space limitations. Specifically, across various preprocessing space limitations (across various MSM scales), our constructions achieve up to about 192× and 223× (159× and 174×) speedup versus two state-ofthe- art preprocessing parallel Pippenger algorithms on GPUs, respectively.
Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun · 5 authors
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.
Vladlen D. Afonin, Sergey Zapechnikov, Igor A. Prostov
Zero-knowledge proofs are being increasingly applied to a wide range of tasks in modern distributed information systems. Of particular interest are such areas of activity as digital asset management systems, anonymous electronic voting systems, and anonymous credentials. Nevertheless, within the framework of the desire of Russian developers to localize the developed products, there is a question of compliance of the used algorithms with the legislative framework of the Russian Federation, which obliges developers to use local cryptographic standards. As our analysis shows, insufficient attention has been paid in the literature to the applicability of these standards to the scenario of use in zero-knowledge proof systems. In particular, the complexity of proof generation, parameters of arithmetic schemes are not analyzed, there is no comparison of computational complexity and cryptographic properties with foreign alternatives. In this paper we consider in detail the peculiarities of implementation of the arithmetic scheme for the function of GOST 34.11-2018 in the most widespread language for arithmetic circuit programming Circom. The developed program code is open and available for use and modification. The characteristics of the scheme, compilation and generation times are analyzed. The obtained results were compared with other popular hash functions: the cryptographic hash function SHA256 included in the standard language library, and the hash function Poseidon, specialized and optimized for use in zero-knowledge proof systems. The results show that while the use of the Russian hash function is possible, it is not desirable in applications that do not require the use of local cryptographic standards, due to the greater time complexity of witness generation and consequently proof generation. Recommendations on usage scenarios are given and further research directions are suggested.
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.
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.
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.
Verifiable computation (VC) protocols enable clients to outsource computations to untrusted servers in the cloud without compromising the integrity of the computation. Although cryptographic approaches for verifiable computation were mostly of theoretical interest in the past, there has been great progress in the area during the past few years. In particular, efficient constructions for Zero-Knowledge Succinct Non-interactive ARguments of Knowledge (zk-SNARKs) were proposed and adopted in practice. These techniques enable an untrusted server to prove the correctness of computations in zero-knowledge using a succinct proof that can be verified efficiently by the client. This thesis aims at addressing some challenges in such VC protocols, and developing practical protocols for cryptocurrency applications. The challenges we address include the proof computation overhead at the prover's side, and the level of expertise expected from the programmers to write secure and efficient programs for VC. More specifically, current protocols require the programmer to carefully express the computation as an arithmetic circuit, in a way that minimizes the proof computation overhead and prevents malicious behavior by the prover, which is a non-trivial task. To address the above challenges, we present a framework that aims to reduce the proof computation overhead, and offer more programmability to non-specialist developers, while automating the task of circuit minimization through a combination of techniques. The framework includes new circuit-friendly algorithms for frequent operations, which achieve constant to asymptotic savings over algorithms used in previous compilers. In addition, we explore and optimize cryptographic primitives that have efficient arithmetic circuit representations. Furthermore, we explore different settings where VC can be used in practice. We present the design of Hawk, a system for privacy-preserving smart contracts. Hawk enables custom decentralized applications in the smart contract setting to run verifiably on top of a public blockchain system, while not revealing the participants' inputs to the network. To achieve practical performance, Hawk relies on a special party per contract (a manager) that is only trusted for posterior privacy, but not for correctness. Finally, we explore how VC techniques and smart contracts could enable practical crimes in the future, which highlights the importance of working on countermeasures.
Background: Past few months have seen the rise of blockchain and cryptocurrencies. In this context, the Ethereum platform, an open-source blockchain-based platform using Ether cryptocurrency, has been designed to use smart contracts programs. These are self-executing blockchain contracts. Due to their high volume of transactions, analyzing their behavior is very challenging. We address this challenge in our paper. Methods: We develop for this purpose an innovative approach based on the non-negative tensor decomposition Paratuck2 combined with long short-term memory. The objective is to assess if predictive analysis can forecast smart contracts activities over time. Three statistical tests are performed on the predictive analytics, the mean absolute percentage error, the mean directional accuracy and the Jaccard distance. Results: Among dozens of GB of transactions, the Paratuck2 tensor decomposition allows asymmetric modeling of the smart contracts. Furthermore, it highlights time dependent latent groups. The latent activities are modeled by the long short term memory network for predictive analytics. The highly accurate predictions underline the accuracy of the method and show that blockchain activities are not pure randomness. Conclusion: Herein, we are able to detect the most active contracts, and predict their behavior. In the context of future regulations, our approach opens new perspective for monitoring blockchain activities.
Hyperledger Fabric (HLF) is a flexible permissioned blockchain platform designed for business applications beyond the basic digital coin addressed by Bitcoin and other existing networks. A key property of HLF is its extensibility, and in particular the support for multiple ordering services for building the blockchain. Nonetheless, the version 1.0 was launched in early 2017 without an implementation of a Byzantine fault-tolerant (BFT) ordering service. To overcome this limitation, we designed, implemented, and evaluated a BFT ordering service for HLF on top of the BFT-SMaRt state machine replication/consensus library, implementing also optimizations for wide-area deployment. Our results show that HLF with our ordering service can achieve up to ten thousand transactions per second and write a transaction irrevocably in the blockchain in half a second, even with peers spread in different continents.