Home
  Organization
  Call for Papers
  Speakers
  Training
  Accepted Papers
  Workshop Program
  Sponsors
  Past Workshops
 






Hilton Orlando Lake Buena Vista, Orlando, FL, USA
December 4-5, 2017
Collocated with ACSAC 2017

Training Sessions

The first day of the SSPREW offers the following training sessions:

Tutorial Slides (ZIP)


Breaking Obfuscated Programs with Symbolic Execution

Presenter: Sebastian Banescu, Technical University of Munich
This tutorial will cover why it is important that an obfuscated program be resilient against symbolic execution attacks. One or two free obfuscation tools such as Tigress and OLLVM will be used to obfuscate C programs. The tutorial will show how naively employing obfuscation transformations can lead to programs which are easy to break using symbolic execution tools such as KLEE, angr or Triton. Finally, the talk will cover how to carefully choose the right obfuscation transformations to significantly raise the bar against symbolic execution.

Virtual machine download: https://hub.docker.com/r/banescusebi/obfuscation-symex/

BINSEC: A Framework for Binary-level Program Analysis

Presenters: Sébastien Bardin and Richard Bonichon, CEA, Saclay, Paris Area, France
Binary-level security analysis, such as malware comprehension or vulnerability detection, are both crucial and challenging. We present in this tutorial the BINSEC framweork, which incorporate the latest advances in low-level program analysis and provide new techniques and tools to reason about binary code at the semantic level.

Virtual machine download: https://rbonichon.github.io/posts/ssprew-17/

Concolic Analysis

Presenter: Vivek Notani, University of Verona
Concolic analysis is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution (testing on particular inputs) path. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs (test cases) with the aim of maximizing code coverage. Symbolic and concolic execution find important applications in a number of security-related program analyses, including analysis of malicious code.