Software Security from ⊤ to ⊥

Introduction This blog post is a quick brain-dump of the work that I was doing during my last month in the Dependable Systems Lab at EPFL. At the time I was working on malware analysis with S2E. While not anything earth-shatteringly novel, I’m hopeful that this post will help others who want to use symbolic execution/S2E to analyse malware behaviour. What makes malware analysis different? My previous blog posts have looked at solving a CTF challenge and analysing file parsers.

Continue reading 

Introduction Recently I’ve been playing around with file parsers in S2E. This typically involves calling s2ecmd symbfile to make the parser’s input symbolic and then running S2E to explore different paths through the parser. However, this is a relatively heavy-handed approach; it makes the entire input file one big symbolic blob, which quickly causes path explosion. Additionally, we may only be interested in exploring paths that exercise specific functionality. So how can we achieve more targeted symbolic execution on file-based programs such as parsers?

Continue reading 

Introduction Symbolic execution tools such as Angr and Manticore have become increasingly popular for analyzing binaries in Capture the Flag (CTF) challenges. In this blog post I will show that we can do the same with S2E, using it to solve a reverse engineering challenge from the 2016 Google CTF. This post walks through the process of writing an S2E plugin “from first principles” to solve this challenge. For comparison, solutions for the challenge using Angr and Manticore are also available.

Continue reading 