Overview

Static analysis techniques have proved their effectiveness at enforcing safety and security properties for source code. For binary code, there are many remaining challenges. The workshop aims at promoting the development of static analysis techniques for low-level code. We propose an exciting program with invited speakers with industrial and academic background. The workshop has as its aims to present the latest research results in security analysis of low-level code and to discuss scientific challenges relevant for the SAS community.

Invited Speakers

  • Thanassis Avgerinos , ForallSecure, USA
    Thanassis Avgerinos grew up in Athens, Greece, where he received his undergraduate degree in Electrical and Computer Engineering from the National Technical University of Athens. In 2009, he moved to Pittsburgh, USA to pursue a PhD in software security and binary program analysis from Carnegie Mellon University. In 2014, after defending his thesis on exploiting tradeoffs in symbolic execution, he started working at ForAllSecure - a startup company he founded with David Brumley and Alexandre Rebert - with the goal of bringing academic research ideas and binary analysis tools into practice.
  • Roberto Giacobazzi , Università degli Studi di Verona, Italy and IMDEA Software Institute, Spain
    Roberto Giacobazzi received the Laurea degree in Computer Science in 1988 from the University of Pisa, and in 1993 he received the Ph.D. in Computer Science from the same university. From 1993 to 1995 he had a Post Doctoral Research position at Laboratoire d'Informatique (LIX), Ecole Polytechnique (Paris) in the equipe Cousot. From 1995 to 1998 he was (tenured) Assistant Professor in Computer Science at the University of Pisa. From May 2000 until now he is Full Professor in Computer Science at the University of Verona. The research interests of Roberto Giacobazzi include abstract interpretation, static program analysis, semantics of programming languages, program verification, abstract model-checking, program transformation and optimization, digital asset protection, code obfuscation, malware detection, software watermarking and lattice theory. He has been Program Chair of SAS, VMCAI, of workshops in programming languages and language based security, and General Chair of ACM POPL2013. He is currently in the Steering committee of SAS and ACM POPL. From 2006 to 2012 he has been Dean of the College of Science of the University of Verona. He is now in his sabbatical year at IMDEA Software Institute. Before he was at University of Louisiana, Irdeto Canada and University of Melbourne.
  • Johannes Kinder , Royal Holloway, University of London, United Kingdom
    Johannes Kinder is a Lecturer (Assistant Professor) in the Department of Computer Science at Royal Holloway, University of London. His research interests lie at the intersection of programming languages, software engineering, systems, and security and are focused on methods for automatically assessing and improving the reliability and security of software. Johannes holds a doctorate in computer science from TU Darmstadt, a Diplom degree from TU Munich, and he completed a postdoc at EPFL in Lausanne.
  • Andy King , University of Kent, UK
    Andy King is a professor of program analysis in the School of Computing at the University of Kent. He is head of the Programming Language and Systems research group. His past work has been in program analysis of logic programming languages, though in recent years he has work on numeric abstract domains, the synthesis of transfer functions for binary programs and, most recently, computer security.
  • Jean-Yves Marion, Université de Lorraine, France
    ean-Yves Marion is professor of computer science at Université de Lorraine in Nancy on the north-east side of France, member of the Institut Universitaire de France (IUF). He is the head of the high security lab (HSL) and also the head of the computer science department of his university. His research covers computer viruses. An objective of his research is to develop new tools to analyse malware, to identity functionality inside binary codes, and to classify malware. Recently, he has worked extensively on the disassembling process of self-moidfying x86-codes.
  • Marcos Orallo, Airbus Group
    Marcos Orallo joined Airbus Group CERT mid-2014, after working for more than 8 years inside public regional and national Computer Emergency Response Teams. His responsibilities have been diverse, ranging from digital forensics and incident response to tool design and implementation. He is a strong supporter of standards, exchange and collaboration within the infosec community. One of his main interests has always been malware analysis, and especially its automation.
  • Frank Piessens, Katholieke Universiteit Leuven, België
    Frank Piessens is a professor in the Department of Computer Science at the Katholieke Universiteit Leuven, Belgium. His research field is software security, where he focuses on the development of high-assurance techniques to deal with implementation-level software vulnerabilities and bugs, including techniques such as software verification, run-time monitoring, type systems and programming language design. He studies the theory behind these techniques as well as their application in many types of software systems, including web applications, embedded software, and mobile applications.
  • Fred Raynal, Quarkslab, France
    Fred Raynal, PhD, is the founder and CEO of QUARKSLAB. Previously, he worked 3 years at EADS, including working as a core member of EADS IW, then created the SOGETI ESEC R&D (lab) team he managed for 5 years. He also is founder of the french conference SSTIC and magazine MISC. Beside "founding", he enjoys both technical hacking, information warfare and finding ways to combine both in order to find different (and hopefully better) ways to do information security.

Title and abstract

  • Title: Exploiting Trade-offs in Symbolic Execution for Identifying Security Bugs
    Speaker: Thanassis Avgerinos

    Over the past 20 years, our society has become increasingly dependent on software. Today, we rely on software for our financial transactions, our work, our communications, even our social contacts. A single software flaw is enough to cause irreparable damage, and as our reliance on software increases, so does our need for developing systematic techniques that check the software we use for critical vulnerabilities.

    In this talk, we investigate trade-offs in symbolic execution for identifying security-critical bugs. In the first part of the talk, we present symbolic execution systems capable of demonstrating control flow hijacks on real-world programs both at the source, and binary level. By exploiting specific trade-offs in symbolic execution, such as state pruning and careful state modeling, we show how to increase the efficacy of vanilla symbolic execution in identifying exploitable bugs.

    In the second part of the talk, we investigate veritesting, a symbolic execution technique for exploiting the trade-off between formula expressivity and number of program states. Our experiments on a large number of programs, show that veritesting finds more bugs, obtains higher node and path coverage, and can cover a fixed number of paths faster when compared to vanilla symbolic execution. Using veritesting, we have checked more than 33,248 Debian binaries, and found more than 11,687 bugs. Our results have had real world impact with 202 bug fixes already present in the latest version of Debian.

  • Title: Reflective Abstract Interpretation
    Speaker: Roberto Giacobazzi

    Reflection happens when programs employ primitives that allow to turn text as executable code at run-time. This makes standard static analysis extremely hard if not impossible because its essential data structures, such as the control-flow graph and the system of recursive equations associated with the program to analyse, are themselves dynamically mutating objects. We introduce the concept of reflective abstract interpretation for a simple imperative dynamic language manipulating strings. The code dynamically built at run-time is statically approximated in an abstract domain of (abstract) symbolic automata, and operations on these strings are specified as symbolic transducers. We introduce the properties of transduction of abstract symbolic automata that allow soundness and completeness of the abstract interpretation of code structures. The resulting abstract interpreter combines the analysis of standard data types (e.g., integers) with the analysis of strings for approx- imating dynamically created code structures. We show how this model may be adapted to the analysis of self-mutating binary code and show an example analysis for preventing cross site scripting attacks.

  • Title: ASAP: High System-Code Security with Low Overhead
    Speaker: Johannes Kinder

    Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like memory accesses. Alas, the induced slowdown usually exceeds by a wide margin what system users are willing to tolerate in production, so these tools are hardly ever used. As a result, the insecurity of real-world systems persists. We present an approach in which developers/operators can specify what level of overhead they find acceptable for a given workload (e.g., 5%); our proposed tool ASAP then automatically instruments the program to maximize its security while staying within the specified " overhead budget." Two insights make this approach effective: most overhead in existing tools is due to only a few " hot " checks, whereas the checks most useful to security are typically " cold " and cheap.

    We evaluate ASAP on programs from the Phoronix and SPEC benchmark suites. It can precisely select the best points in the security-performance spectrum. Moreover, we analyzed existing bugs and security vulnerabilities in RIPE, OpenSSL, and the Python interpreter, and found that the protection level offered by the ASAP approach is sufficient to protect against all of them.

  • Title: The Yin and Yang of Binary Reversing
    Speaker: Andy King

  • Title: Morphological analysis : where are we ?
    Speaker: Jean-Yves Marion

  • Title: Malware analysis from the trenches
    Speaker: Marcos Orallo

  • Title: Sound modular verification of code running in an untrusted binary code context
    Speaker: Frank Piessens

    Modular verification techniques verify a software module M by relying on specifications for the modules that M depends on. Properties verified of M will only hold under the assumption that the modules that M depends on also satisfy their specifications. This assumption is fragile if some of these modules are binary code modules. We propose an approach to harden the binary code of a module by defensive compilation and run time contract checking, such that verified safety and security properties of a module provably hold at run time under minimal assumptions.

  • Title: Real life challenges of source and binary analysis
    Speaker: Fred Raynal

Program

Tuesday, September, 8, 2015

9:00--10:30 Malware analysis

Coffee break

11:00-12:30 Binary analysis: challenge and practice

Lunch break

14:00-15:30 Static analysis

  • Andy King: The Yin and Yang of Binary Reversing
  • Roberto Giacobazzi: Reflective Abstract Interpretation

Coffee break

16:00-17:30 Safe execution


Organising committee