Low level code analysis and applications to computer security
NII Shonan Meeting:
@ Shonan Village Center, March 2-5, 2015
NII Shonan Meeting Report (ISSN 2186-7437):No.2015-4
- Jean-Yves Marion, Lorraine University, France
- Akira Mori, AIST, Japan
- Mizuhito Ogawa, JAIST, Japan
Description of the meeting
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.