Tamarin: Concolic Disequivalence for MIPS

TL;DR

Tamarin is a tool that uses alternating concolic execution to determine disequivalence between MIPS programs, effectively handling unstructured assembly code without prior knowledge.

Contribution

It introduces a novel concolic execution approach for MIPS programs and implements it in Tamarin, enabling automated disequivalence detection.

Findings

Successfully reasoned about program disequivalence in various scenarios

Operates without prior knowledge of the programs

Integrates with Z3 solver for symbolic analysis

Abstract

Given two MIPS programs, when are they equivalent? At first glance, this is tricky to define, because of the unstructured nature of assembly code. We propose the use of alternating concolic execution to detect whether two programs are disequivalent. We have implemented our approach in a tool called Tamarin, which includes a MIPS emulator instrumented to record symbolic traces, as well as a concolic execution engine that integrates with the Z3 solver. We show that Tamarin is able to reason about program disequivalence in a number of scenarios, without any a-priori knowledge about the MIPS programs under consideration.