(p.ost2.fyi) Reverse Engineering 3201: Symbolic Analysis | OpenSecurityTraining2

ROAM_REFS: https://p.ost2.fyi/courses/course-v1:OpenSecurityTraining2+RE3201_symexec+2021_V1/

An online course on SMT solvers for symbolic analysis of programs.

From the course description:

Symbolic execution is a way to analyze a program and determine which inputs (or input groups) cause which specific part of a program to execute. To do so, symbolic execution uses symbolic values instead of regular input values. This allows to construct a result that can be expressed as an equation (or a system of equations) of these symbolic values, and can be solved mathematically. This is where the SMT (satisfiability modulo theories) enters in play, and using all the different constraints, is able to say if there is a solution to our equation, and if so, which one.

Local Graph

org-roam e439a66c-7a3f-4e70-9032-9f1191c713d4 (p.ost2.fyi) Reverse Engineering 3201... 6dc0e86e-3016-4a1e-987a-569f934e9ca1 Satisfiability Modulo Theories (SMT) e439a66c-7a3f-4e70-9032-9f1191c713d4->6dc0e86e-3016-4a1e-987a-569f934e9ca1 //en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories e439a66c-7a3f-4e70-9032-9f1191c713d4->//en.wikipedia.org/wiki/Satisfiability_modulo_theories bb33845d-4e20-4244-9aeb-b9e492a815d3 (x.com) faulty *ptrrr (@0x_shaq) on T... bb33845d-4e20-4244-9aeb-b9e492a815d3->e439a66c-7a3f-4e70-9032-9f1191c713d4