How Type-Driven Development Can Turbocharge your Contract's Security - philogy

Transcript

Hello everyone. Thank you for coming to my talk. It's an honor to present for you and uh I'll be talking about uh smart contract design pattern which uh is called typed driven development. It's applicable elsewhere but I think it's very useful for smart contracts and uh I'm going to talk about it. Uh first the classic a little about myself just to give you some context about how and why I think about things the way I do. Um my name is Philip. I'm also known as Filigy online. I have almost five years experience working with smart contracts in various ways. I've done smart contract development for various DeFi protocols as a freelancer and for Sorella Labs for the past two years.

I've been an auditor uh both for Quanstamp and now Spearbit as a lead security researcher and I'm working on my own um EVM compiler full-time. Um when we write contracts the bar is very high, right? We need to write bugree code or die. It's a bit exaggerated, but the list of teams who have successfully survived a critical bug on chain is very small. And there's very great teams with with good funding that basically have to shut down because they made a mistake in their contract. So when we write contracts, we really have a high bar to clear. You know, anybody who writes any other kind of software knows that, you know, if you're talking about bug free software, that's like, you know, it's a unicorn

that doesn't exist. That's fantasy. But in DeFi, that's like all we have to do like every single day. We have to pull that off, right? So, but in the real world, we have constraints, right? We don't have infinite time to make our contracts perfect. Um, we have deadlines, we have schedules, we have projects, we have kind of partnership announcements, we only have uh so much budget allocated to audits. So, the reality is that our final contract quality or security depends on the resources we have, but also how efficiently we use those resources.

So we can either scale the resources or we can scale the productivity. And under this simple model, things that you might not intuitively expect to have a impact on security are actually quite important. Like for example, developer productivity. If you can improve just smart contract developer productivity by 30%. Then that's 30% that they can invest into testing. That's 30% they can invest into better designs or formal verification. Uh similarly, if you can make auditors more productive, that's more value you get out of your audits, etc. For another uh thing you might not immediately expect is like let's say you have like simple bugs that you usually catch anyway like later in testing or maybe even audits and you know like the lowhanging fruit that always gets found.

Um if you can find that stuff earlier and more easily that's also valuable like even though you would have found it later anyway the lower the cost to finding that and the sooner you find it uh the better for the final result. And then counterintuitively some things like for example a static analysis tool that has a very high false positive rate can actually be bad for security right even if it has a few good results like some some of the new AI tools if it's like 90% garbage the time you waste filtering that garbage is actually going to lead to you having a net worth contract right so this is kind of where type- driven development comes in it's a simple way how you can code and design your contracts that gives you productivity efficiency and like safety gains early on that can kind of compound found into

making your contract much better or more easily. So the highle concepts of typed driven development are the following. It's you want to leverage types as documentation. You want to leverage types as cheap static analysis. And you want to design your contract through types. And don't worry, I'm going to I'm going to explain and elaborate on these concepts. But the highle concept is really the compiler is your friend. And a compiler error is much better than an error at runtime while testing, which is much better than an error at runtime in production. Right? So types are basically a way a thing that you can leverage that the compiler already gives you, a thing that you already deal with every day, but you can leverage it more

to get to find out more about your contracts earlier. So let's dive into a case study. Easy recover. It's the pre-ompile that you use to recover a ser from a signature. No. Yeah. Signer from a signature. Um, and it's built into Solidity and it's built into the compiler. But if you think about the signature, this is roughly it. I hope you can see it. It's large enough. So, it accepts some parameters and then returns an address for the recovered signer. But for anyone here who codes contracts or audits, you know that there's a major foot gun that you always have to like think about and double check when you use this function, which is you have to remember to check that the recovered address is not address zero because solidity the way to inform you about an error in the signature

recovery is by returning like the sentinel value address zero. And this is kind of footnote footgun prone because if you don't check this then your code will basic basically assume it has a valid signature for address zero which can have all kind of weird consequences. And kind of the solution or the type- driven approach to making this better is you can very simply you can just swap out the return type. Right? If you imagine this is like actual code that's defined you can just define a custom type and have that be returned instead. And the great thing about this is that it's a very small change. Right? It's it's like not even one line and then maybe another line to actually define the type. And all of a sudden now the compiler at compile time for free is telling you about this foot gun, right?

And you made a simple change and now this is a thing that as a developer, as an auditor, you never have to think about again. You can actually forget it. It no longer has to be in tutorials or whatever. The API informs you about it. And if you extend a type, uh you can now make it very easy to use, right? You can unwrap it to say you want to revert if there's an error or you can check if it has an error and then handle it. And this is great because um it also serves as documentation, right? One of the principles before is like if you read the function, if you read this definition, you now very clearly see what happens, what it can do. Um now the compiler will also statically check this for you. And um yeah, you don't have to think about it anymore. Next uh case

study. Yeah, this is so you can imagine this custom type kind of encapsulates both the address value and like the error state. Um the next case study is doing math with units. So often in DeFi or finance, you'll have to deal with different currencies and converting between them. And they're technically all numbers, but the numbers mean different things. And if you have like code like this where you for example want to convert the value of one token and another using some price and you have two functions to do it based on the direction, um you want to make sure that you don't mix those up. But the function definition and the types, they don't tell you uh they don't tell you directly what goes with what. like if your naming is good and maybe documentation uh you can find it out but it's still very

footgun prone like when I use the function down there in the function do stuff you'll see that it's actually very easy to to mix these two up right I have amount in A and it's used here and here and actually I'm not meant to use amount A amount in A as the input to convert B to A right it's expecting B but there's nothing um nothing that tells me that this uh can happen so now as a developer and auditor at both stages you have to track and think about this and like okay I have to remember this is a mountain a anywhere it's used is it used correctly um etc even with the price you know it's also just aint um and it's also kind of poorly documented just for the parameter names so again solution is just implement a custom type very simple you

just define a type and now they're incompatible if you try to use it incorrectly like down here it'll give you a type error and at compile time which is the earliest possible place where you can get an error in fact um depending on how well it works you will even get the error in your editor before you even run Forge Build, which is extremely nice because again it's it's a simple thing that arguably you would eventually discover down the line anyway, but it's a thing you never have to think about again. Um, and it frees you up to think about the important things in your contract. And there's some boiler plate here related to the custom types. Um, but you know, it's a small price to pay I think for having like just not having to worry about this issue anymore. Another nice advantage of

this is we can leverage Solidity's uh function overloading to have it automatically choose the right function and simplify the naming. So instead of convert B to A and convert A to B, we just have convert and the right um method will be chosen automatically. Um the final case study I want to share with you is transfer ownership. So super typical you have a public function it accepts addresses and again you have this problem of address zero right you might get address zero and because of maybe like optimization you're using address zero to represent okay there is no owner actually more it was renounced so for that reason you don't want to accept address zero it's not a valid input so you want to check against it but if this is a library and you're implementing set owner you don't

actually know exactly whether people will check before they call set owner or should set owner check So, if you really want to be safe, uh, whoops. If you really want to be safe, you're going to you're going to be basically duplicating you're going to be duplicating the verification logic or you're going to be kind of optimizing and writing like a comment like, "Please check before you call this." And it's just not very robust. And again, it's it's a small detail, but it's a small detail you have to think about that uses up cognitive space and will make you uh slower development. So, again, very simply, same solution, you know, it's the hammer for all the nails. Make a custom type.

very simple. Here's define a custom type. And now it's very clear. If I read the function signature and I and I want to use this function in a library, I know exactly what the requirements are. It's documented there. And if I just try to pass in a normal address, the compiler will tell me, hey, an address is not a non-zero address. It's not the same thing. Please convert them first. Um, and again, same issues. It's like the inputs are not clear. And again, the solution is types. So as um as like um summary for when you will want to apply type- driven development is if you notice yourself documenting subtle requirements of your code in comments.

Um then you can use types instead and there'll be better documentation because you can think about documentation actually as code that's never run, right? It's never run, it's never tested, it's just text. And as you change your code, as you change your logic, it's very easier for documentation to be outdated. And in fact, um, even as an auditor, I often skip reading the documentation of the project because one, it it's often just bad. Two, often it's just out of date. M3 sometimes it'll it'll hide like implicit uh ideas from the developer that are actually wrong and will kind of trick me or trick my mind into thinking that these things are true about the code when they're maybe not. So most of the time I actually ignore documentation

like sometimes for complex assembly code it's nice to have documentation but yeah so types are nice because they actually test it. they're actually part of the interface and as an auditor they also help me they also help me know that okay I don't have to worry about a certain thing um anymore uh another uh tip for when to use type- driven development is when you want the caller of your function of your library even if it's just yourself uh to check or handle certain states right so errors is the primary example uh errors as values is I think a great pattern uh that you can leverage in your code um and then the next thing is if you're using the base types of solidity for similar but distinct concepts. Um so units is one example if you're dealing with different

currencies. Um a very simple stupid one is also like ranges like instead of U and 256 if your function is only meant to work with like values in the 32-bit range. Well then use a U and 32. That's like also a very simple example of typedriven development. So wait a minute. Did you spot the problem in one of the previous examples? There was a small issue hidden in there. Um uh raise your hand if you if you spotted it. If you think you spotted it, just just to make a survey of the crowd. Okay, if I pull up the specific example, do you see it now? Maybe raise your hand if you did. Okay, more people. More people. Good. Well, the issue is here.

Exactly. The custom type you define is address. And you put it in a public interface. But Solidity doesn't really understand that it's a custom type that has special properties. It just sees it as an alias for address. So when you're AI encoding decoding at the top level even if somebody calls it with address zero so that it will say hey it's an address that's fine that's what I expect and it'll create an instance of the non zero address type with the value address zero kind of breaking the thing that you wanted to achieve in the first place right so solidity has no way to magically oh magically infer that uh we were that it was meant to check against zero Right. And um this ends up creating like

a hole in like your nice safe um type environment. And in general when you're using type- driven development with Solidity, there's a few pitfalls you have to watch out for. I think it's a great pattern. And if you're programming outside of Solidity, um it's really nice to apply, but just watch out for a few things. is uh first users and the compiler can manually create your custom types and completely ignore any assumptions you make about them like the non-zero address situation. Then if you're using strrus which are different kind of custom type like a custom type that contain many fields um it's not zero cost like it actually has decent gas overhead in terms of always being allocated in memory. So that's something to watch out for. Also there's a lot of

repetitive boiler plate potentially. So that's also like a small pitfall, but I think it's usually worth it. Um, but yeah, that's another thing to watch out for. And then another thing is there's no standard library like the EC recover example that's built into solidity. And if you want to contribute to that as a developer or change it, you can't really do that. So you have to rely on third party libraries to kind of implement these patterns for the really like core stuff. So if we want to improve this um what can we do? Because if we think about all these like pitfalls um related to trying to do type- driven development, they're really like language level issues, right? So we have like two options. We can we can change the language or we can build our own.

So today I'd like to introduce or announce my new project called Sensei. And it's a new smart contract language for the EVM that I'm developing. And kind of the tagline or the goal is I want to help good devs write better EVM contracts. Right? So if if you're a noob that's going to get hacked anyway, then it might not be the language for you. But I really want to give I I really want to give like the I really want to give like the 80 percentile of devs that are like actually doing this professionally like better better tools to write nice contracts. So um for the language day one goals is I want fast compile times. This is the thing that everybody complains about solidity that I think is quite important is just fast compile times. The goal and this might seem a bit ambitious and I can explain

later if somebody's interested like why I think this is very feasible but the goal is worst case for the largest project at any time. I want the worst case uh uh compile time to be 500 milliseconds. And this is like um this is like a barrier that'll increasingly grow you know as the language gains adoption and the largest project becomes larger and larger as people build larger things like this will be like a continuously moving target. But I think this is a good goal to strive for and there's a lot of reasons to believe that this is extremely feasible and very achievable. The next thing is a standard library very basic like the language should just ship with all the basic things you need like out of the box. Uh and then the last thing uh that I think is also like kind of underrated is just

editor support. Like I want autocomplete to work. I want go to definition to work. I want to see errors in my editor and I want it to always work. Um then specifically related to type- driven development, I want encapsulation. So I want some better way to tell the compiler to tell users uh when I'm developing a library or writing my own code that hey you can't touch these fields or you can't touch these functions. These are only for me in the library and when you're using my thing, you only get to touch certain things. Another thing is for reducing boiler plate generics. And then last thing is I want the compiler to do better gas optimization. So you don't have to worry about inline assembly and gas golfing and all of that. So a lot of you when you hear this idea for a new language,

you'll ask the very valid question, why? Why do we need a new language? We have so many. Uh so what's the problem? Why don't you like them? um or why can't you just contribute to them and make them better? Uh so the first is solidity uh very popular um great language as it like bears most of DeFi but in terms of actually contributing to it to make it better and has a very large backlog of existing issues and I feel like it's a Kobe is very hard to get into furthermore the team is very conservative about changes partially rightfully so but I do believe there's there's space to move faster and I think that's an advantage of a new language is because you have no users at the beginning you can move extremely quickly you can leverage all the hindsight from the past 11 years And then once you get

the first users and you solidify the version like by that time you would have you would have already taken advantage of your faster velocity for a very long time to develop a lot of features. Um then there's Viper. Viper I think is also a very great language actually kind of underrated but their philosophy is kind of simplicity maximalism. like in terms of features that they want for the language, they want to keep it super simple, super readable, which is nice, but as soon as you want to build something more sophisticated, um I do feel like it's lacking a lot of features and components in the language to make it scalable to write larger contracts.

Um, another thing is they're building their own IR but alone and they're building it in kind of the silo in a way that's not reusable by other compilers. And not only do I think this is sad because I can't use their IR, but also because it means that other people like me who are building compilers will not contribute and they will basically miss out um on making their IR better than it could be. And then yeah, there's like basic features that I think are are missing. And then finally, there's core solidity. So I don't know what the logo was, so I just I just cooked something up here. But um uh basically um I think core solidity is great, but it's still a very early stage. Like I was just talking to some of the developers and it's still like a they say a a research

um research level like prototype that they have and they're soon going to start the production one but yeah it's not unclear how to contribute there and I'm I am also wondering like how long will it take to to ship it um because they have a very ambitious set of features. They're also still maintaining uh soul C. Um and also in terms of personal philosophy in terms of how to design a language, I think it's interesting to explore another uh part of the design space where you have a less complex type system uh but you make other features like uh compile time execution more powerful and then you kind of get the same capabilities but the actual implementation of the compiler and the theory becomes so much simpler. Um and then finally beyond just languages I think it'd be good in the

space to have more competition and personally I'm finding it really fun to develop compilers. So I think honestly just having fun uh doing what you do I think is also a very good reason uh to do things. So um how do you get your hands on this? It's not a real language yet. Sensei it's something that I'm actively developing but I want to get something into the hands of people very soon. So if you're interested I'm going to open a closed beta just to like curate the feedback and to make sure that I can do breaking changes very quickly without upsetting too many people. So, if you want to stay up to date with announcements or how the progress is going, um you can scan this QR code and uh join the Telegram channel. Um and then I'll inform you of like whatever developments I'm doing and then

eventually like send out an invite for people to join the the closed beta. All right. And yeah, uh thanks for listening. Um I hope I hope it wasn't too much. And yeah, please please ask questions. Thank you for giving me your attention. And um yeah, if if you have more like direct questions, you can also DM me on any of these uh platforms. Uh thank you so much. [applause] >> Thank you so much, Figy. Um great talk. It definitely puts a lot of things into perspective for ecosystem stakeholders and pushes everyone to refocus on um improving the ecosystem in general and

moving the language forward. Um questions for you. At what point does TDD become too much to do beforehand? >> Um yeah, I mean you can definitely get very nervous time go very deep. I think that's why the language being the language itself being a bit simpler is nice. Like there's some uh languages like theorem provers that give you extremely advanced type systems where you can ext where you can basically take TDD to its logical conclusion and formally verify everything using types. So in a way like like the examples I showed I think are very important like when you apply TDD it should kind of look like that like it should be small changes where you very cleanly communicate um communicate

requirements of your API and also in terms of modeling state um it shouldn't add overhead it should actually make things simpler and there's some stuff in solidity that's missing like some types um um that that make it very nice to like model your your state of the contract where TDD actually makes things simpler. where the sooner you do TDD the simpler it is but there's definitely cases where you can overdo it like for example this often happens in Rust code bases where you have like generics on generics and interfaces so it can be done too much um but that's the nice thing about solidity and hopefully sensei is that the type system is a bit simpler so there's only so much you can actually do >> thank you um these best practices are nice and can be implemented as a library

f uh framework for general use any intention to make one. >> Uh yeah, definitely. I mean, as I mentioned, Sensei will sip with a will ship with a standard library and when I write the standard library and when I accept contributions for the standard library, uh it'll focus on using TDD where where appropriate to make sure the APIs are nice. Like for example, easy recover out of the box in Sensei will will ship with like the API of address or error. So you never have to worry about that foot gun. And what are your thoughts on um languages like Solidity or Sensei being uh formally verifiable by default?

>> Um yeah, I think that's extremely important. Um that's also why I'm interested in building Sensei and having a simple type system is because the theory becomes much simpler. So if you want to formally verify it, the the mechanisms and theory of a language is simpler. So um yeah, I'm definitely in favor of that. And not really a question, but someone said um they they're curious whether you're open to collaboration because they're building a new compiler. >> Yes. >> So there's a few people building compilers. We actually have a group for this. Uh so if you're developing a compiler as well and and want to collaborate on IR on the actual language design, syntax, anything or just want to chat, uh just DM me. We have a group for um compiler developers who are building

like new EVM languages where we just chat and exchange ideas. So if you want to join that, just DM me and I'll invite you. >> I guess the next Dev Connect we should have a compiler conf. >> Yeah, absolutely. [laughter] Yeah. >> Okay, awesome. Uh, thank you so much, Phily, for your talk and answering all of the questions. That would be your time. Um, please give it up for amazing. Moving on to