Table of contents

  • This session has been presented September 25, 2020.

Description

  • Speaker

    Aurélien Francillon (Eurecom)

In this talk I will discuss our recent work, together with Sebastian Poeplau, on Symbolic execution. Symbolic execution has become a popular technique for software testing and vulnerability detection, in particular, because it allows to generate test cases for difficult to reach program paths. However, a major impediment to practical symbolic execution is speed, especially when compared to near-native speed solutions like fuzz testing.We first discuss an extensive evaluation (published at ACSAC 2019) of the current symbolic execution tools (Angr, Klee, Qsym). Most implementations transform the program under analysis to some intermediate representation (IR), which is then used as a basis for symbolic execution. There is a multitude of available IRs, and even more approaches to transform target programs into a respective IR. Therefore, we developed a methodology for systematic comparison of different approaches to symbolic execution; we then use it to evaluate the impact of the choice of IR and IR generation.We will then present SYMCC: our compilation-based approach to symbolic execution. SymCC is an LLVM-based C and C++ compiler that builds concolic execution right into the binary and performs better than state-of-the-art implementations by orders of magnitude. It can be used by software developers as a drop-in replacement for clang and clang++. Using SymCC on real-world software, we found that SymCC consistently achieves higher coverage, and we discovered two vulnerabilities in the heavily tested OpenJPEG project, which have been confirmed by the project maintainers and assigned CVE identifiers.SymCC received a distinguished paper award at Usenix Security 2020.

Practical infos

Next sessions

  • [CANCELLED] Black-Box Collision Attacks on Widely Deployed Perceptual Hash Functions and Their Consequences

    • June 13, 2025 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Aurigny room

    Speaker : Diane Leblanc-Albarel - KU Leuven

    [CANCELLED] Perceptual hash functions identify multimedia content by mapping similar inputs to similar outputs. They are widely used for detecting copyright violations and illegal content but lack transparency, as their design details are typically kept secret. Governments are considering extending the application of these functions to Client-Side Scanning (CSS) for end-to-end encrypted services:[…]
    • Cryptography

    • SoSysec

    • Protocols

  • A non-comparison oblivious sort and its application to private k-NN

    • June 20, 2025 (11:00 - 12:00)

    • Inria Center of the University of Rennes - - Petri/Turing room

    Speaker : Sofiane Azogagh - UQÀM

    Sorting is a fundamental subroutine of many algorithms and as such has been studied for decades. A well-known result is the Lower Bound Theorem, which states that no comparison-based sorting algorithm can do better than O(nlog(n)) in the worst case. However, in the fifties, new sorting algorithms that do not rely on comparisons were introduced such as counting sort, which can run in linear time[…]
    • Cryptography

    • SoSysec

    • Privacy

    • Databases

    • Secure storage

Show previous sessions