Introduction

BINSEC is a binary level code analysis platform developed at CEA List (Université Paris-Saclay) in collaboration with UGA and LORIA.

BINSEC takes as input a binary file containing machine code instructions and can perform symbolic execution ("under-approximated semantic exploration") over it.

This tutorial covers the basic usages of the BINSEC symbolic execution engine over small binary executables.

📄️ Reverse in a nutshell

What is inside a tiny ELF executable.

📄️ Symbolic execution in a nutshell

Get started with the symbolic execution engine.

📄️ Small Challenge

Solve a small challenge yourself.

📄️ Hooks and stubs

How to deal with foreign or complex code.

📄️ Second challenge

Yet another practice session.

📄️ Coredump initialization

How to start the exploration from a concrete state.

📄️ ISA Portfolio

Discover different architectures.