EthCC 2: Josselin Feist

[Applause] okay hi everyone thank you for attending to this presentation on sweeter so briefly why my my name is just no Feist I'm a security researcher at 12 bit if you don't know my company will security oriented company we work on blood-shod project since two or three years by now and we research and development focus we build a lot of tool on the YouTube ecosystem to help you to build a safer software including maanteeeca Akina or a display so the goal of this presentation is to discover what is filter how it works what kind of application you can have on top as little and how you can use it so filter is a static analysis framework for solidity it has four main use case the detection of vulnerability the detection of optimization the help to review and to understand Kurds through visual representation and finally as a generic static analysis framework it it allows to perform it it allows to build static analysis on top of its curve so it's pencils and you can install it full pipe it has almost no dependency so how's the high-level overview the way sceeto works is that it takes very stiff from the compiler it will cover a lot of information from his ice-t if we tell the 3dt expression and convert this expression to its own intermediate representation which is called sweetie we will go through this presentation on what is retail and how does it work from all this information sweetie L will perform a set of inbuilt analysis to give which information about the contract from all this information it's given to all the different usage of theta such as Azran up detection or the optimization detection so the first use care of theta is to detect vulnerability within the tool there are something like 13 public lab detector so sweet talk and detect really critical issues charger 120 of the shadowing of variable to medium severity severity issue two more informational one such as issue with a naming convention or issue when you are using an old version of 3d theater so if you want sweeter on a card base so in this example we have a small piece of card you have an issue because you use an address and you send easier to decide ways but you never assign desirable so basically if you call this contract you would just send all the analogous contract to the advisable if you want sweeter on this contract at all we detect the viable which is not initialized it will tell you at line of four there is an issue because this value business adult and we tell you when and where it's used for each burg you ever saw a reference and if you go to the reference you have a full description of the bug what it is why it's bad and how you can prevent to have this kind of issue in your code bases this is a true for if Burgtheater can detect so as the list of all the people affected tell here I say biblical tech table because we had a set of private detectors that include more complex with mobility such as West condition or overflow in your token manipulation so we built filter to be fast and precise we use it in our own internal audit so we really need to be like fast and accurate it requires no configuration you can directly want theta on any code base we have several way to simplify its usage we have an integration with to offer we have an integration with bluemix we are working on integration with embark we are several option to help you to three-edged the result so as a developer is you can use little out of the box without configuration without anything we just want it on your directory and we'll find the analogy for you in addition to find a vulnerability little can also find optimization that are missed by the compiler typically if you if inside your code base you have one state variable that is never change it's always the same value you can declare this variable as a constant if you do so the compiler will be able to some optimization on this undesirable slitter will help you to detect this kind of optimization data that you've actually done by the compiler is a sin function that are public but never call internally in your contract splitter will tell you that this function should be declared as external so that the compiler will be able to do optimization on them so the detection of vulnerability and the detection of optimization is the usage when you use theta just by running on your card base without any option or anything else if you want to perform some code review on the complex code base sometimes it's a bit tricky to understand how the code base is architectural how it was what are the interaction between the contract and everything sitter will help you because it provides a set of so-called printers which are visual representation of your card base for example we have several graph based representation which will show you the inheritance graph of your contracts the call graph of your contracts the control flow graph of each function we provide us all a lot of summary of the contract for each function what are the available data read return and so on and what also access voyage each function is protected by a zone or not and we also have is a so-called human with a bar semi for which for each count what we show you the card complexity is the restriction if you use a token like for example does the owner can meet in limited amount of token Arnall here you have the full list of all the printer to give you an example here you have to contract and a third one which in a wait for the two contracts if you print inheritance graph you will be able to see this code base as a graph based representation if you have multiple contracts with multiple inheritance sometime it's a bit complex to just follow everything to see okay watch is over with where where is like how does it work see linearization works and wasting jitter will help you to understand so we will Twitter as a generic framework because of that we can use it as a library and we are building utility on top of for example we open source to utility the first one check a great ability which we'll use as little car to analyze your contract if you choose the delegate called proxy pattern for upgradability you might be aware that if you use this specific pattern there is a lot of issue that can occur on your code for example if you don't curl properly or the initialization function you might have a trouble so sceeto will perform a set of every stick on your code base to detect if this occur there is also this suite of fine possibility so sometime when you have a complex code base you have a one internal function and you want to know how this function can be which it's sometime will be difficult to know Twitter will directly find all the possible paths and can reach this given function for you so it will help you to kind of understand what are like all the possible paths for this function if you want to refactor your code or something like that it will help you to kind of have to have like a good idea of oh it's Victor it's written in Python so you have a full API to take all the information for Skeeter and do any kind of analysis the full Python appear also included a dependency so the dependency is ability to know if one variable can influence another variable I will give more information about this in a few slide but just to give you an example in five line of code you can know what are all the functions I can change a given variable so this can be like pretty useful if you are reviewing or eating a code base and you want to understand how this function can be a houses wherever can be changed so if you want about how our setup works as I mentioned sweeter takes HD from the compiler so if you take the fluid from the compiler it's a bit complex to understand everything the way Street are analyzed the size T is that it uses refinement passing strategy where it will analyze the SD in different step each step you will find a new layer of information the first layer will be the contract you will find in this idea what are the control but I was a steady viable and so on once this is done if we analyze the function what are you touch the function without the parameter what does the control flow graph of the function and so on then it relies with nerd of the control flow graph and for each node is a 3d expression once we have this expression which ones from the three digit code it will intermediate representation once we have all this information set up perform a set of inbuilt analysis typically we will find for each variable where it's read and where it's written that you have will precise information about all the usage of all the state variable it will perform a set of those a we stick for example we detect if a function is protected so if you need some kind of ownership to call this function and finally it will perform as a data dependency for all the variable so that you will be able to know if the value of one variable can fianc another variable so as I mentioned we have own it emitted for presentation if you are not familiar with compilation intermediate representation something will really common for high level language like solidity cpython or whatever you are using all this language are meant to be usable and understandable by humans are not meant for be analyzed by machine so people are usually building intermediate representation so that you have a firm representation of your contract which is most suitable for the machine that's why we build as is a suite retire representation so implementation intermediate representation is pretty simple we have less than 30 inspection it's a linear intermediate representation we have no jump everything is built on top of the CFG forms later it's a flat intermediate representation in the sense that there is no little variation so you have one Operator and a set of variable and we perform a lot of code for summation in simplification just to simplify the analysis by the machine typically we will move the Tanna will pay water and we transform into the set of examples to give you a quick example here how it looks with binary operation we support index and mapping with member and index we have a set of opcode as a new operator typically if you follow the grammar from 3G when you create a new structure it's a call to the structure so we change this to specific up code news / - it's just to simplify as analysis from the Machine point of view here you have a mapping of the mapping and you have a subtraction it's a transform this operation 2/3 operation as you can see here so we build a lot of analysis on top of this intermediate representation in particular we have this form which is called single static single assignment as I say which is a really common representation in static analysis basically it's just to have a form where each variable can be written at at most once this specific form is really really useful and powerful if you want to build at a dependency you saw that like the dependency will come for free and we be really precise something which is a bit particular for us SFO is that we do support state variable so we do have a precise data dependency on the state variable generally this is also interpreted well in systems that we will work the change of the variable a quest function and it's also inter transactional or presentation because we can know if you have to function if well if one variable is change in the first function and then another function depend of the charge we'll be able to track this is fact by doing some kind of fixed point computation on our SSI it will make a bit more sense with the example finally we also have an alias analysis and storage reference this is just to be able to analyze complex code base typically if you have a storage reference in a function it can point to many potential objects so which work or the potential object to be able to have a precise information about them so if you have this contract you have to variable by a one enviable - you have to function if you only analyze the direction you exit function you will see that a viable one can be influenced by I and few only annouce the function second function you will see that a viable two can be only influenced by variable one as you can see here we do a fifth one computation to find that if you call both of the function at the end you to know that variable 2 can also depend a viable one being able to of this fully precise representation and this precise information about the data dependency of the contract will help you to have precise dilib detector and it's really like the main the main key to of precise analysis on top of theta so if you are a developer I'll cut a detail you can use fitter directly out of the box just to detect vulnerability and optimization on your code its first it's precise there is no configuration and there is a continuous integration as support so you can just for each commit you can just once to tell and see what is found if you want to go a bit deeper if you want to have some understanding of a new code base you can use the printer to improve your card understanding of the code if you want to do a factor of your code it's also really useful and finally if you are a researcher and you want to perform and create new analytics you static analysis on sorry duty code you can directly use Twitter as a library with any kind of analysis on top of it it's built to be as generic as possible so for the one map we are going to continue to open-source new detector we plan to improve the developer integration for example we are going to have a new visual studio plug-in where you can just click on a variable which will ask Twitter information about this variable for example what are the possible value of this variable what is the dependency of this variable and so on while working on an automatic patching who set off format so for some issue that you can find in new cos theta will be able to directly provide you with a fix we are working to integrate new language in particular diaper and finally we're also working to improve our intermediate representation to have a more formal representation of our area will will you have work in progress you choose that use symbolic computation some prick execution and abstract interpretation so here's a limb to slit our attacker so this opportunity I think the first time we announce it in public but we are going to release these cryptic services so it's a web based services where you can just provide your contract have a filter one or the public and private detector on this contract and additionally you will have support with echidna and monkey car which is which are a further and a symbolic execution framework so that we can just avoid your contract and you will have a lot of analyzer running on top of it to help you to build itself our contract if you want more information about this service you can directly contact our CEO dan wheeler finally if you need help with any of our tool you can directly contact us on slack on a21 and every two weeks we weren't a free one-hour consultation on and out so if you have any question if you want to learn tool to know more about our tool if you have any problem feel free to contact us and we also give bunchy for all of tool for meaningful contribution thank you for attention [Applause] do you have any question thank you for your amazing talking but the tool you're running also the the ability to to make your custom validations and custom detectors so I have a question to the fact that mainly and the continuous integration level almost everyone has at any smart contract level deployment development we implement continuous information to have a real check what is happening when we deploy smart contracts can you have do you have a comparison chart between other tools to really know what's inside yours with comparing the other ones because usually we use to add new checkers and it's quite interesting to know which are covering what and which is the benefits of using one on the other one so you mean like a comparison kind of about also possible to ISIL or similar tools I can show you one if you if you're interested in two so at least for tool what we usually will come on so you know github you will find three type of tool you will find Slater which is a static analyzer you will find echidna which is a further and you will find on chica which is a symbolic execution and run what we usually will come on is to one Sleater out of the box on any contract once you have some kind of confidence in your card and you have some prototype or or you know kind of what the code is going to be you can start using phasing for it so Akina which is a thousand will help you to find a bit more complex bugs that are missed by static analysis once you have some property test with with echidna and you have some confidence about your code you can start with in symbolic execution with maanteeeca to untrue the property of some specific function in your code so the way we do it usually is that we want sweeter once we have a good good knowledge about the code base we want the further and once it's done and if we want this additional step of security and safety who wins a miracle secretion that makes so likeness that you can release we find the simple bug like things like it can't form if you want to find more complex bugs that are built on top of the logic of the contract you will need fuzzing or summary execution that make sense hi Justin thanks for the nice talk and for all the efforts in building these useful tools for the people so I'm actually more cures for the critic or critic system so what kind of formal verification do you do support or aim to support in the future there so it's going to use mantra for formal verification and I don't tell a lot of information I can share right now but you can contact done video for more information we're going to provide more information about this platform soon but thank you for attention