WebAssembly (Wasm) is an increasingly deployed low-level language providing near-native performance to security-critical domains such as web browsers, smart contracts, and edge computing. In all of these domains, establishing the absence of bugs and security vulnerabilities is of utmost importance, which motivates the development of sound and automated static analysis techniques. This is, however, a challenging task since the Wasm formal semantics is not directly amenable to efficient static analysis, Wasm code is typically embedded in statically unknown and possibly malicious contexts, and the low-level nature of the language makes it hard to precisely and yet soundly capture memory management and other core features. In this work, we present Wappler, the first sound and automated static analysis technique for WebAssembly. The core idea is to encode the semantics into Horn clauses so as to make it accessible to automated theorem provers, such as z3. The realization of this approach, however, requires to tackle several challenges. We address the fact that the Wasm semantics is not directly amenable to automation of security proofs by introducing annotations that enable a precise, practical, and yet sound encoding. Furthermore, we devise a formalism to specify embedder behavior and introduce a sound yet precise memory abstraction. We demonstrate the expressiveness of our logical formalism by encoding several general as well as Wasm-specific security properties. Finally, we implement our static analysis technique and conduct an experimental evaluation over the official Wasm test suite to demonstrate its performance.

Ethereum has emerged as the most popular smart contract platform, with hundreds of thousands of contracts stored on the blockchain and covering diverse application scenarios, such as auctions, trading platforms, or elections. Given the financial nature of smart contracts, security vulnerabilities may lead to catastrophic consequences and, even worse, can hardly be fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging. This is as e.g., Ethereum's transaction-oriented programming mechanisms feature a subtle semantics, and since the blockchain data at execution time, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode, and a large-scale experimental evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 94% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.

Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We review the existing approaches to automated, sound, static analysis of Ethereum smart contracts and highlight prevalent issues in the state of the art. Finally, we overview eThor, a recent static analysis tool that we developed following a principled design and implementation approach based on rigorous semantic foundations to overcome the problems of past works