- Speculative Multipliers on DeFi: Quantifying On-Chain Leverage Risks
Authors: Zhipeng Wang, Kaihua Qin, Duc Vu Minh, and Arthur Gervais
Blockchains and DeFi have consistently shown to attract financial speculators. One avenue to increase the potential upside (and risks) of financial speculation is leverage trading, in which a trader borrows assets to participate in the financial market. While well-known overcollateralized loans, such as MakerDAO, only enable leverage multipliers of 1.67×, new under-collateralized lending platforms, such as Alpha Homora (AH), unlock leverage multipliers of up to 8× and attracted over 1.2B USD of locked value at the time of writing.
In this paper, we are the first to formalize a model for under-collateralized DeFi lending platforms. We analytically exposit and empirically evaluate the three main risks of a leverage-engaging borrower: (i) impermanent loss (IL) inherent to Automated Market Makers (AMMs), (ii) arbitrage loss in AMMs, and (iii) collateral liquidation. Based on our analytical and empirical results of AH over a timeframe of 9 months, we find that a borrower may mitigate the IL through a high leverage multiplier (e.g., more than 4×) and a margin trading before supplying borrowed assets into AMMs. We interestingly find that the arbitrage and liquidation losses are proportional to the leverage multiplier. In addition, we find that 72.35% of the leverage taking borrowers suffer from a negative APY, when ignoring the governance token incentivization in AH. Finally, when assuming a maximum ±10% move among two stablecoins, we pave the way for more extreme on-chain leverage multipliers of up to 91.9× by providing appropriate system settings.
Link: https://fc22.ifca.ai/preproceedings/71.pdf
- A specification for a ZK-EVM
Authors: Olivier Bégassat, Alexandre Belling, Théodore Chapuis-Chkaiban, and Nicolas Liochon
We describe a zk-EVM arithmetization supporting the three following design goals: (1) support for all EVM opcodes including internal smart contract calls, error management and gas management (2) ability to execute bytecode as is (3) minimal prover time. We strive to provide an arithmetization that respects the EVM specification as defined in the Ethereum yellow paper [1]. We provide an original and comprehensive approach of the zk-EVM problem which is technically realizable using existing zero-knowledge proving schemes.
Link: Redirect Notice
- SolType: Refinement Types for Arithmetic Overflow in Solidity
Authors: Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng
As smart contracts gain adoption in financial transactions, it becomes increasingly important to ensure that they are free of bugs and security vulnerabilities. Of particular relevance in this context are arithmetic overflow bugs, as integers are often used to represent financial assets like account balances. Motivated by this observation, this paper presents SolType, a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in smart contracts. SolType allows developers to add refinement type annotations and uses them to prove that arithmetic operations do not lead to over- and under-flows. SolType incorporates a rich vocabulary of refinement terms that allow expressing relationships between integer values and aggregate properties of complex data structures. Furthermore, our implementation, called Solid, incorporates a type inference engine and can automatically infer useful type annotations, including non-trivial contract invariants.
To evaluate the usefulness of our type system, we use Solid to prove arithmetic safety of a total of 120 smart contracts. When used in its fully automated mode (i.e., using Solid’s type inference capabilities), Solid is able to eliminate 86.3% of redundant runtime checks used to guard against overflows. We also compare Solid against a state-of-the-art arithmetic safety verifier called VeriSmart and show that Solid has a significantly lower false positive rate, while being significantly faster in terms of verification time.
Link: https://www.cs.utexas.edu/~isil/soltype.pdf
- EtherProv: provenance-aware detection, analysis, and mitigation of Ethereum smart contract security issues
Authors: Shlomi Linoy, Suprio Ray, and Natalia Stakhanova
The rapid adoption of blockchain technologies and particularly smart contracts has been overshadowed by numerous security concerns. Over the past few years, a number of reports exposed smart contracts vulnerabilities and exploits, which mainly stem from the immaturity of the field, and consequently a lack of knowledge and tools for automated analysis and verification of smart contracts. The restricting properties of the blockchain environment, such as the immutability of deployed contracts, encumber the analysis and mitigation of vulnerabilities and bugs in deployed contracts. To address these challenges, we propose EtherProv, a novel provenance tracking system that leverages static and dynamic analysis synergy to enable detection and mitigation of known security issues in Ethereum smart contracts. EtherProv leverages Solidity source code static and dynamic analysis data through contract bytecode instrumentation. The collected data is transformed into a unified, high-level representation, which can be queried using concise and descriptive Datalog queries. Within the provenance framework, EtherProv is able to analyze contracts’ execution flow over time, to detect vulnerabilities within a single contract execution flow and across multiple interacting contracts, and to mitigate new security threats in already deployed contracts. Our evaluation shows that EtherProv can efficiently and precisely identify vulnerable contracts with an average contract instrumentation gas overhead of 18.9%.
- Quick Order Fairness
Authors: Christian Cachin, Jovana Micic, and Nathalie Steinhauer
Leader-based protocols for consensus, i.e. atomic broadcast, allow some processes to unilaterally affect the final order of transactions. This has become a problem for blockchain networks and decentralized finance because it facilitates front-running and other attacks. To address this, order fairness for payload messages has been introduced recently as a new safety property for atomic broadcast complementing traditional agreement and liveness. We relate order fairness to the standard validity notions for consensus protocols and highlight some limitations with the existing formalization. Based on this, we introduce a new differential order-fairness property that fixes these issues. We also present the quick order-fair atomic broadcast protocol that guarantees payload message delivery in a differentially fair order and is much more efficient than existing order-fair consensus protocols. It works for asynchronous and for eventually synchronous networks with optimal resilience, tolerating corruptions of up to one third of the processes. Previous solutions required there to be less than one fourth of faults. Furthermore, our protocol incurs only quadratic cost, in terms of amortized message complexity per delivered payload.
Link: https://fc22.ifca.ai/preproceedings/136.pdf
- An empirical study of two Bitcoin artifacts through deep learning
Authors: Richard Tindell, Alex Mitchell, Nathan Sprague, and Xunhua Wang
Human artifacts like technical papers and computer programs often carry the individual styles of their creators. If retrieved properly, such style information from the artifacts can be used to categorize the artifacts, compare the relative “similarities” among artifacts, and may even be used for tracing the authorship of a new artifact. Bitcoin is a peer-to-peer cryptocurrency and its author(s) goes/go by the pseudonym of Satoshi Nakamoto. In this article, we use deep learning to study the styles of two Bitcoin artifacts: the first version of Bitcoin’s source code, v0.1.0, which was released in early 2009, and the original Bitcoin white paper, which is dated Oct. 2008. Both studies use the deep learning technique, which first utilizes extensive computing power to generate a neural network model from labelled training data and then uses the model to predict the authorship of unknown data. For the Bitcoin source code artifact, the data set is a set of cryptography software that were built around 2008/2009 and it has 16 known labels. Our model achieves 89.1% validation accuracy and our prediction results show that the Bitcoin source code is likely produced by multiple authors and Hal Finney is not one of them. For the Bitcoin white paper, we compiled a second data set of financial cryptography papers that are in the same knowledge domain. This data set has 436 known labels. Our model achieves 55.1% validation accuracy and it has identified four technical papers that are “similar” to the Bitcoin white paper.