پرش به محتوا

اجرای نمادین

از ویکی‌پدیا، دانشنامهٔ آزاد

اجرای نمادین (به انگلیسی: symbolic execution) یا ارزیابی نمادین یا symbex در علوم رایانه، راهی برای تحلیل یک برنامه است که در نتیجه آن تعیین می‌شود که کدام «ورودی» ها منجر به اجرای هر «بخش» از برنامه می‌شود. مفسرهای اجرای نمادین موقع دنبال‌کردن برنامه، به جای مقادیر واقعی برای اجرای نرمال برنامه، «مقادیر نمادین» را برای ورودی‌ها فرض می‌کنند. این اجرا به عبارات به صورت «نمادهایی برای عبارات و متغیرهای موجود در برنامه» برخورد می‌کند، و نیز به محدودیت‌ها در قالب آن «نمادهایی برای نتایج ممکنه هر شاخه شرطی» برخورد می‌کند.

گرایش شبیه‌سازی نمادین همین مفهوم را به سخت‌افزار اعمال می‌کند. گرایش محاسبات نمادین همین مفهوم را به تحلیل عبارات ریاضیاتی اعمال می‌کند.

مثال

[ویرایش]

برنامه زیر را درنظر بگیرید، این برنامه یک مقدار ورودی را می‌خواند و اگر ورودی ۶ باشد، مقدار «شکست» را برمی‌گرداند. 

int f() {
  ...
  y = read();
  z = y * 2;
  if (z == 12) {
    fail();
  } else {
    printf("OK");
  }
}

در مدت اجرای نرمال (یا اجرای واقعی)، برنامه یک مقدار ورودی واقعی (مثل 5) را می‌خواند و آن را به y انتساب می‌دهد. سپس اجرا با یک ضرب و شاخه شرطی ادامه می‌یابد، که به مقدار شکست ارزیابی شده و OK را چاپ می‌کند.

در مدت اجرای نمادین، برنامه یک مقدار نمادین (مثل λ) را می‌خواند و آن را به y انتساب می‌دهد. سپس برنامه با ضرب ادامه می‌یابد و مقدار λ * 2 را به z انتساب می‌دهد. موقعی که به بیانیه if می‌رسد، عبارت λ * 2 == 12 را ارزیابی می‌کند. در این نقطه از برنامه، λ هر مقداری را می‌تواند اخذ کند، و اجرای نمادین می‌تواند در امتداد هر دو شاخه ادامه پیدا کند، این کار با انشعاب‌دهی (fork کردن) به دو مسیر انجام می‌شود. در هر دستورالعمل شاخه‌گزینی به هر مسیر یک «کپی از وضعیت برنامه» و نیز یک «محدودیت مسیری» انتساب داده می‌شود. در این مثال، محدودیت مسیری برای شاخه then همان λ * 2 != 12 و برای شاخه else همان λ * 2 == 12 است. در اینجا هر دو مسیر به صورت مستقل قابل اجرای نمادین هستند. موقعی که مسیر خاتمه پیدا کند (مثلاً به عنوان نتیجه اجرای fail() یا با خارج‌شدن ساده)، اجرای نمادین یک مقدار غیرانتزاعی، برای λ محاسبه می‌کند، این کار با حل کردن محدودیت‌های مسیری انباشه‌شده در هر مسیر انجام می‌شود. این مقادیر غیرانتزاعی را می‌توان به عنوان آزمایه‌های غیرانتزاعی درنظر گرفت، که این مزیت را دارند که مثلاً می‌توانند به توسعه‌دهندگان در ایجاد مجدد اشکال‌های نرم‌افزاری کمک کنند. در این مثال، حل‌کننده محدودیت تعیین می‌کند که برای آنکه به بیانیه fail() برسیم، نیاز است که λ برابر 6 شود.

محدودیت‌ها

[ویرایش]

انفجار مسیری

[ویرایش]

اجرای نمادین همه مسیرهای ممکن برنامه، قابل مقیاس‌دهی به برنامه‌های بزرگ نیست. اگر سایز برنامه افزایش یابد، تعداد مسیرهای ممکن در یک برنامه به صورت نمایی افزایش می‌یابد، و حتی در حالت برنامه‌هایی که تکرارهای حلقه‌ای غیرمحدود دارند، تعداد مسیرها می‌تواند بینهایت باشد.[۱] راه‌حل‌ها برای مسئله «انفجار مسیری» معمولاً یا از هیوریستیک‌هایی برای یافتن مسیر برای افزایش پوشاندن کد استفاده می‌کند،[۲] که زمان اجرا را موازی‌سازی کرده، و مسیرهای مستقل کاهش را می‌دهد،[۳] یا از ادغام مسیرهای مشابه استفاده می‌کنند.[۴]

کارایی وابسته به برنامه

[ویرایش]

از اجرای نمادین برای استنتاج‌هایی در مورد یک برنامه به صورت «مسیر-به-مسیر» استفاده می‌شود، که این موضوع یک مزیت نسبت به استنتاج در مورد برنامه به صورت «ورودی-به-ورودی» (که دیگر الگوهای آزمون، مثل تحلیل پویای برنامه، از آن استفاده می‌کنند) است. با این حال، اگر تعداد کمی از ورودی‌ها در طول برنامه، یک مسیر مشابه را بگیرند، نسبت به حالت آزمون هر ورودی به صورت مجزا، بهبود زیادی حاصل نشده‌است.

دگرنامی به حافظه

[ویرایش]

اگر محل حافظه مشابه توسط نام‌های متفاوتی دستیابی شوند (که به این کار الیاس یا دگرنامی می‌گویند)، اجرای نمادین سخت‌تر شده‌است. همیشه نمی‌توان دگرنام‌ها را به صورت ایستا تشخیص داد، از این رو موتور اجرای نمادین نمی‌تواند تشخیص دهد که اگر مقدار یک متغیر را تغییر بدهیم، دیگری هم تغییر خواهد کرد.[۵]

آرایه‌ها

[ویرایش]

به دلیل آنکه یک آرایه گردآوردی از تعداد زیادی از مقادیر متمایز است، اجرای نمادین می‌تواند به کل آرایه به عنوان یک مقدار برخورد کند یا اینکه با هر عنصر آرایه به صورت یک محل مجزا برخورد کند. اینجا مشکلی که در مورد برخورد با هر عنصر آرایه به صورت مجزا وجود دارد آن است که یک ارجاع مثل "A[i]" را موقعی که یک مقدار واقعی برای i به آن داده‌ایم، فقط به صورت پویا می‌توان تعیین نمود.[۵]

تعامل‌های محیطی

[ویرایش]

برنامه‌ها با انجام تماس سامانه‌ای، گرفتن سیگنال، و غیره با محیط خود تعامل دارند. و مشکلات سازگاری می‌تواند موقعی بروز می‌کند که اجرا به مولفه‌هایی برسد که تحت کنترل ابزار اجرای نمادین نیست (مثل هسته یا کتابخانه). مثال زیر را درنظر بگیرید: 

int main()
{
  FILE *fp = fopen("doc.txt");
  ...
  if (condition) {
    fputs("some data", fp);
  } else {
    fputs("some other data", fp);
  }
  ...
  data = fgets(..., fp);
}

این برنامه یک فایل را باز می‌کند، سپس بر اساس یک شرط، مقادیر متفاوتی از داده را به فایل می‌نویسد. سپس داده نوشته‌شده را بازخوانی می‌کند. از لحاظ نظری، اجرای نمادین دو مسیر را در خط ۵ انشعاب داده است، و هر مسیر از آنجا کپی فایل خاص خود را خواهد داشت. بیانیه موجود در خط ۱۱، مقدار داده‌ای را بازمی‌گرداند که با مقدار «شرط» موجود در خط ۵ سازگار است. در عمل، عملیات فایل به صورت تماس سامانه‌ای در هسته پیاده‌سازی می‌شود، و از کنترل ابزار اجرای نمادین خارج است. دیدگاه‌های اصلی برای رسیدگی به این چالش‌ها از این قرار هستند:

به صورت مستقیم تماس با محیط را اجراکنیم. مزیت این دیدگاه آن است که پیاده‌سازی‌اش ساده است. اما ایرادش آن است که اثرجانبی این تماس‌ها به همه حالت‌های مدیریت شده توسط موتور اجرای نمادین ضربه وارد می‌کند. در مثال بالا، بر اساس ترتیب دنباله‌ای حالت‌ها، دستورالعمل خط ۱۱، مقدار "some datasome other data" یا "some other datasomedata" را برخواهد گرداند.

مدل‌سازی محیط. در این حالت، موتور، تماس سامانه‌ای را با یک «مدل» ابزارسازی می‌کند که این مدل تاثیراتش را شبیه‌سازی کرده، و همه اثرات جانبی‌اش را در ذخیره هر-وضعیتی نگهداری می‌کند. مزیت این کار آن است که موقعی به نتایج درست می‌رسیم که برنامه‌هایی که با محیط تعامل دارند را به صورت نمادین اجرا کنیم. ایرادش آن است که باید مدل‌های بالقوه پیچیده زیادی را برای تماس سامانه‌ای پیاده‌سازی و نگهداری کنیم. ابزارهایی مثل مثل KLEE, Cloud9[۶] و Otter,[۷] از این دیدگاه استفاده کرده‌اند، یعنی آن‌ها مدل‌هایی را برای عملیات سیستم فایل، سوکت‌ها و IPC و غیره پیاده‌سازی کرده‌اند.

انشعاب کل حالت سامانه. ابزارهای اجرای نمادین براساس ماشین مجازی، مسئله محیط را با انشعاب کل حالت VM حل می‌کند. برای مثال، در S2E[۸] هر حالت یک برگرفت مستقل VM است، که قابلیت اجرای جداگانه دارد. این دیدگاه نیاز برای نوشتن و نگهداری مدل‌های پیچیده را کاهش می‌دهد، و همچنین امکان اجرای نمادین مجازی هر برنامه‌ای را می‌دهد. اما این روش، سربار استفاده از حافظه بالاتری دارد (برگرفت‌های VM می‌تواند بزرگ باشند).

ابزارها

[ویرایش]
ابزار هدف URL همه می‌توانند اتسفاده کنند/ متن باز/ قابل دانلود
angr libVEX based (supporting x86, x86-64, ARM, AARCH64, MIPS, MIPS64, PPC, PPC64, and Java) http://angr.io/ yes
BE-PUM x86 https://github.com/NMHai/BE-PUM yes
BINSEC x86, ARM, RISC-V (32 bits) http://binsec.github.io yes
ExpoSE JavaScript https://github.com/ExpoSEJS/ExpoSE yes
FuzzBALL VineIL / Native http://bitblaze.cs.berkeley.edu/fuzzball.html yes
Jalangi2 JavaScript https://github.com/Samsung/jalangi2 yes
janala2 Java https://github.com/ksen007/janala2 yes
JaVerT JavaScript https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf yes
JBSE Java https://github.com/pietrobraione/jbse yes
jCUTE Java https://github.com/osl/jcute yes
JPF Java http://babelfish.arc.nasa.gov/trac/jpf بایگانی‌شده در ۲۰۱۱-۱۰-۱۷ توسط Wayback Machine yes
KeY Java http://www.key-project.org/ yes
Kite LLVM http://www.cs.ubc.ca/labs/isd/Projects/Kite/ yes
KLEE LLVM https://klee.github.io/ yes
Kudzu JavaScript http://webblaze.cs.berkeley.edu/2010/kudzu/kudzu.pdf no
MPro Ethereum Virtual Machine (EVM) / Native https://sites.google.com/view/smartcontract-analysis/home yes
Manticore x86-64, ARMv7, Ethereum Virtual Machine (EVM) / Native https://github.com/trailofbits/manticore/ yes
Mayhem Binary http://forallsecure.com no
Mythril-Classic Ethereum Virtual Machine (EVM) / Native https://github.com/ConsenSys/mythril-classic yes
Otter C https://bitbucket.org/khooyp/otter/overview yes
Oyente-NG Ethereum Virtual Machine (EVM) / Native http://www.comp.ita.br/labsca/waiaf/papers/RafaelShigemura_paper_16.pdf no
Pathgrind[۹] Native 32-bit Valgrind-based https://github.com/codelion/pathgrind yes
Pex .NET Framework http://research.microsoft.com/en-us/projects/pex/ no
pysymemu x86-64 / Native https://github.com/feliam/pysymemu/ yes
Rosette Dialect of Racket https://emina.github.io/rosette/ yes
Rubyx Ruby http://www.cs.umd.edu/~avik/papers/ssarorwa.pdf no
S2E x86, x86-64, ARM / User and kernel-mode binaries http://s2e.systems/ yes
Symbolic PathFinder (SPF) Java Bytecode https://github.com/SymbolicPathFinder yes
SymDroid Dalvik bytecode http://www.cs.umd.edu/~jfoster/papers/symdroid.pdf no
SymJS JavaScript http://www.cs.utah.edu/~ligd/publications/SymJS-FSE14.pdf بایگانی‌شده در ۲۲ سپتامبر ۲۰۱۷ توسط Wayback Machine no
Triton x86 and x86-64 https://triton.quarkslab.com yes
Verifast C, Java https://people.cs.kuleuven.be/~bart.jacobs/verifast yes

نسخه‌های اولیه ابزارها

[ویرایش]

EXE[۱۰] یک نسخه اولیه برای KLEE است. مقاله EXE را می‌توان در اینجا یافت.

تاریخچه

[ویرایش]

مفهوم اجرای نمادین به صورت دانشگاهی با توصیف این موارد معرفی شد: سامانه Select،[۱۱] سامانه EFFIGY،[۱۲] سامانه DISSECT،[۱۳] و سامانه Clarke's.[۱۴] کتابشناسی را برای مقاله‌های فنی‌تر منتشر شده دربارهٔ اجرای نمادین ببینید.

پانویس

[ویرایش]
  1. ↑ Anand, Saswat; Patrice Godefroid; Nikolai Tillmann (2008). "Demand-Driven Compositional Symbolic Execution". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 4963. pp. 367–381. doi:10.1007/978-3-540-78800-3_28. ISBN 978-3-540-78799-0.
  2. ↑ Ma, Kin-Keng; Khoo Yit Phang; Jeffrey S. Foster; Michael Hicks (2011). "Directed Symbolic Execution". Proceedings of the 18th International Conference on Statis Analysis. pp. 95–111. ISBN 978-3-642-23701-0. Retrieved 2013-04-03.
  3. ↑ Staats, Matt; Corina Pasareanu (2010). "Parallel symbolic execution for structural test generation". Proceedings of the 19th International Symposium on Software Testing and Analysis. pp. 183–194. doi:10.1145/1831708.1831732. ISBN 978-1-60558-823-0. S2CID 9898522.
  4. ↑ Kuznetsov, Volodymyr; Kinder, Johannes; Bucur, Stefan; Candea, George (2012-01-01). "Efficient State Merging in Symbolic Execution". Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, NY, USA: ACM. pp. 193–204. CiteSeerX 10.1.1.348.823. doi:10.1145/2254064.2254088. ISBN 978-1-4503-1205-9. S2CID 135107.
  5. ↑ ۵٫۰ ۵٫۱ DeMillo, Rich; Offutt, Jeff (1991-09-01). "Constraint-Based Automatic Test Data Generation". IEEE Transactions on Software Engineering. 17 (9): 900–910. doi:10.1109/32.92910.
  6. ↑ Cadar, Cristian; Dunbar, Daniel; Engler, Dawson (2008-01-01). "KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs". Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI'08: 209–224.
  7. ↑ Turpie, Jonathan; Reisner, Elnatan; Foster, Jeffrey; Hicks, Michael. "MultiOtter: Multiprocess Symbolic Execution" (PDF).
  8. ↑ Chipounov, Vitaly; Kuznetsov, Volodymyr; Candea, George (2012-02-01). "The S2E Platform: Design, Implementation, and Applications". ACM Trans. Comput. Syst. 30 (1): 2:1–2:49. doi:10.1145/2110356.2110358. ISSN 0734-2071. S2CID 16905399.
  9. ↑ Sharma, Asankhaya (2014). "Exploiting Undefined Behaviors for Efficient Symbolic Execution". ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software Engineering. pp. 727–729. doi:10.1145/2591062.2594450. ISBN 978-1-4503-2768-8. S2CID 10092664.
  10. ↑ Cadar, Cristian; Ganesh, Vijay; Pawlowski, Peter M.; Dill, David L.; Engler, Dawson R. (2008). "EXE: Automatically Generating Inputs of Death". ACM Trans. Inf. Syst. Secur. 12: 10:1–10:38. doi:10.1145/1455518.1455522. S2CID 10905673.
  11. ↑ Robert S. Boyer and Bernard Elspas and Karl N. Levitt SELECT--a formal system for testing and debugging programs by symbolic execution, Proceedings of the International Conference on Reliable Software, 1975,page 234--245, Los Angeles, California
  12. ↑ James C. King,Symbolic execution and program testing, Communications of the ACM, volume 19, number 7, 1976, 385--394
  13. ↑ William E. Howden, Experiments with a symbolic evaluation system, Proceedings, National Computer Conference, 1976.
  14. ↑ Lori A. Clarke, A program testing system, ACM 76: Proceedings of the Annual Conference, 1976, pages 488-491, Houston, Texas, United States

منابع

[ویرایش]

مشارکت‌کنندگان ویکی‌پدیا. «Symbolic execution». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۱۱ مهٔ ۲۰۲۱.

برگرفته از «https://fa.wikipedia.org/w/index.php?title=اجرای_نمادین&oldid=39409281»