Symbolically Executing WebAssembly in Manticore

by Eric Hennenfent on January 31, 2020

With the release of Manticore 0.3.3, we’re proud to announce support for symbolically executing WebAssembly (WASM) binaries. WASM is a newly standardized programming language that allows web developers to run code with near-native performance directly within the browser. Manticore 0.3.3 can explore all reachable states in a WASM program, and derive the concrete inputs that produce a given state. Our goal with this feature is to provide a solid foundation for security analysis of WASM programs in the future.

Why WASM?

WASM is becoming an important part of the way software is written. It’s supported by all major web browsers and was recently accepted as a web standard. What’s more, it may help bridge the performance gap in web/native applications, and ease their development by allowing developers to work in familiar languages like C++ and Rust.

One exciting WASM development is the Bytecode Alliance: a proposal from Mozilla to restructure modern package management around small, well-verified WASM nanoprocesses that can be formally shown to have no significant security vulnerabilities. Symbolic execution is uniquely well suited to such problems because it’s designed to evaluate code under all possible conditions. And yet, until now, no significant strides have been made towards symbolically executing WebAssembly. To our knowledge, Manticore is the first actively-maintained symbolic execution engine to support WASM binaries.

Ethereum WASM (EWASM)

WASM is also poised to have a positive impact on our Ethereum smart contract analysis work. As part of the Ethereum 2.0 improvements, the Ethereum foundation plans to replace the Ethereum Virtual Machine (EVM) language with Ethereum-flavored WebAssembly (EWASM). EWASM will look somewhat different from regular WASM, but we think that having some experience developing WASM tools will make it easy to upgrade our existing EVM tools when the transition does take place.

Using WASM in Manticore

Let’s look at a classic example of a problem one might solve with symbolic execution. We’ll use Manticore to solve a simple crackme that’s been cross-compiled to WebAssembly.

Sponsorships Available

We start with the following C program. It reads in a single byte from stdin, then checks it against a concrete value. It does so bit by bit, so we can’t simply read the value from the source code. It also includes a branch counter that increments after each bit is checked so the return code will reflect how many of the leading bits matched the expected value. This also prevents the compiler from optimizing the nested if statements into a single comparison.

Figure 1: A C program that performs a bitwise comparison to a byte from stdin

Since this is just an example, you can probably figure out from the source code that the correct input byte is 0x58 (‘X’). Let’s compile this into WebAssembly using WASMFiddle, then put it into Manticore and see if it can find the same result.

First, we’ll import the Python modules we need to work with WASM:

Figure 2: Python import statements

Since WASM binaries are run within a browser, they don’t have access to the standard library in the same way that native binaries would. Instead, functions like getchar or printf would usually be provided in JavaScript by Emscripten or WASI. Here, we’ll provide a minimal symbolic implementation using the Manticore API:

Figure 3: Symbolic getchar implementation

Though the C program expects an 8-bit integer from getchar, the smallest WASM data type is a 32-bit integer. For this reason, instead of returning an 8-bit value, we return a 32-bit value and constrain it to be between 0 and 256.

We’ll also need a callback that runs upon state termination and checks whether we found the correct answer. We’ll use a Manticore plugin to do this:

Figure 4: Callback that identifies successful states

This callback checks if the value on top of the stack (the return value from main) is zero, and if so, solves for the concrete values of all the symbols in this state.

Finally, we’ll put everything together. We create a new Manticore instance and give it the name of our WASM module and our symbolic getchar implementation. We register the state termination callback, then tell Manticore to begin state exploration starting from the main method.

Figure 5: Python statements to run Manticore

Here’s the final script:

Figure 6: Manticore solution script

When we run this, we can see that Manticore correctly solves for the input byte:

Figure 7: Terminal output showing ‘X’ returning 0

Try it out

You can try out WASM support in Manticore right now by installing the 0.3.3 release from PyPi. WASM support is still in alpha, so please help us make it better by filing bug reports or suggestions as issues on our Github repository. The API may change slightly as we make usability improvements, but we’ll make sure the Github versions of the examples shown above stay up to date. One final thing to note: Manticore’s WASM module doesn’t currently support symbolic floating point semantics, and only has limited support for symbolic memory dereferences. These haven’t been a problem for us so far, but we’re working on them in order to make Manticore the best tool it can be.

We’re always developing ways to work faster and smarter. Need help with your next project? Contact us!