Static Analysis for Zero-Knowledge Programming Languages

Transcript

so imagine that you're the engineer responsible for actually introducing these particular nasty vulnerability in your code base I'm flip and today I'm going to show you two static analysis tools that actually will probably prevent some of these vulnerabilities to show up in your code so I I'm actually a cryptographer at trailer bits and I really like programming languages and for those that don't know trailer beats where software security research and development firm and besides doing research in program

analysis and Engineering we also have an assurance practice which has a blockchain team we have an application security team and we also have the cryptography team where where I'm actually a part of and you probably have heard of some of these tools like Slither and echidna and today I'm going to present you two other tools uh that you could use in this particular code basis so as an overview of today's talk uh we're going to talk about this zero knowledge programming languages and before that we're actually gonna show you what zero knowledge proofs and these

languages are and the languages that we're going to talk about and the static analyzers are going to be Cairo and circum and just to get a sense of the room who has actually heard or programmed in Cairo or circum before all right quite a few people actually so what are Zealand knowledge proofs and what are these languages so zero knowledge proofs allow you to actually perfect about the execution of programs so I can actually for instance prove that I know some secret input to this program that

makes the program output some value output and this proof then I can give it to you and you can actually verify that I was being honest and I actually know the secret input that makes this program output this value and in a way this makes it a very if you need to verify some computation in your application this makes it a very scalable solution so you actually don't need to recompute the program you just need to verify the proof and this is a very simple and efficient task to do so the problem here now is that to be able to generate these proofs these

programs need to be actually encoded in let's say mathematical magic some some constraints and some polynomials and to help you actually do this we have this zero knowledge programming languages and you can see some examples of these languages on the right hand side we have some more basic ones like circum and lip snarks which basically make you write the circuits by hand and then they provide you a way to compile these circuits into the constraints themselves but now we're seeing some more high level programming languages which actually allow you to program in a natural way like you used to program let's say in python or JavaScript

so we get to this this place where we have this new programming Paradigm the languages are very young and most of them are a lot of design quirks and at the same time there are very few developer tools basically only syntax highlighting and this makes it so that development in these languages is very hard and testing even harder so you can really be sure about the code you're writing and as Auditors are trailer bits we also need tools to make our audits easier and find more bugs so we need tools that help us highlight potential vulnerable pieces of code and also to perform variant analysis

which is when we actually manually find a bug we want to make sure that all the rest of the code base is free from this bug so for this we need tools and there are no tools for the languages but still despite this these languages are actually being used to power a lot of services that handle millions and millions of dollars so there's two uh examples here the ydx and tornado cash and the y d x is powered by Cairo and tornado cash recently on the news is powered by circum and these are actually the two languages that we actually are building static analysis for tools for and you can see

here in the example I hope I hope it's readable but this was a burger in tornado cache a couple of years back where the developer actually used the wrong type of assignment so instead of using uh less than equal equals symbol he is just an equal symbol and this is the difference between actually enforcing a constraint on the system and not enforcing the constraint and it would make it so that you could Forge a proof and still funds basically this is a reasonable mistake to make since the language is not that easy to to use for someone

coming from a different language and that's why we need tools to prevent this type of mistakes so I'm going to start by presenting the static analyzer for Cairo programs but since a lot of people also don't know about Cairo I'm going to show you just a simple example and I hope you can read it fine but on the left hand side we have a library Cairo file and you can get a sense of the language so we have function definitions we can assign variables and function calls and we also have on a search so on the first function you you check that the caller and the owner is exactly the same

and then we have a mint internal function which will increase the balance by some amount of tokens and then the developer was actually kind enough to introduce this third function which is the test mean function he just used it to test on the right hand side we have the actual uh interface of the contract and there we import from this Library the two mint internal and assert owner function and then we have the external function the main function which will check that the owner is the same as the caller and then we'll call the mint internal function so can anyone actually find a bug or an issue in this code base yes

yes exactly so yarn knows a lot about Cairo as well so if you look here um this import statement means internal and assert owner it's importing these two functions right but actually this import statement also Imports this test function because of this particular decorator here and it it would make it so that this function is actually exposed in the contract and you could call it directly this is not obvious at all for someone that's coming from a regular programming language where Imports only

import what you're trying to import and because of this we actually need tools to to show you that there's these bugs so this is one of the vulnerabilities that amarna finds and so far we have implemented 14 detectors uh this implicit function import is detector number 12 but we also have more code quality and informational findings like unused arguments in functions or Imports that are never used that you can find um the compiler we used exactly the same parser as the Cairo compiler so we view the code exactly as the Cairo compiler

will review it and this allows us to since the tool is ours and we have the knowledge of how to use it we can actually easily write rules targeting a particular code base let's say I'm auditing a Cairo code base and I find this particular pattern I want to find the pattern repeated across the code base and the tool is also open source you can go check it out and try it in your project if you want uh there's also an amarna action so a GitHub action called the Marna action you can add it to your GitHub Pipeline and every time you push to the repo you'll get some warnings uh on GitHub

directly with the serif view showing that there are some new vulnerabilities being introduced and also it's very easy to use you can just pip install it and run it in your code base there's also a serif export so sorry if it's the standard file format to view static analysis results and you can usually visualize them in vs code so if here you have this function which has this variable a that's not used for anything and you'd get this message saying that you can remove this variable it's not needed so we plan to soon also build the vs code native extension so as you write your

Cairo code you get the findings straight away and directly in vs code instead of having to run this tool by hand and we also plan to introduce SSA and data flow analysis that would enable us to write more complex rules and also decrease the number of false positives that some of the rules still have and this is the static analysis tool that we've been building for Cairo programs but some of these problems and vulnerabilities happen pretty much in any language and that's why we're starting also this new static analysis tool for the circum language and this is called circumspect

so circum is a circuit compiler language and it's much more low level than Cairo so if you look on the right hand side you have this example of a circum program that actually ensures that the product of two numbers is the output of the program and you cannot write a much complex code but still as you saw with the tornado cash bug there's still a lot of problems that could arise in this language by by using this constraint enforcing uh the language will just output this R1 CS constraints these are actually what's

used in a different tool um to prove assertions about your program and just like Cairo there's very few tools for circum besides the compiler obviously and our tool is also written in Rust just like the circum compiler and we also use the circum parser to actually load the code Etc then we also have an intermediate representation already with SSA which allow us to do some basic data flow analysis and so far we have about six or seven detectors and the tool is not yet available but it will be soon available in the next couple weeks

on the right hand side we actually see this very large program but the interesting part is here at the end where this L out and E2 variables are actually never used in a constraint enforcement and this will also be caught by the circumspect because it will find that these variables are never used in a constraint and this is because the constraint here at the end uses n alt instead of using L alt variable so and currently we are focusing uh on finding issues that are not found by the compiler but if you actually use circum

I recommend you to always use this minus minus inspect flag otherwise the compiler will not tell you about some issues that you might have in your code and just like amarna circumspect can actually output results to the sorry file format which then you can use in your GitHub integration or just to view it in vs code and if you have a look here this is actually the result of running circumspect on the previous snippet of code and you see here that the the value assigned to L out is not used in a witness or a constraint generation and this would tell you that there's something wrong with the code I

need to check what's going on and now I have a mission for you which is actually to go and try amarna so just download it or prep install it and circumspect you expect you can expect it soon uh in the next couple weeks thank you for your time [Applause]