skip to main content

Title: Securing Smart Contracts with Information Flow
Securing blockchain smart contracts is difficult, especially when they interact with one another. Existing tools for reasoning about smart contract security are limited in one of two ways: they either cannot analyze cooperative interaction between contracts, or they require all interacting code to be written in a specific language. We propose an approach based on information flow control~(IFC), which supports fine-grained, compositional security policies and rules out dangerous vulnerabilities. However, existing IFC systems provide few guarantees on interaction with legacy contracts and unknown code. We extend existing IFC constructs to support these important functionalities while retaining compositional security guarantees, including reentrancy control. We mix static and dynamic mechanisms to achieve these goals in a flexible manner while minimizing run-time costs.
; ; ;
Award ID(s):
Publication Date:
Journal Name:
International Symposium on Foundations and Applications of Blockchain
Sponsoring Org:
National Science Foundation
More Like this
  1. The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Information flow control has long been proposed as a way to achieve compositional security, offering strong guarantees even when combining software from different trust domains. Unfortunately, this appealing story breaks down in the presence of reentrancy attacks. We formalize a general definition of reentrancy and introduce a security condition that allows software modules like smart contracts to protect their key invariants while retaining the expressive power of safe forms of reentrancy. Wemore »present a security type system that provably enforces secure information flow; in conjunction with run-time mechanisms, it enforces secure reentrancy even in the presence of unknown code; and it helps locate and correct recent high-profile vulnerabilities.« less
  2. We present STORM, a web framework that allows developers to build MVC applications with compile-time enforcement of centrally specified data-dependent security policies. STORM ensures security using a Security Typed ORM that refines the (type) abstractions of each layer of the MVC API with logical assertions that describe the data produced and consumed by the underlying operation and the users allowed access to that data. To evaluate the security guarantees of STORM, we build a formally verified reference implementation using the Labeled IO (LIO) IFC framework. We present case studies and end-to- end applications that show how STORM lets developers specifymore »diverse policies while centralizing the trusted code to under 1% of the application, and statically enforces security with modest type annotation overhead, and no run-time cost.« less
  3. The smart city landscape is rife with opportunities for mobility and economic optimization, but also presents many security concerns spanning the range of components and systems in the smart ecosystem. One key enabler for this ecosystem is smart transportation and transit, which is foundationally built upon connected vehicles. Ensuring vehicular security, while necessary to guarantee passenger and pedestrian safety, is itself challenging due to the broad attack surfaces of modern automotive systems. A single car contains dozens to hundreds of small embedded computing devices known as electronic control units (ECUs) executing 100s of millions of lines of code; the inherentmore »complexity of this tightly-integrated cyber-physical system (CPS) is one of the key problems that frustrates effective security. We describe an approach to help reduce the complexity of security analyses by leveraging unsupervised machine learning to learn clusters of messages passed between ECUs that correlate with changes in the CPS state of a vehicle as it moves through the world. Our approach can help to improve the security of vehicles in a smart city, and can leverage smart city infrastructure to further enrich and refine the quality of the machine learning output.« less
  4. Due to the proliferation of IoT and the popularity of smart contracts mediated by blockchain, smart home systems have become capable of providing privacy and security to their occupants. In blockchain-based home automation systems, business logic is handled by smart contracts securely. However, a blockchain-based solution is inherently resource-intensive, making it unsuitable for resource-constrained IoT devices. Moreover, time-sensitive actions are complex to perform in a blockchainbased solution due to the time required to mine a block. In this work, we propose a blockchain-independent smart contract infrastructure suitable for resource-constrained IoT devices. Our proposed method is also capable of executing time-sensitivemore »business logic. As an example of an end-to-end application, we describe a smart camera system using our proposed method, compare this system with an existing blockchain-based solution, and present an empirical evaluation of their performance.« less
  5. Ethereum Smart Contracts, also known as Decentralized Applications (DApps), are small programs which orchestrate financial transactions. Though beneficial in many cases, such contracts can and have been exploited, leading to a history of financial losses in the millions of dollars for those who have invested in them. It is critical that users be able to trust the contract code they place their money into. One way for verifying a program’s integrity is Symbolic Execution. Unfortunately, while the information derived from symbolic execution is beneficial, performing it is often financially and technically infeasible for users to do. To address this problem,more »this paper describes the design and implementation of a registry of vulnerable Ethereum contracts. The registry compiles the results of exhaustive application of symbolic analysis to deployed contracts and makes it available to users seeking to understand the risks associated with contracts they are intending to utilize.« less