Software security is one of the very major issues of modern societies, since insecure systems can affect people (phishing, unauthorized payment, etc.), organizations (critical information leakage) and even states (cyber attacks). In regard to software security, a crucial problem is to have methods and to devise tools to analyze low-level code for at least three reasons. First, low level codes are usually the one that is effectively run on a computer system. Low-level code is usually obtained by a compilation chain where some parts of the chain maybe unsecure. As a result it is necessary to guarantee low-level code correction ensuring that programs run by the system cannot be attacked. Second, a lot of applications are available on internet as binary codes. Those binary codes are quite obfuscated either to protect the intellectual property or because there are malicious software (malware). Therefore, it is necessary to have tools to analyze binary codes in order to detect malware and prevent an attack.

It may look surprising that such important issues are so poorly addressed by current state-of-the-technology tools, while formal methods in general and automatic program verification in particular have made tremendous progress in the past decade, resulting in many impressive industrial applications, and demonstrating their strength both in bug finding and safety validation. There are two key problems here.

First, security needs are more difficult to characterize (in terms amenable to automatic analysis) than safety needs. Security requirements change depending on the social context, and malicious behavior is not easy to define. For instance, malware often uses windows system calls for malicious behavior, but standard programs also use such capability. To clarify, not only theoretical observation form academia, but also empirical study in industry will be required.

Second, security analyses must often be performed at the level of binary executable. Malicious behavior is often based on very fine low-level details, invisible on the source code (e.g. memory layout, exception handling details, ambiguity in program semantics, bug in compilation), and malware are only available as executable files. This is a key difficulty, as most formal methods have been designed for high-level models or languages, and they rely on hypotheses that no longer hold at the executable code level. For instance, even (static) disassembly is not possible for recent advanced polymorphic virus, like self-decryption. Thus, model generation of binary executables is already a challenging.

The goal of the proposed meeting is to explore all aspects from theory to practice of low-level code analysis, including communication between industry and academia.
The main outcome of this meeting will be to trigger new interactions and enrich the various approaches. For instance,

• Security threat in practice. e.g., vulnerability, overflow attacks on x86 / Android. `
• Malware and botnet
• Static analysis of low level codes
• Obfuscated programs, e.g., self-modifying code, packers, and obfuscation techniques.
• Low level code semantics
• Model generation. e.g., control flow graph reconstruction, disassembly
• CEGAR (Counter example guided abstraction refinement) and loop invariant generation
• Testing and virtual binary emulation, dynamic analysis
• Backend reasoning tools. e.g., SMT (SAT modulo theory), Model checkers

By interacting industry and academia, and among different areas in academia, we will start to tackle the two key problems.

Analyzing security needs. Learn concrete examples from industrial experiences, and manual pattern analysis of malware behavior in malware database. They would lead clear formal definitions of target properties.

Binary executable analysis. Exchanging ideas of state-of-the-art research on binary executable analysis, and look for collaboration opportunity.