skip to main content

Explore Research Products in the NSF-PAR

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.  more » « less
Award ID(s):
1704615
NSF-PAR ID:
10158698
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
International Symposium on Foundations and Applications of Blockchain
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ( , Proceedings of the IEEE Symposium on Security and Privacy)
    null (Ed.)
    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. We 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. 
    more » « less
  2. ( , 2023 7th International Conference on Medical and Health Informatics (ICMHI 2023))
    This paper presents a novel framework for creating a recoverable rare disease patient identity system using blockchain and smart contracts, decentralized identifiers (DIDs), and the InterPlanetary File System (IPFS). Smart contracts are executable code that can be written into decentralized storage such as blockchains in order to enable tamper-proof transactions of data. DIDs provide a secure, decentralized, and extensible way to create, store, and manage digital identities, while IPFS provides a distributed, immutable, and secure storage system for patient identities. Utilizing these technologies with smart contracts, we created a framework to store persistent medical records of patients. Smart contracts additionally allow account recovery without the use of any centralized authority. The framework enables healthcare providers to securely access a patient's data while maintaining the patient's ownership of their data. The paper explores the advantages of using a decentralized identity system and highlights the potential of this approach to improve the security and universality of medical records for patients with rare diseases. 
    more » « less
  3. ; ; ( , Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science, vol)
    Smart contracts are programs that run atop of a blockchain infrastructure. They have emerged as an important new programming model in cryptocurrencies like Ethereum, where they regulate flow of money and other digital assets according to user-defined rules. However, the most popular smart contract languages favor expressiveness rather than safety, and bugs in smart contracts have already lead to significant financial losses from accidents. Smart contracts are also appealing targets for hackers since they can be monetized. For these reasons, smart contracts are an appealing opportunity for systematic auditing and validation, and formal methods in particular. In this paper, we survey the existing smart-contract ecosystem and the existing tools for analyzing smart contracts. We then pose research challenges for formal-methods and program analysis applied to smart contracts. 
    more » « less
  4. ; ; ( , 2022 IEEE 7th European Symposium on Security and Privacy (EuroS&P))
    To prevent applications from leaking users' private data to attackers, researchers have developed runtime information flow control (IFC) mechanisms. Most existing approaches are either based on taint tracking or multi-execution, and the same technique is used to protect the entire application. However, today's applications are typically composed of multiple components from heterogenous and unequally trusted sources. The goal of this paper is to develop a framework to enable the flexible composition of IFC enforcement mechanisms. More concretely, we focus on reactive programs, which is an abstract model for event-driven programs including web and mobile applications. We formalize the semantics of existing IFC enforcement mechanisms with well-defined interfaces for composition, define knowledge-based security guarantees that can precisely quantify the effect of implicit leaks from taint tracking, and prove sound all composed systems that we instantiate the framework with. We identify requirements for future enforcement mechanisms to be securely composed in our framework. Finally, we implement a prototype in OCaml and compare the effects of different compositions. 
    more » « less
  5. ; ; ; ; ; ; ; ( , USENIX Symposium on Operating Systems Design and Implementation)
    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 specify 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. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email