Cairo 1.0: Differences and Security Considerations

DeFi Security Summit 2023 · 15 Jul 2023 · 10:41

Justin Jacob, a security engineer at Trail of Bits, outlines what changed between Cairo 0 and Cairo 1.0 and what it means for security. Cairo 0 required manual memory handling and had no real types, no loops and unusual integer division, while Cairo 1.0 resembles Rust with strong types, traits and a Sierra intermediate representation. He notes that the native felt type is still not overflow safe, and introduces a new open source tool from Trail of Bits.

Speakers

Topics

From DeFi Security Summit 2023, hosted by DeFi Security Summit.

Transcript

okay uh so let's see all right hey everyone this is going to be a talk about the New Cairo version Cairo 1.0 we're going to outline some differences between the old Cairo you have some security considerations and also introduce our new open source tool so who am I my name is Justin I'm a security engineer here at trail of bits I'm interested in probably what everyone else is interested in D5 uh blockchain zero knowledge proof obviously interested in Cairo and starknet as well who is trail of bits uh well we helped secure some of the world's most targeted organizations to do this we also build a lot of Open Source tools you might have heard heard of them like Slither Medusa salsi select and yeah if you're

interested you can give anyone on the blockchain team of follow with the QR code so let's jump right into it uh I'm gonna give some background about Cairo first so what is Cairo if you haven't heard of it Cairo is a programming knowledge for a zero knowledge proofs and basically that just where approver wants to convince a verifier that some computation was done correctly and because of this it has a bunch of unique features like hints which basically means that the prover the guy who's trying to convince the verifier can put arbitrary uh input in the memory and the memory model is also unique you can think of it as being immutable once you write to a memory cell that memory cell can never be changed and so Cairo runs on the starknet blockchain so what is Stark net it's a ZK roll up that helps

to scale ethereum and you basically deploy code there and then it periodically every so often what will happen is batches of transactions will be upperfully generated and it'll be submitted to the ethereum L1 verifier so now that we've introduced that let's talk about the old Cairo version or Cairo zero point x here's a small example of you can that you can see of something called the Fibonacci sequence which most of you have heard about tldr it kind of sucks like you have to write to every memory cell manually you have there are no Loops so you kind of have to implement everything with recursion and basically there's no types so everything is this thing called a field element which is a felt 252 you don't have like you and 256 or anything and also the another caveat

is you have weird integer division so in Cairo there's this invariant x divided by y times y always equals x that will always hold so you don't have truncated integer Division and that's why you have really weird situations where something like 30 divided by 9 is this huge number because in modular arithmetic then variant x times y equals or x divided by y times y will always hold so now that we've outlined the hell that is Cairo zero point x let's move on to Cairo 1.0 and the tldr is basically now you're just writing rust so the memory model is completely abstracted away if you remember we had to write to the memory cell directly we did AP like AP equals something AP plus plus none of that anymore which is super super nice probably for every developer

also we don't need to update any pointers and we have nothing like uh tempvar or Alec locals which is probably one of the best like improvements in devex in a long time so also we have types so Cairo since it's like rust is strongly typed there's no more everything's a felt you have things like uh un-256 un 128 you size Etc uh one caveat that I'd like to mention is the native felt type is still there but it's not overflow safe the other types like un256 are also we have like abstract data types like in nums generics and we have traits which is actually like what the contract implementations use so here's an example of how you would write Cairo in you know uh Cairo 1.0 or the Fibonacci sequence it's just

literally rust so not much more to there we have things like pattern matching we don't have to implement the call trait it's basically a lot simpler and a lot better to write so how do we actually do these things while respecting the memory model because we need to still generate like a ZK proof right that's done entirely through the Sierra IR so the Sierra IR basically consists of uh it's the intermediate representation so previously we would compile directly from the low level higher language directly to this thing called Cairo assembly now we actually go through an intermediate step hence the name intermediate representation so we go from Cairo to the Sierra IR to Cairo assembly and this actually allows us to simplify the memory model and um one of the best things about the

Sierra IR is this thing called a linear type system so I'm not going to get too into it but the linear type system basically allows us to ensure that every object is used once and only once and it also uses like the rust memory model so basically there's no invalid references or D references we also the Sierra IR basically consists of type Generations or type declarations as you'll see and then these things called lib funks lib funks are basically the functions that are actually used in Sierra IR so I'll give you some examples of them later but the cool thing about lib funks is they generate rust code that's correct by construction so when you use a lib funk in the Sierra IR you'll always know that the a Cairo assembly generated will be valid another core difference between Cairo uh

the old Cairo Cairo 0.x and Cairo 1.0 is gas metering so previously we couldn't charge for any failed transactions because if you had a statement in Cairo that was like that led to it like assert false for example we it would lead to a sequence of constraints that are unsatisfiable and then we can't actually generate a ZK proof for it because we can't generate a ZK proof for it there's no way for the sequencer to include it in a block so basically the sequencer would lead to it would do free work and this is problematic because then you could just do us the sequencer by spamming a whole bunch of transactions that had unsatisfiable constraints but now what we would do is we basically would calculate the gas for every operation and we have this withdraw gas and Branch align lib funks that kind of

just syncs everything out another thing that is not mentioned in the slides is that every single Sierra code will basically generate branches so let's say you have something like assert false what would happen is in the previous Cairo version it would just lead to a strict revert and you couldn't include it in a block now the Sierra code will generate a branch it'll propagate get the error back to the main VM entry point and then the sequencer will basically be able to charge so this is pretty big because we prevent a really huge like dos opportunity so with all these things these three things combined we basically allow for a pretty Flawless Dev experience where you can you know just write rust like I'm sure most of you have been writing but we still have the same like low-level guarantees of the memory and respect the

memory model that Cairo does so here's a small example of like a Cairo program and I'm just gonna briefly go over the Sierra representation like we have the type declarations we have each of those lib funks and then we have their actual like what the lib funks do if you I'm not going to go into depth too much because of time but if you see you'll actually notice that on the right hand side once we reuse an Op brand like on the left hand side as an input we won't ever reuse that memory like that ID again and that's the linear type system so now that we've explored what the IR does there's a very important question to ask if that's it's security solved well let's look at this particular curious chiro contract that may or may

not have a bug in it well the answer is it does and even if you have like type safety and some memory guarantees you don't have logic errors so to do that uh to help developers find bugs in their code we open source this tool called caracal which is our static analysis tool and if you're on caracal on the previous contract I just showed you well it'll point out that there's a reentrancy in it so caracal is built on top of the Sierra IR we have some uh very we use some very common static analysis techniques like data flow analysis and uh analysis also we have um seven detectors so far so each of these detectors basically point out a common chiral vulnerability and will flag it obviously since we use static analysis it's somewhat conservative so we do

recommend that you go try Edge every single finding from caracal and use it in the same way that you would use Slither another uh core thing about caracal is if you use scarb it's really easy to use with the scarb directory you literally just would use it in the same same way that you'd run Slither or something on like a Foundry project so the dev experience is pretty good uh we also have two printer so we have a printer for the CFG the control flow graph and we also have a printer for the function called a graph and that might be really useful for just basically visualizing how your contracts actually interact and how the like functions flow to one another so are there any questions foreign yeah sure

so as you can see this is like actually if you look at the detector we call this re-entrancy benign because we don't actually read the variable before but we do write to it after so we have three re-entrancy detectors there's uh one re-entrancy which is you know you read from an external variable you do a external function call and then you write to the variable so that's like a pure re-entrancy this is re-entrancy benign because what we do is we don't read from the variable but then we write to it directly after and there's one reentrancy for events which is that if there's an external call it may just make the events out of order are there any bugs that solidity is susceptible to that Cairo is not um that's a good question actually I think like a mod the model is a lot

different there are a lot of bugs with like just like the way the evm works like for example like a lot there are a lot of like vulnerabilities that are common like just logic vulnerabilities like for example re-entrancy I think since solidity has a different model like specifically in yield for example there's a lot of bugs with like you know checking like return I think there's a talk before about like checking return data size those kinds of things Cairo now that we have there were a lot of uh different bugs before in the old version because we had things like for example the on the weird division that you know developers may not expect but now we more or less have like the same kind of logic vulnerabilities and it's not like the same I guess it's instead of having solidity vulnerabilities and it's more

like uh business logic vulnerabilities rather than logic in like the programming language itself if that makes sense [Music] box for New Cairo uh I think there is the Cairo playground like for 1.0 and but I'm for running caracal I think you just run it on your repo specifically I don't think we don't have like any sort of sandbox or caracal specifically but for Cairo 1.0 there should be a playground on the starknet like website yeah there will also be a remix plugin soon for your playground thank you thank you everyone for for

everything [Applause]