Can we formally verify implementations of cryptographic libraries like the c-kzg lib... | Devcon SEA

[Music] thank you very much uh I am tanyan and uh I'm now going to uh tell you whether we can formally verify implementations of cryptographic libraries like the ckg library this is a CH work between me the team and Roberto santin so we all know that cryptography plays an important role in the ecosystem and uh it has a lot of applications like identification or signature uh however the implementation is very challenging you can see on the slide multiple attack techniques on some common libraries and uh we don't want similar but things happen to the ecosystem the ethereum ecosystem and uh how can we do that a typical approach is to use and uh formal methods to formul reasoning about the cryptographic algorithms in both the design and implementation and this is very active research area in the last decades and uh many Frameworks have been introduced uh for example we have ripto of fosa and others and now I'm going to show you a running example example the ckg library which is uh used a lot in the EIP 4844 so this library has a SP specification but its implementation is done in C so a natural question is that how can we ensure that the implementation correctly follows the specification and finding a solution is very challenging because those languages Python and C are not closed and the C implementation has a lot of optimization uh that is not included in the specification so here is our solution we uh apply a framework called crypto and um first you can see that we manually translate the Bon specification into the ripto specification and then we generate a test suit to check the equivalence between them then we automatically generate an lvm implementation for this library and then uh finally we conduct a form approve to show that the lvm implementation correctly follows the crypto specification that is the general picture and I'm going to show you more details so uh we already finished writing a crypto specification for the library so here you can see on the slide that is the specification for a function comput kg proof and you can see that the syntax uh of rpto is similar to programming functional programming and uh is readable uh we also have test cases to show the equivalence between the python specifications and the scripto functions for example that the compute K proof and finally we already formally conduct approv for some C functions like bit reverse permutation okay we are going to the end so in this talk I have presented how we apply foral verification to Reon about rography and um the QR code is about uh our GitHub ritory on our work on the CK GG Library so if you are interested I'm happy to discuss more and uh you can find me on telegram or Twitter my handle is there is my name hanyon and that's all thank you for listening uh thank you very much for your talk and um I have a quick question how did you start your journey journey in formal verification how question from me yeah yeah how did you start a you know journey in formal verification okay um how did you start working on formal verification what is your background ah okay my background okay um a few years ago I uh started my uh pit the into UA and I develop a moto cheer for t plus and then I uh join consensus to uh apply mod verification technique to uh blockchain protocols like D or like the uh SEC Library yeah yeah thank you very much and uh do you have any other questions no I think we're also running out of time so we will take a short break uh three three minutes and start with the next lightning uh session thank you yeah thank you very