58 citations · 90 across the 9 of their papers we have counts for
11 papers
Schooling to Exploit Foolish Contracts
Tamer Abdelaziz, Aquinas Hobor
We introduce SCooLS, our Smart Contract Learning (Semi-supervised) engine. SCooLS uses neural networks to analyze Ethereum contract bytecode and identifies specific vulnerable func…
Usenix'23 Extended Version: Smart Learning to Find Dumb Contracts
Tamer Abdelaziz, Aquinas Hobor
We introduce the Deep Learning Vulnerability Analyzer (DLVA) for Ethereum smart contracts based on neural networks. We train DLVA to judge bytecode even though the supervising orac…
OverChain: Building a robust overlay with a blockchain
Vijeth Aradhya, Seth Gilbert, Aquinas Hobor
Blockchains use peer-to-peer networks for disseminating information among peers, but these networks currently do not have any provable guarantees for desirable properties such as B…
Complexity Analysis of Tree Share Structure
Xuan-Bach Le, Aquinas Hobor, Anthony W. Lin
The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are…
Proof Pearl: Magic Wand as Frame
Qinxiang Cao, Shengyi Wang, Aquinas Hobor +1
Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating…
Exploiting The Laws of Order in Smart Contracts
Aashish Kolluri, Ivica Nikolic, Ilya Sergey +2
We investigate a family of bugs in blockchain-based smart contracts, which we call event-ordering (or EO) bugs. These bugs are intimately related to the dynamic ordering of contrac…
BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof
Shweta Shinde, Shengyi Wang, Pinghai Yuan +3
New trusted computing primitives such as Intel SGX have shown the feasibility of running user-level applications in enclaves on a commodity trusted processor without trusting a lar…
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
Ivica Nikolic, Aashish Kolluri, Ilya Sergey +2
Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new s…
Scilla: a Smart Contract Intermediate-Level LAnguage
Ilya Sergey, Amrit Kumar, Aquinas Hobor
This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspe…
A Concurrent Perspective on Smart Contracts
Ilya Sergey, Aquinas Hobor
In this paper, we explore remarkable similarities between multi-transactional behaviors of smart contracts in cryptocurrencies such as Ethereum and classical problems of shared-mem…
Barriers in Concurrent Separation Logic: Now With Tool Support!
Aquinas Hobor, Cristian Gherghina
We develop and prove sound a concurrent separation logic for Pthreads-style barriers. Although Pthreads barriers are widely used in systems, and separation logic is widely used for…