Follow blockchain research across journals, conferences, and preprint repositories.
1,684 results · page 52 of 71
Gordon J. Pace, César Sánchez, Gerardo Schneider
No abstract is available for this record.
Joshua Ellul
No abstract is available for this record.
Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian · 9 authors
No abstract is available for this record.
Bernhard Beckert, Jonas Schiffl, Mattias Ulbrich
No abstract is available for this record.
Mirko Staderini, Andrea Bondavalli
The Minisymposium investigated areas that cover embedded information systems, dependability and security, artificial intelligence, bioinformatics, and cyber-physical systems.
Ning Han, Ximeng Li, Guohui Wang, Zhiping Shi · 5 authors
No abstract is available for this record.
João Santos Reis, Paul Crocker, Simão Melo de Sousa
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and aims to preserve the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.
Cosimo Laneve, Adele Veschetti
We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.
Wentian Yan, Jianbo Gao, Zhenhao Wu, Yue Li · 7 authors
Smart contracts are the back-end programs of blockchain-based applications and the execution results are deterministic and publicly visible. Developers are unwilling to release source code of some smart contracts to generate randomness or for security reasons, however, attackers still can use reverse engineering tools to decompile and analyze the code. In this paper, we propose EShield, an automated security enhancement tool for protecting smart contracts against reverse engineering. EShield replaces original instructions of operating jump addresses with anti-patterns to interfere with control flow recovery from bytecode. We have implemented four methods in EShield and conducted an experiment on over 20k smart contracts. The evaluation results show that all the protected smart contracts are resistant to three different reverse engineering tools with little extra gas cost.
Bernhard Beckert, Jonas Schiffl
No abstract is available for this record.
Alexander J. M. Milne, Arnold Beckmann, Pardeep Kumar
Cyber Physical Trust Systems (CPTS) are Cyber Physical Systems and Internet of Things enriched with trust as an explicit, measurable, testable and verifiable system component. In this paper, we propose to use blockchain, a distributed ledger technology, as the trust enabling system component for CPTS. We propose two schemes for CPTSs driven by blockchain in relation to two typical network model cases. We show that our proposed approach achieves the security properties, such as device identification, authentication, integrity, and non-repudiation, and provides protection against popular attacks, such as replay and spoofing. We provide formal proofs of those properties using the Tamarin Prover tool. We describe results of a proof-of-concept which implements a CPTS driven by blockchain for physical asset management and present a performance analysis of our implementation. We identify use cases in which CPTSs driven by blockchain find applications.
Zijian Bao, Qinghao Wang, Wenbo Shi, Lei Wang · 6 authors
As a decentralized, public, and digital ledger technology in Peer-to-Peer network, blockchain has received much attention from various fields, including finance, healthcare, supply chain, etc. However, some challenges (e.g., scalability, privacy, and security issues) severely affects the wide adoption of blockchain technology. Recently, Intel software guard extensions (SGX), as new trusted computing technologies, have provided a new solution to the above challenges in the blockchain area. Although many studies have focused on using SGX technology to enhance their schemes in the blockchain areas, no comprehensive survey has systematically analyzed and delineated these studies. This article is the first to systematically discuss the application status of SGX in the blockchain area. In this article, we study the scheme designs, advantages, and disadvantages of the existing works using a six-layer hierarchical structure of the blockchain. We also summarize the functions of SGX and formally analyze the advantages and disadvantages of SGX. Finally, we review the remaining challenges and present a list of possible directions for future research.
Massimo Bartoletti, Maurizio Murgia, Roberto Zunino
BitML is a process calculus to express smart contracts that can be run on Bitcoin. One of its current limitations is that, once a contract has been stipulated, the participants cannot renegotiate its terms: this prevents expressing common financial contracts, where funds have to be added by participants at run-time. In this paper, we extend BitML with a new primitive for contract renegotiation. At the same time, the new primitive can be used to write recursive contracts, which was not possible in the original BitML. We show that, despite the increased expressiveness, it is still possible to execute BitML on standard Bitcoin, preserving the security guarantees of BitML.
Pedro Antonino, A. W. Roscoe
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that they have been fixed. In this paper, we present a formalisation of Solidity and the Ethereum blockchain using the Solid language and its blockchain; a Solid program is obtained by explicating/desugaring a Solidity program. We make some abstractions that over-approximate the way in which Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. It translates Solid into Boogie, an intermediate verification language, that is later verified using Corral, a bounded model checker for Boogie. Unlike much of the work in this area, we do not try to find specific behavioural/code patterns that might lead to vulnerabilities. Instead, we provide a tool to find errors/bad states, i.e. program states that do not conform with the intent of the developer. Such a bad state, be it a vulnerability or not, might be reached through the execution of specific known code patterns or through behaviours that have not been anticipated.
Jonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel
No abstract is available for this record.
Xueping Liang, Sachin Shetty, Peter Foytik, Deepak K. Tosh
Distributed Ledger Technology (DLT) utilizes an architecture that can host a large number of nodes without pre-established trust to provide decentralized services. The blockchain is the most widely used architecture of distributed ledger, where transactions across the whole network are visible to all participants in a chain to prevent tampering. However, transactions may contain sensitive information such as business contract. To secure the system and protect user privacy, we propose a multi-channel architecture that leverages Intel Software Guard Extensions (SGX). We illustrate how SGX capabilities help to defend against attacks on distributed ledgers, by way of SGX enforcement on the participating machines. We adopt the design and implementation of a two layer architecture for securing the blockchain mining process and enhancing the transaction privacy. The security analysis and performance evaluation show that the design and protocols are capable of protecting privacy, defending against adversarial attacks and scalable.
Mouhamad Almakhour, Layth Sliman, Abed Ellatif Samhat, Abdelhamid Mellouk
No abstract is available for this record.
Wai Kok Chan, Ji‐Jian Chin, Vik Tor Goh
No abstract is available for this record.
Ákos Hajdu, Naghmeh Ivaki, Imre Kocsis, Attila Klenik · 8 authors
Blockchain has become particularly popular due to its promise to support business-critical services in very different domains (e.g., retail, supply chains, healthcare). Blockchain systems rely on complex middleware, like Ethereum or Hyperledger Fabric, that allow running smart contracts, which specify business logic in cooperative applications. The presence of software defects or faults in these contracts has notably been the cause of failures, including severe security problems. In this paper, we use a software implemented fault injection (SWIFI) technique to assess the behavior of permissioned blockchain systems in the presence of faulty smart contracts. We emulate the occurrence of general software faults (e.g., missing variable initialization) and also blockchain-specific software faults (e.g., missing require statement on transaction sender) in smart contracts code to observe the impact on the overall system dependability (i.e., reliability and integrity). We also study the effectiveness of formal verification (i.e., done by solc-verify) and runtime protections (e.g., using the assert statement) mechanisms in detection of injected faults. Results indicate that formal verification as well as additional runtime protections have to complement built-in platform checks to guarantee the proper dependability of blockchain systems and applications. The work presented in this paper allows smart contract developers to become aware of possible faults in smart contracts and to understand the impact of their presence. It also provides valuable information for middleware developers to improve the behavior (e.g., overall fault tolerance) of their systems.
Asma Lahbib, Abderrahim Ait Wakrime, Anis Laouiti, Khalifa Toumi · 5 authors
No abstract is available for this record.
Yepeng Ding, Hiroyuki Satō
Decentralized techniques are becoming crucial and ubiquitous with the rapid advancement of distributed ledger technologies such as the blockchain. Numerous decentralized systems have been developed to address security and privacy issues with great dependability and reliability via these techniques. Meanwhile, formalization and verification of the decentralized systems is the key to ensuring correctness of the design and security properties of the implementation. In this paper, we propose a novel method of formalizing and verifying decentralized systems with a kind of extended concurrent separation logic. Our logic extends the standard concurrent separation logic with new features including communication encapsulation, environment perception, and node-level reasoning, which enhances modularity and expressiveness. Besides, we develop our logic with unitarity and compatibility to facilitate implementation. Furthermore, we demonstrate the effectiveness and versatility of our method by applying our logic to formalize and verify critical techniques in decentralized systems including the consensus mechanism and the smart contract.
Richard Banach
No abstract is available for this record.
Jens Neureither, Alexandra Dmitrienko, David Koisser, Ferdinand Brasser · 5 authors
No abstract is available for this record.
Nikos Fotiou, Iakovos Pittaras, Vasilios A. Siris, Spyros Voulgaris · 5 authors
OAuth 2.0 is the industry-standard protocol for authorization. It facilitates secure service provisioning, as well as secure interoperability among diverse stakeholders. All OAuth 2.0 protocol flows result in the creation of an access token, which is then used by a user to request access to a protected resource. Nevertheless, the definition of access tokens is transparent to the OAuth 2.0 protocol, which does not specify any particular token format, how tokens are generated, or how they are used. Instead, the OAuth 2.0 specification leaves all these as design choices for integrators. In this paper, we propose a new type of OAuth 2.0 token backed by a distributed ledger. Our construction is secure, and it supports proof-of-possession, auditing, and accountability. Furthermore, we provide added-value token management services, including revocation, delegation, and fair exchange by leveraging smart contracts. We realized a proof-of-concept implementation of our solution using Ethereum smart contracts and the ERC-721 token specification.