Symbolic Execution and Program Analysis

okay the next speaker is also a friend of mine um he's also just as a child's we've also work together for on quite a number of projects and I know many of you know him he's a bit noisy especially on Twitter so um I won't say much about him I'm going to introduce Trevor who's coming to not just below some fuses in our brains but she's going to talk about some complicated stuff which I should be taking a seat so that I can also gather as much as I can so let's hope welcome Trevor somebody

[Applause] and what's importance is presentation will be for you all so I made with this topic because of the body interests of doing reverse engineering and at school development it was inspired by an actual CTF I played a while ago and an amazing writer I came acrossed by my good friends in Black robots so I did more research about it ended up planning a lot we'll talk about a real life example I'm going to discuss a concept of execution Parts take you through the first demo talk about the problems of symbolic executions that bring you to the final demo that showcases how to get around the same problem so if you have your laptops be prepared to get your

hands dirty if you want to code along with me so what is the symbolic execution does anyone from the audience have actually I try to make this interactive in busy what the answer questions Okay so symbolic execution is a method of testing problems where instead of supplying normal inputs we give the program symbolic inputs that represent arbitrary values my sound might sound a bit convoluted but let's think of it like this symbolic inputs these symbolic inputs that I'm talking about are like abstract values like variables uh so what essentially mean is that we look at inputs as abstract values like X Phi Lambda Sigma another way to think of it is basic algebra take you back to

class four five you can have a simple equation x plus 4 equals to eight there are several ways of solving this equation if you are to solve it statically we can say let's iterate through all the values of x [Music] each [Music] but there's another more efficient method of solving for x we can rearrange the equation and solve for x see something like x equals to H over so it gives you before and the satisfying the equation so in symbolic execution X is going to represent our symbol and this particular symbol is bounded by what we call an execution path so it can Road may follow that is going to take us eight we we have x x is going to equal some

particular value and this value is going to lead us to our output which approach [Music] so that's what symbolic execution does to us it walks us through the various execution paths that will lead to our output [Music] so what about the second example x squared plus 6X plus 18 equals to 12. if we try to go through all the values of x we start with one we start with two we start in three we go on we might probably take millions of uh hours to solve this equation it will be feasible because we are doing it again it started coming uh join talked about static analysis of code there's a question I wanted to ask

how about I saved it for this session and you'll see what I mean in the next slides so this is an example of a static way of testing code where we provide the input values ourselves so if you've used python before JavaScript whichever languages we have this uh Assad almost equal you can say anything can search before and what it does is it's going to compare uh you can see here we have two eight so basically a cuboid volume it's a function and that's something probably calculates the cube of functions or maybe by the area of a cube so if it was a function it takes two values the top I mean as parameters we are going to supply them

as a two date in our self-watch as such almost equal and you're going to test this particular function and see if in this case as such organization is going to check if these two values are almost equal so we are testing statically we are providing the input values ourselves that's that static testing

so we now have a general idea of what symbolic Constitution is we are not providing inputs to programs rather we are going to solve them symbolically we are going to analyze the various execution paths that programs have uh we'll see we'll see this uh in a couple of slides later and uh let's go on to why this topic is important so for a fact as a Alfred mentioned we have thousands possibly millions of problems being created every day we use these programs to solve problems on a daily basis with help for computers but to actually solve problems well we need reliable problems right so there is an unscale introduction of programs for fact and manual static

analysis may be invisible if you're dealing with millions of lines of code it might be hard to test manually giving inputs check the outputs and generalize and maybe say for positive integers this is the output we expect but what if instead of analyzing the inputs we analyze execution paths and again I'll show you what execution parts are execution parts are basically I can say that basically like roads that are going to lead you to various destinations destinations could be an output of a problem if we analyze these parts we can infer how programs are going to behave and make techniques like debugging reverse engineering easier [Music] so an example of this destination of angle that we may want to achieve is

finding a part of code that is going to violate uh unexpected output let's say I have a function that is going to really perform some mathematical operations and I made an internal writing report that uh doesn't account for a division by zero it may be hard to test this manually using a such such a method going through uh maybe negative values uh positive values integers and so on and so forth instead you can analyze execution parts and see if you make no sense the later slides so I have an example here where in the year 2014 we had a famous bank and this is a block of code that caused the bug I give you one or

two minutes to tell me where the body is and what it might cause and if you get to church and I have a lot for you yeah okay if you look at the approach is the second go-to thing these ones that are clearly highlighted for you go to failing this second go to fail what it does is [Music] it's always going to be executed whether the function fails or it passes so what that means is all this code that is here the important code that is going to be skipped this is this was in the Apple the SSL implementation in 2014 where uh we don't know if it was an intentional uh mistake done by developer but it has

very serious implications because if this SSL row verify is skipped that means we can't effectively verify the cell certificates and an attacker can craft an editing a certificate create a malicious website and orchestrate and social engineering attack like what was happening with Uber so one of the key applications of symbolic execution is to catch programming errors so you talked about uh sneak and code ql and the various implementations that are there but uh for symbolic execution what we are going to do is we're going to automatically discover this this Azure how we have various functions think of the functions like States if this SSL row verify is a state and we can analyze the execution path that takes us to this

state and figure out that we actually can't reach this stage then you can be you can begin to look for why why confuses State and if you go back there you figure out that you go to fail it keeps all this and we can't see some states in the program that's what symbolic execution is going to help us with

so I've mentioned a lot about execution Parts an Institutional part is how you travel as a program teacher Union stage whereas they explained us before a stage could be an output that we want it could be a successful returning from a function and so on and so forth you have this simple instruction it's a python pseudo code with a Python program that asks us for an input and prints either success or try again so if we were to break it down in terms of execution paths we'll have two execution parts success and try again for we have a stage that will take us to try again we don't need to take us to success so the input that we are talking

about is going to be a symbolic value Supply let's say uh past 123 in this case to look at it in terms of symbols the input will be a symbol and it's going to represent our input valuable so in this execution path we arriving at success and what the various libraries that I'm going to introduce you will do it will work us back and try to figure out using some very complex operations what inputs will consider this particular execution path but I've slowly attribute a trivial example but what about this example here I don't know if the code is a is eligible but the first lines of the code are very complex mathematical operations into some sheets some excels and watch

not if I asked you to reverse this by having telling me what the input will be between probably be very difficult for you might not get the answer but this can be represented in terms of execution paths in the various states that we are trying to reach to and if we have a if you have the appropriate tools we can try and backtrack and figure out what the input is so for the assume in this example our input is also represented by Lambda and to find this value of Lambda they say we walk back our execution path is in very complex techniques an example of this complex complex techniques is called the satisfability modular Theory or

receptive this is a core that drives the Z3 tool if you've ever used it before it's basically proving that mathematical formulas are satisfied so now connect the dots with this and the algebra example that I I showed you while we are trying to prove that X plus 4 equals eight we are trying to satisfy the equation so if it were more complicated we are going to introduce things like the smt theories that works back and does the various calculations for us and a good thing is that we have tools that abstract this smt solving methods such as anger so we don't have to like figure out ourselves what is happening behind the screens anger is a binary

analysis framework I'm sure if in case it yes how many reversing probably heard of this it's a binary analysis framework that is based on a suit of for example three libraries that allow you to carry various execution tasks like [Music] so the various tasks like static and symbolic execution or analysis of problems so the interest to which is here now we are going to we're going to get our hands dirty our lab is going to be based on binaries provided to us by the guys that commit anger okay [Music]