ReverseEngineering
قسمت سی و چهارم بافر اورفلو Dynamic Taint Analysis دنبال کردن داده در زمان اجرای واقعی برنامه تا اینجا بیشتر از روی Assembly و ساختار برنامه مسیر داده رو بررسی کردیم یعنی برنامه رو اجرا نکردیم و سعی کردیم از روی کد بفهمیم داده ممکنه از کجا وارد بشه و به…
We see the same actual path
But here we have a problem
Dynamic Analysis does not see everything
Suppose the program looks like this
Input
↓
if (condition)
↓
Path B
If the condition is not met
Path B
will not be executed at all
But here we have a problem
Dynamic Analysis does not see everything
Suppose the program looks like this
Input
↓
if (condition)
↓
Path B
If the condition is not met
Path B
will not be executed at all
Therefore, dynamic analysis cannot provide information about an unexecuted path with the same level of certainty as it does for an executed one.
For this reason, these two methods are generally more valuable when used together:
Static Analysis
+
Dynamic Analysis
Static
Helps us understand what paths and dependencies might exist.
Dynamic
Helps us understand what actually happened during a
specific execution.
Tools
There are various tools and frameworks available for Dynamic Binary Analysis and Taint Tracking:
Intel Pin
DynamoRIO
Triton
angr
PANDA
However, we shouldn't assume all these tools do exactly the same thing; their instrumentation models and capabilities differ.
For example:
Triton
Offers features like Taint Analysis and Symbolic Execution for Dynamic Binary Analysis.
Connection to Fuzzing
This is where it gets interesting.
Previously, we had:
Fuzzer
↓
Interesting Input
↓
Crash
Now, we can use Dynamic Taint Analysis to examine the data path.
For example:
Interesting Input
↓
Tainted Data
↓
Parser
↓
Variable
↓
Memory Operation
↓
Crash
So, we don't just say the program crashed;
we can also trace the path the input data took during execution and identify where it contributed to the issue.
Static + Dynamic
A logical analysis workflow might look like this:
Fuzzing
↓
Crash
↓
Crash Triage
↓
Static Analysis
↓
Find Source / Sink
↓
Dynamic Analysis
↓
Trace Data
↓
Root Cause
Here, we gradually move from a simple crash to a better understanding of the path that caused the bug.
Dynamic Taint Analysis
Means tracking specific data or data dependencies during the actual execution of the program.
Key concepts:
Source
↓
Taint
↓
Propagation
↓
Register / Memory ↓
Control Flow
↓
Sink
An important point is that static analysis and dynamic analysis are not rivals.
Static analysis
primarily answers this question:
What possible paths might exist?
Dynamic analysis
primarily answers this question:
What path was actually taken during this specific execution?
When we combine these two with fuzzing and crash analysis,
we can trace a path from
Crash
to
Input
↓
Data Flow
↓
Instruction
↓
Memory Operation
↓
Crash
↓
Root Cause
And this is precisely the point where analyzing a crash shifts from observing a simple event to understanding the bug's root cause.
@reverseengine
For this reason, these two methods are generally more valuable when used together:
Static Analysis
+
Dynamic Analysis
Static
Helps us understand what paths and dependencies might exist.
Dynamic
Helps us understand what actually happened during a
specific execution.
Tools
There are various tools and frameworks available for Dynamic Binary Analysis and Taint Tracking:
Intel Pin
DynamoRIO
Triton
angr
PANDA
However, we shouldn't assume all these tools do exactly the same thing; their instrumentation models and capabilities differ.
For example:
Triton
Offers features like Taint Analysis and Symbolic Execution for Dynamic Binary Analysis.
Connection to Fuzzing
This is where it gets interesting.
Previously, we had:
Fuzzer
↓
Interesting Input
↓
Crash
Now, we can use Dynamic Taint Analysis to examine the data path.
For example:
Interesting Input
↓
Tainted Data
↓
Parser
↓
Variable
↓
Memory Operation
↓
Crash
So, we don't just say the program crashed;
we can also trace the path the input data took during execution and identify where it contributed to the issue.
Static + Dynamic
A logical analysis workflow might look like this:
Fuzzing
↓
Crash
↓
Crash Triage
↓
Static Analysis
↓
Find Source / Sink
↓
Dynamic Analysis
↓
Trace Data
↓
Root Cause
Here, we gradually move from a simple crash to a better understanding of the path that caused the bug.
Dynamic Taint Analysis
Means tracking specific data or data dependencies during the actual execution of the program.
Key concepts:
Source
↓
Taint
↓
Propagation
↓
Register / Memory ↓
Control Flow
↓
Sink
An important point is that static analysis and dynamic analysis are not rivals.
Static analysis
primarily answers this question:
What possible paths might exist?
Dynamic analysis
primarily answers this question:
What path was actually taken during this specific execution?
When we combine these two with fuzzing and crash analysis,
we can trace a path from
Crash
to
Input
↓
Data Flow
↓
Instruction
↓
Memory Operation
↓
Crash
↓
Root Cause
And this is precisely the point where analyzing a crash shifts from observing a simple event to understanding the bug's root cause.
@reverseengine
Pointer Aliasing
تا اینجا فهمیدیم داده میتونه از Register بره داخل Memory و دوباره از طریق Pointer برگرده
حالا یک مشکل مهم تر داریم
ممکنه دو Pointer مختلف به یک قسمت از Memory اشاره کنن
مثلا:
int value = 100;
int *p = &value;
int *q = &value;
اینجا p و q دو Pointer مختلف هستن
ولی هر دو به یک Memory اشاره میکنن
value
|
0x5000
/ \
/ \
p q
پس اگر این کار رو انجام بدیم
*p = 200;
مقدار value تغییر میکنه
و وقتی بعدا این رو بخونیم
printf("%d", *q);
مقدار 200 رو میبینیم
چون p و q در واقع به یک محل اشاره میکنن
به این وضعیت میگیم
Pointer Aliasing
این موضوع برای Reverse Engineering خیلی مهمه
چون ممکنه داخل یک تابع ببینید
mov [rax], 200
و چند خط پایین تر ببینید
mov ecx, [rbx]
در نگاه اول ممکنه فکر کنید این دو دستور هیچ ارتباطی ندارن
ولی اگر
RAX = 0x5000
RBX = 0x5000
باشه
هر دو دارن با یک Memory مشترک کار میکنن
RAX ─────┐
↓
0x5000
↑
|
RBX ─────┘
پس تغییر از طریق RAX میتونه مستقیما روی چیزی که از طریق RBX خونده میشه اثر بذاره
اینجا Data Flow دیگه فقط بین Register ها نیست
باید رابطه Pointer ها و Memory Address ها رو هم دنبال کنید
یک مثال ساده تر
int value = 10;
int *p = &value;
int *q = p;
*p = 50;
int x = *q;
مسیر واقعی داده
value
↓
p
↓
q
↓
Memory
↓
50
↓
x
اما از نظر Address
p ──┐
├──> value
q ──┘
پس p و q دو مسیر متفاوت برای رسیدن به یک داده هستن
در Reverse Engineering
وقتی با Pointerها کار میکنید فقط نپرسد
این Pointer کجاست؟
باید بپرسید
این Pointer به کجا اشاره میکنه؟
چه Pointer های دیگه ای ممکنه به همین Address اشاره کنن؟
چه کسی مقدار اون Memory رو تغییر داده؟
چه کسی بعدا اون مقدار رو خونده؟
این سوال‌ها کمک میکنن ارتباط هایی رو پیدا کنی که از روی Control Flow معمولی مشخص نیستن
تمرین:
این کد رو بررسی کنید
int value = 10;
int *p = &value;
int *q = p;
*p = 100;
int result = *q;
مسیر Data Flow رو رسم کنید
value
↓
p
↓
q
↓
*p = 100
↓
*q
↓
result
بعد مشخص کن چرا result برابر 100 میشه
در مرحله بعد میریم سراغ یک موضوع مهم‌تر
Memory Aliasing
در توابع مختلف
اونجا دیگه دو Pointer داخل یک تابع نداریم
یک تابع Memory رو تغییر میده و یک تابع دیگه از طریق Pointer متفاوت همون Memory رو میخونه
و دقیقا همینجا تحلیل Data Flow در باینری های واقعی شروع میکنه به دردسر درست کردن
@reverseengine
تا اینجا فهمیدیم داده میتونه از Register بره داخل Memory و دوباره از طریق Pointer برگرده
حالا یک مشکل مهم تر داریم
ممکنه دو Pointer مختلف به یک قسمت از Memory اشاره کنن
مثلا:
int value = 100;
int *p = &value;
int *q = &value;
اینجا p و q دو Pointer مختلف هستن
ولی هر دو به یک Memory اشاره میکنن
value
|
0x5000
/ \
/ \
p q
پس اگر این کار رو انجام بدیم
*p = 200;
مقدار value تغییر میکنه
و وقتی بعدا این رو بخونیم
printf("%d", *q);
مقدار 200 رو میبینیم
چون p و q در واقع به یک محل اشاره میکنن
به این وضعیت میگیم
Pointer Aliasing
این موضوع برای Reverse Engineering خیلی مهمه
چون ممکنه داخل یک تابع ببینید
mov [rax], 200
و چند خط پایین تر ببینید
mov ecx, [rbx]
در نگاه اول ممکنه فکر کنید این دو دستور هیچ ارتباطی ندارن
ولی اگر
RAX = 0x5000
RBX = 0x5000
باشه
هر دو دارن با یک Memory مشترک کار میکنن
RAX ─────┐
↓
0x5000
↑
|
RBX ─────┘
پس تغییر از طریق RAX میتونه مستقیما روی چیزی که از طریق RBX خونده میشه اثر بذاره
اینجا Data Flow دیگه فقط بین Register ها نیست
باید رابطه Pointer ها و Memory Address ها رو هم دنبال کنید
یک مثال ساده تر
int value = 10;
int *p = &value;
int *q = p;
*p = 50;
int x = *q;
مسیر واقعی داده
value
↓
p
↓
q
↓
Memory
↓
50
↓
x
اما از نظر Address
p ──┐
├──> value
q ──┘
پس p و q دو مسیر متفاوت برای رسیدن به یک داده هستن
در Reverse Engineering
وقتی با Pointerها کار میکنید فقط نپرسد
این Pointer کجاست؟
باید بپرسید
این Pointer به کجا اشاره میکنه؟
چه Pointer های دیگه ای ممکنه به همین Address اشاره کنن؟
چه کسی مقدار اون Memory رو تغییر داده؟
چه کسی بعدا اون مقدار رو خونده؟
این سوال‌ها کمک میکنن ارتباط هایی رو پیدا کنی که از روی Control Flow معمولی مشخص نیستن
تمرین:
این کد رو بررسی کنید
int value = 10;
int *p = &value;
int *q = p;
*p = 100;
int result = *q;
مسیر Data Flow رو رسم کنید
value
↓
p
↓
q
↓
*p = 100
↓
*q
↓
result
بعد مشخص کن چرا result برابر 100 میشه
در مرحله بعد میریم سراغ یک موضوع مهم‌تر
Memory Aliasing
در توابع مختلف
اونجا دیگه دو Pointer داخل یک تابع نداریم
یک تابع Memory رو تغییر میده و یک تابع دیگه از طریق Pointer متفاوت همون Memory رو میخونه
و دقیقا همینجا تحلیل Data Flow در باینری های واقعی شروع میکنه به دردسر درست کردن
@reverseengine
ReverseEngineering
Pointer Aliasing تا اینجا فهمیدیم داده میتونه از Register بره داخل Memory و دوباره از طریق Pointer برگرده حالا یک مشکل مهم تر داریم ممکنه دو Pointer مختلف به یک قسمت از Memory اشاره کنن مثلا: int value = 100; int *p = &value; int *q = &value; اینجا p…
Pointer Aliasing
So far we have understood that data can go from Register to Memory and back again through Pointer
Now we have a more important problem
Two different Pointers may point to the same part of Memory
For example:
int value = 100;
int *p = &value;
int *q = &value;
Here p and q are two different Pointers
But both point to the same Memory
value
|
0x5000
/ \
/ \
p q
So if we do this
*p = 200;
the value of value will change
And when we read this later
printf("%d", *q);
We see the value 200
Because p and q actually point to the same location
We call this situation
Pointer Aliasing
This is very important for Reverse Engineering
Because you might see inside a function
mov [rax], 200
And a few lines down
mov ecx, [rbx]
At first glance you might think these two instructions have nothing to do
But if
RAX = 0x5000
RBX = 0x5000
Well
They are both working with the same memory
RAX ─────┐
↓
0x5000
↑
|
RBX ─────┘
So a change through RAX can directly affect what is read through RBX
Here the Data Flow is not just between Registers
You should also follow the relationship between Pointers and Memory Addresses
A simpler example
int value = 10;
int *p = &value;
int *q = p;
*p = 50;
int x = *q;
Actual data path
value
↓
p
↓
q
↓
Memory
↓
50
↓
x
But in terms of Address
p ──┐
├──> value
q ──┘
So p and q are two different paths to reach the same data
In Reverse Engineering
When working with Pointers, don't just ask
Where is this Pointer?
You should ask
Where does this Pointer point to?
What other Pointers might point to the same Address?
Who changed the value of that Memory?
Who later read that value?
These questions help you find connections that are not obvious from normal Control Flow
Exercise:
Examine this code
int value = 10;
int *p = &value;
int *q = p;
*p = 100;
int result = *q;
Draw the Data Flow path
value
↓
p
↓
q
↓
*p = 100
↓
*q
↓
result
Then determine why result is equal to 100
Next, we will move on to a more important topic
Memory Aliasing
In different functions
There we no longer have two pointers inside a function
One function modifies the Memory and another function reads the same Memory through a different Pointer
And this is exactly where Data Flow analysis in real binaries starts to cause trouble
@reverseengine
So far we have understood that data can go from Register to Memory and back again through Pointer
Now we have a more important problem
Two different Pointers may point to the same part of Memory
For example:
int value = 100;
int *p = &value;
int *q = &value;
Here p and q are two different Pointers
But both point to the same Memory
value
|
0x5000
/ \
/ \
p q
So if we do this
*p = 200;
the value of value will change
And when we read this later
printf("%d", *q);
We see the value 200
Because p and q actually point to the same location
We call this situation
Pointer Aliasing
This is very important for Reverse Engineering
Because you might see inside a function
mov [rax], 200
And a few lines down
mov ecx, [rbx]
At first glance you might think these two instructions have nothing to do
But if
RAX = 0x5000
RBX = 0x5000
Well
They are both working with the same memory
RAX ─────┐
↓
0x5000
↑
|
RBX ─────┘
So a change through RAX can directly affect what is read through RBX
Here the Data Flow is not just between Registers
You should also follow the relationship between Pointers and Memory Addresses
A simpler example
int value = 10;
int *p = &value;
int *q = p;
*p = 50;
int x = *q;
Actual data path
value
↓
p
↓
q
↓
Memory
↓
50
↓
x
But in terms of Address
p ──┐
├──> value
q ──┘
So p and q are two different paths to reach the same data
In Reverse Engineering
When working with Pointers, don't just ask
Where is this Pointer?
You should ask
Where does this Pointer point to?
What other Pointers might point to the same Address?
Who changed the value of that Memory?
Who later read that value?
These questions help you find connections that are not obvious from normal Control Flow
Exercise:
Examine this code
int value = 10;
int *p = &value;
int *q = p;
*p = 100;
int result = *q;
Draw the Data Flow path
value
↓
p
↓
q
↓
*p = 100
↓
*q
↓
result
Then determine why result is equal to 100
Next, we will move on to a more important topic
Memory Aliasing
In different functions
There we no longer have two pointers inside a function
One function modifies the Memory and another function reads the same Memory through a different Pointer
And this is exactly where Data Flow analysis in real binaries starts to cause trouble
@reverseengine
_assembly-language-for-x86-processors-8-ed.pdf
11.5 MB
Assembly Language for x86 Processors
_security_automation_with_python_practical_python_solutions_for.pdf
40 MB
Security Automation with Python
From BlackCat to Panda Workshop: Inside the Evolving C2 Panel Behind RATHat
https://www.cleafy.com/cleafy-labs/from-blackcat-to-panda-workshop-inside-the-evolving-c2-panel-behind-rathat
@reverseengine
https://www.cleafy.com/cleafy-labs/from-blackcat-to-panda-workshop-inside-the-evolving-c2-panel-behind-rathat
@reverseengine
Cleafy
From BlackCat to Panda Workshop: Inside the Evolving C2 Panel Behind RATHat | Cleafy
Cleafy's TIR team analyzed the operator infrastructure behind RATHat, an Android banking trojan that abuses Accessibility Services to enable wireless debugging on the victim's phone, obtain a shell, and deploy a hidden native service outside the app. The…
NeedyMantis: Unpacking a post-compromise malware family used in targeted operations
https://microsoft.com/en-us/security/blog/2026/09/28/needymantis-unpacking-a-post-compromise-malware-family-used-in-targeted-operations
@reverseengine
https://microsoft.com/en-us/security/blog/2026/09/28/needymantis-unpacking-a-post-compromise-malware-family-used-in-targeted-operations
@reverseengine
Microsoft News
NeedyMantis: Unpacking a post-compromise malware family used in targeted operations
Microsoft Threat Intelligence identified NeedyMantis, a modular post-compromise malware framework used in targeted intrusions that combines custom loaders, encrypted archives, and extensible components to maintain long-term access and support follow-on operations.
An AI-Assisted Cyber Attack: Inside a Unit 42 Investigation
injecting backdoor in to terraform
https://unit42.paloaltonetworks.com/ai-assisted-cyber-attack-inside-a-unit-42-investigation
@reverseengine
injecting backdoor in to terraform
https://unit42.paloaltonetworks.com/ai-assisted-cyber-attack-inside-a-unit-42-investigation
@reverseengine
Unit 42
An AI-Assisted Cyber Attack: Inside a Unit 42 Investigation
Using autonomous AI agents, an attacker breached an enterprise network in a matter of hours. Understand how to address and defend against agentic attacks.
exploit_reversing_10_ios.pdf
25.5 MB
Exploiting Reversing (ER) series, Article 10:
iOS Security Research (part 01), Sep 2026.
Opens a multi-part sequence on iOS, and the first article in the series aimed at iOS itself rather than macOS. It first sets out the stack a kernel chain must cross in sequence - KASLR, Pointer Authentication, kalloc_type segregation with zone_require assertions, PPL and its successors SPTM at GL2 and TXM at GL0, Exclaves and trust-cache code signing - and why each layer pushes exploitation further toward data-only technique
iOS Security Research (part 01), Sep 2026.
Opens a multi-part sequence on iOS, and the first article in the series aimed at iOS itself rather than macOS. It first sets out the stack a kernel chain must cross in sequence - KASLR, Pointer Authentication, kalloc_type segregation with zone_require assertions, PPL and its successors SPTM at GL2 and TXM at GL0, Exclaves and trust-cache code signing - and why each layer pushes exploitation further toward data-only technique
From BlackCat to Panda Workshop: Inside the Evolving C2 Panel Behind RATHat
https://www.cleafy.com/cleafy-labs/from-blackcat-to-panda-workshop-inside-the-evolving-c2-panel-behind-rathat
https://www.cleafy.com/cleafy-labs/from-blackcat-to-panda-workshop-inside-the-evolving-c2-panel-behind-rathat
Cleafy
From BlackCat to Panda Workshop: Inside the Evolving C2 Panel Behind RATHat | Cleafy
Cleafy's TIR team analyzed the operator infrastructure behind RATHat, an Android banking trojan that abuses Accessibility Services to enable wireless debugging on the victim's phone, obtain a shell, and deploy a hidden native service outside the app. The…
FortiBleed Is Still Active, Now Locking Orgs Out
https://socradar.io/blog/fortibleed-still-active-locking-organizations-out/
https://socradar.io/blog/fortibleed-still-active-locking-organizations-out/
SOCRadar® Cyber Intelligence Inc.
FortiBleed Is Still Active, Locking Organizations Out
On October 6, 2026, the FBI and the U.S. Secret Service published a joint Cybersecurity Advisory on FortiBleed, the active global credential compromise,,,
Threat Actors Abuse Trusted Software Lures and Cloudflare Tunnels to Deploy ScreenConnect RMM Agents Across Windows and macOSScreenConnect RMM Agents Across Windows and macOS
Analyzing SMOKE#SCREEN:
https://www.securonix.com/blog/smoke-screen-screenconnect-rmm-abuse-cloudflare-tunnels/
Analyzing SMOKE#SCREEN:
https://www.securonix.com/blog/smoke-screen-screenconnect-rmm-abuse-cloudflare-tunnels/
Securonix
SMOKE#SCREEN: ScreenConnect RMM Abuse, Cloudflare Tunnels, and Trusted Software Lures
Securonix Threat Research: Analyze the SMOKE#SCREEN campaign abusing ScreenConnect RMM, Cloudflare Tunnels, and trusted software lures to gain persistent access across Windows and macOS.
Cursor 0day: When Full Disclosure Becomes the Only Protection Left
https://mindgard.ai/blog/cursor-0day-when-full-disclosure-becomes-the-only-protection-left
https://mindgard.ai/blog/cursor-0day-when-full-disclosure-becomes-the-only-protection-left
mindgard.ai
Cursor 0day: When Full Disclosure Becomes the Only Protection Left - Mindgard
The vulnerability nobody seems interested in fixing
Bluetooth Headphone Jacking: Full Disclosure of Airoha RACE Vulnerabilities
https://insinuator.net/2025/12/bluetooth-headphone-jacking-full-disclosure-of-airoha-race-vulnerabilities/
https://insinuator.net/2025/12/bluetooth-headphone-jacking-full-disclosure-of-airoha-race-vulnerabilities/
قسمت سی و چهارم بافر اورفلو
Symbolic Execution
از ورودی واقعی تا ورودی نماد ها
تا اینجا یاد گرفتیم چطور داده رو داخل برنامه دنبال کنیم و بفهمیم چطور به یک Crash میرسه
حالا میخوایم یک قدم جلوتر بریم
فرض کنید یک برنامه شرطی داره که فقط وقتی ورودی مقدار خاصی داشته باشه وارد یک مسیر مشخص میشه
میتونیم هزاران ورودی مختلف امتحان کنیم تا بالاخره به اون مسیر برسیم
ولی راه بهتری هم وجود داره
به جای اینکه فقط مقدارهای واقعی رو امتحان کنیم میتونیم از Symbolic Execution استفاده کنیم تا بفهمیم چه شرط هایی باید برقرار باشن تا برنامه وارد مسیر موردنظر بشه
اینجا به جای حدس زدن ورودی‌ها سعی میکنیم محدودیت های مسیر رو استخراج کنیم و اون‌ها رو حل کنیم
ایده اصلی چیه
فرض کنید برنامه اینه
C
int check(int x)
{
if (x == 1337)
return 1;
return 0;
}
در اجرای معمولی ممکنه این مقدار رو به برنامه بدیم
x = 10
برنامه شرط رو بررسی میکنه
10 == 1337
نتیجه غلطه و برنامه وارد مسیر دوم میشه
حالا فرض کن به جای مقدار واقعی از یک مقدار نمادین استفاده کنیم
x = X
در این حالت شرط برنامه میشه
X == 1337
حل کننده میتونه نتیجه بگیره که برای ورود به مسیر اول باید مقدار
X برابر 1337 باشهپس به جای امتحان کردن مقدارهای مختلف میتونیم شرط لازم برای رسیدن به مسیر رو به دست بیاریم
Path Constraint
فرض کنید این کد رو داریم
C
int process(int x)
{
if (x > 10)
{
if (x < 20)
return 1;
}
return 0;
}
برای رسیدن به
return 1 باید هر دو شرط برقرار باشنx > 10
AND
x < 20
به مجموعه شرط‌هایی که برای رسیدن به یک مسیر مشخص باید برقرار باشن میگیم
Path Constraint
پس محدودیت مسیر موردنظر اینه
10 < x < 20
چون
x از نوع int هست جواب‌های ممکن شامل این مقدارها میشن11, 12, 13, 14, 15, 16, 17, 18, 19
حل کننده میتونه یکی از جواب‌های معتبر رو پیدا کنه
مثلا:
x = 15
نکته مهم اینه که Symbolic Execution فقط شرط فعلی رو در نظر نمیگیره
بلکه شرطهای قبلی مسیر رو هم نگه میداره
چون برای رسیدن به یک نقطه از برنامه باید تمام شرطهای لازم در مسیر برقرار باشن
وقتی مسیرها چند شاخه میشن
این برنامه رو ببینید
C
int process(int x)
{
if (x > 10)
return 1;
if (x == 5)
return 2;
return 0;
}
از دید Symbolic Execution میتونیم مسیرهای مختلف برنامه رو بررسی کنیم
x = X
|
x > 10 ?
/ \
Yes No
| |
return 1 x == 5 ?
/ \
Yes No
| |
return 2 return 0
حالا فرض کنید میخوایم به
return 2 برسیماول باید شرط اول برقرار نباشه
X <= 10
بعد باید شرط دوم برقرار باشه
X == 5
پس Path Constraint ما میشه
X <= 10
AND
X == 5
در نتیجه
X = 5
یک ورودی معتبر برای رسیدن به این مسیر محسوب میشه
این همون ایده اصلی Symbolic Execution هست
برنامه رو دنبال میکنیم و برای هر مسیر شرطهای لازم رو جمع میکنیم
نقش SMT Solver
خب تا اینجا فهمیدیم که میتونیم شرطهای مسیر رو استخراج کنیم ولی وقتی تعداد شرطها زیاد بشه حل کردن اون‌ها با دست سخت میشه
اینجا از ابزاری به اسم
SMT Solver
استفاده میکنیم
یکی از ابزارهای شناخته‌شده در این زمینه
Z3
هست که توسط Microsoft Research توسعه داده شده
فرض کنید شرطهای ما اینا باشن
X > 10
X < 20
X != 15
حل کننده باید مقداری پیدا کنه که تموم شرط ها رو همزمان برقرار کنه
مثلا:
X = 11
این مقدار معتبره چون هر سه شرط رو برقرار میکنه
ولی اگر شرطها این باشن
X > 20
X < 10
هیچ مقدار حقیقی نمی‌تونه هر دو شرط رو همزمان برقرار کنه
در نتیجه مسئله
Unsatisfiable
هست
یعنی جواب معتبری وجود نداره
در مقابل اگر حداقل یک جواب وجود داشته باشه مسئله
Satisfiable
محسوب میشه
البته SMT Solver فقط برای شرطهای ساده عددی نیست
بسته به منطق و قابلیت های حل کننده میتونه محدودیت‌های مربوط به Bit Vectorها و عملیات بیتی رو هم بررسی کنه
این موضوع برای تحلیل باینری ها خیلی مهمه چون پردازنده با مقدارهایی با اندازه مشخص مثل 8 و 32 و 64 بیت کار میکنه و رفتار اون‌ها همیشه مثل اعداد صحیح ریاضی نیست
ارتباط Symbolic Execution با Reverse Engineering
فرض کنید یک باینری دارید و داخلش چنین منطقی وجود داره
C++
int validate(int value)
{
if (value < 100)
return 0;
if (value > 200)
return 0;
if (value == 150)
return 1;
C
return 0;
}
با تحلیل معمولی میفهمیم برنامه چند شرط داره
ولی Symbolic Execution میتونه شرطهای لازم برای رسیدن به مسیر موفق رو استخراج کنه
value >= 100
AND
value <= 200
AND
value == 150
در نتیجه
value = 150
یک جواب معتبره
این قابلیت در Reverse Engineering کاربردهای مهمی داره
تحلیل منطق اعتبارسنجی
پیدا کردن ورودی های لازم برای رسیدن به یک مسیر مشخص
بررسی شرطهای پیچیده داخل باینری
تحلیل مسیر های منتهی به Crash
و بررسی اینکه چه محدودیت هایی باعث میشن یک مسیر قابل دسترسی یا غیرقابل دسترسی باشه
البته در باینری واقعی ممکنه شرطها به چند تابع مختلف وابسته باشن یا تحت تأثیر حافظه و وضعیت Runtime قرار بگیرن
در این شرایط ساختن مدل دقیق برنامه سخت‌تر میشه
تفاوت Symbolic و Concrete Execution
این تفاوت رو خوب یاد بگیرید
Concrete Execution
برنامه با مقدار واقعی اجرا میشه
x = 15
در این حالت پردازش برنامه بر اساس مقدار واقعی
Symbolic Execution
به جای مقدار واقعی از یک مقدار نمادین استفاده میکنیم
x = X
وقت رسیدن به شرط ها محدودیت هایی روی
مقایسه ساده
یک نکته مهم
Symbolic Execution
تضمین نمیکنه تمام مسیرهای برنامه رو بررسی کنه
حلقه‌ها و تعداد زیاد شاخه ها میتونن باعث ترکیدن مسیرها بشن😁
محاسبات پیچیده و تعامل با سیستم عامل یا کتابخونه های خارجی هم ممکنه تحلیل رو دشوار کنن
پس حتی Symbolic Execution هم محدودیت‌های خودش رو داره
ارتباط با Fuzzing
اینجا Symbolic Execution به یکی از کاربردهای جذابش میرسه
فرض کنید Fuzzer یک ورودی تولید کرده و برنامه رو اجرا کرده
Input
↓
Program
↓
Branch A
↓
Branch B
↓
Crash
حالا میخوایم مسیر جدیدی رو بررسی کنیم که به خاطر برقرار نشدن یک شرط بهش نرسیدیم
مثلا برنامه چنین شرطی داره
Javascript
if (x == 1337)
dangerous_function();
اگر ورودی فعلی ما این باشه
x = 10
برنامه وارد
Symbolic Execution
میتونه شرط شاخه رو استخراج کنه
X == 1337
بعد حل کننده یک مقدار معتبر پیشنهاد میده
X = 1337
این مقدار رو میشه به عنوان ورودی جدید در فرآیند تست استفاده کرد
پس ارتباط کلی میشه
Fuzzer
↓
Input
↓
Program Execution
↓
Uncovered Branch
↓
Path Constraint
↓
SMT Solver
↓
New Input
↓
Fuzzing Again
این ایده در روش‌هایی مثل Concolic Execution هم استفاده میشه
در Concolic Execution برنامه با ورودی های واقعی اجرا میشه ولی همزمان مقادیر و شرطها به شکل نمادین هم دنبال میشن به این ترتیب اجرای واقعی و تحلیل نمادین در کنار هم قرار میگیرن
ابزارهای کاربردی
برای آشنایی عملی با این مبحث چند ابزار ارزش بررسی دارن
angr
یک Framework برای تحلیل باینری که قابلیت‌هایی مثل Symbolic Execution و تحلیل مسیر داره
مخزن رسمی:
https://github.com/angr/angr
Triton
یک Framework برای Dynamic Binary Analysis که قابلیت‌هایی مثل Taint Analysis و Symbolic Execution ارائه میده
مخزن رسمی:
https://github.com/JonathanSalwan/Triton
Z3
یک SMT Solver که میتونه محدودیت‌های نمادین رو حل کنه
مخزن رسمی:
https://github.com/Z3Prover/z3
این ابزارها دقیقا یک کار رو انجام نمیدن
angr
بیشتر برای ساختن و تحلیل مسیرهای نمادین در باینری کاربرد داره
Triton
قابلیت‌های تحلیل پویای باینری و محاسبات نمادین رو فراهم میکنه
Z3
هم حل کننده محدودیت هاست و به تنهایی یک ابزار کامل برای تحلیل مسیرهای اجرایی باینری محسوب نمیشه
مسیر کلی
Symbolic Execution این شکلیه
Symbolic Input
↓
Program Analysis
↓
Branch Conditions
↓
Path Constraints
↓
SMT Solver
↓
Possible Input
در قسمت‌های قبلی یاد گرفتیم داده از کجا وارد برنامه میشه و چطور در Register ها و Memory حرکت میکنه
حالا یاد گرفتیم چطور شرطهای اجرای برنامه رو تحلیل کنیم تا بفهمیم چه ورودی هایی میتونن به یک مسیر خاص برسن
وقتی این مفاهیم رو کنار هم قرار بدیم
Fuzzing
↓
Interesting Input
↓
Dynamic Taint Analysis
↓
Data Flow
↓
Symbolic Execution
↓
Path Constraints
↓
New Input
↓
Crash Analysis
↓
Root Cause
دیگه فقط به اجرای برنامه و دیدن Crash اکتفا نمیکنیم میتونیم مسیر داده رو دنبال کنیم شرطهای لازم رو بفهمیم و برای بررسی مسیر های جدید ورودی های هدفمند تری بسازیم
@reverseengine
return 0;
}
با تحلیل معمولی میفهمیم برنامه چند شرط داره
ولی Symbolic Execution میتونه شرطهای لازم برای رسیدن به مسیر موفق رو استخراج کنه
value >= 100
AND
value <= 200
AND
value == 150
در نتیجه
value = 150
یک جواب معتبره
این قابلیت در Reverse Engineering کاربردهای مهمی داره
تحلیل منطق اعتبارسنجی
پیدا کردن ورودی های لازم برای رسیدن به یک مسیر مشخص
بررسی شرطهای پیچیده داخل باینری
تحلیل مسیر های منتهی به Crash
و بررسی اینکه چه محدودیت هایی باعث میشن یک مسیر قابل دسترسی یا غیرقابل دسترسی باشه
البته در باینری واقعی ممکنه شرطها به چند تابع مختلف وابسته باشن یا تحت تأثیر حافظه و وضعیت Runtime قرار بگیرن
در این شرایط ساختن مدل دقیق برنامه سخت‌تر میشه
تفاوت Symbolic و Concrete Execution
این تفاوت رو خوب یاد بگیرید
Concrete Execution
برنامه با مقدار واقعی اجرا میشه
x = 15
در این حالت پردازش برنامه بر اساس مقدار واقعی
15 انجام میشهSymbolic Execution
به جای مقدار واقعی از یک مقدار نمادین استفاده میکنیم
x = X
وقت رسیدن به شرط ها محدودیت هایی روی
X ساخته میشنمقایسه ساده
یک نکته مهم
Symbolic Execution
تضمین نمیکنه تمام مسیرهای برنامه رو بررسی کنه
حلقه‌ها و تعداد زیاد شاخه ها میتونن باعث ترکیدن مسیرها بشن😁
محاسبات پیچیده و تعامل با سیستم عامل یا کتابخونه های خارجی هم ممکنه تحلیل رو دشوار کنن
پس حتی Symbolic Execution هم محدودیت‌های خودش رو داره
ارتباط با Fuzzing
اینجا Symbolic Execution به یکی از کاربردهای جذابش میرسه
فرض کنید Fuzzer یک ورودی تولید کرده و برنامه رو اجرا کرده
Input
↓
Program
↓
Branch A
↓
Branch B
↓
Crash
حالا میخوایم مسیر جدیدی رو بررسی کنیم که به خاطر برقرار نشدن یک شرط بهش نرسیدیم
مثلا برنامه چنین شرطی داره
Javascript
if (x == 1337)
dangerous_function();
اگر ورودی فعلی ما این باشه
x = 10
برنامه وارد
dangerous_function نمیشهSymbolic Execution
میتونه شرط شاخه رو استخراج کنه
X == 1337
بعد حل کننده یک مقدار معتبر پیشنهاد میده
X = 1337
این مقدار رو میشه به عنوان ورودی جدید در فرآیند تست استفاده کرد
پس ارتباط کلی میشه
Fuzzer
↓
Input
↓
Program Execution
↓
Uncovered Branch
↓
Path Constraint
↓
SMT Solver
↓
New Input
↓
Fuzzing Again
این ایده در روش‌هایی مثل Concolic Execution هم استفاده میشه
در Concolic Execution برنامه با ورودی های واقعی اجرا میشه ولی همزمان مقادیر و شرطها به شکل نمادین هم دنبال میشن به این ترتیب اجرای واقعی و تحلیل نمادین در کنار هم قرار میگیرن
ابزارهای کاربردی
برای آشنایی عملی با این مبحث چند ابزار ارزش بررسی دارن
angr
یک Framework برای تحلیل باینری که قابلیت‌هایی مثل Symbolic Execution و تحلیل مسیر داره
مخزن رسمی:
https://github.com/angr/angr
Triton
یک Framework برای Dynamic Binary Analysis که قابلیت‌هایی مثل Taint Analysis و Symbolic Execution ارائه میده
مخزن رسمی:
https://github.com/JonathanSalwan/Triton
Z3
یک SMT Solver که میتونه محدودیت‌های نمادین رو حل کنه
مخزن رسمی:
https://github.com/Z3Prover/z3
این ابزارها دقیقا یک کار رو انجام نمیدن
angr
بیشتر برای ساختن و تحلیل مسیرهای نمادین در باینری کاربرد داره
Triton
قابلیت‌های تحلیل پویای باینری و محاسبات نمادین رو فراهم میکنه
Z3
هم حل کننده محدودیت هاست و به تنهایی یک ابزار کامل برای تحلیل مسیرهای اجرایی باینری محسوب نمیشه
مسیر کلی
Symbolic Execution این شکلیه
Symbolic Input
↓
Program Analysis
↓
Branch Conditions
↓
Path Constraints
↓
SMT Solver
↓
Possible Input
در قسمت‌های قبلی یاد گرفتیم داده از کجا وارد برنامه میشه و چطور در Register ها و Memory حرکت میکنه
حالا یاد گرفتیم چطور شرطهای اجرای برنامه رو تحلیل کنیم تا بفهمیم چه ورودی هایی میتونن به یک مسیر خاص برسن
وقتی این مفاهیم رو کنار هم قرار بدیم
Fuzzing
↓
Interesting Input
↓
Dynamic Taint Analysis
↓
Data Flow
↓
Symbolic Execution
↓
Path Constraints
↓
New Input
↓
Crash Analysis
↓
Root Cause
دیگه فقط به اجرای برنامه و دیدن Crash اکتفا نمیکنیم میتونیم مسیر داده رو دنبال کنیم شرطهای لازم رو بفهمیم و برای بررسی مسیر های جدید ورودی های هدفمند تری بسازیم
@reverseengine
GitHub
GitHub - angr/angr: A powerful and user-friendly binary analysis platform!
A powerful and user-friendly binary analysis platform! - angr/angr
ReverseEngineering
قسمت سی و چهارم بافر اورفلو Symbolic Execution از ورودی واقعی تا ورودی نماد ها تا اینجا یاد گرفتیم چطور داده رو داخل برنامه دنبال کنیم و بفهمیم چطور به یک Crash میرسه حالا میخوایم یک قدم جلوتر بریم فرض کنید یک برنامه شرطی داره که فقط وقتی ورودی مقدار خاصی…
Part 34 Buffer Overflow
Symbolic Execution
From Concrete Inputs to Symbolic Inputs
So far, we have learned how to trace data through a program and understand how it leads to a crash.
Now, let's take it a step further.
Imagine a program has a conditional statement that directs execution along a specific path only when the input holds a particular value.
We could try thousands of different inputs until we finally reach that path.
However, there is a better way.
Instead of testing only concrete values, we can use *Symbolic Execution* to determine the conditions that must be met for the program to enter the desired path.
Here, rather than guessing inputs, we attempt to extract and solve the path constraints.
What is the core idea?
Suppose we have the following program:
C
int check(int x)
{
if (x == 1337)
return 1;
return 0;
}
During a standard execution, we might provide this value:
x = 10
The program checks the condition:
10 == 1337
The result is false, and the program follows the second path.
Now, suppose we use a symbolic value instead of a concrete one:
x = X
In this case, the program's condition becomes:
X == 1337
A solver can deduce that for the program to enter the first path, the value of X must be 1337.
Thus, instead of testing various values, we can determine the necessary condition to reach that path.
Path Constraint
Suppose we have this code:
C
int process(int x)
{
if (x > 10)
{
if (x < 20)
return 1;
}
return 0; }
To reach
return 1, both conditions must be met:x > 10
AND
x < 20
We refer to the set of conditions that must hold true to reach a specific path as a
Path Constraint
So, the constraint for the path in question is:
10 < x < 20
Since
x is of type int, the possible solutions include these values:11, 12, 13, 14, 15, 16, 17, 18, 19
The solver can find one of the valid solutions
For example:
x = 15
An important point is that Symbolic Execution does not consider only the current condition;
it also maintains the path's preceding conditions,
because reaching a specific point in the program requires all necessary conditions along the path to be satisfied.
When paths branch out
Consider this program:
C
int process(int x)
{
if (x > 10)
return 1;
if (x == 5)
return 2;
return 0;
}
Using Symbolic Execution, we can examine the program's various paths:
x = X
|
x > 10 ?
/ \
Yes No
| |
return 1 x == 5 ?
/ \
Yes No
| |
return 2 return 0
Now, suppose we want to reach the
return 2 statement.First, the initial condition must *not* hold:
X <= 10
Then, the second condition *must* hold:
X == 5
So, our path constraint becomes:
X <= 10
AND
X == 5
Consequently:
X = 5
...is considered a valid input to reach this path.
This is the core idea behind Symbolic Execution:
We trace the program and gather the necessary conditions for each path.
The Role of the SMT Solver
So far, we’ve seen that we can extract path conditions, but solving them manually becomes difficult when the number of conditions grows.
This is where we use a tool called an
SMT Solver.
One well-known tool in this field
is Z3,
developed by Microsoft Research.
Suppose our conditions are:
X > 10
X < 20
X != 15
The solver must find a value that satisfies all conditions simultaneously.
For example:
X = 11
This value is valid because it satisfies all three conditions.
However, if the conditions were:
X > 20
X < 10
No real value could satisfy both conditions at the same time.
Consequently, the problem is
Unsatisfiable;
meaning there is no valid solution.
Conversely, if at least one solution exists, the problem
is considered Satisfiable.
Of course, SMT solvers aren't limited to simple numerical conditions.
Depending on the logic and capabilities of the solver, they can also handle constraints involving bit-vectors and bitwise operations.
ReverseEngineering
قسمت سی و چهارم بافر اورفلو Symbolic Execution از ورودی واقعی تا ورودی نماد ها تا اینجا یاد گرفتیم چطور داده رو داخل برنامه دنبال کنیم و بفهمیم چطور به یک Crash میرسه حالا میخوایم یک قدم جلوتر بریم فرض کنید یک برنامه شرطی داره که فقط وقتی ورودی مقدار خاصی…
This is crucial for binary analysis, as processors operate on values of specific sizes—such as 8, 32, or 64 bits—and their behavior is always... It is not like mathematical integers.
The connection between Symbolic Execution and Reverse Engineering
Suppose you have a binary containing the following logic:
C++
int validate(int value)
{
if (value < 100)
return 0;
if (value > 200)
return 0;
if (value == 150)
return 1;
The connection between Symbolic Execution and Reverse Engineering
Suppose you have a binary containing the following logic:
C++
int validate(int value)
{
if (value < 100)
return 0;
if (value > 200)
return 0;
if (value == 150)
return 1;