Символьное выполнение

[ppsmoke]

Добрый вечер, форумчане! Мб кто знает какие нибудь хорошие статьи/источники где можно почитать про символьное выполнение, смт решатели и тд. Пишу курсач на тему "Автоматизированное решение crackme с использованием символьного выполнения".
Решил использовать тритон, разобрался как в его вм эмулировать выполнение кода, но возникли сложности с нахождением/решением ограничений. В общем, буду рад любой информации, любой помощи.
А может быть кто-то сам хочет разобраться в этой теме? Можем аккумулировать усилия и накодить что то вместе.
Спасибо!

 

[weaver]

Добрый вечер, форумчане! Мб кто знает какие нибудь хорошие статьи/источники где можно почитать про символьное выполнение, смт решатели и тд.

Можешь почитать книгу "Practical Binary Analysis" она кстати есть в переводе, но перевод оставляет желать лучшего.

http://xssforum7mmh3n56inuf2h73hvhnzobi7h2ytb3gvklrfqm7ut3xdnyd.onion/threads/120395/

В главе 3, там, как раз таки рассматривается символическое исполнение в том числе с тритон.

Part III: Advanced Binary Analysis
Chapter 8: Customizing Disassembly
Chapter 9: Binary Instrumentation
Chapter 10: Principles of Dynamic Taint Analysis
Chapter 11: Practical Dynamic Taint Analysis with libdft
Chapter 12: Principles of Symbolic Execution
Chapter 13: Practical Symbolic Execution with Triton

Если какие-то базовые вещи понять и освежить память, то можешь посмотреть видео от SpbCTF
__youtube.com/watch?v=tfO7dwPcIkU&list=PLLguubeCGWoZIZBfJ1ZfJytjHLZyFFrMk

 

[shrekushka]

You can finish reading this in a couple of hours

A Survey of Symbolic Execution Techniques

Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program's authentication...

arxiv.org

then what weaver said

 

[ppsmoke]

Можешь почитать книгу "Practical Binary Analysis" она кстати есть в переводе, но перевод оставляет желать лучшего.

http://xssforum7mmh3n56inuf2h73hvhnzobi7h2ytb3gvklrfqm7ut3xdnyd.onion/threads/120395/

В главе 3, там, как раз таки рассматривается символическое исполнение в том числе с тритон.


Если какие-то базовые вещи понять и освежить память, то можешь посмотреть видео от SpbCTF
__youtube.com/watch?v=tfO7dwPcIkU&list=PLLguubeCGWoZIZBfJ1ZfJytjHLZyFFrMk

Спасибо! Изучу

 

[ZAGREB2030]

Курс MIT «Безопасность компьютерных систем». Лекция 10: «Символьное выполнение», часть 3​

Спойлер: урл

ÐÑÑÑ MIT «ÐезопаÑноÑÑÑ ÐºÐ¾Ð¼Ð¿ÑÑÑеÑнÑÑ ÑиÑÑем». ÐекÑÐ¸Ñ 10: «СимволÑное вÑполнение», ÑаÑÑÑ 3

ÐаÑÑаÑÑÑеÑÑкий ТеÑнологиÑеÑкий инÑÑиÑÑÑ. ÐÑÑÑ Ð»ÐµÐºÑий #6.858. «ÐезопаÑноÑÑÑ ÐºÐ¾Ð¼Ð¿ÑÑÑеÑнÑÑ ÑиÑÑем». Ðиколай ÐелÑдовиÑ, ÐÐ¶ÐµÐ¹Ð¼Ñ ÐикенÑ. 2014 год Computer Systems Security â ÑÑо кÑÑÑ Ð¾ ÑазÑабоÑке и...

habr.com

 

[handersen]

статьи/источники где можно почитать про символьное выполнение

Есть пара pdf на английском:

Enhancing Symbolic Execution with Veritesting http://**************************************************************/b/38IjchN88KkUPLQ5taoM8J

Techniques to facilitate symbolic execution of real-world programs http://**************************************************************/b/e8DWdRYj7a10H0nrtCEp