Diana Initiative 2021-Christina Johns-Work SMTer Not Harder - Concolic Execution for CTF

00:24 - And we’ll be having another session with another speaker today.

00:27 - So, thanks to the previous speaker. And first of all, going to the speaker track, I just wanted to thank our track sponsors.

00:36 - That is iNE eLearn Security, Axonius, MongoDB, Juniper Networks, Corelight, Google, We Hack Purple and BridgeCrew by Prisma Cloud.

00:48 - Very, very thankful to the sponsors for making it and making The Diana Initiative so big.

00:54 - So, today we have our speaker, Christina Johns who will be talking about Work SMTer Not Harder Concolic Execution for CTF.

01:04 - Christina Johns is a cybersecurity engineer at MIT RE with over 10 years of experience.

01:12 - She has worked in a variety of areas including web application assessment, Android forensics, incident response, and most recently she has started working on reverse engineering.

01:24 - Her research interests lie at the intersection of automating binary analysis and malware reverse engineering.

01:33 - She has started multiple intro to CTF workshops, volunteers with the Cyberjutsu girls academy and sharing her skills and helping other to do the same.

01:47 - Welcome, Christina, and good luck for your session.

01:52 - CHRISTINA: Thank you. Welcome, everyone.

01:55 - I’m Christina and I’m going to be talking about something that I think is cool, concolic execution and how it can be used to solve reverse CTF challenges.

02:09 - An overview of what we’re talking about today.

02:14 - A little bit about why use automation in the first place.

02:19 - And then we’re gonna talk about a specific automated analysis technique called concolic execution.

02:25 - And two technologies and tools that are useful for concolic execution.

02:32 - Angr, a binary analysis framework, and Z3, an SMT solver.

02:37 - You can think of an SMT solver as a tool that you can give an equation with unknown variables, and it will tell you if the equation is satisfiable.

02:46 - If it is, it will give you values for the variables.

02:50 - However, it’s possible it might not solve this in a reasonable time.

02:53 - That’s possible to keep in mind. We’ll then be applying these tools and techniques to three problems.

03:01 - They won’t be full walk throughs, because that would take too long.

03:04 - But we will be focus on how these tools specifically can help you solve the challenge.

03:11 - As you might have guessed, this is a pretty large topic.

03:15 - It could probably do multiple days, a deep dive into this.

03:20 - But the goal of this talk is to give you a foundation to explore this on your own.

03:26 - So, why automation? The simple answer is to get your flags faster so you can get more points so you can run the CTF.

03:38 - But even if that wasn’t your goal, some of the most difficult classes of reverse engineering challenges can require some sort of automation.

03:44 - So, it might be the scale of the problem. Each part of you might have hundreds of binaries to analyze, and each part might not be that complicated.

03:55 - But the sheer number of them is too much to do by hand.

03:58 - Or it could be there’s complex computation or obfuscation that is would be unreasonable to solve in a weekend if you didn’t do some sort of automation to help you out.

04:12 - So, concolic execution. Concolic execution is a portmanteau of symbolic and concrete execution.

04:20 - So, symbolic education execution is a software technology first explored in the ‘70s for software verification.

04:30 - In the early 2000s, there was renewed research in this area due to improvements and SMT solvers as well as additional computation power.

04:39 - Such that these techniques were more feasible than they were when they were originally proposed.

04:46 - So, concolic execution is one of these one of the results of this research.

04:55 - It is techniques to combine symbolic and concrete execution.

05:00 - And the reason for this is to enable strategies to overcome some of the challenges with pure symbolic execution.

05:06 - And we’ll talk about some of those a little bit later.

05:10 - So, here we have an example program. It takes some input.

05:15 - It has a few compares. And then it enters one of two states.

05:22 - And so, maybe we are really interested in the print foo state for whatever reason.

05:27 - Maybe that’s a bad outcome, we’re worried about it.

05:29 - We want to know what are the possible inputs that could lead to that state? So, some of the options we have for this would be to start trying random variables or values for X.

05:41 - So, just kind of blindly guessing. X maybe an exhaustive search so we knew what everybody we had tried.

05:49 - A third technique is symbolic execution which is what we’re gonna talk about.

05:56 - So, here we have the symbolic analysis tree drawn out for our example program.

06:05 - So, at the beginning, we’re going to say that the variable we care about, X, the input, is going to be symbolic.

06:13 - So, we’ll assign it to alpha. And then Y is assigned zero by program.

06:18 - So, you come to the first branch. If X is greater than 6, you take the true path.

06:23 - If it’s less, you take the false path. And the great thing about symbolic execution is that it analyzes both paths.

06:30 - So, with normal execution, you would have to test the value and then see which way you went.

06:37 - This way you can explore both simultaneously.

06:40 - So, if we take the true branch, we now have a state that alpha has to be greater than 6.

06:47 - Because that was the condition. And Y is now equal to 3.

06:50 - And the constraints to follow this path were that alpha was greater than 6.

06:55 - So, for our next branch statement we have X plus Y is equal to 9.

07:02 - So, now the true path says that our state remains the same.

07:08 - But we add an additional constraint that alpha plus Y is equal to 9.

07:13 - And so, we do that for all all the paths through the program.

07:17 - So, now when we we so, the state we were interested in was foo.

07:23 - So, we’re going to look at the specific state and constraint data for states where we print foo.

07:32 - So, for the first one, we can solve the we give the constraints to our SMT solver.

07:38 - And the SMT solver tell us that’s unsatisfiable.

07:41 - There is not a number that is greater than 6 that you can add to Y and get to 9.

07:48 - So, we know that it’s not possible to come down this path to get to foo.

07:55 - However, the other state, which prints foo, had alpha less than or equal to 6.

08:01 - And so, the SMT solver will tell us in order to satisfy the constraints for that state, alpha would have to be 6.

08:08 - Or 6 is one value, at least, that would get you to that path.

08:15 - So, this chart is not so much meant to be read.

08:20 - It’s from Wikipedia. It is the symbolic execution frameworks that are on Wikipedia.

08:27 - So, you can see there’s a lot of them. And a lot of them are open source.

08:31 - Which is really exciting. And we’re gonna talk specifically about one of them which is angr.

08:37 - So, oops. Sorry about that. So, an overview of angr.

08:47 - Angr is a Python open source binary analysis framework.

08:51 - It’s on GitHub. It was developed by UCSB as part of their 2016 DARPA Grand Challenge entry.

09:00 - The goal of the grand challenge was to create automated systems and find bugs and patch them.

09:06 - It has a large community with continued development and great documentation.

09:12 - So, it’s frequently updated, and they’ve taken, you know, something that’s pretty complicated to make and I think through their documentation they’ve made it about as understandable as you probably could.

09:24 - So, I’m a big fan. So, these are some of the components that make up angr.

09:31 - We’re gonna talk a little bit about. So, the project is the overarching structure that holds the analysis information.

09:39 - So, you give it the path to your binary and you’re going to be using it like throughout your analysis.

09:48 - CLE is the loader that loads your binary. It has multi architecture support.

09:56 - It stands for CLE Loads Everything. The solver, that we talked a little bit about SMT solvers.

10:05 - The library they use is Claripy. It looks similar to Z3 it uses Z3 in the backend.

10:14 - And it looks kind of similar to Z3’s Python interface.

10:19 - SimStates are how you look at and manipulate state data.

10:26 - So, for each basic block that you your analysis goes through, you can set and read memory information, registry information for that state and execution.

10:36 - And then the simulation manager is how you run your analysis.

10:41 - There’s multiple execution engines. One possible option is Unicorn which is a emulator which can speed up your analysis.

10:51 - And the other main execution engine is based on Vex.

10:58 - Which uses the Vex intermediate representation.

11:04 - So, diving in a little bit to the solver. So, this is what the syntax of the solver is gonna look like.

11:12 - You can create bit vectors. Which are concrete values.

11:20 - And you can also create symbolic vectors. So, that is really important for, you know, symbolic execution, right? The values that we want to solve for.

11:30 - We’re going to make symbolic vectors. Then you can create you can access the solver through your Claripy.

11:39 - And add constraints. That’s the equation part of what the constraints have to be for how your variables interact.

11:50 - And then you can ask Claripy to evaluate your symbolic variable.

11:55 - So, you know, you can ask it to give you a value that satisfies that equation or to tell you that it can’t.

12:05 - So, I mentioned Z3 a couple times. Z3 is an SMT solver, again.

12:11 - It was created by Microsoft Research. It’s the current solver in Claripy used by angr.

12:17 - It has its it uses a domain specific language.

12:22 - But it also has a lot of different language bindings.

12:26 - So, there is there are Python bindings so you can program it in Python which is really great.

12:33 - And it is also open source and on GitHub. So, it can be used on its own to solve certain problems which we’ll talk about also.

12:41 - So, like I mentioned, SimStates before. After you create your project, you want to create an entry state to begin your execution.

12:54 - So, this is sort of the beginning of what your program is.

12:59 - And so, to that first state, you can add constraints on the memory and registers to the solver that it can use as it does its analysis.

13:10 - This simulation engine, you pass the state that you want to explore.

13:16 - And there’s a few different options for exploration.

13:19 - So, you can step, which will advance you one basic walk at a time.

13:23 - You can ask it to explore and give it a find address or a find equation.

13:31 - Or you can tell it an equation or an address that you want to avoid.

13:36 - Or both. And there’s also an option to just tell it to run.

13:40 - So, it will run until it terminates. And like I mentioned before, Unicorn and Vex are part of the simulation engine.

13:50 - So, we’ve covered a little bit of the theory behind symbolic execution and some of the real specifics to using angr.

14:01 - So, now we’re going to talk about how you can get all the flags.

14:06 - So, a lot of reverse engineering CTF problems have this map nicely to the find/avoid construct.

14:16 - So, you you know, you take some input. It checks.

14:21 - It runs a function against that. It returns a result and then there’s an if statement of if it’s this thing, you win.

14:30 - Otherwise, try again, or no. So, you want to find the state that prints you win, and you want to avoid obviously, the state that says try again.

14:42 - You don’t want to try again. You just want the flag.

14:46 - So, this is an example from last year’s Diana CTF.

14:51 - I’ve pulled part of it out from the compiler.

14:56 - So, you can some RE on the challenge, and get the inputs and check the bytes against the array that it has.

15:07 - If something doesn’t match, it tells you nope! And if everything matches, you found the flag.

15:15 - So, we’re gonna use that with angr’s explorer functionality.

15:21 - So, to create our angr script, we’re gonna start with a project.

15:28 - And then we’re going to create this symbolic variable for our input.

15:33 - So, we’re using Claripy here to create a array of symbolic bytes for the length of the input.

15:44 - So, through reverse engineering we figured out this is how long our flag should be.

15:49 - We then concatenate that array together to create our flag input.

15:57 - And then we use the entry state to create the beginning of our challenge and then the arguments are for Linux the name of the binary and then this challenge takes a parameter as input.

16:13 - So, we put our symbolic input there. And we’re going to use the option to use angr, or to use Unicorn to speed up our analysis.

16:22 - So, now that we have the state created, we want to add constraints based on the information we know about the challenge.

16:32 - So, this will help angr solve it faster. It reduces this space that it has to search for an answer.

16:42 - So, we know, for example, that our flag is going to be printable characters.

16:47 - So, we can tell it that each of those bytes should be less than the top end of the ASCII range and greater than the bottom.

16:59 - And if it’s a CTF that has a really specific flag format, you could put constraints on the first few bytes to say it should match the flag format.

17:12 - So, to run the simulation, we have two options.

17:15 - We can use the explore functionality to give it the find the address of the flag print statement.

17:24 - And avoid the nope print statement. Or we can just say, I want to run the whole analysis and then now look at results afterwards.

17:32 - So, once it’s run, we want to get results. If you choose the explore strategy, you so, I should explain that the simulation manager as it’s running, it uses stashes to keep track of the states it has.

17:50 - So, it will have an active stash which are states that are still being explored.

17:55 - Or states to explore. A dead ended stash which are states that have reached the end of execution.

18:02 - And if you’re using explorer, it will have, it will put states into found or avoid.

18:08 - So, we can hopefully the CTF challenge only has one answer.

18:14 - So, you can look at the first found state and then use the solver to evaluate for each byte in our symbolic variable to get the flag.

18:24 - If you chose to use the run strategy, you can look through all of the dead ended states for the output that’s the flag.

18:35 - So, you want the state where you got to that that’s the flag statement and you can look for that and standard out.

18:43 - And then you would evaluate the same way, asking the solver to evaluate each character of the flag.

18:50 - So, to recap that challenge, the things you needed to find via reverse engineering for the challenge were the length of the flag and the address of the fail and win states or the successful print statement.

19:05 - So, you still have to do some REs. You don’t get out of all of it.

19:09 - But you do have to do maybe less. So, this challenge was from redpwn 2020.

19:21 - It took a flag as input using fgets. The length of the flag was 73 bytes and then it did a series of compares for each byte of the flag against the other characters in the flag itself.

19:34 - So, this is a small output of you can see it moves two different parts of the array into registers, compares them and jumps based on that comparison.

19:46 - And it was a little bit trickier in that this initial jump label was not always there was a second jump to the actual fail statement.

19:57 - So, you couldn’t just look you couldn’t just rename one of these fail and then like quickly see which way you wanted to do the compare.

20:08 - So, the name of the challenge was SMarT solver.

20:14 - Our script would look pretty similar, even though there’s the second jump, it’s similar to the first jump.

20:24 - There were two library calls in this challenge that were causing execution to take longer than was really feasible.

20:33 - So, one thing you can do if you know that you have one output or a simpler output for those library calls, is you can hook the library calls with angr.

20:44 - Is, we knew the length of the string we were giving it.

20:47 - And we knew that we were only going to give it alphanumeric characters.

20:51 - So, we could create hooks for these two functions so that they returned something quick.

20:59 - And speed up the analysis. So, an alternative solution and most of the write ups that I saw for this challenge used Z3.

21:10 - So, the challenge is this series of compares.

21:13 - So, it maps really nicely to Z3 constraints.

21:15 - However, you would probably still want to do some automation.

21:20 - Because there were around 5,000 compares. So, you’d probably want to automate parsing of compares and translating that into Z3 to in order to solve it.

21:34 - But it’s this is one that would be possible to do with Z3 and you wouldn’t have to use angr.

21:41 - So, what are some of the things you might ask yourself to decide do I want to try angr or Z3? So, if the binary has some properties which make angr challenging to use, like maybe lots of system calls or you can’t write a hook that simplifies them.

21:59 - Or if it’s written in a language that has a lot of runtime calls.

22:03 - Like maybe go arrest. That’s going to be really hard for angr to churn through.

22:07 - So, if it’s feasible to extract constraints like that, then if that’s fairly easy, then Z3 is probably the way to go.

22:20 - So, the last example challenge we’re gonna talk about is FLARE 2018 magic.

22:28 - So, in this example, we’re going to solve a we’re going to use angr to solve a sub component of the problem.

22:36 - So, a high level overview of this challenge.

22:40 - It was pretty complex. So, there’s lots of details I’m leaving out.

22:43 - But the input was broke into an 33 different pieces and each piece was passed to one of seven algorithms to check.

22:52 - And then the order of the algorithms was scrambled.

22:56 - And this was repeated 666 times. So, angr does have support for self modifying code through unicorn.

23:06 - But 666 of those might still be a lot. I’m not sure.

23:12 - I didn’t my attempts at solving it without breaking it out didn’t work.

23:16 - But maybe you could. So, it’s too large to just fire and forget.

23:21 - But can we divide the problem up? So, what I did was I extracted each algorithm while using a script.

23:31 - And then I asked angr to solve for each piece of the key for each algorithm.

23:37 - So, once you do that, the other 665 keys can be calculated.

23:43 - So, you only need it to solve that first key.

23:48 - So, the extracted programs are not full programs.

23:53 - They are just shellcode, right? Because they are called from within within program.

23:58 - But that’s not a problem. Angr has support for shellcode.

24:02 - So, you can load the shellcode into a project and then you can create a blank state.

24:10 - So, one option that is helpful is this zero fill unconstrained memory.

24:18 - So, if you know that you’re gonna have a lot of memory that, you know, there won’t be the setup code from regular program execution, this can really help speed things up if it’s okay for that not to be symbolic.

24:35 - So, the shellcode expected three arguments.

24:40 - So, one of those was our the part that it was checking.

24:45 - That we made symbolic. And then we used concrete variables for the two others that we knew.

24:56 - So, starting with a blank initial state, there’s going to be a lot that program expects.

25:04 - So, don’t necessarily try to read this. But it’s more to illustrate that you can store information in memory for the initial state.

25:13 - You can set registers. And if you’re doing something with shellcode.

25:17 - You might need to do that because you’re going to be missing context for program execution that shellcode expects.

25:25 - And then this was an example where there wasn’t there were multiple requirements for the find state.

25:36 - So, you can define a function that asks questions about the state of the program.

25:43 - So, have I returned from this function? So, this was the return address that I put on the stack so I can find it.

25:53 - And what are are there certain registers I care about? So, in this case, the return value of 1 indicated that it was successful.

26:01 - So, you can pass this function to explore’s find variable and it will find it for you.

26:11 - So, to summarize that challenge, we can use automation to extract for parts of code we need.

26:19 - And then we can solve for the key using angr.

26:21 - So, obviously, there’s still a lot of other work to do.

26:24 - It’s not a push button solution. But you didn’t have to this allowed you to not reimplement each of those seven algorithms and reverse those individual functions.

26:36 - And then there was a key scrambling algorithm.

26:40 - So, once you had the first key, if you reimplemented their key scrambling, you could get all of the keys, feed it back to the binary and get the flag.

26:50 - So, we’ve seen three examples with where symbolic execution, concolic execution really helped us out a lot.

26:59 - But it’s important to remember that there’s no silver bullet.

27:03 - There are challenges that you want to think about when you’re writing your scripts.

27:06 - So, path explosion where you create a lot of state really quickly is one.

27:13 - You might run out of resources. Laps and recursion are two things that can cause that to happen.

27:22 - So, you’ll want to watch for that. And just kind of, you know, anything you can think of to reduce the amount of state it’s gonna create.

27:30 - Any more constraints you can give to it is going to help it solve in a faster time.

27:36 - And then also library and system call modeling.

27:39 - There’s a lot they’re called Sim procedures.

27:41 - There’s a lot that come with angr. But sometimes they return symbolic variables.

27:48 - They can’t make assumptions about your program.

27:50 - So, if there’s stuff you know about program that you’re analyzing that you can tell angr, that’s going to help you out.

27:57 - So, in conclusion, concolic execution not just for academics.

28:03 - You too can use it to solve all the CTF problems faster.

28:10 - And maybe even some challenges that otherwise would have taken you way too long.

28:16 - But it’s important to remember, there are limitations.

28:18 - So, you know, you have to engineer around those.

28:25 - These are some resources. Angr’s documentation, like I mentioned before, is really good.

28:29 - So, there is a lot of it. So, it can be a little inundating.

28:33 - I recommend reading it in conjunction with looking at this CTF, the angr CTF.

28:39 - Angr CTF is I think really cool. It has a lot of scaffolding code.

28:44 - It’s meant for you to learn. So, it’s a great resource and reading about the reading about the components while you’re using them, you know, kind of helps reinforce that.

28:56 - And there’s also a Ghidra plugin out if for angr.

29:00 - So, that’s all. Thanks. I guess, are there any questions? SAMAN: Thank you so much, Christina.

29:13 - That was really, really amazing. And I really appreciated it, and I guess everyone here agreed that the mention of the code.

29:22 - Like showing off codes was really helpful. And really got a good hold of, you know, how and what can go around.

29:31 - Okay. So, the question we have here.

29:36 - You spoke about multiple exit criteria where you were looking for an exit from a library.

29:42 - Could you explain a little on this? CHRISTINA: So, I…

29:52 - I think the question is asking about the function I showed where I said there was it wasn’t just you wanted to get to an address.

29:58 - So, for in the first few I showed, just getting to a state where the address said you win meant that you got the flag.

30:08 - But there are cases like, for example, the shellcode that I was pulling out that it could exit, and I wouldn’t necessarily know if it was successful or not.

30:19 - So, I had to add another another value in there to say, was the return register, REX, was that equal to 1? Because that meant that it had been successful.

30:33 - Yeah, that would have been the case if there’s not a single state where you can say this was successful, then you might have to say, well, I know that I need this memory to be this value.

30:45 - Or I know that this return value should be there.

30:49 - So, that’s the case where you might want to define a function.

30:51 - SAMAN: Are thanks, Christina. I guess, Jaynie, that answers your question.

31:02 - I guess been getting a lot of appreciation pointers for you, Christina.

31:07 - CHRISTINA: I’m glad. If you think of a question later, feel free to reach out to me on the Diana Slack.

31:16 - Just my name, Christina Johns. SAMAN: Also, Christina, if you could just pin down those three links.

31:24 - I guess they’re really interested in having those three URLs that you just provided although the end.

31:31 - CHRISTINA: Yeah. SAMAN: And everyone, I’ve just shared along Christina’s Twitter handle and how you can connect back to her on Diana’s Slack.

31:50 - Okay. The URLs are in. Great, great.

32:05 - Okay. Jaynie, yes, it will be available on YouTube.

32:20 - You can check The Diana Initiative YouTube page.

32:23 - It will be later posted there. Apart from there, Christina, there’s just one more question.

32:30 - You talk about using CTF. So, what is some real world applications of SMT solvers? CHRISTINA: Yeah.

32:40 - SMTs solvers are used in software verification.

32:43 - So, I think that’s why Microsoft did the research, right? They wanted to make their code better.

32:50 - And the same with concolic execution frameworks or binary execution frameworks like angr.

32:56 - The DARPA Grand Challenge was for patching.

32:59 - That’s a really common use case. But any sort of binary analysis that you would want to do.

33:06 - There’s certain malware obfuscation techniques where it can help simplify a terrible looking static analysis situation.

33:19 - So, it can be used for that as well. SAMAN: Thanks, Christina.

33:28 - Hope, Steve, that answers your question. Okay.

33:34 - The URLs look fine. In that case, I guess, if there are any more issues, or any more questions regarding her session, you can connect back with Christina on Diana’s Slack.

33:51 - She’s readily available there and she can answer your questions there.

33:54 - And apart from that, I will just post a speaker survey over here for her.

34:00 - If you could go back and give a small feedback, that would be great.

34:06 - And apart from that, I encourage you to stop at the socials or expo halls.

34:12 - There’s some really amazing events going on there.

34:15 - So it will be really great for you all to be there and hang on there.

34:19 - You can network with people and attend a lot of sessions at the expo hall.

34:23 - Okay. Great time. CHRISTINA: Thanks so much! SAMAN: Yep.

34:29 - Thank you. Thanks, everyone!.