Michael N. Jones, Matthew Johnson, Mark Shervey, Joel T. Dudley · 5 authors
BACKGROUND: The protection of private data is a key responsibility for research studies that collect identifiable information from study participants. Limiting the scope of data collection and preventing secondary use of the data are effective strategies for managing these risks. An ideal framework for data collection would incorporate feature engineering, a process where secondary features are derived from sensitive raw data in a secure environment without a trusted third party. OBJECTIVE: This study aimed to compare current approaches based on how they maintain data privacy and the practicality of their implementations. These approaches include traditional approaches that rely on trusted third parties, and cryptographic, secure hardware, and blockchain-based techniques. METHODS: A set of properties were defined for evaluating each approach. A qualitative comparison was presented based on these properties. The evaluation of each approach was framed with a use case of sharing geolocation data for biomedical research. RESULTS: We found that approaches that rely on a trusted third party for preserving participant privacy do not provide sufficiently strong guarantees that sensitive data will not be exposed in modern data ecosystems. Cryptographic techniques incorporate strong privacy-preserving paradigms but are appropriate only for select use cases or are currently limited because of computational complexity. Blockchain smart contracts alone are insufficient to provide data privacy because transactional data are public. Trusted execution environments (TEEs) may have hardware vulnerabilities and lack visibility into how data are processed. Hybrid approaches combining blockchain and cryptographic techniques or blockchain and TEEs provide promising frameworks for privacy preservation. For reference, we provide a software implementation where users can privately share features of their geolocation data using the hybrid approach combining blockchain with TEEs as a supplement. CONCLUSIONS: Blockchain technology and smart contracts enable the development of new privacy-preserving feature engineering methods by obviating dependence on trusted parties and providing immutable, auditable data processing workflows. The overlap between blockchain and cryptographic techniques or blockchain and secure hardware technologies are promising fields for addressing important data privacy needs. Hybrid blockchain and TEE frameworks currently provide practical tools for implementing experimental privacy-preserving applications.
Patrick L. Chapman, Dianxiang Xu, Lin Deng, Yin Xiong
Blockchain in recent years has exploded in popularity with Ethereum being one of the leading blockchain platforms. Solidity is a widely used scripting language for creating smart contracts in Ethereum applications. Quality assurance in Solidity contracts is of critical importance because bugs or vulnerabilities can lead to a considerable loss of financial assets. However, it is unclear what level of quality assurance is provided in many of these applications. Mutation testing is the process of intentionally injecting faults into a target program and then running the provided test suite against the various injected faults. Mutation testing is used to evaluate the effectiveness of a test suite, measuring the test suiteâs capability of covering certain types of faults. This thesis presents Deviant, the first implementation of a mutation testing tool for Solidity smart contracts. Deviant implements mutation operators that cover the unique features of Solidity according to our constructed fault model, in addition to traditional mutation operators that exist for other programming languages. Deviant has been applied to five open-source Solidity projects: MetaCoin [30], MultiSigWallet [31], Alice [29], aragonOS [32], and OpenZeppelin [33]. Experimental results show that the provided test suites result in low mutation scores. These results indicate that the provided tests cannot ensure high-level assurance of code quality. Such evaluation results offer important guidelines for Solidity developers to implement more effective tests in order to deliver trustworthy code and reduce the risk of financial loss.
Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax.
Modern blockchain systems support creation of smart contracts -- stateful programs hosted and executed on a blockchain. Smart contracts hold and transfer significant amounts of digital currency which makes them an attractive target for security attacks. It has been shown that many contracts deployed to public ledgers contain security vulnerabilities. Moreover, the design of blockchain systems does not allow the code of the smart contract to be changed after it has been deployed to the system. Therefore, it is important to guarantee the correctness of smart contracts prior to their deployment. Formal verification is widely used to check smart contracts for correctness with respect to given specification. In this work we consider program synthesis techniques in which the specification is used to generate correct-by-construction programs. We focus on one of the special cases of program synthesis where programs are modeled with finite state machines (FSMs). We show how FSM synthesis can be applied to the problem of automatic smart contract generation. Several case studies of smart contracts are outlined: crowdfunding platform, blinded auction and a license contract. For each case study we specify the corresponding smart contract with a set of formulas in linear temporal logic (LTL) and use this specification together with test scenarios to synthesize a FSM model for that contract. These models are later used to generate executable Solidity code which can be directly used in a blockchain system.
Public blockchains in support of Smart Contracts (SC), like Ethereum enable everyone to represent scarce, valuable resources (like cryptocurrencies) as so-called tokens. Token issuing and management was the first blockchain use case. However, programming languages and runtime systems used in the current blockchains for their SCs lack a secure and straightforward way to implement and handle tokens. The unnecessary complexity in doing so can lead to erroneous implementation of tokens and applications built on top of these, including the loss or theft of tokens as it happened. The most known attack was "TheDAO" attack which led to the "loss" of tokens, valued at that time at approximately 60 M US Dollar. A better and secure token representation directly embedded into a SC runtime and SC programming language could prevent loss of tokens. Thus this paper presents an approach including parts of a programming language using it. The core of the model is to use opaque and substructural data types together with an onchain soundness checker to generically represent tokens securely as values similar to integers and booleans. Such opaque data types enforce that only a designated piece of code can create values of that type. The substructural data types allow arbitrary values to express scarcity by preventing the duplication and elimination of values. The on-chain soundness checker ensures that the deployed code does not violate guarantees given by the type system, which includes opaque and substructural data types.
The wide deployment of tokens for digital assets on top of Ethereum implies the need for powerful trading platforms. Vickrey auctions have been known to determine the real market price of items as bidders are motivated to submit their own monetary valuations without leaking their information to the competitors. Recent constructions have utilized various cryptographic protocols such as ZKP and MPC, however, these approaches either are partially privacy-preserving or require complex computations with several rounds. In this paper, we overcome these limits by presenting Trustee as a Vickrey auction on Ethereum which fully preserves bids' privacy at relatively much lower fees. Trustee consists of three components: a front-end smart contract deployed on Ethereum, an Intel SGX enclave, and a relay to redirect messages between them. Initially, the enclave generates an Ethereum account and ECDH key-pair. Subsequently, the relay publishes the account's address and ECDH public key on the smart contract. As a prerequisite, bidders are encouraged to verify the authenticity and security of Trustee by using the SGX remote attestation service. To participate in the auction, bidders utilize the ECDH public key to encrypt their bids and submit them to the smart contract. Once the bidding interval is closed, the relay retrieves the encrypted bids and feeds them to the enclave that autonomously generates a signed transaction indicating the auction winner. Finally, the relay submits the transaction to the smart contract which verifies the transaction's authenticity and the parameters' consistency before accepting the claimed auction winner. As part of our contributions, we have made a prototype for Trustee available on Github for the community to review and inspect it. Additionally, we analyze the security features of Trustee and report on the transactions' gas cost incurred on Trustee smart contract.
The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (representing the required actions on contracts), and execute them in some order. Once this sequence of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we propose a true concurrent model of smart contract execution. Based on this, we show how static analysis of smart contracts can be exploited to parallelize the execution of transactions.
Solidity is an object-oriented and high-level language for writing smart contracts that are used to execute, verify and enforce credible transactions on permissionless blockchains. In the last few years, analysis of smart contracts has raised considerable interest and numerous techniques have been proposed to check the presence of vulnerabilities in them. Current techniques lack traceability in source code and have widely differing work flows. There is no single unifying framework for analysis, instrumentation, optimisation and code generation of Solidity contracts. In this paper, we present SIF, a comprehensive framework for Solidity contract analysis, query, instrumentation, and code generation. SIF provides support for Solidity contract developers and testers to build source level techniques for analysis, understanding, diagnostics, optimisations and code generation. We show feasibility and applicability of the framework by building practical tools on top of it and running them on 1838 real smart contracts deployed on the Ethereum network.
Matthias Grundmann, Marc Leinweber, Hannes Hartenstein
We explore challenges of and present a concept for a decentralized payment service which is based on trusted execution environments. The system guarantees that users can always cash out their funds without depending on the cooperation of other network members, hence minimizing the trust required in other network members. We present an overview of the system, motivate key components for a secure architecture and provide a communication protocol. We prove that the payment service users can cash out their funds at any time without any dependence on other network members.
MichaĆ KrĂłl, Alberto Sonnino, Mustafa Al-Bassam, Argyrios G. Tasiopoulos · 6 authors
As cryptographic tokens and altcoins are increasingly being built to serve as utility tokens, the notion of useful work consensus protocols is becoming ever more important. With useful work consensus protocols, users get rewards after they have carried out some specific tasks useful for the network. While in some cases the proof of some utility or service can be provided, the majority of tasks are impossible to verify reliably. To deal with such cases, we design âProof-of-Prestigeâ (PoP)âa reward system that can run directly on Proof-of-Stake (PoS) blockchains or as a smart contract on top of Proof-of-Work (PoW) blockchains. PoP introduces âprestige,â which is a volatile resource that, in contrast to coins, regenerates over time. Prestige can be gained by performing useful work, spent when benefiting from services, and directly translates to users minting power. Our scheme allows us to reliably reward decentralized workers while keeping the system free for the end-users. PoP is resistant against Sybil and collusion attacks and can be used with a vast range of unverifiable tasks. We build a simulator to assess the cryptoeconomic behavior of the system and deploy a full prototype of a content dissemination platform rewarding its participants. We implement the blockchain component on both Ethereum (PoW) and Cosmos (PoS), provide a mobile application, and connect it with our scheme with a negligible memory footprint. Finally, we adapt a fair exchange protocol allowing us to atomically exchange files for rewards also in scenarios where not all the parties have Internet connectivity. Our evaluation shows that even for large Ethereum traces, PoP introduces sub-millisecond computational overhead for miners in Cosmos and less than 0.013$ smart contract invocation cost for users in Ethereum.
This paper describes Slither, a static analysis framework designed to provide rich information about Ethereum smart contracts. It works by converting Solidity smart contracts into an intermediate representation called SlithIR. SlithIR uses Static Single Assignment (SSA) form and a reduced instruction set to ease implementation of analyses while preserving semantic information that would be lost in transforming Solidity to bytecode. Slither allows for the application of commonly used program analysis techniques like dataflow and taint tracking. Our framework has four main use cases: (1) automated detection of vulnerabilities, (2) automated detection of code optimization opportunities, (3) improvement of the user's understanding of the contracts, and (4) assistance with code review. In this paper, we present an overview of Slither, detail the design of its intermediate representation, and evaluate its capabilities on real-world contracts. We show that Slither's bug detection is fast, accurate, and outperforms other static analysis tools at finding issues in Ethereum smart contracts in terms of speed, robustness, and balance of detection and false positives. We compared tools using a large dataset of smart contracts and manually reviewed results for 1000 of the most used contracts.
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that performs deductive verification on an Ethereum Blockchain application based on smart contracts, which are self-executing digital contracts. Blockchain systems manipulate cryptocurrency and transaction information. Therefore , if a bug occurs in the blockchain, serious consequences such as a loss of money can happen. Thus, the aim of this paper is to propose a language dedicated to deductive verification, called Why3, as a new language for writing formal and verified smart contracts, thereby avoiding attacks exploiting such contract execution vulnerabilities. We first write a Why3 smart contracts program; next we formulate specifications to be proved as absence of RunTime Error properties and functional properties, then we verify the behavior of the program using the Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, we give a set of generic mathematical statements that allows verifying functional properties suited to any type of smart contracts holding cryptocurrency, showing that Why3 can be a suitable language to write smart contracts. To illustrate our approach, we describe its application to a realistic industrial use case.
Franklin Schrans, Daniel Hails, Alexander Harkness, Sophia Drossopoulou · 5 authors
The Ethereum blockchain platform supports the execution of decentralised applications or smart contracts. These typically hold and transfer digital currency to other parties on the platform; however, they have been subject to numerous attacks due to the unintentional introduction of bugs. Over a billion dollars worth of currency has been stolen since its release in July 2015. As smart contracts cannot be updated after deployment, it is imperative that the programming language supports the development of robust contracts. We propose Flint, a new statically-typed programming language specifically designed for writing robust smart contracts. Flint's features enforce the writing of safe and predictable code. To encourage good practices, we introduce protection blocks. Protection blocks restrict who can run code and when (using typestate) it can be executed. To prevent vulnerabilities relating to the unintentional loss of currency, Flint Asset traits provide safe atomic operations, ensuring the state of contracts is always consistent. Writes to state are restricted, simplifying reasoning about smart contracts.
This paper describes a new but state-of-the-art approach to provide authenticity in mqtt sessions using the means of zero-knowledge-proofs. This approach completely voids session hijacking for the mqtt protocol and provides authenticity without the need for any network-security nor channel-security nor broker-based predefined ACLs. The presented approach does not require the broker to keep any secrets for session handling, what so ever. Moreover, it allows the clientID, which represents the identification for a session, to be publicly known. The presented approach allows completely anonymous but authentic sessions, hence the broker does not need any a priori knowledge of the client-party. As it is especially targeted for applications within the world of IoT, the presented approach is tuned to require only the minimum in extra power in terms of energy and space. The approach does not introduce any new concept, but simply fusions a state-of-the-art cryptographic zero knowledge proof of identity with the existing MQTT-5 specification. Thus no protocol extension is required in order to provide the targeted security properties. The described approach is completely agnostic to the application layer at the client side and is only required during mqtt-session establishment.
Summary We present an overview of hybrid Casper the Friendly Finality Gadget (FFG), a proofâofâstake checkpointing protocol overlaid onto Ethereum's proofâofâwork blockchain. We describe its core functionalities and reward scheme and explore its properties. Our findings indicate that Casper's implemented incentives mechanism ensures liveness, while providing safety guarantees that improve over standard proofâofâwork protocols. On the basis of a minimal impact implementation of the protocol as a smart contract on the blockchain, we discuss additional issues related to parametrization, funding, throughput, and network overhead and detect potential limitations.
This paper reports on the development of a formal symbolic process virtual machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security of Ethereum-based services at the source code level of smart contracts, and a Coq proof assistant is employed for both programming the system and for proving its correctness. The current version of FSPVM-E adopts execution-verification isomorphism, which is an application extension of Curry-Howard isomorphism, as its fundamental theoretical framework to combine symbolic execution and higher-order logic theorem proving. The four primary components of FSPVM-E include a general, extensible, and reusable formal memory framework, an extensible and universal formal intermediate programming language denoted as Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, the corresponding formally verified interpreter of Lolisa, denoted as FEther, and assistant tools and libraries. The self-correctness of all components is certified in Coq. Currently, FSPVM-E supports the ERC20 token standard, and can automatically and symbolically execute Ethereum-based smart contracts, scan their standard vulnerabilities, and verify their reliability and security properties with Hoare-style logic in Coq. To the best of authors' knowledge, the present work represents the first hybrid formal verification system implemented in Coq for Ethereum smart contracts that is applied at the Solidity source code level.
In the last year we have seen a great deal of both academic and practical
interest in the topic of vulnerabilities in smart contracts, particularly those
developed for the Ethereum blockchain. In this paper we survey the 21,270
vulnerable contracts reported by six recent academic projects. Contrary to what
might have been believed given the reported number of vulnerable contracts,
there has been precious little in terms of actual exploitation when it comes to
these vulnerabilities. We find that at most 504 out of 21,270 contracts have
been subjected to exploits. This corresponds to at most 9,066 ETH (~1.8 million
USD), or only 0.29% of the 3 million ETH (600 million USD) claimed in some of
the papers. While we are certainly not implying that smart contract
vulnerability research is without merit, our results suggest that the potential
impact of vulnerable code had been greatly exaggerated.
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning · 5 authors
Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and enforce protocols, Nomos is based on shared binary session types. To control resource usage, Nomos employs automatic amortized resource analysis. To prevent the duplication or deletion of assets, Nomos uses a linear type system. A monad integrates the effectful session-typed language with a general-purpose functional language. Nomos' prototype implementation features linear-time type checking and efficient type reconstruction that includes automatic inference of resource bounds via off-the-shelf linear optimization. The effectiveness of the language is evaluated with case studies about implementing common smart contracts such as auctions, elections, and currencies. Nomos is completely formalized, including the type system, a cost semantics, and a transactional semantics to instantiate Nomos contracts on a blockchain. The type soundness proof ensures that protocols are followed at run-time and that types establish sound upper bounds on the resource consumption, ruling out re-entrancy and out-of-gas vulnerabilities.
We propose a framework for threshold cryptosystems under a permissionless-economic model in which the participants are rational profit-maximizing entities. To date, threshold cryptosystems have been considered under permissioned settings with a limited adversary. Our framework relies on an escrow service that slashes and redistributes deposits to incentivize participants to adhere desired behaviors. Today, more than ever, sophisticated escrow services can be implemented over public blockchains like Ethereum, without additional trust assumptions. The key threat to rational threshold cryptosystems is collusion---by cooperating `illegally', a subset of participants can reveal the cryptosystem's secret, which, in turn is translated to unfair profit. Our countermeasure to collusion is framing. If the escrow is notified of collusion, it rewards the framer and slashes the deposits of all other participants. We show that colluding parties find themselves in the prisoner's dilemma, where the dominant strategy is framing.
Blockchain frameworks enable the immutable storage of data. A still open practical question is the so called "oracle" problem, i.e. the way how real world data is actually transferred into and out of a blockchain while preserving its integrity. We present a case study that demonstrates how to use an existing industrial strength secure element for cryptographic software protection (Wibu CmDongle / the "dongle") to function as such a hardware-based oracle for the Hyperledger blockchain framework. Our scenario is that of a dentist having leased a 3D printer. This printer is initially supplied with an amount of x printing units. With each print action the local unit counter on the attached dongle is decreased and in parallel a unit counter is maintained in the Hyperledger-based blockchain. Once a threshold is met, the printer will stop working (by means of the cryptographically protected invocation of the local print method). The blockchain is configured in such a way that chaincode is executed to increase the units again automatically (and essentially trigger any payment processes). Once this has happened, the new unit counter value will be passed from the blockchain to the local dongle and thus allow for further execution of print jobs.
Trusted Execution Environments (TEEs), such as Intel SGX enclaves, use hardware to ensure the confidentiality and integrity of operations on sensitive data. While the technology is available on many processors, the complexity of its programming model and its performance overhead have limited adoption. TEEs provide a new and valuable hardware functionality that has no obvious analogue in programming languages, which means that developers must manually partition their application into trusted and untrusted components. This paper describes an approach that fully integrates trusted execution into a language. We extend the Go language to allow a programmer to execute a goroutine within an enclave, to use low-overhead channels to communicate between the trusted and untrusted environments, and to rely on a compiler to automatically extract the secure code and data. Our prototype compiler and runtime, GOTEE, is a backward-compatible fork of the Go compiler. The evaluation shows that our compiler-driven code and data partitioning efficiently executes both microbenchmarks and applications. On the former, GOTEE achieves a 5.2Ăthroughput and a 2.3Ă latency improvement over the Intel SGX SDK. Our case studies, a Go ssh server, the Go tls package, and a secured keystore inspired by the go-ethereum project, demonstrate that minor source-code modifications suffice to provide confidentiality and integrity guarantees with only moderate performance overheads.
Open access
Security and Verification in Computing
Advanced Malware Detection Techniques
Physical Unclonable Functions (PUFs) and Hardware Security