I was @ SSPREW'19 to present our work regarding:

• the state-of-the-art in anti-DSE software protection (paper)
• preliminary results and observations concerning improved stochastic code deobfuscation.

It was the last SSPREW edition before the merger with the SPRO workshop, but it was a good one!

I enjoyed the workshop as usual, for its constructive purpose and nice people. There were 3 highlights to me:

• the Binary Ninja tutorial. This was my second introduction to this tool, and I must say this is just a superb tool, which is coded by nice guys as well.
• the talk about the Guard Lines memory protection, called Preventing Zero-Day Exploits of Memory Vulnerabilities with Guard Lines; and
• Yuan Gu's keynote about AI Security and Smart Asset Protection.

We will talk about how we use symbolic execution in BINSEC at USE'18 @ ICST'18.

Here are the slides of the presentation..

For more, this presentation is a mashup of different results obtained by our group during the last 2 years from the following articles.

• Backward-bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes. <br/> Robin David, Sébastien Bardin, Jean-Yves Marion. <br/> SP 2017.
• Finding the needle in the heap: combining static analysis and dynamic symbolic execution to trigger use-after-free.<br/> Josselin Feist, Laurent Mounier, Sébastien Bardin, Robin David, Marie-Laure Potet. <br/>SSPREW@ACSAC 2016.
• Recovering high-level conditions from binary programs. <br/>Adel Djoudi, Sébastien Bardin. <br/> FM 2016.
• BINSEC-SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis. <br/> Robin David, Sébastien Bardin, Thanh Dinh Ta, Laurent Mounier, Josselin Feist, Marie-Laure Potet, Jean-Yves Marion. <br/> SANER 2016
• Specification of Concretization and Symbolization Policies in Symbolic Execution. <br/> Robin David, Sébastien Bardin, Josselin Feist, Thanh Dinh Ta, Laurent Mounier, Marie-Laure Potet, Jean-Yves Marion. <br/>ISSTA 2016
• BINSEC: Binary Code Analysis with Low-Level Regions. <br/> Adel Djoudi, Sébastien Bardin. <br/>TACAS 2015.

There will be a BINSEC tutorial @ SSPREW-7.

The tutorial uses a virtual machine which contains a compiled development snapshot of BINSEC and some examples.

You can download it from ftp://ftp.cea.fr/incoming/y2k01/binsec_ssprew.ova (md5: 8d473d800b1fd2d3a2a929a51d1cb990).

• username : vagrant
• password : vagrant

The examples are found in the examples directory.

The above link will be active for 2 weeks only from November, 30.

Here are the slides.

In this post, we are interested in the basic disassembly abilities of BINSEC

In November 2012, a thread on the OCaml devel mailing list mentioned that using format strings, through either the Printf or Format modules, had a measurable performance impact. It even mentioned that using Format had some further performance penalties over Printf, e.g., regarding printing newlines.

I am particularly drawn to OCaml's format module since I find it one of the best not-very-well-known features of its compact standard library.

You might know that, since then, format strings handling has been changed and now uses GADT. In theory, this should have brought performance enhancements. So, in this post, I aim to revisit the performance question raised in 2012. It's 2017: what's the performance penalty of format strings over direct printing functions now in OCaml ?

We — my colleague Sébastien and I — are organizing the 8th International Summer School on Information Security and Protection.

For those of you interested in software protection in particular and in analyzing binary code in general, this is a great opportunity to meet some of the best academics and professionals of the domain.

For more information about ISSISP '17, the website is up and running there.

I will be @ RESSI to talk about BINSEC on behalf of all the group.

The Software Reliability Lab at CEA LIST (Paris Saclay, France) is offering postdoc positions about Software security through binary-level analysis.

Full description is here.