ReverseEngineering

Turnaround Time از زمانی که یک Job وارد سیستم میشه تا زمانی که کاملا تموم بشه چقدر زمان گذشته؟ فرمول: Turnaround Time = Completion Time - Arrival Time مثلا: Arrival Time = 0 Completion = 10 پس: Turnaround Time = 10 یعنی Process از اول تا اخر 10 واحد زمانی داخل سیستم بوده @reverseengine

C change(&a); read_value(&b); read_value(&a); } Determine which function call reads the value modified by change and why. Note that the read_value function reads the value but does not return it, nor does it store it elsewhere. A key takeaway from this section: When analyzing data flow, it is not always necessary for two functions to interact directly. Sometimes, one function modifies a value in memory, and another function—with no direct connection to the first—accesses that same location via a pointer. In reverse engineering, tracing these very indirect connections can reveal the program's actual behavior. @reverseengine

If we mistakenly assume that two pointers are the same, we may analyze the order of memory changes and, as a result, the actual path of program execution incorrectly. Exercise: Examine the following code. C void change(int *p) { *p = 50 ; } void read_value(int *q) { int x = *q; int main() int a = 10; int b = 20;

Memory Aliasing Between Functions So far we have seen how two pointers can point to the same memory address. Now we want to examine a more important case. Suppose we have a function that modifies a value in memory and another function reads the same value from memory. The point here is that these two functions may use different pointers, but both access the same address. This is very important in reverse engineering, because we may not notice the relationship between them by examining each function alone. A simple example with C void set_value(int *p) { *p = 100; } int get_value(int *q) { return *q; } int main() { int value = 10; set_value(&value); int result = get_value(&value); return result; } What is happening here? First, the value is 10 Then the address of value is given to the set_value function The set_value function changes the value at that address to 100 Then the same address is given to the get_value function and the new value is read from memory Finally, the result is 100 The main point is that the pointers p and q have different names and variables, but in this example they both access the same memory location So the connection between these two functions is formed through memory, not through the return value of one of them Now, how does this look in assembly? Suppose the set_value function is compiled like this set_value: mov dword ptr [rdi], 100 ret This example is written according to the System V AMD64 calling convention, which is commonly used in 64-bit Linux programs According to this convention, the first argument of the function is placed in the RDI register Now let's examine this instruction mov dword ptr [rdi], 100 This instruction writes the number 100 to the address located in RDI Note that the value of RDI is different from the value stored in memory RDI holds the address and the expression [rdi] refers to the data located at that address Now look at the get_value function get_value: mov eax, dword ptr [rdi] ret Here the four-byte value located at the address RDI is read and placed in EAX. Since the return value of the function is of type int, this value is stored in the register EAX is returned, so one function writes to memory and another function reads from the same memory, provided that the address given to both functions points to the same memory location. Now how do we find it in reverse engineering? When you are examining a binary file in Ghidra or Disassembler, follow these steps Step 1: Examine the function arguments See what pointers the function receives and whether it uses them to read or write memory Step 2: Look for memory write instructions For example, consider the following command mov dword ptr [rdi], 100 This command shows that the function uses the address in RDI to write data Step 3: Examine other functions See if other functions receive the same address or associated pointer and later read something from that memory Don't just look for identical variable or register names - the address may be passed through another register, stored in a structure, or obtained with several calculation steps Step 4: Look for relationships between functions Don't just look at the function name or its return value - a function may change memory It does not return any value, but the effect of its change can be seen in another function a few steps later. Therefore, you must follow the path of transferring pointers and reading and writing memory. An important point about Must Alias ​​and May Alias. We cannot always be sure that two pointers point to the same address based on the similarity of the arguments. Here we have two important concepts. Must Alias ​​means that according to the information and conditions we have examined, two pointers must point to the same memory location. May Alias ​​means that two pointers may point to the same memory location, but the available information is not enough to prove this definitively. This difference is very important in program analysis.

C change(&a); read_value(&b); read_value(&a); } مشخص کنید کدوم فراخوانی مقدار تغییر کرده توسط change رو میخونه و چرا به این نکته هم توجه کن که تابع read_value مقدار رو میخونه اما اون رو برنمیگردونه و در جای دیگه‌ای هم ذخیره نمیکنه نکته‌ای که باید از این قسمت یادتون بمونه برای تحلیل جریان داده همیشه لازم نیست دو تابع مستقیما با هم ارتباط داشته باشن بعضی وقتا یه تابع مقداری رو داخل حافظه تغییر میده و تابع دیگه‌ای که هیچ ارتباط مستقیمی با اون نداره از طریق یه Pointer به همون محل دسترسی پیدا میکنه در مهندسی معکوس دنبال کردن همین ارتباط‌ های غیرمستقیم میتونه رفتار واقعی برنامه رو مشخص کنه @reverseengine

Memory Aliasing بین توابع تا اینجا دیدیم که چطور ممکنه دو تا Pointer به یه آدرس از حافظه اشاره کنن حالا میخوایم یه حالت مهم‌تر رو بررسی کنیم فرض کنید یه تابع داریم که یه مقدار رو توی حافظه تغییر میده و یه تابع دیگه همون مقدار رو از حافظه میخونه نکته اینجاست که ممکنه این دو تا تابع از Pointer های متفاوتی استفاده کنن ولی هر دو به یه آدرس مشترک دسترسی داشته باشن این موضوع توی مهندسی معکوس خیلی مهمه، چون ممکنه با بررسی هر تابع به‌تنهایی متوجه ارتباط بین اون‌ها نشیم یه مثال ساده با C void set_value(int *p) { *p = 100; } int get_value(int *q) { return *q; } int main() { int value = 10; set_value(&value); int result = get_value(&value); return result; } اینجا چه اتفاقی میفته؟ اول مقدار value برابر 10 هست بعد آدرس value به تابع set_value داده میشه تابع set_value مقدار موجود در اون آدرس رو به 100 تغییر میده بعد همون آدرس به تابع get_value داده میشه و مقدار جدید از حافظه خونده میشه در نهایت result برابر 100 میشه نکته اصلی اینه که Pointerهای p و q اسم و متغیرهای متفاوتی دارن اما در این مثال هر دو به همون خانه حافظه دسترسی دارن پس ارتباط بین این دو تابع از طریق حافظه شکل گرفته، نه از طریق مقدار برگشتی یکی از اون‌ها حالا این موضوع توی اسمبلی چه شکلیه؟ فرض کنید تابع set_value به این شکل کامپایل شده set_value: mov dword ptr [rdi], 100 ret این مثال بر اساس قرارداد فراخوانی System V AMD64 نوشته شده که معمولا توی برنامه‌های 64 بیتی لینوکس استفاده میشه طبق این قرار داد آرگومان اول تابع داخل رجیستر RDI قرار میگیره حالا این دستور رو بررسی کنیم mov dword ptr [rdi], 100 این دستور عدد 100 رو در آدرسی مینویسه که داخل RDI قرار داره دقت کنید که مقدار RDI با مقداری که داخل حافظه ذخیره شده فرق داره RDI آدرس رو نگه میداره و عبارت [rdi] به داده‌ ای اشاره میکنه که در اون آدرس قرار داره حالا تابع get_value رو ببینید get_value: mov eax, dword ptr [rdi] ret اینجا مقدار چهار بایتی موجود در آدرس RDI خونده میشه و داخل EAX قرار میگیره از اونجایی که مقدار برگشتی تابع از نوع int هست این مقدار در رجیستر EAX برگردونده میشه پس یه تابع توی حافظه مینویسه و تابع دیگه از همون حافظه میخونه البته به شرطی که آدرسی که به هر دو تابع داده شده به همون محل حافظه اشاره کنه حالا توی مهندسی معکوس چطور پیداش کنیم؟ وقتی داری یه فایل باینری رو توی Ghidra یا Disassembler بررسی میکنید این مراحل رو دنبال کنید مرحله اول: آرگومان‌های تابع رو بررسی کنید ببینید تابع چه Pointer هایی دریافت میکنه و از اون‌ها برای خوندن یا نوشتن حافظه استفاده میکنه یا نه مرحله دوم: دنبال دستورهای نوشتن حافظه بگردید مثلا دستور زیر رو در نظر بگیرید mov dword ptr [rdi], 100 این دستور نشون میده تابع از آدرسی که داخل RDI قرار داره برای نوشتن داده استفاده میکنه مرحله سوم: تابع‌های دیگه رو بررسی کنید ببینید تابع‌ های دیگه همون آدرس یا Pointer مرتبطی رو دریافت میکنن و بعدا از اون حافظه مقداری میخونن یا نه فقط دنبال اسم یکسان متغیرها یا رجیسترها نباشید ممکنه آدرس از طریق رجیستر دیگه‌ای منتقل بشه داخل ساختار ذخیره بشه یا با چند مرحله محاسبه به دست بیاد مرحله چهارم: ارتباط بین تابع‌ ها رو دنبال کنید فقط به اسم تابع یا مقدار برگشتی اون توجه نکنیدممکنه یه تابع حافظه رو تغییر بده و هیچ مقداری برنگردونه ولی اثر تغییرش چند مرحله بعد داخل تابع دیگه‌ای دیده بشه برای همین باید مسیر انتقال Pointer ها و خوندن و نوشتن حافظه رو دنبال کنید یه نکته مهم درباره Must Alias و May Alias همیشه نمیتونیم از روی شباهت آرگومان ها مطمئن بشیم که دو Pointer به یه آدرس اشاره میکنن اینجا دو مفهوم مهم داریم Must Alias یعنی طبق اطلاعات و شرایطی که بررسی کردیم دو Pointer حتما به یه محل حافظه اشاره میکنن May Alias یعنی ممکنه دو Pointer به یه محل حافظه اشاره کنن ولی اطلاعات موجود برای اثبات قطعی این موضوع کافی نیست این تفاوت توی تحلیل برنامه اهمیت زیادی داره اگه دو Pointer رو اشتباهی یکی فرض کنیم ممکنه ترتیب تغییرات حافظه و در نتیجه مسیر واقعی اجرای برنامه رو اشتباه تحلیل کنیم تمرین: کد زیر رو بررسی کنید C void change(int *p) { *p = 50; } void read_value(int *q) { int x = *q; } int main() { int a = 10; int b = 20;

In previous sections, we learned where data enters the program and how it moves through registers and memory. Now, we have learned how to analyze program execution conditions to determine which inputs can reach a specific path. When we combine these concepts: Fuzzing ↓ Interesting Input ↓ Dynamic Taint Analysis ↓ Data Flow ↓ Symbolic Execution ↓ Path Constraints ↓ New Input ↓ Crash Analysis ↓ Root Cause We no longer limit ourselves to simply running the program and observing crashes; we can trace the data path, understand the necessary conditions, and generate more targeted inputs to explore new paths. @reverseengine

C return 0; } Standard analysis reveals that the program has several conditions. However, Symbolic Execution can extract the conditions necessary to reach a successful execution path: value >= 100 AND value <= 200 AND value == 150 Consequently, value = 150 is a valid solution. This capability has significant applications in reverse engineering: Analyzing validation logic Finding the inputs required to reach a specific path Examining complex conditions within the binary Analyzing paths that lead to a crash Determining which constraints make a path reachable or unreachable Of course, in a real binary, conditions might depend on multiple functions or be influenced by memory and runtime state. In such scenarios, constructing an accurate model of the program becomes more difficult. The difference between Symbolic and Concrete Execution Make sure to understand this distinction well. Concrete Execution The program runs with a concrete (actual) value. x = 15 In this case, program processing is based on the actual value of 15. Symbolic Execution Instead of a concrete value, we use a symbolic value. x = X When conditions are encountered, constraints are generated for X. A simple comparison An important point Symbolic Execution does not guarantee that all program paths will be examined. Loops and a large number of branches can lead to a "path explosion." 😁 Complex calculations and interactions with the operating system or external libraries can also complicate the analysis. So, even Symbolic Execution has its own limitations. Connection to Fuzzing This is where Symbolic Execution demonstrates one of its most interesting applications. Suppose a fuzzer has generated an input and executed the program: Input ↓ Program ↓ Branch A ↓ Branch B ↓ Crash Now, let's examine a new execution path—one that wasn't reached because a specific condition wasn't met. For instance, the program contains a condition like this: JavaScript if (x == 1337) dangerous_function(); If our current input is: x = 10 The program does not enter dangerous_function. Symbolic Execution can extract the branch condition: X == 1337 Then, the solver suggests a valid value: X = 1337 This value can be used as a new input in the testing process. So, the overall workflow looks like this: Fuzzer ↓ Input ↓ Program Execution ↓ Uncovered Branch ↓ Path Constraint ↓ SMT Solver ↓ New Input ↓ Fuzzing Again This concept is also utilized in methods like Concolic Execution. In Concolic Execution, the program runs with concrete inputs while values ​​and conditions are simultaneously tracked symbolically; thus, concrete execution and symbolic analysis are combined. Practical Tools To gain hands-on experience with this topic, a few tools are worth exploring: angr A binary analysis framework featuring capabilities such as Symbolic Execution and path analysis. Official repository: https://github.com/angr/angr Triton A framework for Dynamic Binary Analysis that offers capabilities like Taint Analysis and Symbolic Execution. Official repository: https://github.com/JonathanSalwan/Triton Z3 An SMT solver capable of solving symbolic constraints. Official repository: https://github.com/Z3Prover/z3 These tools do not perform exactly the same function: angr Is primarily used for constructing and analyzing symbolic paths within binaries. Triton Provides capabilities for dynamic binary analysis and symbolic computation. Z3 Is a constraint solver; while it is not a standalone, all-in-one tool for analyzing binary execution paths, it is a crucial component of such systems. It’s not possible [to do it that way]. The general workflow of Symbolic Execution looks like this: Symbolic Input ↓ Program Analysis ↓ Branch Conditions ↓ Path Constraints ↓ SMT Solver ↓ Possible Input

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;

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.

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 در این حالت پردازش برنامه بر اساس مقدار واقعی 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

قسمت سی و چهارم بافر اورفلو

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;

Bluetooth Headphone Jacking: Full Disclosure of Airoha RACE Vulnerabilities https://insinuator.net/2025/12/bluetooth-headphone-jacking-full-disclosure-of-airoha-race-vulnerabilities/

Cursor 0day: When Full Disclosure Becomes the Only Protection Left https://mindgard.ai/blog/cursor-0day-when-full-disclosure-becomes-the-only-protection-left

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/

FortiBleed Is Still Active, Now Locking Orgs Out https://socradar.io/blog/fortibleed-still-active-locking-organizations-out/

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