Order of Six Angles
4.68K subscribers
386 photos
27 videos
42 files
1.96K links
Х.Р.А.М Сатаны

www.orderofsixangles.com

Thatskriptkid
Download Telegram
Deus x64 is a series of increasingly difficult computer security challenges pertaining to reverse-engineering and binary exploitation.

deusx64.ai
Consider the following sample x86 assembly
code, with the assumption that byte in the AL register is
under attacker control:
0: add al, al
1: sub al, 0x0f
2: test al, al
3: jz 5
4: ...
5: jmp 7
6: ...
If we represent the input byte as b0, and create a new
variable bn on each write to a variable, then at address
6 the path condition for the byte in AL is the following
conjunction of clauses
b1 = b0 + b0 ∧ b2 = b1 − 15 ∧ b2 = 0
whereas at address 4 the path condition is
b1 = b0 + b0 ∧ b2 = b1 − 15 ∧ b2 6= 0
One can then use a SMT solver to ask queries about the
states represented by these formulae by appending con-
straints and looking for satisfying assignments. For ex-
ample, if we wanted to check at address 4 whether the
value 11 can be in the AL register we would create the
formula:
b1 = b0 + b0 ∧ b2 = b1 − 15 ∧ b2 6= 0 ∧ b2 = 11
An SMT solver will then return a satisfying assignment,
if one exists, such as b0 = 13 in this case.


Интересная тема, поиск rop gadget с помощью smt solvers и автоматическая генерация вредоносных шелкодов