Awesome
Description
1nsanity is a LLVM pass that obfuscates against symbolic execution. It includes mathematical obfuscation, bogus control flow injection, and tacks on additional complexity to switch cases and branch instructions. It also includes infinite loop traps along with the use of the Collatz Conjecture as an opaque predicate. Included are challenges solved with both Angr and Manticore along with solve times both before and after obfuscation. A variety of test cases were used ranging from basic ctf challenges to a simple unix shell.
Example
Simple C program
int main(){
int f = 986;
while (f != 1){
printf("%d\n", f);
if ((f & 1) == 1){
f *= 3;
f += 1;
}
else{
f /= 2;
}
}
return f;
}
Before Obfuscation
Binary Size: 8.0K
CFG in function main:
After Obfuscation:
Obfuscated Binary Size: 8.0K
CFG in function main:
Solve Times with Manticore:
Manticore Challenge
Solver for mant_chal.c
Size: 12K
=====NORMAL=====
real 0m43.738s
user 0m43.274s
sys 0m0.977s
=====NORMAL=====
Solver for obfuscated mant_chal.c
Size: 16K:
===OBFUSCATED=====
real 16m42.648s
user 16m34.412s
sys 0m22.461s
===OBFUSCATED=====
Solve Times with Angr:
Angr Challenge
Solver for recruit.c
Size: 12K
-----NORMAL------
real 1m17.714s
user 1m3.453s
sys 0m14.607s
-----NORMAL-------
Solver for obfuscated recruit.c
Size: 20K:
----OBFUSCATED----
real 10m34.944s
user 10m17.969s
sys 0m17.233s
----OBFUSCATED----
Further Work
The end goal of 1nsanity would be to cause state explosion in all symbolic execution engines. An idea I want to implement is detecting symbolic buffers, and looping over each byte and seeing if it satisfies some predicate, I know this is a bit vague, but I have some ideas as to how to accomplish this with the LLVM API. Currently 1nsanity outputs 32 bit executables. 64 bit executables may be outputted, but I need to fix the way I am detecting integer types in the LLVM Pass.