Smart contracts have been widely and rapidly used to automate financial and business transactions together with blockchains, helping people make agreements while minimizing trusts. With millions of smart contracts deployed on blockchain, various bugs and vulnerabilities in smart contracts have emerged. Following the rapid development of deep learning, many recent studies have used deep learning for vulnerability detection to conduct security checks before deploying smart contracts. These approaches show effective results on detecting whether a smart contract is vulnerable or not whereas their results on locating suspicious statements responsible for the detected vulnerability are still unsatisfactory.
As computer programs run on top of blockchain, smart contracts have proliferated a myriad of decentralized applications while bringing security vulnerabilities, which may cause huge financial losses. Thus, it is crucial and urgent to detect the vulnerabilities of smart contracts. However, existing fuzzers for smart contracts are still inefficient to detect sophisticated vulnerabilities that require specific vulnerable transaction sequences to trigger. To address this challenge, we propose a novel vulnerability-guided fuzzer based on reinforcement learning, namely RLF, for generating vulnerable transaction sequences to detect such sophisticated vulnerabilities in smart contracts. In particular, we firstly model the process of fuzzing smart contracts as a Markov decision process to construct our reinforcement learning framework. We then creatively design an appropriate reward with consideration of both vulnerability and code coverage so that it can effectively guide our fuzzer to generate specific transaction sequences to reveal vulnerabilities, especially for the vulnerabilities related to multiple functions. We conduct extensive experiments to evaluate RLFâs performance. The experimental results demonstrate that our RLF outperforms state-of-the-art vulnerability-detection tools (e.g., detecting 8%-69% more vulnerabilities within 30 minutes).
When do classical zero-knowledge protocols remain secure against quantum attacks? In this work, we develop the techniques, tools, and abstractions necessary to answer this question for foundational protocols:1)We prove that the Goldreich-Micali-Wigderson protocol for graph non-isomorphism and the Feige-Shamir protocol for NP remain zero-knowledge against quantum adversaries. At the heart of our proof is a new quantum rewinding technique that enables extracting information from multiple invocations of a quantum adversary without disturbing its state.2)We prove that the Goldreich-Kahan protocol for NP is post-quantum zero knowledge using a simulator that can be seen as a natural quantum extension of the classical simulator.Our results achieve negligible simulation error, appearing to contradict a recent impossibility result due to Chia-Chung-Liu-Yamakawa (FOCS 2021). This brings us to our final contribution:3.We introduce coherent-runtime expected quantum polynomial time, a simulation notion that (a) precisely captures all of our zero-knowledge simulators, (b) cannot break any polynomial hardness assumptions, (c) implies strict polynomial-time Δ-simulation and (d) is not subject to the CCLY impossibility. In light of our positive results and the CCLY negative results, we propose coherent-runtime simulation to be the appropriate quantum analogue of classical expected polynomial-time simulation.
Shuhao Zheng, Yanxi Lin, Yang Yu, Ye Yuan · 6 authors
Auditing the information leakage of latent sensitive features during the transborder data flow has attracted sufficient attention from global digital regulators. However, there is missing a technical approach for the audit practice due to two technical challenges. Firstly, there is a lack of theory and tools for measuring the information of sensitive latent features in a dataset. Secondly, the transborder data flow involves multi-stakeholders with diverse interests, which means the audit must be trustless. Despite the tremendous efforts in protecting data privacy, an important issue that has long been neglected is that the transmitted data in data flows can leak other regulated information that is not explicitly contained in the data, leading to unaware information leakage risks. To unveil such risks trustfully before the actual data transfer, we propose FIAT, a Fine-grained Information Audit system for Trustless transborder data flow. In FIAT, we use a learning approach to quantify the amount of information leakage, while the technologies of zero-knowledge proof and smart contracts are applied to provide trustworthy and privacy-preserving auditing results. Experiments show that large information leakage can boost the predictability of uninvolved information using simple machine-learning models, revealing the importance of information auditing. Further performance benchmarking also validates the efficiency and scalability of the FIAT auditing system.
Abstract The realization of fully autonomous vehicles in great scale is already in sight. However, to be safe and reliable, autonomous driving requires a significant amount of communication with cloud services, which are prone to many kinds of failures and malicious attacks. This paper introduces the use of AIngle, a novel distributed-ledger technology developed to guarantee real-time encrypted communication among IoT devices. Not only AIngle tackles various kinds of malicious attacks by design, such as Sybil attacks, but it also enables semantic distributed applications (Sem D Apps). Sem D Apps decentralize supporting driving services, such as traffic and route mapping, which are typically centralized in cloud services. AIngle provides a new paradigm for Sem D Apps, that will support future-proofed, fast, reliable, intelligent distributed applications for the autonomous vehicle industry.
WebAssembly (Wasm) smart contracts have shown growing popularity across blockchains (e.g., EOSIO) recently. Similar to Ethereum smart contracts, Wasm smart contracts suffer from various attacks exploiting their vulnerabilities. Even worse, few developers released the source code of their Wasm smart contracts for security review, raising the bar for uncovering vulnerable contracts. Although a few approaches have been proposed to detect vulnerable Wasm smart contracts, they have several major limitations, e.g., low code coverage, low accuracy and lack of scalability, unable to produce exploit payloads, etc. To fill the gap, in this paper, we design and develop WASAI, a new concolic fuzzer for uncovering vulnerabilities in Wasm smart contract after tackling several challenging issues. We conduct extensive experiments to evaluate WASAI, and the results show that it outperforms the state-of-the-art methods. For example, it achieves 2x code coverage than the baselines and surpasses them in detection accuracy, with an F1-measure of 99.2%. Moreover, WASAI can handle complicated contracts (e.g., contracts with obfuscation and sophisticated verification). Applying WASAI to 991 deployed smart contracts in the wild, we find that over 70% of smart contracts are vulnerable. By the time of this study, over 300 vulnerable contracts have not been patched and are still operating on the EOSIO Mainnet. One fake EOS vulnerability reported to the EOSIO ecosystem was recently assigned a CVE identifier (CVE-2022-27134).
Privacy-preserving federated learning allows multiple users to jointly train a model with coordination of a central server. The server only learns the final aggregation result, thereby preventing leakage of the usersâ (private) training data from the individual model updates. However, keeping the individual updates private allows malicious users to degrade the model accuracy without being detected, also known as Byzantine attacks. Best existing defenses against Byzantine workers rely on robust rank-based statistics, e.g., setting robust bounds via the median of updates, to find malicious updates. However, implementing privacy-preserving rank-based statistics, especially median-based, is nontrivial and unscalable in the secure domain, as it requires sorting of all individual updates. We establish the first private robustness check that uses high break point rank-based statistics on aggregated model updates. By exploiting randomized clustering, we significantly improve the scalability of our defense without compromising privacy. We leverage the derived statistical bounds in zero-knowledge proofs to detect and remove malicious updates without revealing the private user updates. Our novel framework, zPROBE, enables Byzantine resilient and secure federated learning. We show the effectiveness of zPROBE on several computer vision benchmarks. Empirical evaluations demonstrate that zPROBE provides a low overhead solution to defend against state-of-the-art Byzantine attacks while preserving privacy.
Privacy and data security have become the new hot topic for regulators in recent years. As a result, Federated Learning (FL) (also called collaborative learning) has emerged as a new training paradigm that allows multiple, geographically distributed nodes to learn a Deep Learning (DL) model together without sharing their data. Blockchain is becoming a new trend as data protection and privacy are concerns in many sectors. Technology is leading the world and transforming into a global village where everything is accessible and transparent. We have presented a blockchain enabled security model using FL that can generate an enhanced DL model without sharing data and improve privacy through higher security and access rights to data. However, existing FL approaches also have unique security vulnerabilities that malicious actors can exploit and compromise the trained model. The FL method is compared to the other known approaches. Users are more likely to choose the latter option, i.e., providing local but private data to the server and using ML apps, performing ML operations on the devices without benefiting from other usersâ data, and preventing direct access to raw data and local training of ML models. FL protects data privacy and reduces data transfer overhead by storing raw data on devices and combining locally computed model updates. We have investigated the feasibility of data and model poisoning attacks under a blockchain-enabled FL system built alongside the Ethereum network and the traditional FL system (without blockchain). This work fills a knowledge gap by proposing a transparent incentive mechanism that can encourage good behavior among participating decentralized nodes and avoid common problems and provides knowledge for the FL security literature by investigating current FL systems.
Shunhui Ji, Shaoqing Zhu, Pengcheng Zhang, Hai Dong · 5 authors
Smart contracts are commonly deployed for safety-critical applications, the quality assurance of which has been a vital factor. Test cases are standard means to ensure the correctness of data flows in smart contracts. To more efficiently generate test cases with high coverage, we propose an improved genetic algorithm-based test-case generation approach for smart contract data flow testing. Our approach introduces the theory of particle swarm optimization into the genetic algorithm, which reduces the influence brought by the randomness of genetic operations and enhances its capability to find global optima. A set of 30 real smart contracts deployed on Ethereum and GitHub is collected to perform the experimental study, on which our approach is compared with three baseline approaches. The experimental results show that, in most cases, the coverage of the test cases generated by our approach is significantly higher than the baseline approaches with relatively lower numbers of iterations and lower execution time.
Alex Groce, Kush Jain, Rijnard van Tonder, Goutamkumar Tulajappa Kalburgi · 5 authors
Bitcoin is one of the most prominent distributed software systems in the world. This paper describes an effort to investigate and enhance the effectiveness of the Bitcoin Core fuzzing effort. The effort initially began as a query about how to escape saturation in the fuzzing effort, but developed into a more general exploration. This paper summarizes the outcomes of a two-week focused effort. While the effort found no smoking guns indicating major test/fuzz weaknesses, it produced a large number of additional fuzz corpus entries, increased the set of fuzzers used for Bitcoin Core, and ran mutation analysis of Bitcoin Core fuzz targets, with a comparison to Bitcoin functional tests and other cryptocurrenciesâ tests. Our conclusion is that for high quality fuzzing efforts, improvements to the oracle may be the best way to get more out of fuzzing.
Francesco Zola, Lander Segurola-Gil, Jan L. Bruse, Mikel Galar · 5 authors
Abstract Classification of Bitcoin entities is an important task to help Law Enforcement Agencies reduce anonymity in the Bitcoin blockchain network and to detect classes more tied to illegal activities. However, this task is strongly conditioned by a severe class imbalance in Bitcoin datasets. Existing approaches for addressing the class imbalance problem can be improved considering generative adversarial networks (GANs) that can boost data diversity. However, GANs are mainly applied in computer vision and natural language processing tasks, but not in Bitcoin entity behaviour classification where they may be useful for learning and generating synthetic behaviours. Therefore, in this work, we present a novel approach to address the class imbalance in Bitcoin entity classification by applying GANs. In particular, three GAN architectures were implemented and compared in order to find the most suitable architecture for generating Bitcoin entity behaviours. More specifically, GANs were used to address the Bitcoin imbalance problem by generating synthetic data of the less represented classes before training the final entity classifier. The results were used to evaluate the capabilities of the different GAN architectures in terms of training time, performance, repeatability, and computational costs. Finally, the results achieved by the proposed GAN-based resampling were compared with those obtained using five well-known data-level preprocessing techniques. Models trained with data resampled with our GAN-based approach achieved the highest accuracy improvements and were among the best in terms of precision, recall and f1-score. Together with Random Oversampling (ROS), GANs proved to be strong contenders in addressing Bitcoin class imbalance and consequently in reducing Bitcoin entity anonymity (overall and per-class classification performance). To the best of our knowledge, this is the first work to explore the advantages and limitations of GANs in generating specific Bitcoin data and âattackingâ Bitcoin anonymity. The proposed methods ultimately demonstrate that in Bitcoin applications, GANs are indeed able to learn the data distribution and generate new samples starting from a very limited class representation, which leads to better detection of classes related to illegal activities.
A zero-knowledge (ZK) proof guarantees that the result of a computation is correct while keeping part of the computation details private. Some ZK proofs are tiny and can be verified in short time, which makes them one of the most promising technologies for solving two key aspects: the challenge of enabling privacy to public and transparent distributed ledgers and, enhancing the scalability limitations of distributed ledgers. Most practical ZK systems require the computation to be expressed as an arithmetic circuit that is encoded as a set of equations called rank-1 constraint system (R1CS). In this paper, we present \circom, a programming language and a compiler for designing arithmetic circuits that are compiled to R1CS. More precisely, with \circom, programmers can design arithmetic circuits, and the compiler outputs (i) a file with the R1CS description, (ii) \wasm and \cpp programs to efficiently compute all values of the circuit. We also provide an open-source library called \circomlib, with multiple circuit templates. Moreover, \circom can be complemented with \snarkjs, a tool for generating and validating ZK proofs from R1CS. Altogether, our software tools abstract the complexity of the proving mechanisms and provide a friendly interface to model low-level descriptions of arithmetic circuits.
The Open Vote Network is a self-tallying decentralized e-voting protocol suitable for boardroom elections. Currently, it has two Ethereum-based implementations: the first, by McCorry et al., has a scalability issue since all the computations are performed on-chain. The second implementation, by Seifelnasr et al., solves this issue partially by assigning a part of the heavy computations to an off-chain untrusted administrator in a verifiable manner. As a side effect, this second implementation became not dispute-free; there is a need for a tally dispute phase where an observer interrupts the protocol when the administrator cheats, i.e., announces a wrong tally result. In this work, we propose a new smart contract design to tackle the problems in the previous implementations by (i) preforming all the heavy computations off-chain hence achieving higher scalability, and (ii) utilizing zero-knowledge Succinct Non-interactive Argument of Knowledge (zk-SNARK) to verify the correctness of the off-chain computations, hence maintaining the dispute-free property. To demonstrate the effectiveness of our design, we develop prototype implementations on Ethereum and conduct multiple experiments for different implementation options that show a trade-off between the zk-SNARK proof generation time and the smart contract gas cost, including an implementation in which the smart contract consumes a constant amount of gas independent of the number of voters.
Federated learning is known to be vulnerable to both security and privacy issues. Existing research has focused either on preventing poisoning attacks from users or on concealing the local model updates from the server, but not both. However, integrating these two lines of research remains a crucial challenge since they often conflict with one another with respect to the threat model. In this work, we develop a principle framework that offers both privacy guarantees for users and detection against poisoning attacks from them. With a new threat model that includes both an honest-but-curious server and malicious users, we first propose a secure aggregation protocol using homomorphic encryption for the server to combine local model updates in a private manner. Then, a zero-knowledge proof protocol is leveraged to shift the task of detecting attacks in the local models from the server to the users. The key observation here is that the server no longer needs access to the local models for attack detection. Therefore, our framework enables the central server to identify poisoned model updates without violating the privacy guarantees of secure aggregation.
Elizabeth Nathania Witanto, Yustus Eko Oktian, Sang-Gon Lee
AI has been implemented in many sectors such as security, health, finance, national defense, etc. However, together with AIâs groundbreaking improvement, some people exploit AI to do harmful things. In parallel, there is rapid development in cloud computing technology, introducing a cloud-based AI system. Unfortunately, the vulnerabilities in cloud computing will also affect the security of AI services. We observe that compromising the training data integrity means compromising the results in the AI system itself. From this background, we argue that it is essential to keep the data integrity in AI systems. To achieve our goal, we build a data integrity architecture by following the National Institute of Standards and Technology (NIST) cybersecurity framework guidance. We also utilize blockchain technology and smart contracts as a suitable solution to overcome the integrity issue because of its shared and decentralized ledger. Smart contracts are used to automate policy enforcement, keep track of data integrity, and prevent data forgery. First, we analyze the possible vulnerabilities and attacks in AI and cloud environments. Then we draw out our architecture requirements. The final result is that we present five modules in our proposed architecture that fulfilled NIST framework guidance to ensure continuous data integrity provisioning towards secure AI environments.
Jiasi Weng, Jian Weng, Gui Hong Tang, Anjia Yang · 6 authors
We propose a new approach for privacy-preserving and verifiable convolutional neural network (CNN) testing in a distrustful multi-stakeholder environment. The approach is aimed to enable that a CNN modeldeveloperconvinces auserof the truthful CNN performance over non-public data frommultiple testers, while respecting model and data privacy. To balance the security and efficiency issues, we appropriately integrate three tools with the CNN testing, including collaborative inference, homomorphic encryption (HE) and zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK). We start with strategically partitioning a CNN model into a private part kept locally by the model developer, and a public part outsourced to an outside server. Then, the private part runs over the HE-protected test data sent by a tester, and transmits its outputs to the public part for accomplishing subsequent computations of the CNN testing. Second, the correctness of the above CNN testing is enforced by generating zk-SNARK based proofs, with an emphasis on optimizing proving overhead for two-dimensional (2-D) convolution operations, since the operations dominate the performance bottleneck during generating proofs. We specifically present a new quadratic matrix program (QMP)-based arithmetic circuit witha single multiplication gatefor expressing 2-D convolution operations between multiple filters and inputs in a batch manner. Third, we aggregate multiple proofs with respect to a same CNN model but different testersâ test data (i.e., different statements) into one proof, and ensure that the validity of the aggregated proof implies the validity of the original multiple proofs. Lastly, our experimental results demonstrate that our QMP-based zk-SNARK performs nearly 13.9Ă faster than the existing quadratic arithmetic program (QAP)-based zk-SNARK in proving time, and 17.6Ă faster in Setup time, for high-dimension matrix multiplication. Besides, the limitation on handling a bounded number of multiplications of QAP-based zk-SNARK is relieved.
The internet-of-Vehicle (IoV) can facilitate seamless connectivity between connected vehicles (CV), autonomous vehicles (AV), and other IoV entities. Intrusion Detection Systems (IDSs) for IoV networks can rely on machine learning (ML) to protect the in-vehicle network from cyber-attacks. Blockchain-based Federated Forests (BFFs) could be used to train ML models based on data from IoV entities while protecting the confidentiality of the data and reducing the risks of tampering with the data. However, ML models created this way are still vulnerable to evasion, poisoning, and exploratory attacks using adversarial examples. This paper investigates the impact of various possible adversarial examples on the BFF-IDS. We proposed integrating a statistical detector to detect and extract unknown adversarial samples. By including the unknown detected samples into the dataset of the detector, we augment the BFF-IDS with an additional model to detect original known attacks and the new adversarial inputs. The statistical adversarial detector confidently detected adversarial examples at the sample size of 50 and 100 input samples. Furthermore, the augmented BFF-IDS (BFF-IDS(AUG)) successfully mitigates the adversarial examples with more than 96% accuracy. With this approach, the model will continue to be augmented in a sandbox whenever an adversarial sample is detected and subsequently adopt the BFF-IDS(AUG) as the active security model. Consequently, the proposed integration of the statistical adversarial detector and the subsequent augmentation of the BFF-IDS with detected adversarial samples provides a sustainable security framework against adversarial examples and other unknown attacks.
A smart contract is a computer program which is automatically executed with some conditional statements such as âif/thenâ. Since smart contracts can include some vulnerable program codes, smart contract exploit was recently highlighted as one of the severe threats to Ethereum blockchain. As one of the efficient and effective smart contract vulnerability detection methods, deep learning methods have been studied due to the fast detection speed and the high detection accuracy. Recently, the deep learning methods using convolutional neural network(CNN) have actively studied to classify images transformed from smart contracts into vulnerable or invulnerable. However, while simply transforming a smart contract into an image and analyzing, semantics and context of the smart contract are ignored to cause false detection alarms. To detect vulnerable smart contracts while maintaining their semantics and context, we propose a new code-targeted CNN architecture, called CodeNet. To improve the performance of CodeNet, we also design a data pre-processing procedure, where a smart contract is transformed into an image while maintaining locality. From the experimental results under various types of vulnerabilities, the proposed CodeNet-based vulnerability detection method shows the good-enough detection performance and detection time compared to well-known state-of-the-art vulnerability detection tools.
Blockchain technology and its applications are gaining popularity day by day. It is a ground-breaking technology that allows users to communicate without the need of a trusted middleman. A smart contract (self-executable code) is deployed on the blockchain and auto executes due to a triggering condition. In a no-trust contracting environment, smart contracts can establish trust among parties. Terms and conditions embedded in smart contracts will be imposed immediately when specified criteria have been fulfilled. Due to this, the malicious assailants have a special interest in smart contracts. Blockchains are immutable means if some transaction is deployed or recorded on the blockchain, it becomes unalterable. Thus, smart contracts must be analyzed to ensure zero security vulnerabilities or flaws before deploying the same on the blockchain because a single vulnerability can lead to the loss of millions. For analyzing the security vulnerabilities of smart contracts, various analysis tools have been developed to create safe and secure smart contracts. This paper presents a systematic review on Ethereum smart contracts analysis tools. Initially, these tools are categorized into static and dynamic analysis tools. Thereafter, different sources code analysis techniques are studied such as taint analysis, symbolic execution, and fuzzing techniques. In total, 86 security analysis tools developed for Ethereum blockchain smart contract are analyzed regardless of tool type and analysis approach. Finally, the paper highlights some challenges and future recommendations in the field of Ethereum smart contracts.
S. Kate Devitt, Jason Scholz, Timo Schless, L Lewis
Abstract Artificial intelligences (AI) will increasingly participate digitally and physically in conflicts yet there is a lack of trusted communications with humans for humanitarian purposes. For example, in disasters and conflicts messaging and social media are used to share information, however, international humanitarian relief organisations treat this information as unverifiable and untrustworthy. Furthermore, current AI implementations can be brittle, with a narrow scope of application and wide scope of ethical risks. Meanwhile, human error can cause significant civilian harms even by combatants committed to compliance with international humanitarian law. AI offers an opportunity to help reduce the tragedy of war and better deliver humanitarian aid to those who need it. However, to be successful, these systems must be trusted by humans and their information systems, overcoming flawed information flows in conflict and disaster zones that continue to be marked by intermittent communications, poor situation awareness, mistrust and human errors. In this paper, we consider the integration of a communications protocol (the âWhiteflag protocolâ), distributed ledger âblockchainâ technology, and information fusion with artificial intelligence (AI), to improve conflict communications called âProtected Assurance Understanding Situation & Entitiesâ (PAUSE). Such a trusted human-AI communication network could provide accountable information exchange regarding protected entities, critical infrastructure, humanitarian signals and status updates for humans and machines in conflicts. Trust-based information fusion provides resource-efficient use of diverse data sources to increase the reliability of reports. AI can catch human mistakes and complement human decision making, while human judgment can direct and override AI recommendations. We examine several realistic potential case studies for the integration of these technologies into a trusted human-AI network for humanitarian benefit including mapping a conflict zone with civilians and combatants in real time, preparation to avoid incidents and using the network to manage misinformation. We finish with a real-world example of a PAUSE-like network, the Human Security Information System (HSIS), being developed by USAID, that uses blockchain technology to provide a secure means to better understand the civilian environment.
Yinxing Xue, Jiaming Ye, Wei Zhang, Jun Sun · 7 authors
Smart contract transactions are increasingly interleaved by cross-contract calls. While many tools have been developed to identify a common set of vulnerabilities to guard smart contracts, the cross-contract vulnerability is however overlooked by existing tools. Cross-contract vulnerabilities are exploitable bugs that manifest in the presence of more than two interacting contracts. Existing methods are however limited to analyze a maximum of two contracts at the same time. Detecting cross-contract vulnerabilities is highly non-trivial. With multiple interacting contracts, the search space is much larger than that of a single contract. To address this problem, we present xFuzz, a machine learning guided smart contract fuzzing framework. The machine learning models are trained with novel features (e.g., word vectors and instructions) and are used to filter likely benign program paths. Comparing with existing static tools, machine learning model is proven to be more robust, avoiding directly adopting manually-defined rules in specific tools. We compare xFuzz with three state-of-the-art tools on 7,391 contracts. xFuzz detects 18 exploitable cross-contract vulnerabilities, of which 15 vulnerabilities are exposed for the first time. Furthermore, our approach is shown to be efficient in detecting non-cross-contract vulnerabilities as well-using less than 20% time as that of other fuzzing tools, xFuzz detects twice as many vulnerabilities.
Zhiyong Fang, David Darais, Joseph P. Near, Yupeng Zhang
Static program analysis tools can automatically prove many useful properties of programs. However, using static analysis to prove to a third party that a program satisfies a property requires revealing the program's source code. We introduce the concept of zero-knowledge static analysis, in which the prover constructs a zero-knowledge proof about the outcome of the static analysis without revealing the program. We present novel zero-knowledge proof schemes for intra- and inter-procedural abstract interpretation. Our schemes are significantly more efficient than the naive translation of the corresponding static analysis algorithms using existing schemes. We evaluate our approach empirically on real and synthetic programs; with a pairing-based zero knowledge proof scheme as the backend, we are able to prove the control flow analysis on a 2,000-line program in 1,738s. The proof is only 128 bytes and the verification time is 1.4ms. With a transparent zero knowledge proof scheme based on discrete-log, we generate the proof for the tainting analysis on a 12,800-line program in 406 seconds, the proof size is 282 kilobytes, and the verification time is 66 seconds.
Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, IĆıl Dillig · 5 authors
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.