Follow blockchain research across journals, conferences, and preprint repositories.
1,684 results · page 61 of 71
Elli Androulaki, Artem Barger, Vita Bortnikov, Christian Cachin · 21 authors
The success of public blockchains, such as Bitcoin and Ethereum, led to growing interest in Blockchain technology and its application as a distributed system in the most innovative business use cases.
Raymond Cheng, Fan Zhang, Jernej Kos, Warren He · 9 authors
Smart contracts are applications that execute on blockchains. Today they manage billions of dollars in value and motivate visionary plans for pervasive blockchain deployment. While smart contracts inherit the availability and other security assurances of blockchains, however, they are impeded by blockchains' lack of confidentiality and poor performance. We present Ekiden, a system that addresses these critical gaps by combining blockchains with Trusted Execution Environments (TEEs). Ekiden leverages a novel architecture that separates consensus from execution, enabling efficient TEE-backed confidentiality-preserving smart-contracts and high scalability. Our prototype (with Tendermint as the consensus layer) achieves example performance of 600× more throughput and 400× less latency at 1000× less cost than the Ethereum mainnet. Another contribution of this paper is that we systematically identify and treat the pitfalls arising from harmonizing TEEs and blockchains. Treated separately, both TEEs and blockchains provide powerful guarantees, but hybridized, though, they engender new attacks. For example, in naïve designs, privacy in TEE-backed contracts can be jeopardized by forgery of blocks, a seemingly unrelated attack vector. We believe the insights learned from Ekiden will prove to be of broad importance in hybridized TEE-blockchain systems.
Franklin Schrans, Susan Eisenbach, Sophia Drossopoulou
Blockchain-based platforms such as Ethereum support the execution of versatile decentralized applications, known as smart contracts. These typically hold and transfer digital currency (e.g., Ether) to other parties on the platform. Contracts have been subject to numerous attacks, losing hundreds of millions of dollars (in Ether). We propose Flint, a new type-safe, capabilities-secure, contract-oriented programming language specifically designed for writing robust smart contracts. To help programmers reason about access control of functions, Flint programmers use caller capabilities. To prevent vulnerabilities relating to the unintentional loss of currency, transfers of assets in Flint are performed through safe atomic operations, inspired by linear type theory.
Jiao Jiao, Shuanglong Kan, Shang‐Wei Lin, David Sanán · 6 authors
Bitcoin has attracted everyone's attention and interest recently. Ethereum (ETH), a second generation cryptocurrency, extends Bitcoin's design by offering a Turing-complete programming language called Solidity to develop smart contracts. Smart contracts allow creditable execution of contracts on EVM (Ethereum Virtual Machine) without third parties. Developing correct smart contracts is challenging due to its decentralized computation nature. Buggy smart contracts may lead to huge financial loss. Furthermore, smart contracts are very hard, if not impossible, to patch once they are deployed. Thus, there is a recent surge of interest on analyzing/verifying smart contracts. While existing work focuses on EVM opcode, we argue that it is equally important to understand and define the semantics of Solidity since programmers program and reason about smart contracts at the level of source code. In this work, we develop the structural operational semantics for Solidity, which allows us to identify multiple design issues which underlines many problematic smart contracts. Furthermore, our semantics is executable in the K framework, which allows us to verify/falsify contracts automatically.
Paweł Szałachowski
The Transport Layer Security (TLS) protocol is a de facto standard of secure client-server communication on the Internet. Its security can be diminished by a variety of attacks that leverage on weaknesses in its design and implementations. An example of a major weakness is the public-key infrastructure (PKI) that TLS deploys, which is a weakest-link system and introduces hundreds of links (i.e., trusted entities). Consequently, an adversary compromising a single trusted entity can impersonate any website. Notary systems, based on multi-path probing, were early and promising proposals to detect and prevent such attacks. Unfortunately, despite their benefits, they are not widely deployed, mainly due to their long-standing unresolved problems. In this paper, we present Persistent and Accountable Domain Validation (PADVA), which is a next-generation TLS notary service. PADVA combines the advantages of previous proposals, enhancing them, introducing novel mechanisms, and leveraging a blockchain platform which provides new features. PADVA keeps notaries auditable and accountable, introduces service-level agreements and mechanisms to enforce them, relaxes availability requirements for notaries, and works with the legacy TLS ecosystem. We implemented and evaluated PADVA, and our experiments indicate its efficiency and deployability.
Giuseppe Destefanis, Michele Marchesi, Marco Ortu, Roberto Tonelli · 6 authors
Smart Contracts have gained tremendous popularity in the past few years, to the point that billions of US Dollars are currently exchanged every day through such technology. However, since the release of the Frontier network of Ethereum in 2015, there have been many cases in which the execution of Smart Contracts managing Ether coins has led to problems or conflicts. Compared to traditional Software Engineering, a discipline of Smart Contract and Blockchain programming, with standardized best practices that can help solve the mentioned problems and conflicts, is not yet sufficiently developed. Furthermore, Smart Contracts rely on a non-standard software life-cycle, according to which, for instance, delivered applications can hardly be updated or bugs resolved by releasing a new version of the software. In this paper we advocate the need for a discipline of Blockchain Software Engineering, addressing the issues posed by smart contract programming and other applications running on blockchains.We analyse a case of study where a bug discovered in a Smart Contract library, and perhaps "unsafe" programming, allowed an attack on Parity, a wallet application, causing the freezing of about 500K Ethers (about 150M USD, in November 2017). In this study we analyze the source code of Parity and the library, and discuss how recognised best practices could mitigate, if adopted and adapted, such detrimental software misbehavior. We also reflect on the specificity of Smart Contract software development, which makes some of the existing approaches insufficient, and call for the definition of a specific Blockchain Software Engineering.
Norsefire, ToCsIcK
This paper introduces the underlying mechanics and interface for PhoeniχCoin (PHX), an Ethereum ERC223-compliant cryptocurrency. The supply of PHX tokens is tied directly to the Ethereum balance of the smart contract underpinning the ‘EthPhoenix’ decentralised application, and mined using a novel, generalisable technique we refer to as proof-of-volatility.
Anastasia Mavridou, Áron Lászka
Blockchain-based distributed computing platforms enable the trusted execution\nof computation - defined in the form of smart contracts - without trusted\nagents. Smart contracts are envisioned to have a variety of applications,\nranging from financial to IoT asset tracking. Unfortunately, the development of\nsmart contracts has proven to be extremely error prone. In practice, contracts\nare riddled with security vulnerabilities comprising a critical issue since\nbugs are by design non-fixable and contracts may handle financial assets of\nsignificant value. To facilitate the development of secure smart contracts, we\nhave created the FSolidM framework, which allows developers to define contracts\nas finite state machines (FSMs) with rigorous and clear semantics. FSolidM\nprovides an easy-to-use graphical editor for specifying FSMs, a code generator\nfor creating Ethereum smart contracts, and a set of plugins that developers may\nadd to their FSMs to enhance security and functionality.\n
Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena · 5 authors
Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new systematic characterization of a class of trace vulnerabilities, which result from analyzing multiple invocations of a contract over its lifetime. We focus attention on three example properties of such trace vulnerabilities: finding contracts that either lock funds indefinitely, leak them carelessly to arbitrary users, or can be killed by anyone. We implemented MAIAN, the first tool for precisely specifying and reasoning about trace properties, which employs inter-procedural symbolic analysis and concrete validator for exhibiting real exploits. Our analysis of nearly one million contracts flags 34,200 (2,365 distinct) contracts vulnerable, in 10 seconds per contract. On a subset of3,759 contracts which we sampled for concrete validation and manual analysis, we reproduce real exploits at a true positive rate of 89%, yielding exploits for3,686 contracts. Our tool finds exploits for the infamous Parity bug that indirectly locked 200 million dollars worth in Ether, which previous analyses failed to capture.
Yuanyu Zhang, Shoji Kasahara, Yulong Shen, Xiaohong Jiang · 5 authors
This paper investigates a critical access control issue in the Internet of Things (IoT). In particular, we propose a smart contract-based framework, which consists of multiple access control contracts (ACCs), one judge contract (JC), and one register contract (RC), to achieve distributed and trustworthy access control for IoT systems. Each ACC provides one access control method for a subject-object pair, and implements both static access right validation based on predefined policies and dynamic access right validation by checking the behavior of the subject. The JC implements a misbehavior-judging method to facilitate the dynamic validation of the ACCs by receiving misbehavior reports from the ACCs, judging the misbehavior and returning the corresponding penalty. The RC registers the information of the access control and misbehavior-judging methods as well as their smart contracts, and also provides functions (e.g., register, update, and delete) to manage these methods. To demonstrate the application of the framework, we provide a case study in an IoT system with one desktop computer, one laptop and two Raspberry Pi single-board computers, where the ACCs, JC, and RC are implemented based on the Ethereum smart contract platform to achieve the access control.
Xiaomin Bai, Zijing Cheng, Zhangbo Duan, Kai Hu
Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an agreement on the contents of the contract and perform the contracts according to the behaviors written in certain computer algorithms. It not only needs to make sure about the correctness of smart contracts code, but also should provide a credible contract code execution environment. Blockchain provides a trusted execution and storage environment for smart contracts by the distributed secure storage, consistency verification and encryption technology. Current challenge is how to assure that smart contract can be executed as the parties' willingness. This paper introduces formal modeling and verification in formal methods to make smart contract model and verify the properties of smart contracts. Formal methods combined with smart contracts aim to reduce the potential errors and cost during contract development process. The description of a general and formal smart contract template is provided. The tool of model checking, SPIN, is used to verify the correctness and necessary properties for a smart contract template. The research shows model checking will be useful and necessary for smart contracts.
Ence Zhou, Hua Song, Bingfeng Pi, Jun Sun · 7 authors
Currently, Bitcoin and Ethereum are the two most popular cryptocurrency systems, especially Ethereum. It permits complex financial transactions or rules through scripts, which is called smart contracts. Since Ethereum smart contracts hold millions of dollars, their execution correctness is crucial against attacks which aim at stealing the assets. In this paper, we proposed a security assurance method for smart contract source code to find potential security risks. It contains two main functions, the first is syntax topological analysis of smart contract invocation relationship, to help developers to understand their code structure clearly; the second is logic risk (which may lead to vulnerabilities) detection and location, and label results on topology diagram. For developers' convenience, we have built a static analysis tool called SASC to generate topology diagram of invocation relationship and to find potential logic risks. We have made an evaluation on 2,952 smart contracts, experiment results proved that our method is intuitive and effective.
Tesnim Abdellatif, Kei-Léo Brousmiche
Blockchain technology has attracted increasing attention in recent years. One reason of this new trend is the introduction of on-chain smart contracts enabling the implementation of decentralized applications in trust-less environments. Along with its adoption, attacks exploiting smart contract vulnerabilities are inevitably growing. To counter these attacks and avoid breaches, several approaches have been explored such as documenting vulnerabilities or model checking using formal verification. However, these approaches fail to capture the Blockchain and users behavior properties. In this paper, we propose a novel formal modeling approach to verify a smart contract behavior in its execution environment. We apply this formalism on a concrete smart contract example and analyze its breaches with a statical model checking approach.
Marcus Brandenburger, Christian Cachin
Modern Trusted Execution Environments (TEEs), such as Intel SGX, gain more and more popularity in the blockchain community and their adoption has already been started. Combining smart-contract execution with TEEs promises efficient solutions for protecting data privacy in distributed ledgers, as an alternative to much more costly cryptographic protocols. This paper describes practical challenges that arise from the combination of smart contracts with TEEs. In particular, we discuss existing solutions and their conceptional differences of on-chain and off-chain execution followed by technical challenges on attestation, key management, and non-deterministic execution.
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky · 7 authors
Callbacks are essential in many programming environments, but drastically\ncomplicate program understanding and reasoning because they allow to mutate\nobject's local states by external objects in unexpected fashions, thus breaking\nmodularity. The famous DAO bug in the cryptocurrency framework Ethereum,\nemployed callbacks to steal $150M. We define the notion of Effectively Callback\nFree (ECF) objects in order to allow callbacks without preventing modular\nreasoning.\n An object is ECF in a given execution trace if there exists an equivalent\nexecution trace without callbacks to this object. An object is ECF if it is ECF\nin every possible execution trace. We study the decidability of dynamically\nchecking ECF in a given execution trace and statically checking if an object is\nECF. We also show that dynamically checking ECF in Ethereum is feasible and can\nbe done online. By running the history of all execution traces in Ethereum, we\nwere able to verify that virtually all existing contracts, excluding the DAO or\ncontracts with similar known vulnerabilities, are ECF. Finally, we show that\nECF, whether it is verified dynamically or statically, enables modular\nreasoning about objects with encapsulated state.\n
Zhangbo Duan, Hongliang Mao, Zhidong Chen, Xiaomin Bai · 6 authors
As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.
Ilya Sergey, Amrit Kumar, Aquinas Hobor
This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich interaction patterns, and a programming component, which enjoys principled semantics and is amenable to formal verification. Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode. We describe the automata-based model of Scilla, present its programming component and show how contract definitions in terms of automata streamline the process of mechanised verification of their safety and temporal properties.
Bram Cohen, Krzysztof Pietrzak
No abstract is available for this record.
Bernhard Beckert, Mihai Herda, Michael Kirsten, Jonas Schiffl
Smart contracts are programs building on blockchain technology. They implement functionality that has been agreed on between the concerned parties on a network. However, their immutability and exposed position make them vulnerable to programming errors, leading to faulty behavior and possible exploits. Therefore, smart contracts demand a particularly thorough analysis, ideally using formal program verification. In this paper, we present an approach for the deductive verification of Hyperledger Fabric smart contracts using the KeY prover. We have extended KeY to handle Fabric ledger implementations; in particular, we have developed mechanisms for reasoning about serialization and object persistence. The feasibility of our approach is demonstrated with a small case study.
Dakshita Khurana
The notion of simulation is central to cryptography: often, to demonstrate that an adversary did not recover any information about private inputs of other participants, we exhibit the existence of a simulator that generates the adversary's view without access to inputs of honest participants. The primary method used to build simulators is rewinding, where a simulator resets the adversary to a previous point in the protocol and tries to complete the protocol tree multiple times until it achieves a favorable outcome.First introduced in the context of zero-knowledge proof systems and secure computation, today the rewinding technique is synonymous with protocol security and polynomial simulation. Prior to this work, all known rewinding techniques in the plain model required multiple rounds of back-and-forth interaction between participants.In this thesis, we demonstrate the first rewinding techniques that require only a single message from each participant. Using these techniques, we overcome several barriers from literature to construct for the first time, based on standard sub-exponential cryptographic assumptions, the following core protocols, and several subsequent applications:- Two message commitments satisfying non-malleability (with respect to commitment).- Two-message delayed-input weak zero-knowledge arguments for NP. These imply arguments for NP satisfying witness hiding and strong witness indistinguishability.
Yu xin Song, Zhong xia Liao, Yan hua Liang
Trusted computing is principle measure to ensure the security of computing platform, which improves the creditability by functions including data protection, identity authentication, integrity measurement, storage and reports. In order to easily provide architecture for security authentication of terminal members, and to protect the user's privacy and secret data, this article studies the remote identification for TPM. It introduces DAA anonymous authentication technology to traditional PKI and adopts improved DAA scheme to provide trusted identity authentication, secure channel establishment and sub-certificate update operation. We propose a new model for identity authentication under trusted computing environment. The scheme constructs a safe elliptic hyperbola by ISSUER and generate DAA certificate, which awards zero knowledge proof to each platform to achieve DAA certificate respectively. Then the code service provided by OPENSSL is used to establish PCA and simulated the AIK certificate process according to creation of AIK certificate. Finally, the experiments are performed under VMware-workstation and SUSE virtual machines, with TPM Emulator and TPM chips simulation, to verify the feasibility of remote user trustworthiness authentication scheme. The remote authentication scheme focused by this article is a protocol with anonymity, authentication and security, which will be useful and applicable in current information society.
Weijin Wang, Jingbin Liu, Yu Qin, Dengguo Feng
No abstract is available for this record.
Aggelos Kiayias, Annabell Kuldmaa, Helger Lipmaa, Janno Siim · 5 authors
No abstract is available for this record.
Zuoxia Yu, Man Ho Au, Rupeng Yang, Junzuo Lai · 5 authors
No abstract is available for this record.