Formalising Decentralised Exchanges in Coq
Authors: Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters
The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. In order to address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions.
We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter’s implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain.
Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.
Collaborative Learning for Cyberattack Detection in Blockchain Networks
Authors: Tran Viet Khoa, Do Hai Son, Dinh Thai Hoang, Nguyen Linh Trung, Tran Thi Thuy Quynh, Diep N. Nguyen, Nguyen Viet Ha, and Eryk Dutkiewicz
This article aims to study intrusion attacks and then develop a novel cyberattack detection framework for blockchain networks. Specifically, we first design and implement a blockchain network in our laboratory. This blockchain network will serve two purposes, i.e., generate the real traffic data (including both normal data and attack data) for our learning models and implement real-time experiments to evaluate the performance of our proposed intrusion detection framework. To the best of our knowledge, this is the first dataset that is synthesized in a laboratory for cyberattacks in a blockchain network. We then propose a novel collaborative learning model that allows efficient deployment in the blockchain network to detect attacks. The main idea of the proposed learning model is to enable blockchain nodes to actively collect data, share the knowledge learned from its data, and then exchange the knowledge with other blockchain nodes in the network. In this way, we can not only leverage the knowledge from all the nodes in the network but also do not need to gather all raw data for training at a centralized node like conventional centralized learning solutions. Such a framework can also avoid the risk of exposing local data’s privacy as well as the excessive network overhead/congestion. Both intensive simulations and real-time experiments clearly show that our proposed collaborative learning-based intrusion detection framework can achieve an accuracy of up to 97.7% in detecting attacks.
A Decentralized Governance Framework for Open Source Software Organizations
Author: Jozef Siu
Decentralized Autonomous Organizations (DAO) are a nascent phenomenon. The execution and immutable registration of smart contracts on blockchains have presented the opportunity for smart contracts to be used in the governance of decentralized organizations in an autonomous manner. They enable new forms of decentralized decision making processes, incentive designs and more.
As DAOs can be traced back to Open Source Software(OSS) and are similarly founded on decentralization and transparency, this study approaches DAO governance from an OSS perspective. The study contributes an understanding of DAO governance from the perspective of OSS project governance for OSS organizations. This research proposes the DAO for OSS governance framework, that presents the governance dimensions and the respective governance concepts for a DAO for OSS.
Four case studies were conducted with DAOs, ranging from starting DAOs to mature DAOs. The mature DAOs have a complete governance model and utilize complex governance mechanisms. The case studies show that the framework is (I) useful for starting DAOs to understand the governance structures and governance considerations, (II) it serves as an intermediate check for DAOs to measure the maturity of their governance, (III) it serves as a research framework to analyze DAOs and (IV) it can be used as a checklist to track governance growth as a DAO develops.
The presented DAO for OSS governance framework provides a solid foundation for further research of DAO governance and contributes to the understanding of DAO for OSS governance.
SoK: Differential Privacy on Graph-Structured Data
Authors: Tamara T. Mueller, Dmitrii Usynin, Johannes C. Paetzold, Daniel Rueckert, and Georgios Kaissis
In this work, we study the applications of differential privacy (DP) in the context of graph-structured data. We discuss the formulations of DP applicable to the publication of graphs and their associated statistics as well as machine learning on graph-based data, including graph neural networks (GNNs). The formulation of DP in the context of graph-structured data is difficult, as individual data points are interconnected (often non-linearly or sparsely). This connectivity complicates the computation of individual privacy loss in differentially private learning. The problem is exacerbated by an absence of a single, well-established formulation of DP in graph settings. This issue extends to the domain of GNNs, rendering private machine learning on graph-structured data a challenging task. A lack of prior systematisation work motivated us to study graph-based learning from a privacy perspective. In this work, we systematise different formulations of DP on graphs, discuss challenges and promising applications, including the GNN domain. We compare and separate works into graph analysis tasks and graph learning tasks with GNNs. Finally, we conclude our work with a discussion of open questions and potential directions for further research in this area.
Hierarchical Consensus: A Horizontal Scaling Framework for Blockchains
Authors: Alfonso de la Rocha, Lefteris Kokoris-Kogias, Jorge M. Soares, and Marko Vukolic
We present the Filecoin Hierarchical Consensus framework, which aims to overcome the throughput challenges of blockchain consensus by horizontally scaling the network. Unlike traditional sharding designs, based on partitioning the state of the network, our solution centers on the concept of subnets –which are organized hierarchically– and can be spawned on-demand to manage new state. Child subnets are firewalled from parent subnets, have their own specific policies, and run a different consensus algorithm, increasing the network capacity and enabling new applications. Moreover, they benefit from the security of parent subnets by periodically checkpointing state. In this paper, we introduce the overall system architecture, our detailed designs for cross-net transaction handling, and the open questions that we are still exploring.
Bonanza Mine: an Ultra-Low-Voltage Energy-Efficient Bitcoin Mining ASIC
Authors: Vikram B. Suresh, Chandra S. Katta, Srinivasan Rajagopalan, Tao Z. Zhou, Amit Kumar Patel, Raju Rakha, Nikhil Krishna Gopalakrishna, Sanu Mathew, and Ajat Hukkoo
Bitcoin is the leading blockchain-based cryptocurrency used to facilitate peer-to-peer transactions without relying on a centralized clearing house . The conjoined process of transaction validation and currency minting, known as mining, employs the compute-intensive SHA256 double hash as proof-of-work. The one-way property of SHA256 necessitates a brute-force search by sweeping a 32b random input value called nonce. The 2 32 nonce space search results in energy-intensive pool operations distributed on high-throughput mining systems, executing parallel nonce searches with candidate Merkle roots. Energy-efficient custom ASICs are required for cost-effective mining, where energy costs dominate operational expenses, and the number of hash engines integrated on a single die govern platform cost and peak mining throughput . In this paper, we present BonanzaMine, an energy-efficient mining ASIC fabricated in 7nm CMOS (Fig. 21.3.7), featuring: (i) bitcoin-optimized look-ahead message digest datapath resulting in 33% C dyn reduction compared to conventional SHA256 digest datapath; (ii) a half-frequency scheduler datapath, reducing sequential and clock power by 33%; (iii) 3-phase latch-based design with stretchable non-overlapping clocks, eliminating min-delay paths; (iv) robust ultra-low-voltage operation at 355mV using board-level voltage-stacking; and (v) mining throughput of 137GHash/s at an energy efficiency of 55J/THash.
Rethinking selfish mining under pooled mining
Authors: Suhyeon Lee and Seungjoo Kim
Bitcoin’s core security requires honest participants to control at least 51% of the total hash power. However, it has been shown that several techniques can exploit the fair mining in the Bitcoin network. This study focuses on selfish mining, which is based on the idea, ”keeping blocks secret.” Herein, we analyze selfish mining regarding competition between mining pools. We emphasize that mining-related information is shared between mining pools and participants. Based on shared information about selfish mining, we have developed an effective and practical counter strategy.
Transactions fees optimization in the Ethereum blockchain
Authors: Arnaud Laurent, Luce Brotcorne, and Bernard Fortz
In blockchains, transactions fees are fixed by the users. The probability for a transaction to be processed quickly increases with the fee level. In this paper, we study the transactions fees optimization problem in Ethereum blockchain. This problem consists in determining the minimum price a user should pay in order that its transaction be processed with a given probability in a given amount of time. To reach this goal, we define a new solution method based on a Monte Carlo approach to predict the probability that a transaction be mined within a given time limit. Numerical results on real data highlight the quality of the results.