Pyrometer: A Next-Gen Solidity Security Tool With Brock Elmore

Hello everyone. Thank you for coming to my talk. I'll be presenting Pyrometer, a next-gen Solidity security tool. Little bit of intro. I am Brock Elmore.

I'm the chief architect at Nascent. Nascent's an early-stage venture firm. I am also a Public Goods fanboy, a Foundry core contributor. My Twitter is up there. My GitHub's up there.

Um and let's just jump in to what is Pyrometer. So, in general, Pyrometer is something that measures the heat of something without actually touching the material. And so, the analogy here is your contracts may be hot, and you don't want that hotness uh long-term. A hot contract is a buggy contract. So, Pyrometer is a Solidity security uh tool.

It'll eventually be language-agnostic, so it will be able to work across languages. Um and it uses something called abstract interpretation. Think symbolic execution light. And the demos I have in the slides here are simple by design. Um and in general, what the tool is trying to be is Slither on steroids.

I imagine everyone here is familiar with Slither. Uh an auditor's best friend, a dev's best friend, and blazing fast with hopefully IDE integration. So, you'll be able to run this as you're programming. At its core, uh Pyrometer is bound analysis. So, what bound analysis is is when you have variables in your contract, they will change over time throughout the uh contract.

And so, what are those range of values that a function can return that will be passed into another function? And those kinds of questions. And so, just a little bit of an example uh that's really hard to read. I apologize. Um but, you can see that there's a bunch of require statements and a bunch of math at the bottom here.

And so, if our if you were to ask any auditor, they would not be able to tell you what the bounds are on the return of this function. But, that can be very useful for a number of reasons. For example, for optimizations or um determining if there's going to be an unexpected overflow. And so, what my tool does, if we go to the next slide, is you can kind of see it on the slides here, but effectively, you have some function, and it has these inputs. And initially, those inputs are between uh 0 and 2 to the 256 - 1, right?

The max value of uint256. And as we step through the program, it updates. So, if you have a require y is greater than equal to 1, now that sets the minimum to 1, and the upper bound is still uint256 max. And as you go through, it continually updates. And so, you'll get to the math uh statements, and you start to see where this really comes to uh its power.

And so, at the end, you can tell, okay, this is between 0 and this 970-some thousand number. Um And so, this is what is happening at the core of Pyrometer. Is this very uh interesting range and bound analysis. So, what does that do? So, it actually allows us to build a ton of analyzers on top of that bound analysis.

So, you have an access control analyzer, which I'll demonstrate here in a minute. You can build a taint analyzer. So, are you checking all of the inputs of your function? You can have an invariant analyzer. So, what are, if I step back here, right?

So, c is equal to Z * Y, right? And I have it here concretized to 10,201, but under the hood, it's really just Z * Y. And so, you can actually build up invariants in terms of other variables and get a sense of what your contract is actually stating. You can do simple things like a reentrancy analyzer, and I talked talked about the optimization analyzer a little bit as well. Um but in this example, sorry.

In this example, right? You could do unchecked math on the A * B / C purely because you it already knows and it could recommend, "Hey, you can make this unchecked and save some gas." Also, you can ask it things like, "I want to write a particular um value to a storage variable." And it will tell you how you can do that. What inputs are required to reach that state.

And you can also ask it, "I want to execute this line of code. How can I get to that place?" So, let's dive into the access control analyzer. So, here's a very simple function uh or contract where you have some variable like my very secure variable. And this determines whether or not they can steal a billion dollars from your protocol or not.

And you have set var which has the require message.sender equals owner. But you also have this nested call where um you know, inner sneak it also sets my very secure variable. And so, what the tool can do is you can just ask it, "Hey, how can I write to my very secure variable?" And so, you can see at the very bottom here, right access of storage variable function set var if message.

sender is equal to owner is true. And then you have an unrestricted right access of storage variable my secure variable via function much sneak, right? And so, it'll a lot of the access control issues that we have today in Solidity will start to show their heads a lot sooner as you're developing. And so, these are very simple examples, but as your protocol grows in complexity, this will keep up with that complexity. It can do cross-function analysis.

It can do cross-contract analysis. So, if there was an external call here, it would be able to evaluate what's inside that external call and still proceed as you would expect. So, also, let's um This is a another relatively simple um contract here, but let's say you want to check if state one could be set to true. How How can that be done? And so, you can ask it, "Hey, I want state one equal to true."

And it will tell you uh yes, found storage right that could lead to the target value. And you see here this where statement, right? And so, this where statement actually comes from the conditionals inside of your contract. So, you see if B is less than three and if D is less than one. And if those both are true, then that variable will be set.

And it can very easily tell you this thing in less than a millisecond. Okay, I want to back up real quickly and just talk a little bit about the behind the scenes here. So, there are multiple types in Solidity and um each one of them have different ranges. And so, one thing you can expect as you start to explore this tool is, you know, uh if you see a uint128, it will have these bounds. Then you have address e um which is the full range.

Um and what's interesting about this method is that if I come back up to Sorry, this one. Um Right, this is all based on math, but it doesn't have to be, right? So, if you saw Polygon recently had a picked out a $2.2 million bounty. And that was because they have an EC recover function that when it EC recover can return the address zero.

And they had a transfer with sig, and so you could transfer unlimited Polygon MATIC from the zero address because of this. And I ran that program through Pyrometer, and it instantly showed that the bounds on the from was address zero. Okay. I also want to talk about conditionals cuz I think this is really cool. Um so, if you have an if statement, the way this program works is you you enter the function, then you come to a conditional.

And what happens behind the scenes is it actually forks the world. It It treats it as if in one case it's true, and the other it's false, right? And so, in this example, world one is where the true statement is, and so that bounds X between zero and nine. And in the other case that you know the bounds are from 10 to U and 256 max. And so, as you go along, regardless of the complexity of your program, you can tell what the bounds are despite any conditionals that you may have.

And all of this works on a graph IR. So, this is a little complicated, but it's really cool. So, you can actually visualize your Solidity program in this graph view. And so, this is sort of a what's called an SSA form, single uh single assignment, basically. Um and uh you can explore the control flow graph and how your variables change inside of the program.

Um So, let's see. Um so, I'm running pretty quick here. Sorry. Um but the release date is very soon. An alpha version will be out March 15th.

You can find it at github.com/nascentxyz. Um Nascent is incredible. They really support open source and they allow me to contribute to open source. Um and thank you.

Uh These are my Twitter uh information. Um I would love to answer questions on this. There's a whole bunch of things I didn't cover. Um but yeah. Any questions?

Yeah, Patrick. Yeah, so for dependencies, what it does it actually just um acts like anything else. So, if you have uh you know, if you're importing it it'll work like Foundry effectively where it'll read the foundry.toml. I plan to integrate Foundry and Hardhat dependency management.

So, um as you go through, it will basically bring it in and analyze all of the contracts actually in a project. And if you have let's say you have a just an interface versus the full contract as a dependency. If you have that contract as a dependency uh in your source files, it anytime you call a a function in those contracts, it will be able to evaluate the inside of that function call and apply that back. So, if you're doing taint analysis, right? If you have an just an interface, it will be the widest bounds because you don't know what that contract is going to do.

But if you actually have the contract in your repo, it'll evaluate the inside of that and actually have accurate bounds on the return of that uh function call. Yeah. You You mentioned that, for example, you can ask the tool uh when this state will be true or false, right? Yes. How do you make these questions?

As a developer, how am I going to make these questions? I can I can do a little demo here, but effectively, it's just a CLI. Um So, if I ask it, uh hopefully not leaking anything. Um But, so, if I save that, uh I can ask it right query state This is all it is. It's just cargo run uh you know, pyrometer.

You give it the the the file. You ask it for a right query state one. So, if I if I do that, then it tells me found storage uh value, and it gives me the the information D less than one, B less than three. Um and I'm still working on the CLI. Uh I can make this larger, but um I'm still working on the CLI.

Uh I will be opening this up and hope for contributors. So, if you are Rust aficionados, I would love to have you help. Yeah, Patrick. It It looks like it's doing like Solidity analysis to get the bounds, but then you have that part about uh IR, which makes me think, "Oh, do I have to compile with the via IR flag?" Or No, so, an IR is uh intermediate representation.

And so, I have my own intermediate representation. And so, this works on Solidity right now, right? And all I have to do to add another language is actually just uh convert that language into my IR. So, I could take Viper and convert it to into my IR, um as opposed to trying to convert it into ULIR or something like that. Yeah, does this do any like gas ranging like the difference between like hot and cold accesses?

Yeah, so um one thing I didn't cover in here and that's very intentional is uh for loops. So, for loops are very tricky for this kind of analysis. Um but my plan is I don't currently do gas analysis, but one trick I can do is in the EVM it's really interesting cuz you always know what's going to halt at some point because you have this metering functionality. And so, my plan is to actually do some basic gas estimation of what's going to happen inside of your contract. And so, with that you can actually put an upper bound on variables based just purely on the gas limit.

Um so, that hopefully that answers your question. Yeah, Matt. How does it handle calls if you don't know what's on the other side of that call? Right. So, with calls you fundamentally So, with raw calls I don't you just get bytes back, right?

Um and so, it just treats it as a any kind of byte max bound for bytes. Um but if you have the interface, then it will base it off of the the return of the interface. So, if it's returning a uint256, you know, it's going to be zero to the uint256 max. W- what maybe you mentioned CI or kind of a slither on steroids, what's a good first step for us to integrate into our CI pipelines to get started using the tool? Yeah, so um the plan is pretty much to focus on getting the CLI working correctly and then get a GitHub action.

Um I've never written a GitHub action myself. Uh so if any contributors want to help on that, that'd be an awesome contribution. Um and then kind of longer term, I want to actually have this It can basically act as a language server for Solidity in general. With this added hint stuff with the bound analysis in line. Um and so that's a little bit longer term.

Um additionally longer term, I want to add a query language. So if you recall in the uh there was that simple CLI for accessing um how do you write to this state, right? But you can actually abstract this into a query language so that if you want to write your own analyzers, it's just a relatively simple SQL-like statement into the the program. And that will be able you'll be able to write your own analyzers, and we'll be able to grow the the overall ecosystem of Pyrometer. And also on the future plans is if any of you guys are Foundry users, this is actually super useful for the fuzzer.

So the fuzzer right now it's it's basically random random number generation. What this does is it's informed random number generation, and we have all these interesting values associated with every step of the program. And so we'll be able to take those values that are spit out by the bound analysis, and use that to more intelligently generate fuzzing. And so Foundry should get a major uplift in their Foundry uh in their fuzzer performance as this gets integrated. Yeah.

Uh you can just Sorry. Yeah, I just had a quick question on the differences back to Slither and Mythril. Like obviously Slither notoriously spits out a bunch of false positives. So, trying to understand, you know, can we expect a ton less false positives, more accurate results? Yes.

Um so, thus far, I've not found any false positives. There is an element of the auditor needing to or the dev needing to understand, right? So, I brought up the Polygon example with the EC recover earlier. You would actually have to know currently that transform from address zero is a bad thing. Um but it at least tells you, right?

And so, it it puts that forefront. And it doesn't The bound analysis doesn't prescribe very much. It's the analyzers that are built on top. And so, I imagine each analyzer will actually have a different false positive rate, but in general, it should be pretty It'll be much more limited than uh Slither. Cool.

Well, that's all the time I have. Thank you very much.