An introduction to rune

What is symbolic execution?

Symbolic execution implies assumption of abstract symbolic values for variables to determine flow behaviour of the program.

This concept was put forth in a paper titled “Symbolic Execution and Program testing” by James C. King. Rather than using the data objects provided by the programming language for storing values, we use arbitrary symbolic values for computation. As can be noted, normal computation is a special case of symbolic execution wherein we provide concrete inputs for the values.

Current state of the art

Symbolic execution saw a rise in interest and research due to increase in CPU speed and the ability to execute things parallely. It is one of the very few ideas which has made it to the industry and practice, breaking out of the academic bubble.

Symbolic emulators try to reason about execution paths in a program, generating path equations and collecting constraints on symbolic variables assuming them to be abstract values. We have both source-based and binary-based engines being worked upon right now. Although both are equally interesting, binary analysis is probably more challenging.

EDIT: Some of the others I managed to miss are BAP, OpenREIL, BitBlaze, PANDA and S2E. The list above is not meant to be exhaustive at all.

rune

For radare2 to become a swiss-knife in a reverse engineer’s toolkit, it is missing a symbolic emulation engine. That’s where rune comes in!

The complete architecture and API design is attributed to our very own sushant94. Although in a very young stage, rune promises a flexible, modular structure and strives to extensible for security research. It is a symbolic emulator (engine) aimed at analysing parts of binaries for a better understanding of their execution semantics. rune can be used as a library for writing automated analysis and for manual debugging through an interactive console.

rune has several dependencies:

Overall architecture

rune

rune can be considered to be made up of multiple modules:

Usage

rune is written in Rust(duh!). You can use the rsoc branch for testing out my progress. It currently works with the fix branch of libsmt-rs(my fork) due to unmerged build-fixes.

Why not have a demo?!

asciicast

What does the future hold?

The future for rune does look promising! Apart from the ones discussed before, below are some of things I plan to work on in upcoming months:

That’s all from my side. I would like to thank all r2 devs to giving me this oppotunity to work on the project. Some of the concepts are new to me as well so I am learning as I go along. I would love to hear from everyone about what they think about some of the ideas I have proposed. Hope you had a fun read. I will post another update as soon as I finish implementing another milestone.

Till then, get a pro r2 license! ;)