# Smart Contract Security - Incentives Beyond the Launch by Phil Daian (Devcon4)

- Speakers: [Phil Daian](https://streameth.org/speakers/phil-daian)
- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2019-10-09
- Duration: 29:22
- Topics: blockchain, smart contracts, distributed ledger, Science & Technology
- Watch: https://streameth.org/watch/yt-i-oWE8hg6-0
- YouTube: https://www.youtube.com/watch?v=i-oWE8hg6-0

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/4/smart-contract-security-incentives-beyond-the-launch

To mitigate security issues that were quickly present in the deployment of smart contracts, the community has turned to a wide variety of security techniques.  Standard when deploying new contracts is manual review by an externally contracted company/individual.  In many ways this has been a success, reducing the number of observed security incidents.
In this talk, we take a look at how unique incentives in smart contracts affect the process of securing them. For example, smart contracts are often non-upgradeable: enshrinement at release time encourages security processes that end after the deployment of the contract, leaving blind spots in long-term  security guarantees against evolving threats.  Pressure to ship often leaves critical security guarantees out-of-scope of external reviews, and auditor incentives tend away from detailed or fundamental criticisms of contracts' protocols.
In this talk, we review the reviews and take a look at several top contracts in the ecosystem: what are the provided guarantees, who were they reviewed by, and what is missing?  How do these guarantees compare to guarantees provided users in systems outside the smart contract ecosystem?  And how can we most effectively deploy the immense talent coming into the community towards more secure, more usable systems for end-users?

Speaker(s): Phil Daian
Skill level: Intermediate
Track: Security
Keywords: contracts, audits, incentives, reviews

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 4 was held in Prague, Czech Republic on Oct 30 - Nov 2, 2018.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

hey everyone I'm Phil Diane and I am a PhD student at Cornell Tech and I see three and I'm gonna be talking about smart contract security incentives beyond the launch so let's just get right into it what is security recently I was lucky enough to attend this fascinating talk at the USENIX Security Summit which is a gathering of professionals and academics by James Mickens from Harvard University so I know the title is long but if you google James Mickens you can find this talk and I'm actually gonna steal all his philosophical insights for my talk so sort of classically when we define security as a community we've looked at historically this Cartesian product between people programs and computational resources this was originally motivated by wanting to make statements like coder who is on the other side of the Iron Curtain in his bad cannot use the login daemon to access the US government ARPANET and this definition sort of naturally has been adopted by the the block chain space and extends into this space saying things like killer who's the DAO hacker cannot use reentrant c to access my tokens or can't use overflow to access my tokens or self-destruct so in the last two years we've gotten a lot right with regards to this notion of security so two years ago was sort of the eve of the DAO hack and it still wasn't even clear whether we would be able to build secure smart contracts at all since then we've seen sort of this blossoming of project projects many of whom are talking here including hydro projects sakura phi mithril new languages like VIPRE the Kay framework say hi to the runtime verification booth and Manticore and many more and we've also seen a wide wide variety of publications about smart contract security smart contract formal verification and more so unlike two years ago we have a range of tools a robust audit community in a robust culture a deep toolkit of formal methods much better testing practices and higher standards now that's not to say we're perfect but we've been substantially successful at optimizing for this notion of cartesian product security so let's keep calm and give ourselves a pat on the back all right great and that concludes the talk thank you guys very much I'm just kidding because that would be ignoring the dumpster fire in the corner and that is the way I see Oh incentives are set up to create a security culture in this space up until now most community attention and audit attention has focused on tokens icos and other form of launched once walk away contracts so these are contracts that you stand up they start running and then they're not upgradeable so you kind of take your hands off and let them run themselves so this is great for some sort of business purposes but unfortunately it creates this sort of vicious cycle of incentives so you launch your token it goes to the moon you pat yourself on the back if your den Larimore maybe you restart that whole process a few times and what does that give you so what it gives you is lack of in-house security experience that many of these projects because you sort of don't need to engage in continual development and continual security processes it gives a big desire for rubber-stamp audits to sort of approve something for a strict production deadline sign off on it and defer that risk sort of on to someone else and it gives zero incentive to set up the kind of security life cycle processes we have in the space so I'm gonna go back to James Mickens who argued that for the broader security community as a whole we need a more holistic view of security and that really the high-level goal of computer security when you break it down is to ensure that the systems we're building will do the right thing even in the presence of malicious inputs now you might say what is the right thing is the right thing that what these Cartesian things we've been talking about before and actually these are these are too simple in the world where technology sort of pervades and impacts every aspect of our lives it's no longer sufficient to just ask can someone access the resource can someone steal my tokens we have to ask as a security community what guarantees do we want these systems to provide their users and we have to reason about broader and more nebulous moral questions so for example should a particular action be possible from a moral perspective and if so how do we get socially beneficial outcomes out of our systems so in a nutshell basically the role of security is to separate the good from the inscrutable so a good system it's a system that does what users expect it leads to socially good outcomes and it fails in known and predictable ways that the user is aware of before they engage with the system an inscrutable system our systems that often violate the expectations of their users they lead to socially negative or socially morally bad outcomes and they fail in unpredictable and surprising and often catastrophic ways so as a security community how do we separate these two kinds of systems well we sort of lean on this rich culture in this rich tradition in this rich history of extensive modeling formal modeling and proofs field data philosophical reflections and reviews on the type of modeling and the type of data we're using and whether that's actually getting us the type of security we really want and experience from all of you guys people in industry people who are actually building things and are on the ground every day talking to users and putting these systems into production so you might say Phil I saw you use the poo emoji instead of inscrutable and I actually blame Twitter for everything in this talk so I ran to polls about this talk if you hate the talk what you should probably do is follow me on Twitter after and vote in the next poll and maybe you'll like the next one more and if you did vote in the poll then it's all your fault I guess so this is the main thesis of my talk and this is sort of what we're gonna be focusing on for the rest of the talk and that is the idea that we simply don't understand how to build principled secure smart contract systems at all yet right so this is not a it's a little bit of a dooming loom talk but it's not completely hopeless we are sort of moving in the right direction and there is you know quite a chance that we will be able to eventually understand how to build these systems but right now we do not so I'm gonna say that again we simply don't understand how to build principled and secure smart contract systems yet and I'm gonna prove this in three lemmas so the first one I'm going to show that many Dex's are inscrutable we do not understand how to build a secured X for our users right now as a community from sort of a theoretically optimal and and an academic standpoint as well as from a practical standpoint I'm going to talk about why on chained voting is also inscrutable so we don't understand how to build a good on chain voting system this implies that building anything more complex especially when you're using one of these two pieces somewhere in your system is also going to lead to something that's inscrutable and so these three levels together are gonna prove that we just don't know how to build even the simplest mechanisms and then I'm going to talk about why this is sort of threatening to aetherium as a whole and the security of a theorem as a whole as well as what we can do about it so let me tell you a story there's this fascinating book called flash boys which is sort of about this this ban of traders on Wall Street who figured out that by sort of cutting down the latency people were using by a little bit and getting access to sort of very quick market inefficiencies that were momentary in a continuous market you could actually profit systematically and extract mechanical rent out of the market itself regardless of sort of how the market was moving or what users actually wanted to trade so it's a fascinating book and I'm gonna tell you the story of flash boys 2.0 which is a very similar story to that but on the etherium network so who are the flash boys 2.0 well it's you and Schiele and Xuan Zhao who were primarily responsible for the initial work of coding and operating the trading BOTS that I'm going to be talking about as well as myself Lorentz Breidenbach idle Ito ben tov re jules tyler kel and rafael Paz and these are all affiliated with Cornell or Cornell Tech so Lorenzen Tyler actually here at this conference I highly suggest you find them and talk to them about this work and they're also giving a talk tomorrow on one potential mitigating solution to this kind of problem so this story starts on August 13th 2017 when we published this blog post about the cost of decentralization in Xerox and ether Delta this was over a year ago and what we said in that blog post is that decentralized exchange leaves users vulnerable to minor front-running that means if a user comes and puts them in order on a decentralized exchange a minor can see that and can with guaranteed profit essentially insert their own transactions on either side of that order to sandwich that order this is something that's frowned on in regular markets if you're if you're doing activity like this either the market design will try to design to make sure you can't do that or you'll get banned from whoever whatever broker you're trading through or whatever but in on chain systems this is very prevalent and not only that but it actually gets worse so many of the systems we built now have slow cancellation which means that because an order is sitting on the blockchain and you have to bring your cancellation to the blockchain by the time you go to cancel your order if the price has changed essentially that's a juicy order for miners to come take quickly before you're able to cancel it and you're just gonna waste the gas price of your cancellation there's also an issue of high gas cost for competing transactions so multiple transactions trying to take a juicy order that's on the blockchain essentially engaged in this bidding war on gas to see who can get mine first by the miner and who can get that transaction so 0x followed this up later with with a nice article about front-running griefing and the perils of virtual sediment on the blockchain where they sort of described this process of minor front running and how miners insert their own transactions when assembling these blocks now you might say Phil you're in your ivory tower over there talking about this but we're building real systems that's not actually the case so we practice what we preach so we actually ran the numbers on this in the 24 hours in on August 11th 2017 and on that day you could have made approximately $4,500 or approximately 1.6 million dollars a year front-running ether Delta alone so remember this was before sort of the rise of many Dex's that came out shortly after this work as well as before much of the many of the users started using these Dex's with better.you eyes so it's likely these numbers are actually much worse today we also ran an arbitrage bot and observed our own success rate of actually taking these opportunities at 58.3% which applied approximately 2500 dollars a day in profit or 8.32 if a day in 2017 and of course the reactions we got looks something like this well spoiler alert we didn't and so quick warning the next few slides contain preliminary data I'm a big believer of sort of doing science in the open and showing you guys what we have as soon as we have a form that we can show it to you in so take this data with a grain of salt and sort of watch out on my Twitter for when I when I sort of tweet that this is finalized and you can really have confidence in this data and we're also gonna be releasing it and open sourcing everything I talked about today for peer review within the next month or so so quantifying the front-running problem so between around blocks three point eight seven million in a around block six point six million which was I think a week or two ago we saw around two million five hundred thousand of these programmatic arbitrage bot transactions which is about 30% of all blocks on the network in that time containing such a transaction we also saw 21 trillion total guei bid in the network for the gas to pay for these transactions which paid for nine hundred eighty nine billion gas or sorry bid nine hundred eighty nine billion gas the transaction could potentially use less than it bid and that's equivalent to about a hundred twenty thousand full blocks of gas so you can see this is already happening actively on the system today now let's sort of zoom in a little bit and look at the the graphical data of what this market looks like so that purple line over there is the date we published the post you can see before that it was maybe us trading around and experimenting a little in one bot and shortly after that sort of this rapid professionalized economy rose up taking these arbitrage opportunities often competitively so the way you should read this graph is the top line is that is the gray top line of the top graph is the Gawai bid including failures and what that means is we include transactions that didn't necessarily successfully arbitrage things and we're using a pretty loose heuristic which might accidentally identify transactions that are trading programmatically through Dex's for other reasons so we're looking through that data manually and just validating it take this with a grain of salt right now but approximately this is what the shape of the market looks like and the way you should read this is essentially we chunked up time into 10,000 block intervals and just looked at how much gas and whey was being used in each of those 10,000 block unit rules so it's not actually a moving average sorry for that misleading label but if you see for example the bottom line 15 billion gasps that means in those ten thousand blocks 15 billion total gas was was sort of bid which means 1.5 million gas per block was demanded by these arbitrage errs the law world two lines so show the successful arbitrage rates and these are transactions which actually managed to execute trades on index programmatically through other smart contracts and the bottom red line is the fill is the gas used and the top is the gas bid so again the gas pit is the price you offered to pay and the gas use is the price you pay so you can see this market has sort of been steadily increasing slowly in gas but decreasing in the amount of gas it's burning for two reasons number one the general gas market has cooled off a little bit since that sort of spike right after our blog post and another one users are actually making smaller and smaller trades on these Dex's as they hit the mainstream which means the average size of the opportunity is decreasing over time so we went and actually measured this market in much more detailed because we wanted to know how are these BOTS that are doing this actually competing what does it take to be competitive in this market so we deployed eight nodes with 256 peers each deeply paired with the etherion network geo distributed this across three different server providers in south and north america europe and asia we collected 215 million observations over a period of about a month and a half and what an observation is is essentially every time a peer sent us an arbitrage transaction we record the precise time we saw it synchronized to the microsecond as well as which peer related and things like that and the goal was to eventually sort of geo locate these bots ask where in the world are the latency advantage is strongest as well as understand their operation and the dynamics between them and collect precise timing data on these auctions so what did we see when we did that this is what a typical competition between two BOTS trying to take a profitable opportunity looks like the graph is showing the bids over time so on the right is time passing you can see the auction ends about two and a half seconds after it starts and the y-axis is sort of the gas price these bots are bidding for these opportunities so you can see two things number one the bids are happening very fast many bids in two minutes and also the Green Dot is that is the bots that eventually won and the red dot is the one that got mined and paid the fees but didn't get the opportunity so how does this game work well at some point in time some random orange line will drop on this graph and that orange line is when the block template was formed by the pool mining the block and when the pool that eventually is going to mine the successful block forms that template and includes those transactions the two transactions that at that point in time have paid the highest price will be included so in that case it's those two in this case it would be those two and the guy on the right would win and the guy on the Left would lose so this actually induces a latency war because whoever sort of had the last word in this back and forth is the most likely to win the market and it actually gets even weirder than that so here's an example of an auction in which the winner and the loser happened right at the start of the auction and the bots kept bidding afterwards even though the winner and loser were already locked in so why did this happen this happened because sort of in the network there's this difference between when this orange line drops that sort of locks in the auction results and when this red line drops that actually finds the solution to them to the block on an ASIC and distributes it to the rest of the network so by making the distance between these orange and red lines smaller the pool could have taken a later bid and potentially profited a lot more from this auction than it did but instead the pool was a little bit inefficient it took about seven seconds without reflect refreshing its block and it lost out on a few fees as a result so I'm gonna claim that the transparency in this mechanism is a lie because when you read the ether Delta smart contractor the zero X smart contract it doesn't imply this game at all the real game people are playing on these networks from a game theoretic perspective is continuous-time it's imperfect information because you don't know when that orange line is going to drop it's all pay because even losing BOTS pay gas for attempted execution its probabilistic both in execution and duration and it's rate limited because you can only send out transactions so fast on the etherium network so this gives these BOTS a wide range of sort of angles to optimize on to be more profitable at taking these opportunities so our conclusion in the blog was to recommend a centralized order book and say essentially there's a fundamental trade-off between who confront run you either you have an exchange operator who confronted on you if they do the routing and matching for your orders or you have some sort of peer-to-peer network or blockchain involved in your routing in your orders at which points someone in an advantageous position on that network could potentially have information asymmetry advantages that lead to mechanical rent and we prove that this is sort of fundamental no matter what kind of global peer-to-peer marketplace you build so just centralize it maybe it will fix it we don't know all right so the real competition here again is on latency connectivity etc just like traditional hft just like flash boys etc and the transparency is a lie because what we have on chain is actually not all the data so of all the data I just showed you in the auctions only one or two of those transactions even makes it to the chain or even makes it to ether scan because most of them just get replaced so quickly that no one in the network sees them so sort of under this surface mechanism that we're building that looks simple we have this iceberg of sort of bot strategies and interacting BOTS and weird liquidity pools backroom channels of influence and potential Black Swan events if these things behave poorly so there's actually a lot of complexity that still remains out of line it's not enough to just say oh we're making the trades more transparent and therefore we've this is bringing our users more security that is absolutely not necessarily the case so now you might be saying to me Phil isn't that just an efficient market isn't that just how the world works so let's talk about user experience in this brave new world of Dex's so here's a user who says would you have the heart to return 24 east of my address I am a stay at home parent and day trade to keep my family above water in your heart you know this isn't right here's another one I have faith in you man faith in you man please send my money back so these are users who went to cancel their order and were immediately front run by these bots who sort of detected a fat finger and essentially took all their money and and here's another one please please please this was an accident I did not mean to make this transaction please can we reverse this please be kind and karma will be kind for you too I'm a single parent trying to make ends meet at a job I hate please have some mercy and Benjamin Huffman goes on to write again it's all I have please have some mercy or there's alpha here who says please please please return at least 1/8 I give you the rest willingly if God ever asked you I really needed to continue my education I might need to sell my car to pay and last but not least you have Rajesh Kumar here who says sir this was an error order this is all of my village rupee I trade for them if I do not receive back 'if I will be in the in track inscrutability sir please so you can see that this is something that's really impacting real users today these issues that we pointed out in 2017 and that most of the projects in this space just went on to ignore and launched anyway and there are hundreds of these comments on the ether scan comments of all these trading bots that we've sort of found so I encourage you to go look for yourself after the talk and of course we have a few comments like this lol making people pay for their fat fingers how do you do this tell me your secret sauce so the conclusion is we don't understand existing decks designs or sort of how these will behave in the eventual game theoretic equilibrium of these systems and while we're sitting here in in decadence that these conferences going to parties enjoying popping the champagne real users are losing money on the systems we've built and it's having real world impact on them and unfortunately a lot of the reaction the space a lot of the time kind of looks like this so instead let's learn from history we can look at a wide variety of work on this kind of high frequency trading and market design this is a recent paper I highly recommend by Buddhist Crampton and xem which sort of says that these opportunities and mechanical rents are fundamental inside continuous markets and it's not just healthy competition because it creates an arms race that induces mechanically a prisoner's dilemma and charges of liquidity tax on the system that's paid by all of its users and this this actually gets worse with the blockchain so let's let's imagine we're a miner for a second we have these transactions on Nexus getting fees f1 f2 f3 if we insert our own transactions here suddenly we have fee f1 f2 f3 + the profit from the first transaction + the profit from the second transaction or maybe we can switch the order of transactions 1 & 2 and then we get P 3 and P 4 instead and that's actually more so figuring out the optimal ordering and insertions here is actually an optimization problem that's provably undecidable with turning complete transactions in np-hard without which makes it a substantial vector for minor competition not only that but in the long term iterated game equilibrium miners can out-compete non mining arbitrage BOTS for these ordering opportunities and are incentivized to sort of minimize those orange and red differences we were talking about earlier in absurd levels 2 milliseconds are lower if they don't do this they just won't be competitive with miners who are and they'll be driven out of the system so what you get is huge opportunities that lead to reorge Orphanage selfish mining fee estimator errors we've seen this already with systems like pao h 3d and you get mining that's dominated by a small set of high-frequency trading firms using proprietary relay and optimization networks just like we have on Wall Street but not only that these guys will also be powerful players and governments so you can't have a system that's full of intractable mechanisms that we don't understand that's still secure all right I'm gonna talk about another simple mechanism here on chain voting so this is the one used in the etherium example documentation and we have two posts about this as well on hacking distributed and also my personal website talking about how on chain voting is open to trustless frictionless bribery it does not satisfy the classic properties and security literature of coercion resistance receipt freedom all these things people have been studying for over 30 years now for real elections we also released a vote buying mechanism for carbon vote that you can use to publicly by people who votes on that platform and we described a new construction called a dark Dao which is sort of this trustless hidden cartel that operates in trusted Hardware where I can buy your vote you don't have to give me control of your funds or anything like that I'm only buying your vote for a specific vote and you can tell how I'm gonna buy it and nobody in the system can tell whose boats are whose votes are bought whose votes are sold or how much money is even bought or sold at any given time so this can undermine the legitimacy of the process even without having any money in it because it's cryptographically there's simply no way to know how far this attack has advanced so I encourage you to check the details of that scheme in our post the conclusion is that we do actually understand voting dark downs can also be used in other mechanisms in our space so any sort of Nash equilibrium incentive model you set up you can modify using a dark dial by paying users to behave in a conditional way and this motivates the bribing attacker model it motivates cooperative game theory and it motivates using much stronger models than we've been using for security in the blockchain space and actually you can use the dark now even to attack consensus itself because proof of stake and proof of work are just a form of voting so I can pay you to censor someone or do a 51% attack or whatnot so the conclusion is that on chained voting is inscrutable so what about more complex mechanisms this is the picture from documentation a little bit old a little bit outdated but from a real project in the space and this is a more up-to-date sort of version of that same picture so as you can see we're building incredibly complex interacting mechanisms with a multitude of components and we're looking at it and saying well it works because it works right but if you zoom into something like this you see that but one small piece of this sort of like mess of interactions is is an admin multi-sig that's eventually going to be replaced with something like on chain voting so again here because this on chain voting feeds back into every single aspect of the security of these systems and we simply don't even know how to build on chain voting that's secure and incentive compatible how can we possibly build something like this that's incentive compatible we simply don't understand how to do that yet so the conclusion is that any more complex mechanisms or any form of sort of substantial complexity is inscrutable and a corollary there is that we should stop hyping these things up and stop selling them to regular users because we don't understand what they are we don't understand how to build them we understand that they work because they work so far but they're not necessarily more transparent and they're not necessarily better so when you're selling this to normal people and saying there's no risk here you're doing them a great disservice alright so why did we get here I'm gonna kick it back to James Mickens who has this sort of scathing critique of the the technology industry in that talk that I suggest that you all watch and we got here because often technology is soon technologists assume that technology is value neutral so that means that you deploy a technology and that automatically leads to good outcomes for everyone so new kinds of technology should just be developed and deployed as quickly as possible without taking some any time to reflect on a general idea of how the technology works or how it will develop or what the social impact of deploying these technologies in the widespread fashion will be and this belief sort of comes with the idea that history is uninteresting because the past has nothing to teach us so because we are reinventing everything anyway so we might as well not look back at old academic work from 30 years ago or any of that because they don't understand us today and this is a very very flawed culture that cryptocurrency is inheriting while existing in decadence so we're throwing our hands up and saying these mechanisms are more transparent so what we've built is sort of enough but but as we said before that's that even that is actually a lie and we can't afford to become detached as a community from these security outcomes in this fashion because if we do what's gonna happen is that we're poised to just reinvent the same systems that we're telling people we're going to escape and we're poised to reinforce the same power corridors that exist in the world today at which point sort of all of this that we've done here has just been a way to fund some like Burning Man style parties and so we're really really just not learning enough from our mistakes in this process but we have a chance to turn it around so here's the happy part of the talk let's break out of technological determinism and let's be more skeptical let's learn from history let's do our homework and let's listen to people who criticize our systems in principled and smart ways and let's start today so announcing an early preview of front run me which is a little dashboard that we've built where you can view a small subset of the data we've talked about today so you can see sort of a view of the day's auctions and see how these arbitrage is are competing against each other sort of have some insight into their dynamics you can drill down into individual auctions and sort of see data about them including the price they've they've been the bidder you know what the gas limit is how much gas to actually paid etc and you can also go to a sort of a strategy breakdown which graphs things like the bots latency against themselves and against other players in the market as well as what strategies are using this auction in terms of raises and things like that so this is super preliminary data there are some known bugs in the software but I just want to release it for you guys to sort of get an idea of the story we're gonna tell here so what are we gonna do next we're gonna integrate much more data into front Ronnie so of that hundreds of gigabytes of data that we've talked about maybe only 1% is currently integrated into that dashboard so we really only have the tip of the iceberg we're also going to do things like geolocation studies and more we also have robust game theory that's currently sort of being formalized and finalized behind how these markets actually work and what users can actually expect from these systems validated by the data that were experimentally collecting here on front run dot me and we're gonna do the same for blockchain voting over the next year so we're gonna create a tax on existing protocols that were actually going to implement and deploy and we're also going to build schemes that have rigorous and provable security and sort of outline the contours of when these schemes are appropriate to be deployed and when not so let me say that as a community we have a chance here to set a positive example and get out of the poop emoji and into this world of sunshine and rainbows that we're all promising everyone will exist someday all right that's pretty much all I have thank you guys so much for coming and listening if you're interested to know more you can visit my website at PD on comm follow me on twitter at phil diane there's also projects to cago do so project Chicago aims to study resource markets in aetherium and things like fee markets etc and actually this is a part of project Chicago because you can't really understand fee markets at all without understanding these additional ordering fees that are introduced by smart contract systems like aetherium and these arbitrage auctions that we've sort of talked about today I'm also part of this cryptocurrency research initiative called IC 3 at in its e3 org so a bunch of us are here come say hi and a company for formal verification called run time verification they are in my opinion the best at this Cartesian product security we talked about on the first few slides and thank you to the etherium community and foundation for always supporting our independent research thank you to the NSF for supporting me and and our whole lab through grants and thank you to all our industry partners for amazing conversations support insight from events and more and of course you know all this work has at least five or six co-authors on it it wouldn't be possible without them and my sincere thanks go out to them unfortunately I don't think I have time to take questions but you can find me on Twitter or after the talk in the hallway and I'm happy to do that Thanks you