Transcript

Hello everyone. Today I’m gonna be talking about hacking OCaml. So OCaml is a programming language that we use a lot at Jane Street and today we’re gonna be taking a look at it from a different angle than people usually look at it. And namely, we’re gonna be looking under the covers at the runtime to understand what’s going on and try to do some exploitation where we break OCaml open and do things you’re not usually supposed to do.

So a little bit about me, on my day job, I work with GPUs and how to make neural net training models run really fast. And I also, outside of work, spend a bunch of time doing Capture the Flag hacking the competitions. And in particular I’ve spent a bunch of time at DEF CON CTF and have been fortunate enough with my team to win DEF CON six times over my time there. And those are the skills, those hacking skills that I’m gonna apply to sort of like my day job in OCaml today. So we’re gonna combine the two worlds and take a look under the covers at OCaml.

So, the context for this talk is a challenge that I wrote back in 2021 called “Secure OCaml Sandbox”. And the setup there is I sandboxed OCaml to make it harder for you to do things and I asked you to read a file. This is, you know, pretty easy to do in OCaml and the challenge is like how did I block this and how do you escape this sandbox that I’ve made for you?

And well, you might be asking, like, what is CTF? Like why would I write this kind of challenge? So CTF is this kind of hacking competition where your job is to get into some system and exfiltrate a string that is the flag. And so this is how you capture the flag. There’s lots of different kinds of things that you can do in a CTF. One of them is this binary exploitation. That’s gonna be the main topic of this talk, which is you’re trying to deeply understand the behavior of a particular binary or a particular application and expose some memory corruption or other kinds of bugs in that application and then use those bugs to exploit it.

There’s also lots of other kinds of challenges. There’s cryptography challenges where you’re trying to understand a crypto system and be able to decrypt something even though you don’t have the decryption key, or there’s web exploitation where you’re trying to find bugs in a web application and exploit those. Or there’s reverse engineering where you try to just deeply understand a system so that you can figure out its behavior without needing to like understand the source code. So I think these are a whole bunch of different interesting categories. Today we’re gonna be focusing primarily on binary exploitation.

And I guess another thing about this particular challenge and CTFs in general is they’re often about education where you’re trying to teach someone about a system or like get people exposure to the system. So in this case, OCaml, I’m trying to get more exposure to OCaml to understand how the runtime works. The point is not to be realistic. If you wanted to build a sandbox in real life, you would use something like NsJail or bwrap. You wouldn’t use my sandbox. But in general, it’s nice to have these sort of like slightly non-realistic challenges that are very good for educational purposes.

So the challenge itself, like I said, your goal is to read a file. I’ve blocked the file reading, file opening primitives. So how can you possibly read a file if you can’t even open it? And then I’ve also blocked a whole bunch of other bad functions that are inside OCaml. And these bad functions are things that break the soundness of the language.

So you might be asking, what do I mean by soundness? Well by soundness I mean when you write a program, it doesn’t do things that you didn’t ask it to do. That was like a lot of negatives. Basically I mean like the program only does the things that you asked it to do. And this is sort of intimately tied in with what does it mean when you ask a program to do something. And that’s like defined in the language semantics. So just sort of the base layer of like, what does it mean to program?

And I think in a lot of languages, they have semantics but they don’t cover all the cases. Like in particular languages like C, they just have this whole body of things that you can do that don’t have defined behavior. And this like undefined behavior is a big area where you can find bugs because anytime you enter into a region of undefined behavior, the compiler can do whatever it wants. The actual execution of the program can do whatever it wants. There’s no constraints on what should happen. And so if you happen to write a piece of code that like delves into that undefined semantics, you run into all sorts of issues.

This also ties intimately in with memory safety because the like memory abstraction is like a key component of being able to reason about your programs. And so if you are breaking out of the memory abstraction, then you get memory unsafety and that gives you lots and lots of bugs.

And in OCaml, the way that we think about the behavior of our program is through the type system. And so type safety is like the key component of the semantics of the language. When you look at a particular type, you know what the memory representation and the runtime representation of the values of that type are. And so then you can reason about your program. And so breaking that type safety is a classic way that you can break the soundness of the language.

So OCaml has a bunch of things embedded into it that make it easier to interoperate with things outside of OCaml. For example, the foreign function interface is like a classic thing where you want OCaml to interface with C, and at the boundary between OCaml and C, that like interface, like the semantics of OCaml don’t match the semantics of C. And so at the interface boundary, you’re just gonna run into all sorts of places that you can break soundness because you have that boundary between the languages. So the external FFI is like one of the things that I need to block because that is like a thing that will just like let you break soundness indiscriminately.

And then OCaml also has a whole bunch of other functions in it that allow you to break soundness. So we can take a little bit of a look at what the sandbox is in order to understand how we’re blocking these things.

So in OCaml, you have modules that describe lots and lots of values and we also have this thing where you’re able to shadow a thing, shadow values and shadow functions. And what that means is that you can override the definition of a particular function or a particular value and set it equal to something else. And so the challenge is set up as I have one big file that blocks a whole bunch of things from the standard library at, for example, these unsafe functions are just set to this blocked value. And what that means is that when you open the sos.ml, at the top of your OCaml file, you’re no longer able to access the original definition of the function. Instead you only can access the blocked, and in that way I prevent you from accessing a large class of these unsafe or these bad functions that are breaking the soundness of OCaml.

And then obviously I’ve also blocked the file reading primitives and, sorry, the file opening primitives. And in that way, the whole challenge is constructed. You have to open the sos.ml at the top of your file and then you can write arbitrary OCaml code and the challenge is set up such that you can upload your OCaml program and it will compile and run it for you and you have free reign of the system within that sort of sandbox where you weren’t able to access any of the unsafe functions. And your goal is to be able to get through that and figure out a way to break the soundness of OCaml and get out the flag even though I’ve blocked all of these like sort of easy versions.

And so the way that we’re gonna actually figure out how to do this challenge is by employing a thought process that’s commonly used in the hacking context. Your goal is to think adversarially and think about the ways in which the person who originally wrote the program didn’t anticipate their program would be used. And so I think this, like, this skill of looking carefully at the way things work and understanding the real behavior of the system as opposed to the intended behavior of the system and trying to find the gap between the real and the intended behavior, that’s where all the bugs are. That’s where you’re gonna find the juice to solve the challenge.

And that’s like actually a super useful skill outside of the CTF context. Like for example, when you’re reviewing code and you’re trying to make sure that the person who wrote the feature wrote a feature that actually does what you think it does, that is a place where this like adversarial mindset and thinking about the real behavior versus the intended behavior is super useful. And even more so now in the context of AI and LLMs where we have Claude writing all of our code for us, being able to like carefully reason and verify that the code does what you want it to do and not what you, like, code actually does what you want it to do and doesn’t do something else, like understanding the real behavior of the code versus like the intended behavior and like finding gaps there. I think in the context where we’re not writing all the code, this is like an even more important skill than it used to be because it used to be like when you wrote the code, you sort of wrote the right code but now the LLM is gonna write the code for you and so your job as like verification of the correctness of the code becomes even more important.

So using that mindset, I guess the first thing that we need to do is sort of understand the shape of our sandbox, understand what the challenge is actually asking us to do. So here are a selected subset of four of the functions that were blocked. And so we wanna take a look at these and sort of understand why these things were blocked.

So, open_in, that’s like pretty obvious why it’s blocked. So if you’re not familiar with OCaml syntax, what I have here on the left side is the name of the function that’s being blocked and on the right side the type of the function. So here, open_in, takes a string and returns an in_channel which is the thing that allows you to read files. So I blocked open_in because I don’t want you to open any files.

I’ve also blocked Sys.command because that is another way you can just sort of break open the soundness of OCaml. Sys.command allows you access to write code in bash, which is like an entirely different language. You’re no longer within the nice confines of OCaml, and it returns, it’s a string arrow in so the string is the command that you’re gonna run. Yeah, so clearly we need to block that.

Array.unsafe_set, well it has the word unsafe in its name so it kind of gives you an intuition that is not gonna be sound or safe. So, here what it allows us to do is it allows us to write arbitrarily out of bounds within the array so we can write on other memory that the OCaml memory model does not expect us to be writing into and just like be totally breaking soundness by writing out of bounds.

And finally Obj.magic, well that one is kind of like the essence of unsoundness. Like if you think about OCaml, the like foundation of thinking about the soundness of OCaml is thinking about the type system. And Obj.magic is just a tool that directly allows you to break the type system. So Obj.magic’s type is alpha arrow beta. That’s like the tick A arrow tick B. So what that means is it can take a value of any type and turn it into any other type. And when you’re reasoning about the type system, the types are telling you things about the shape of the values. So if you’re able to change the type of something to something else entirely, like the shape of the value is totally not gonna match what the type is telling you. And so all your reasoning about the correctness via reasoning about the types is gonna be totally wrong. And so obviously we need to block this.

So how can we actually solve this challenge? Well, one idea is maybe I just made a simple mistake. Like, maybe the challenge itself, you know, accidentally left in a, like, a sort of stupid cheese solution. And like I think this is a great thing to look for in general because sometimes the most obvious things are like the easiest path forwards. And this is again like a classic example of like the real behavior versus the intended behavior. Like the challenge is intended for you not to be able to do something like this, but the real behavior is you can access any function that’s not blocked. And so if you can find a place where there’s a function that just like allows you to open an in_channel, then you can just solve the challenge super quickly.

So how might we look for this? I’m gonna give you a second to think and think about how you might be able to look in and understand where the accidental hole might be.

Great, so to do that what we’re gonna do is we’re gonna pull open the source code of OCaml and do a little grep search throughout. So to do that I’ve got the source code of OCaml here which you can download by going to GitHub and just downloading the source code. And then what we can do here is we can just do a quick ripgrep search. So one thing that we might wanna look for is any functions that return an in_channel. So we can do that pretty easily. We just look for something that returns an in_channel and we probably want this to be only in the mli files. And we see that I failed to, yeah, do ripgrep correctly. And so we do this, we see there’s like a whole bunch of functions with in_channel and what we can do is cross-reference these functions that return in_channel with functions that are blocked by the sandbox. And if there are any functions that return in_channel that are not blocked by the sandbox, then we’re golden, and there’s just like not that many here so it’s pretty easy to check all of them.

Okay, so assuming that I did a reasonable job and I didn’t forget any of these, what are other ways that we can break this challenge? And so the next way that I want to like look into is like the intended way to look into it but I think this is just like the next obvious thing is looking for soundness bugs. And kind of the best place for soundness bugs is in this kind of, this thing called exceptional, that I called exceptional polymorphism where you have free betas or free like polymorphic variables coming, like the tick b coming out of thin air. And this can rise when you raise an exception because raising an exception also produces this like extra polymorphism. But if you have real behavior where you’re not raising an exception and transferring control flow, then that is like the sort of essence of unsoundness here. Like if we can find any function that produces an extra alpha, then immediately we’ve found like a solution to the challenge because that extra alpha is something that totally breaks it.

So we can look for this in a similar way. We want to go back to the standard library and we wanna do some grepping. I think the grepping is a little bit more difficult here because polymorphism appears not just inside of the functions that actually let us open a file. Like we can have ticks throughout the source code of the mlis and so we’re gonna have a little bit more stuff to check. But I think it will give us like a pretty reasonable set of things to like look into and it’s pretty easy to discard the things that are not reasonable.

So we can go in, do that ripgrep over the standard library and find some examples. And in fact when I do that, I find three things that all look pretty suspect. So here, Callback.register is a function that takes in a string and takes in an alpha and returns nothing. And if you think about this a little bit, at first it seems like it’s not gonna do anything too dangerous because, you know, it’s taking in an alpha, it’s not giving us back an alpha. So we can’t really do anything with that alpha that we’re putting in. But if you think about the name Callback.register, it’s gotta be registering it somewhere, and the person that is gonna be using the registered value has gotta have something where they look at the value that you put in but there were no constraints on the type of the value that you put in. And so if you put in a value different than the person who’s taking out the thing expects, then you’ve got a bug and that’s really bad.

The other two are like a little bit more obvious why they’re so bad. Stdlib.input_value takes an in_channel and returns an alpha. Like how can the in_channel possibly know what the right alpha to return is? That’s not encoded at runtime. Like it’s really easy for this Stdlib.input_value to just like give you back a totally different value than what you’re expecting. And that totally breaks soundness.

Similarly, Parsing.peek_val, instead of coming from an in-channel, it comes from a parser environment, but same idea. We’re returning an alpha out of nowhere. Like we didn’t have any way to like tell the runtime what alpha to produce. And so that’s like if we tell the runtime, I expect you to give me an int and the runtime parses from the in_channel and gets back a string. Like that int is gonna be expected to be a string and just like completely, there is no runtime checks in OCaml. Unlike other languages that are dynamically typed, there are no runtime checks. The runtime just proceeds directly ahead and will take the thing that it assumes is an int and use it like an int even though it’s a string or vice versa. And that can totally break this.

So this exceptional polymorphism is where we’re gonna look at stuff and I think all three of these are solutions that would enable us to solve the challenge. But I’m gonna go with Callback.register because that’s the one that I actually used.

So let’s take a look at what we can do with Callback.register. And to do that, what we need to do is go back to the standard library and co-open the definition and understand what’s going on inside of Callback.register. So let’s go back to the standard library and let’s look for callback.ml because Callback.register is defined in callback.ml. And so we can see here Callback.register calls Safe.register, and Safe.register calls register_named_value, and register_named_value is an external. And so that’s - at the point where we see that external, we know there’s something suspicious going on and we also see there’s an Obj.t which tells us that there’s something suspicious going on because anytime you’re going to an FFI, that’s a place where there could be unsafety.

So let’s look a little bit more and see if we can look at the runtime where caml_register_named_value is defined. So I’m gonna look for caml_register_named_value and I find it in callback.c which makes a lot of sense. And we can see that what’s happening is we’re doing a whole bunch of stuff to add things into this named_value_table.

Okay, so now that we’ve added stuff to the named_value_table, we need to understand where those things are actually used. So we can look for where the named_value_table is used and we can see that it’s used inside this function caml_named_value. So okay, now we need to find all the places that call caml_named_value because those are the places that the things that we registered are gonna be actually used.

So let’s look inside the runtime for uses of caml_named_value. Okay, you got a whole bunch of results. So there’s not that many. We could just go through and look at all of them. But some of them are a little bit more interesting than others. And in particular the one that seems really interesting to me is this function Printexc_handle_uncaught_exception. So, handle_uncaught_exception, you’re gonna see here we get this thing const value handle_uncaught_exception out of the register table. And then what do we do with it? Well we just call the function. caml_callback2 is a function that like does function call in OCaml. And so here, handle_uncaught_exception must be a function and it’s being called with two arguments, the exception and this extra Boolean value.

But this exception is the uncaught exception. And so that means it’s a thing that we as a user can control. We can raise any exception and not catch it. So we can control anything that’s being passed into this exception guy and that means that we can control what the argument to Printexc.handle_uncaught_exception is. But we can also control what the handle_uncaught_exception function is. So we control both the argument and the function and we can set them to be things of any type. So that gives us like kind of a lot of control, like we can just make it do something that it’s not supposed to do.

So let’s take a look at… Let’s take a look at one thing that we might be able to do which is just like, you know, using Callback.register to do something funky. So okay, we’ll do Callback.register with Printexc.handle_uncaught_exception and we’ll raise an exception, but we’ll treat that exception as an integer. So, we’re gonna raise an exception, catch it like in this handle_uncaught_exception, like an integer and then print it out. And this is gonna be like a completely reinterpretation like breaking the soundness of OCaml or treating an exception as an integer. And we’re gonna see what happens.

So let’s run this magic_callback1.exe and see what happens. All right, we’ve got a number and then we got a segmentation fault. And we saw a segmentation fault. That means we know we’re cooking, that means we’re like on the right track. And in order to turn this change where we’ve done the magic, we’ve converted an exception into an integer and the type checker didn’t complain. OCaml compiler thinks everything is fine but we’ve broken the soundness of the language. How do we turn that into an actual flat? Because if you think about it, our goal wasn’t to break the soundness of OCaml. That’s not the goal of the challenge. The goal of the challenge is to read a file. So how do we turn, we’ve broken the soundness of OCaml into reading a file?

And in order to be able to do that, we need to sort of dive under the covers, look deeply at the runtime, and understand what’s going on. And to do that, we’re gonna pull open our hacker’s toolbox and try to use some of the tools that I would normally use from binary exploitation to delve into the behavior of the runtime of OCaml.

And so the tools that I’m gonna be using today, I’m primarily gonna be doing dynamic analysis, which means analysis of the program while it’s running. And to do that, I’m gonna be using a tool GDB, which is the new debugger. It’s a great debugger, it has a lot of features, and on top of it I’m gonna be using PEDA, which is an extension to GDB that makes it a lot more user friendly and nice to use. I think there’s a lot of other good extensions that are more fully featured than PEDA. PEDA is nice because it’s a single Python file so it’s super easy to install but I also recommend Pwndbg as another tool. It’s like a more fully featured version of PEDA and it adds a whole bunch of nice features and gives you like Python, like really nice Python functions to call inside of your GDB session that make it much easier to debug. And so I commonly use Pwndbg when doing CTFs.

There’s also this whole other branch of analysis tools that are called static analysis tools that instead of looking at what the programs does as it’s running, you look at what the program does without running it. And these are super useful in context when you’re doing like malware analysis where the actual act of running the program is something that’s super scary and you don’t want to do. People commonly use things like Ghidra or IDA Pro or Binary Ninja in order to do this kind of static analysis, disassembling the program without actually running it. But today mostly we’re gonna be looking at GDB and looking at the program as it’s run.

So the first thing that we’re gonna do is try to dig under the covers of OCaml. And so to do that, I prepared some little samples, programs to just like take a peek under the hood. And so the first way we’re gonna that is, I’ve defined this function atxxx. That’s the identity function. It just takes in x and returns x and I’m gonna call this identity function with hello and I’m gonna compile and run this program. And what naming the function atxxx makes that function really easy to identify in the program’s output, sorry, in the program’s symbol table. And what that allows us to do is break on the right function.

So let me quickly try to look and see if I can find that symbol inside of the program. So like look at take_a_peek.exe and we’ll look for atxxx. And in fact we see it. It’s the super long name, but at the end we see the atxxx, and this is a function so that is something that we can break on.

So let’s gdb take_a_peek.exe and break on camlBin_prefix_block_sizing atxxx and then we’ll run the program. And here PEDA steps in and gives us a nice, like huge bit of information about where we’ve currently broken. So we’ve hit breakpoint 1 which is atxxx and then it also tells us a whole bunch of information about the stack and it tells us a whole bunch of information about what code we’re running and it tells us a whole bunch of information about the registers.

And so here, we can see that the first instruction that we’re gonna execute is move rax into rbx and then return. And so if you remember this was the identity function and so it takes in a value and returns that value. And so the fact that we’re doing move rax into rbx tells us that the return value has gotta be in rbx and the argument has gotta be in rax. And so using that information, we can go back and look at our registers and we see that rax is, well it’s this blue value and so blue means data just like how red means code and white means not data or code. And so we see this blue value that’s this data points to something and well that’s something is like, you know, H-E-L-L-O, so it is pointing to hello. So we see that rax does indeed contain the string hello. And in fact if we want to look at the string inside rax, we can and we see that it says hello.

So now we’ve gotten a little bit of understanding about what’s going on. A string is just like a pointer that points to the contents of that string. So that’s great, you made some progress.

The next thing that we wanna do is get a little bit more information about how the runtime works. And so what I’m gonna look at is many values all at once. And so here, what we have is again the same atxxx thing we had before, but instead of taking a single argument, I may take many arguments and then I return a tuple containing all of them. And what that will allow us to do is see a whole bunch of arguments at once. And so what I’m gonna use is I’m gonna use the atxxx to look at a bunch of integers to understand what the representation of integers is. I’m gonna look at a bunch of variants to understand what the representation of these variants are. And then I’m gonna look at, you know, an exception and a record and some tuples and get an idea of what the shape of exceptions and records are. And hopefully that will give us enough information to be able to use that Callback.register and exploit the challenge.

So let’s do it. Let’s dive in. So gdb many_values.exe and let’s see if we can get tab complete to save us and then we’ll run. And so the first thing that we need to do is we need to figure out where the arguments are stored, like which registers have which arguments. And so to do that, I’m gonna disassemble the function and we can take a look at everything that’s going on.

So what we’ll see is we have a bunch of like prologue and we have an epilogue, and in the middle, we have all of these mov QWORD pointers. And so what mov QWORD pointer is, is it’s moving one register into memory and we can see that there’s a sequence of moving registers into memory at successive addresses. And so first we use rax, then rbx, then rdi, and then rsi. And so because we’re storing a tuple of four elements, this kind of gives us the sense that the first argument is gonna be an rax, the second one rbx, then rdi and then rsi. And there’s also this one weird thing at the beginning at the address like eight bytes before the beginning of rax where we store this value and I’m not really sure what’s going on here, like why we’re storing that value there, but maybe it’s interesting and like so maybe there’s like something that occurs right before the tuple that tells the OCaml runtime, hey, this is a tuple.

So okay, let’s take a look at our registers. So remember the first argument is in rax and we see it’s 1. And then the second argument is in rbx and we see it’s 3 and I’m actually a little bit confused right now because I remember that in our code, the first argument was supposed to be 0, the second argument was supposed to be 1. Okay, and here we’re seeing 1 and 3. Well let’s keep going. rdi is 513 and it’s supposed to be 256 and rsi is this big thing and we can quickly jump over to Python to see what that actually corresponds to. 2,000,001 and it’s supposed to be one million.

So hmm. It seems like integers are not really represented in memory how they should be or how we expect them to be. It seems like they’re represented as 2x + 1 instead of just x. So that’s a little bit weird. Not really sure why that is but I guess we can just continue on knowing that that’s true.

So going back to the GDB. We can continue on and look at some other things. So we can look at variants. So remember that rax is the first argument. We see that it’s 1. And rbx is the second and we see that it’s 3. So it seems like the representation for 0 is the same as the representation for Foo and the representation for 1 is the same as the representation for Bar. So that’s kind of interesting.

Then we can continue on rdi, well that’s a pointer to 21 which kind of matches what we expect, and rsi is a pointer to 23 which kind of matches what we expect. So, you can take a look at rdi and rsi. So this is print out 10 giant words and they’re called giant words because, you know, they’re eight bytes and eight bytes is like a lot of bytes compared to back when GDB was originally written. So no, 10 giant words and we’re gonna look at rdi and remember that there was that header word or thing before that we saw when we were assembling the tuples. So maybe variants have that thing as well. So let’s look at rdi - 0x10 and rsi - 0x10 and we’ll see that, well rdi, this was the one that has 15 as the first thing and it also has this like 0x0700 guy before it. And then rsi has affects 17 as the first thing which matches what the argument value we expect and has this 0x0701 thing before it. So it seems like this 0100 thing is telling us like which variant to this, which is pretty interesting.

Okay, let’s continue on and look at the exception. Remember the thing that we’re looking for is an exception and then a record on some more tuples. So rax should have the exception and in fact we see rax is like a pointer to a pointer to a pointer that contains the string value. So it seems like this is probably the exception. Let’s take a look in more detail at it. So we can look at x/10gx rax - x10 and we’ll see it has this like 0b00 guy before, then it has this which remember is the pointer to the exception like tag or like telling you what kind of exception it is. And then we have the 5 which is the thing we expected, right? Because we were doing My_exn of 2. So this 5 totally makes sense. So it seems like the structure of an exception is first you have the header word, then you have the type of the exception, and then finally you end with like the contents of the exception.

So we can also look at what rbx is and remember rbx is a record. And so we can see, oh wow, the header word for a record and an exception is the same. That’s kind of interesting. And then inside the body of the record, we see, well the 7 that matches the 3. So the first field of the record and then the second field of the record is Bar. And if we in fact look at this as a string, we expect it to see a Bar. So great. So it seems like the representation of a record and an exception are kind of like the same.

So maybe we can use that to actually create Obj.magic which is like, you know, we’re trying to demonstrate that we have control over the language, we’re trying to demonstrate the essence of unsoundness. So let’s see if we can create Obj.magic using this thing, this like record versus exception correspondence.

And so to do that, we have a bunch of code here. So let me walk through what’s going on and you can like explain everything that’s going on here and how we’re creating Obj.magic. So the first thing is we’re gonna raise an exception and the body of that exception is gonna be an identity function, unit arrow unit. It’s like a function that does nothing, it just returns its argument. Great. So then, we’re gonna convert this exception object into a record object using the Callback.register trick. And the record object, if you remember the correspondence, the record has like the same representation as the exception except there’s that tag thing before. So here we’ve like represented a record field for the tag and then we have a record field for the body. And what’s gonna happen is the body of the exception is gonna be filled into the body field of the record. And here, I’m using some pretty special syntax. It’s alpha beta dot alpha arrow beta. All this means is my function is gonna be fully general. It’s gonna be able to take in any alpha and any beta when I use it. It’s just some special OCaml syntax.

So the plan is we’re gonna raise an exception E and fit it into like_e and that’s gonna give us this like super general body that like lets you do alpha to beta for any alpha and any beta, any two arbitrary types. So we Callback.register and we register that in handle_uncaught_exception, we’re gonna use the magic. And so using the magic is where we actually get to like do the Obj.magic stuff. And so this use of the magic takes in an argument of type like_e which is this record. And so first, we raise an exception E with the identity function, unit arrow unit identity function. And so that’s gonna get converted into this record like_e. And once I use_magic, we have the record like_e and we can access the body field and the body field has the Obj.magic function so we can convert true into an integer and we can convert hello into an integer. And so if everything works correctly, we’ll raise the exception. It’ll convert this identity function into the type conversion function and then we’ll be able to call it and use it arbitrarily.

So let’s try that out. magic_callback2.exe. Boom, so we see true is a 1 and we see that string is this like other random value and that kind of makes sense. We already saw that strings are pointers to their contents. So we expect this to be the pointer to hello and great. So now we’ve created Obj.magic. We’ve like fully demonstrated our power over OCaml, and sorry, I guess like maybe I forgot a little bit, but the point was not to demonstrate mastery over OCaml, the point was to read a file. So hang on, maybe we need to take another step back and like think about how we can actually read a file using this power.

So what do we wanna do? We wanna be able to read a file and maybe I’ll give you like a little bit of time to think about how can we use this unsoundness, this Obj.magic to turn something into being able to read a file.

Well, one idea we might have is what if we can just create an in_channel? We’ll like do Obj.magic and turn something into an in_channel and then we can pass that to like the file reading functions and then read the flag out? Unfortunately we can’t just magic something into an in_channel. An in_channel has some runtime representation. That’s great, but it also has this whole like OS component of like having a file descriptor stored in the kernel that describes here’s the file, this is the inode where the contents are, this is how you actually read that file and a whole bunch of like runtime code outside of OCaml for actually doing the reading. So we can’t Obj.magic something into an in_channel.

But the thing that we can do is maybe we can just call the function open_in. Like remember open_in was blocked. Like I prevented you from calling it, but maybe something else in the program calls open_in, and like maybe that code, that code that knows how to do the syscall to actually open the file still lives somewhere inside the binary. And if we have that code that calls that syscall, we can just call that syscall ourselves and take control over the program, open the file, read it, and then we’re done.

So how might we do that? Well, we can just like check to see if open_in still exists. So magic_callback2.exe is when we got the Obj.magic. Does open_in exist? Boom, okay, we’re actually kind of golden, like there’s like a lot of open_ins here. So here we see a function, open_in, Stdlib_open_in, exactly the thing that we want. It has some address. So I guess that means like we can totally do this, we can like totally jump to the code for open_in, but I guess the question is how do we jump to that code?

And in order to do that, we kind of need to understand closures because closures are the things that have function pointers and those are the things that we could Obj.magic into a closure. And then in executing that closure, we need to use that function pointer, and because we Obj.magic it, we totally controlled the memory representation of the closure and so that we control where we’re jumping. And so yeah, then we have like total control over the program.

So let’s take a look at closures. So same trick, atxxx, except this time, we’re gonna pass in a bunch of functions as the values and this way we can look and see what closures look like. So gdb closures.exe. Let’s break on a normal place. And run it. And so if you remember, all right let’s actually, let’s take a quick look. rax indeed still has the first argument and the first argument to the first call is just like a simple function that does x + 2. And so we can see if rax what rax has. And you’ll see that rax indeed is a pointer to code, and remember from before, red is code. And so we can see that the first thing inside of this rax pointer is a code pointer. And in fact, you can see the name f1yyy at rax, well, hang on a second. I thought we were adding 2, and I thought that in OCaml, integers were represented as 2x + 1. So two times two plus one is five, not four. But actually if you think about it, this function, so let’s disassemble f1yyy, it’s rax 4 and then ret. So if rax is an integer, it’s represented as 2x + 1. And what we wanna do is we wanna do two times x plus two plus one. So to do that we actually only need to add four, not five because that plus one, it’s linear. So that plus one is just gonna stick around. And this is actually gonna be important later because, well, I guess you’ll see. This will become important later.

Okay, so great. We kind of now understand the representation of closures. I guess we can look in more detail, we can look like rax - 0x10, we’ll see, okay, it’s got this other F7, maybe we can get by by just like turning it into a record and back and we can try it and see what happens. The first thing again is the code pointer. That’s great. Then there’s like some more stuff, like, I don’t really wanna think about all this stuff. Maybe we can just like say, oh, we’re turning it into a record, we modify the first field, and then, you know, we turn that back into a closure and then we’re good to go.

So let’s try it. How do we do it? exploit_callback. All right, so let me talk through this whole thing and recap the strategy for how we’re gonna do this exploit. So first we have an exception E. E as an identity function at this argument. So we’re gonna raise E and it’s gonna be caught by handle_uncaught_exception and it’s gonna be turned, this E exception is gonna be turned into the record like_e and that unit arrow unit function is gonna be turned into this Obj.magic function.

So once we have the Obj.magic function, we’re gonna be able to do more magic. So what we’re gonna do is we’re gonna take a closure that points to my function. A closure that calls my function and we’re gonna turn it into this alternate closure type where the first field is the function pointer and we’re gonna look at that as an integer. And what we’re gonna do is we’re gonna turn the closure of my function into the closure record. We’re gonna modify the function pointer to point to a better function, namely open_in, because that’s the thing that you’re trying to call. Then we’re gonna turn it back into, you know, a normal function and we’re gonna say it’s a string arrow in_channel. So that’s the type function that we want. We want to call open_in, we want a string arrow in_channel. So after we’ve done the modification, we turn it back into this function, then we just call it and we’re done.

So here, we’re just like modifying the function pointer, call it we’re done. So let’s try it out and see what happens. Oh man. Segfault and we did not get the flag. Okay, something’s wrong. Let’s take a look at exploit_callback_open.exe and let’s break. So if you think about what’s going on here, we’re doing Callback.register and we’re calling it to use_magic. So the place where like all the interesting stuff happens is inside of use_magic. So let’s break on use_magic. And run the program. Great, we hit use_magic so we can disassemble use_magic to see what all the code is and that’s kind of a lot of code but you can sort of like parse through what’s going on.

So if you remember the first argument to use_magic is gonna be that exception. And so here we see rax is being stored on the stack and then we’re pulling out something out of rax. And so this has gotta be the Obj.magic function. And so here we’re doing a call rdi and rdi is coming out of rbx and rbx is that thing we just read out of the first argument. So this has gotta be where we’re calling Obj.magic. So these calls have gotta be the calls to Obj.magic. And so that corresponds to this call to Obj.magic and this call to Obj.magic, this e.body call. So the next call that we see, this call has gotta be the one where we’re calling open_in because that’s the next call in this. So let’s step forward and look for when we’re actually doing that call. So here’s the first call to Obj.magic. Then here’s the second call to Obj.magic. And then here is the third call. So rdi is the function that we’re calling. So we expect rdi to be open_in. gc_events_suffix_string does not look like open_in.

Okay, so it seems like we got the wrong function address. We’re not calling the right place. So let’s double check that we made sure we got the right function addresses. So how do we do that? Well, we’ll do a readelf –syms on exploit_callback_open.exe. And first we wanna look for my function because that’s where we’re coming from, remember? So that address is where we’re coming from. So that’s the thing that we want to subtract. So here, replace the thing that we wanna subtract, and then we wanna look for open_in, and that’s the thing we want to add. Okay. Great.

Okay, so now we’ve tried again to fix the function pointer and let’s try running exploit_callback_open. Boom, got the flaw. So we just need to fix the function pointer. That was all. And so remember I said that that 2x + 1 thing was gonna be important. Well, if you look at the addresses of open_in, you’ll see that it ends in a 0. And so if we had tried to just write the address for open_in directly as an integer, we wouldn’t have been able to write in that address because we can only write odd numbers because everything is 2x + 1. But by using this trick where we’re like adding the difference of open_in and my function, we’re able to get around that restriction because like see, my function also ends in a 0. And so because these are both even their difference is even. And so adding the difference, well that difference doesn’t need the extra one and so OCaml just like blindly charges ahead assuming that everything is 2x + 1 but in actuality in this case it’s a 0 and so it just works out. So that’s how we’re able to solve the challenge.

You know, you can try the challenge yourself. You can go to archive.plaidctf.com and look at the challenge, download it yourself back from 2021. The original challenge is on a much older version of OCaml but I think it still should be pretty interesting and you can sort of like pull open and dig in and understand things.

There’s actually a bunch of other solutions to this challenge. So we looked at like one particular solution. We looked at one particular solution, but there’s actually a bunch of other things you can do. So we used a particular OCaml runtime API in order to break the soundness of OCaml, but there are soundness bugs directly in the compiler. Like when you have a really big and complicated language with lots of new features, it’s often really hard to make sure you’ve gotten all of the type system correct and sometimes little soundness bugs creep in. And so there are a couple of soundness bugs that have been fixed after people worked a bunch of time to fix them. But there are some that are still outstanding and these are other ways that even if I perfectly patched the standard library to get rid of Callback.registering, get rid of Stdlib.input_value and all the other functions, you would still have these remaining compiler bugs and those are ways that you can break soundness without thinking about the runtime itself. So I don’t know, I think that’s pretty cool that you have this like these compiler bugs that allow you to just like break open the language. Fortunately they’re not that many and the compiler devs are good at fixing them, but I think it’s pretty fun.

There’s also a bunch of other techniques that you could use for how to exploit it. So we use one technique where we modified a closure to point from some original function pointer to open_in function instead. But there’s other things that you can do. So when I originally wrote this challenge, the technique that I used was actually a little bit different. What I did was I wrote a bunch of shellcode. So that’s just like assembly instructions that are like very perfect, they’re very crafted to do exactly the behavior you want and I packed those into integer literals. And if you have integer literals, those integers will appear directly in the program text. And so by jumping directly to an integer literal, I can jump to arbitrarily controlled assembly. And this was like a little tricky because, you know, we had that 2x + 1 thing, remember? So if you want to have an integer literal in your program, then the integer is gonna be a little bit different than you expect. And also you only have 63 bits worth of data per integer literal. And so then you’re like sort of a little bit stuck and that’s really only like seven bytes worth of data and you also need the jump instruction. So it gets a little complicated but that is totally a technique you can use.

There’s also a whole bunch of other function pointers that exist in the runtime inside of glibc for example. Like there’s malloc hook and free hook, and though OCaml is one particular language, it also does refer to some of these other function pointers over the course of its execution. And so by overriding one of those other function pointers, you can also get control and then get control over the program and write the flag. But I think that’s a little bit trickier than the approach that we use today.

Finally, there’s this like totally wild other approach where you can load the flag into memory a bunch of times. And actually there is an API. The MD5 API that allows you to load the flag into memory a bunch of times to compute the MD5 sum of it. And because OCaml’s a garbage collected language, and if you, you know, do the appropriate things to tune your heap, you can actually leave those strings littered all across the heap that needs it from your file. And then all you need to do is have a carefully crafted string that spans the entirety of the heap. You know, you can control the memory. So you can change the length of the string to say, oh, actually my string is like 10 times longer than I said it was. And like look over the entire heap and then you can just leak out the flag. You don’t need to actually do anything, you don’t need to get code execution. All you need to do is load the flag into memory and link it. And so that’s another approach that someone solved, someone used to solve the challenge in the actual CTF and they have a writeup here you can take a look at.

So thank you so much for listening to this talk. Hope you enjoyed digging into OCaml and hope you learned something about how the runtime works and how you can use GDB to like take a peek under the covers of your favorite applications. Thanks.