Modeling State Transitions to Find Unique Bugs

Transcript

Hello everyone. I'm Phil. Um I'm talking about modeling straight state transitions. Uh it will be it sounds different to everyone because uh it uses Excel which is much more of a finance tool than a dev tool. But anyways uh when we are auditing a protocol we must deeply understand uh state changing functions because that's where vulnerabilities leave. And this means understanding for example uh the step-by-step logic uh that each function does uh how it interacts with state what does it read and when and what does it write to the state and also what are what's the universe of valid arguments

that can be passed to each function and then uh this can be very complex and uh that complicity makes it hard for you to understand only in your what what's going on. But not only this, you can uh draw a diagram for example. Uh but then one limitation on that is that you cannot test uh it's it's difficult to test different inputs or different arguments. Um and then I have an example here. This is a a faucet uh that uh that hves a hing faucet that uh uh that h um that drops drips tokens hovering every year. And then uh it's a

function that only returns one output but this is the size of the function. So um the thing that I do to uh bypass that complexity is modeling uh the state changes on a spreadsheet. So this is uh a very simplified example of what that looks like. So uh on a horizontally uh I track the state uh so how it goes before the call and then after the call.

So this becomes the before that call and then after that call and down here I have a helper uh that I draw the stepby-step logic of it function and vertically as I said uh how each function call changes the state. I imagine that this might not be very helpful. So I have a uh a real uh a real world example. So this is that function that I showed and this is how I modeled this exact function uh uh on on a live protocol.

So uh this is this is the model and while I was uh building this model uh so I asked myself some questions. So this is a a hing faucet. So uh are the hing boundaries properly handled? So does it actually h every ear for example? And another one is are the unexpected timestamps properly handled because it's a hing faucet that hves every year. But what if it's not called uh any time inside of a year? Uh how will that uh how would that work on the following year? And it turns out that most of the things work correctly in this function. Uh but the second

question the answer is no. The unexpected timestamps uh are not properly handled. Uh so this is what happens and this is what I modeled uh I I modeled the entire uh the entire distribution of tokens and then on the last uh distribution if it's called with uh 12 seconds delay so uh on on mainet one block later than it should it uh it underflows and breaks the entire thing. So this is a protocol that introduced a faucet to uh incentivize the usage of the protocol.

Uh and then what would have happened if this bug hadn't been found uh was that by by the sixth year if the functions was not called exactly on that time stamp the entire protocol will be will be bricked. uh and I found this in a contest that with over 400 researchers uh uh participating uh and this was a unique bug. So for me this proves the value of of of doing this. Thank you. >> Very cool.