|23 August||Monday||0900-17:00 SGT/GMT+8||8 Hours|
|24 August||Tuesday||0900-17:00 SGT/GMT+8||8 Hours|
|25 August||Wednesday||0900-17:00 SGT/GMT+8||8 Hours|
In this training, we get to know state-of-the-art code obfuscation techniques and have a look at how these complicate reverse engineering. Afterwards, we gradually become familiar with different deobfuscation techniques and use them to break obfuscation schemes in hands-on sessions. Thereby, participants will deepen their knowledge of program analysis and learn when and how (not) to use different techniques.
First, we have a look at important code obfuscation techniques and discuss how to attack them. Afterwards, we analyze a virtual machine-based (VM-based) obfuscation scheme, learn VM hardening techniques and see how to deal with them.
In the second part, we cover SMT-based program analysis. In detail, students learn how to solve program analysis problems with SMT solvers, how to prove characteristics of code, how to deobfuscate mixed Boolean-Arithmetic and how to break weak cryptography.
Before we use symbolic execution to automate large parts of code deobfuscation, we first introduce intermediate languages and compiler optimizations to simplify industrial-grade obfuscation schemes. Following, we use symbolic execution to automate SMT-based program analysis and break opaque predicates.
The last part covers program synthesis, an approach that learns the code’s semantics based on its input-output behavior. We explore how to collect input-output pairs; then, we use program synthesis to deobfuscate mixed Boolean-Arithmetic and learn the semantics of VM instruction handlers.
- motivation - application scenarios - program analysis techniques
- opaque predicates - control-flow flattening - mixed Boolean-Arithmetic - virtual machines - virtual machine hardening
- compiler optimizations - reconstructing control flow - SMT-based program analysis - taint analysis - symbolic execution - program synthesis
- dead code elimination - constant propagation/folding - static single assignment (SSA) - optimizing obfuscated code
- SAT and SMT solvers - encoding programs analysis problems for SMT solvers - proving semantic equivalence - proving properties of a piece of code - solving complex program constraints - deobfuscating mixed Boolean-Arithmetic - breaking weak cryptography
- intermediate languages for reverse engineering - symbolic and semantic simplification of obfuscated code - automation in reverse engineering - deobfuscating VM-based obfuscation schemes - interaction with SMT solvers - breaking opaque predicates
- concept of program synthesis - learning code semantics based on its input/output behavior - obtaining input/output pairs from code - deobfuscating mixed Boolean-Arithmetic - learning semantics of VM instruction handlers