More Like this

1. Summary-Based Symbolic Evaluation for Smart Contracts

   Feng, Yu; Torlak, Emina; Bodik, Rastislav (January 2020, 35th IEEE/ACM International Conference on Automated Software Engineering (ASE ’20))

   null (Ed.)

   This paper presents Solar, a system for automatic synthesis of adversarial contracts that exploit vulnerabilities in a victim smart contract. To make the synthesis tractable, we introduce a query language as well as summary-based symbolic evaluation, which sig- nificantly reduces the number of instructions that our synthesizer needs to evaluate symbolically, without compromising the preci- sion of the vulnerability query. We encoded common vulnerabilities of smart contracts and evaluated Solar on the entire data set from Etherscan. Our experiments demonstrate the benefits of summary- based symbolic evaluation and show that Solar outperforms state- of-the-art smart contracts analyzers, teether, Mythril, and Con- tractFuzzer, in terms of running time and precision. 

   more » « less
2. SGXonerated: Finding (and Partially Fixing) Privacy Flaws in TEE-based Smart Contract Platforms Without Breaking the TEE

   https://doi.org/10.56553/popets-2024-0035  

   Jean-Louis, Nerla; Li, Yunqi; Ji, Yan; Malvai, Harjasleen; Yurek, Thomas; Bellemare, Sylvain; Miller, Andrew (January 2024, Proceedings on Privacy Enhancing Technologies)

   TEE-based smart contracts are an emerging blockchain architecture, offering fully programmable privacy with better performance than alternatives like secure multiparty computation. They can also support compatibility with existing smart contract languages, such that existing (plaintext) applications can be readily ported, picking up privacy enhancements automatically. While previous analysis of TEE-based smart contracts have focused on failures of TEE itself, we asked whether other aspects might be understudied. We focused on state consistency, a concern area highlighted by Li et al., as well as new concerns including access pattern leakage and software upgrade mechanisms. We carried out a code review of a cohort of four TEE-based smart contract platforms. These include Secret Network, the first to market with in-use applications, as well as Oasis, Phala, and Obscuro, which have at least released public test networks.The first and most broadly applicable result is that access pattern leakage occurs when handling persistent contract storage. On Secret Network, its fine-grained access pattern is catastrophic for the transaction privacy of SNIP-20 tokens. If ERC-20 tokens were naively ported to Oasis they would be similarly vulnerable; the others in the cohort leak coarse-grained information at approximately the page level (4 kilobytes). Improving and characterizing this will require adopting techniques from ORAMs or encrypted databases.Second, the importance of state consistency has been underappreciated, in part because exploiting such vulnerabilities is thought to be impractical. We show they are fully practical by building a proof-of-concept tool that breaks all advertised privacy properties of SNIP-20 tokens, able to query the balance of individual accounts and the token amount of each transfer. We additionally demonstrate MEV attacks against the Sienna Swap application. As a final consequence of lacking state consistency, the developers have inadvertently introduced a decryption backdoor through their software upgrade process. We have helped the Secret developers mitigate this through a coordinated vulnerability disclosure, after which their state consistency should be roughly on par with the rest. 

   more » « less
3. A Resource-Efficient Smart Contract for Privacy Preserving Smart Home Systems

   https://doi.org/10.1109/SWC50871.2021.00079  

   Saquib, Nazmus; Bakir, Fatih; Krintz, Chandra; Wolski, Rich (October 2021, IEEE SmartWorld)

   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-sensitive 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. 

   more » « less
4. Does blame shifting work?

   https://doi.org/10.1145/3371133  

   Lazarek, Lukas; King, Alexis; Sundar, Samanvitha; Findler, Robert_Bruce; Dimoulas, Christos (December 2019, Proceedings of the ACM on Programming Languages)

   Contract systems, especially of the higher-order flavor, go hand in hand with blame. The pragmatic purpose of blame is to narrow down the code that a programmer needs to examine to locate the bug when the contract system discovers a contract violation. Or so the literature on higher-order contracts claims. In reality, however, there is neither empirical nor theoretical evidence that connects blame with the location of bugs. The reputation of blame as a tool for weeding out bugs rests on anecdotes about how programmers use contracts to shift blame and their attention from one part of a program to another until they discover the source of the problem. This paper aims to fill the apparent gap and shed light to the relation between blame and bugs. To that end, we introduce an empirical methodology for investigating whether, for a given contract system, it is possible to translate blame information to the location of bugs in a systematic manner. Our methodology is inspired by how programmers attempt to increase the precision of the contracts of a blamed component in order to shift blame to another component, which becomes the next candidate for containing the bug. In particular, we construct a framework that enables us to ask for a contract system whether (i) the process of blame shifting causes blame to eventually settle to the component that contains the bug; and (ii) every shift moves blame ``closer'' to the faulty component. Our methodology offers a rigorous means for evaluating the pragmatics of contract systems, and we employ it to analyze Racket's contract system. Along the way, we uncover subtle points about the pragmatic meaning of contracts and blame in Racket: (i) the expressiveness of Racket's off-the-shelf contract language is not sufficient to narrow down the blamed portion of the code to the faulty component in all cases; and (ii) contracts that trigger state changes (even unexpectedly, perhaps in the runtime system's data structures or caches) interfere with program evaluation in subtle ways and thus blame shifting can lead programmers on a detour when searching for a bug. These points highlight how evaluations such as ours suggest fixes to language design. 

   more » « less
5. Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)

   https://doi.org/10.4230/LIPIcs.ECOOP.2025.42  

   Moy, Cameron; Jung, Ryan; Felleisen, Matthias (January 2025, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)

   Aldrich, Jonathan; Silva, Alexandra (Ed.)

   Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature. 

   more » « less