What Can We Actually Verify? AI and Ethereum Security

Transcript

[music] [music] So thank you so much professor for being here and having this fireside uh chat discussion with us. So just to do a quick introduction uh professor sub Sharma is an associate professor and pankage Gupta chair professor in privacy and decentralization uh the department of computer science and engineering at IIT Delhi. So I must correct you. I was the >> uh right. Okay. So uh sorry about that. Uh but yeah, Prof is an expert. Yeah, >> that's fine.

>> Yeah. So uh so both is an expert in Ethereum security, AI statistic verification, privacy and public verifiability. Uh so a lot of this topic is a lot of the I said chat is going to be um a little informal in the sense that I would encourage people to just stop us midway with any questions and we'll trying to make this as interactive as possible. Uh if not I also have a bunch of questions that I would like to pick uh you know some's brain on so we can keep talking about that all day. Uh but I guess the first place to start is uh from your perspective, what makes Ethereum a particularly interesting place to study software security? So drawing on your work across like

concurrent systems and smart contracts, what makes Ethereum's challenges sort of like distinctive? Um and which lessons from the wider software verification community do you think the ecosystem should be more receptive to and and the ecosystem should try and adopt more? Uh first of all thanks Sham um for that generous introduction and thanks uh to the Devcon community for having me here. Um uh I must say it's u you know very nicely managed um conference. Um and your questions have quite a few parts.

So if I forget uh please remind me. Uh let me pick up on the first part. Um why Ethereum? uh why blockchain in general and Ethereum in particular is a good place for security researchers. Um so Ethereum like any other system is a software um construct and it inherits all the problems that software systems inherit. Uh except that you know in a in a usual classical vanilla uh software system if something goes off uh in the worst case you would lead to you you would witness a crash or you would witness some sort of a service

disruption. But here the stakes are much higher. If there is a problem then it leads to um you know possibly irreversible financial loss right. Um and in this setting the stakes because are so high security has to be accurate. It has to be precise and it has to be scalable right. So which means that many of the security issues that one witnesses in the usual software landscape uh are all borrowed and inherited in this landscape except that they become much more important.

Um uh so so I mean uh drawing from what I have been looking at at you know systems like concurrency and distributed systems of course all of those issues exist um and they manifest in very uh subtle and devious ways. Um but I think um one must understand that the security research in this space is not just about software security right so um it is not to say that oh I have shown this particular contract or this particular blockchain solution to be um safe and I'm done with it. Uh that won't cut it because safety alone does not amount to security right. Um and I

think um um you know the community is aware of that fact but the solutions that we see that we witness today are largely safety oriented um uh and we have to uh start looking towards or moving towards a space where we talk about end to-end security and you know I was um listening to talks yesterday about the bybit attack and why did it happen even though the smart contract um that was deployed to orchestrate the system was shown to be verified and safe but what got executed downstream uh did not match what was verified right so um so I think u there is a need to

understand um uh what verification/security means um uh where does it operate uh it doesn't operate in vacuum and I think uh there are lots of very interesting issues for security researchers to pick on in this space uh There was a second part to that question. Uh >> yes. So the second part is uh what you know sort of common practices and what lessons rather from the wider software uh you know verification community can the Ethereum ecosystem be more open to sort of embracing and adopting like where do you think uh the gaps currently are and and what are the biggest lessons the Ethereum community can learn?

>> I see. Great question Sham. Um I think from my personal limited experience and I'm you know I invite the audience to add to it. Um see verification doesn't like I said I mean I'm building on that argument verification doesn't happen in vacuum right so verification as an activity we must first understand what it is um uh because I got a sense um that verification as a term is interpreted differently by different people not just in this community but uh in general um verification is a process of establishing um um some sort of a mapping between the specification of a system and its implementation whether or not this the

implementation of that system uh subscribes to uh its specification uh down to the tn dot right so so so that's a process and it doesn't happen in a vacuum it requires certain assumptions under which the system is going to be deployed it requires uh somebody to tell me um about what are the no goes zones about that system, right? So, what are uh the safety properties, what are the security properties, what are the uh privacy properties, what are the performance uh obligations that the system must uh conform to, right? So all of these back in the day if you develop see I mean even now I mean a classical

software development subscribes to a software development cycle where requirements elicitation is an extremely important aspect >> and I think this is something that um this community um uh should uh adopt even more fiercely >> is if verification has to happen then the developer should provide me with if I am a verification engineer. Um I I I should have some requirements elicited out from the developer or from the use from the end user who has asked me to develop a particular uh application.

Right? So I need to be able to have a precise specification for that application. Um it could very well be in natural language, right? And that essentially leads to you know the use of AI and there's so much of AI talk um in this conference but we'll get to that and once the specification is there then look verification as an activity by its very nature is not scalable right um there have been four decades of work in this space lot of water has passed under the bridge and what we have realized is that verification by its very nature the kind of formal assurances that it

provides would mean an exhaustive search or near exhaustive search and the way the the moment you define it this way means that it's not going to scale which means that you one one would have to start thinking about how do I do verification in the small and generalize my results uh in the large right which means that one has to start thinking from scratch match especially in this community that how can I do verification in the small and then compose the results composability is going to be an extremely important aspect make it hierarchical right uh and see where we can take it right the techniques that verification

engineers use interactive theorem proving bounded model checking static analysis all have their own you know uh strengths but also flaws Right. Um so I think the key takeaways for this community is to have a fierce emphasis on requirements formal specifications because that lays the foundation and I'm you know at the you know at the cost of sounding stupid because I'm reiterating but I think this emphasis is important is that specification is the heart of it right and if you see you know some of the talks today and yesterday are really about bug-free

uh correct by construction contracts or solutions with a lot of emphasis on the starting point which is clarity on specifications and requirements. So that's the first part and the second part is I think the community has to at large has to um um for a lack of a better word come out of its slumber and start accepting formal verification uh u with more vigor and I'll stop there. Yeah. >> Right. >> Yeah. Thank you for that u very detailed answer. So in preparation for this talk, I did you know read some of your papers uh around Zeus which you know distinguishes uh you know safe programming practices from actually

adearing to the intended business logic and I think a lot of your arguments just now were sort of like based on that. So uh it was very interesting to u hear that. [snorts] But I guess my next follow-up question to you would be uh in your you know opinion which is really the harder problem here. Uh is it to check the code or actually deciding what the code should be and the what what the code should do? >> Yeah I think u see checking the code itself. Um so I I must draw a distinction checking a code is not the same activity as verifying the code for its correctness. Right? Um now verification by itself is a hard is is a difficult process

right it's it's a difficult task um but there have been a lot of research in this space where they've you know figured out um near I mean is techniques that can scale you know if you if you come up with right abstractions um you can come up with techniques that could scale so for example static analysis traditional data flow analysis techniques, control flow analysis techniques, they can scale to millions of lines of code. But then the question I mean so they have that their strength in that uh but then at the same time um you know there's a high rate of false positives. Why? Because the abstractions the moment you make your abstractions in static analysis tighter uh the cost of

doing that static analysis at scale um would outgrow the benefits. Right? So um um now now but there are techniques but I would you know I mean the answer is sort of obvious specification uh getting developer intent is a much harder problem um and you don't have to essentially rely on evidences in this landscape right uh look at the history of software development how software development ment has happened. Somebody came up to you and said that okay I want this system to be designed and you would see that in your software development cycle

there is an explicit uh point for requirements engineering. Why? because the one who wants that system to be designed they themselves have a very fuzzy idea of what they want uh you know other than their final objective that this is what I want they don't know how to get there and therefore they don't know what are the safety and security properties uh along the way they would want to be ensured so uh and it's a common problem I have been building systems and from the get-go I would not have the entire safety security picture in front of me in absolely absolute clarity. It is uh it it dawns upon me as I build the system. Right? So I think

getting specification right as at step one is an extremely hard problem. And even if you have gotten the specification in some form and shape, does it truly capture developer intent is yet another problem. It's yet another leap. And there's a distinction between the two. Now if you look at what lot of people are doing not just here but in general uh software industry is to capture specification via prompts. >> This is what I want to do and let LLMs or these a AI frameworks or agentic AI setups um you know um through their extensive training figure out infer um a specification in natural language and

then maybe transpile it into a formal language later on. All of that could be done with certain uh you know with certain level of integrity but the question is is it actually capturing the developer intent and there has been lot of work in recent past which um has demonstrated that they are not capturing developer intent and here is an example um I'll take a very simple data structures example right so it's a course that uh we teach to our second year undergraduate students. Um, and I tell you here's a list of integers.

Um, remove duplicates from this list. Now, this is the specification. Uh, this is the prompt that I give LLM and we have, you know, there's there's a paper by Microsoft uh, research uh, and they experimented it with chat GPT4 and whatnot. And these agents would go uh the these systems would go ahead and would be unable to disambiguate what is the developer intent whether the developer wants the numbers which are appearing in duplicates to be removed altogether or to keep at least one instance of it in the list. Right.

>> Right. >> Right. So to disambiguate this they'll have to actually then ask again what did you intend while I understand what is your final objective that you want the duplicates to be removed duplicates to be removed is ambiguous in its current aftar you need to tell me whether all instances of duplicates have to be removed or at least one instance of that entity that is getting duplicated be preserved >> right and it has huge implications in in maintaining the sanctity of that data which then will be used in downstream tasks. Right? So what I'm trying to say is developer intent is different from specification and you

require human in the loop. I think uh as as a um as a computing industry, we have been overly fascinated with automation and uh I you know I want to sound out a you know a note of caution when you are ex when you are trying to extract intention from the code uh whether or not it can be completely automated is a writing on the wall. It's not going to go away. You require a human in the loop.

uh and if you don't I mean there may be a time when this could would could also be completely automated but then we have to think from scratch what kind of questions will have to be asked from developers so that they can provide these partial specifications in the form of input output pairs that will allow these LLM agents to then fortify their specifications inching towards developer intent right so it's a hard it's a hard problem but I think worth solving Hey uh GM so uh profile I have a question that is kind of like lingering around the ease of access to uh one both the knowledge and the tools. Um so right

now if we talk about one extreme definitely is AI and just like wipe coding a lot of stuff. Uh but like also on the other hand when we talk about formal verifications and you know just like proving contracts and its sanctity um for like for a product guy like me that is transitioning into tech it has been really hard learning lean and building um enterprisegrade internal tools to actually make stuff like that. Uh it's like so yes like just adding like to your uh to to your take. Um it is kind of like very easy to just go and v code this. But at the same time on the other hand the other options that we have for example in this case lean is

and finding invariance and and and just like then proving them uh that is like also on the other extreme of the scenario where the amount of um I would say the effort required is just monumentally on the other level. So like what what are your take on like achieving a middle ground on uh stuff like this where security is more accessible to people and then like in that case we increase the surface area of developers who are more cautious on the um verification side of things.

>> Yeah. Uh great question. In fact, >> uh you're right. Um and uh we won't move forward as a security community until unless we acknowledge that this entire um um story uh becomes usable, right? Um one cannot expect developer to be an expert in you know 100 different areas, right? Uh your question directly hits at the standing problem. That's the elephant in the room.

And you know my perspective is that going forward there has to be a larger and more intense collaboration between industry and academia. Um we heard uh Shuti's talk just before um they are doing extremely deep stuff. um I am from a neighboring um discipline uh from hers and I couldn't understand bits and pieces of her talk right and I can only imagine developers who are great at software engineering how much difficulty they would face in absorbing this top research content that is coming

out from industry. So I think there has to be a larger collaboration between industry and academia where um uh or between industry and industry whatever that may be where there are these groups who have figured out what uh very specialized techniques and they make it palatable for developer community at large which means that there's a lot of back and forth that has has that has to happen between these communities. How would that happen? So let's take an instance right you are an FE expert and I am a developer right I don't understand FE why because um I don't have you know I've not done those undergraduate or graduate level courses I don't

understand how to develop lean models but I know that through agentics uh AI I can spend uh you know some $200 and get a very fancy lean model out and it would be smoke tested and whatnot by the agentic AI frameworks uh they will build automated tactic sequences to make sure that the lean models discharge in the lean prover right all of that is done without me not even knowing one aspect of how to write a lean model but that takes my agency away as a developer because now I have to trust these agentic setups and I don't know whether these lean models are accurately capturing my intention or what the code is supposed to do and what

they have proved is something what I wanted I don't even know that. So what's the way forward? I think the developer community has to come back to and and come up with data sets saying I know here is a contract or here is a sequence of transactions that are buggy. Where are they buggy? What is the location where the bug manifests? And by the way, fault localization is is an extremely hard problem, right? Bug discovery is relatively easier. I was uh just talking to my you know colleagues and we were just having this discussion that fault localization is in in the complexity theory is sigma p2 right so so it's like an np oracle require np you know np

queries so so you need to provide me a data set a label data set which says that okay here are the specifications which are near comprehensive if not comprehensive here are the faults where they manifest test. These are not just bugs. These are faults which are exploitable which can lead to an exploitation. So bug detection is one aspect and then there's a whole road that one has to traveled to actually exploit showing an exploit which means that there has to be an exploit synthesis. A test harness has to be synthesized to show that their exploit is real. All of these are real problems.

Once you provide that, once I provide this to the FV community, say you are an FV fellow, you will be able to come up with an ecosystem or a framework where you can use all the sophisticated tools but augment that with a layer where what you have produced the outcomes could be made more palatable to the developer community. Right? So I think that stitchup is necessary otherwise um yeah we will be just going in circles. This is a this is a huge problem. I acknowledge that.

Sorry for that long- winded answer but um uh yeah it's it's a it's a hard question. Yeah. >> Wonderful. Uh I I also especially love that call for action that you mentioned where we need to sort of bridge better gaps between um security experts uh whether or just more broadly like researchers whether they're in academia or industry um and you know the ecosystem at large and I think that's part of what we're trying to achieve with you know the academic day here with you know bringing academics to defcon and and also with our >> yeah I can you know just allow me 10 more seconds you know we've been writing papers on uh smart contract security.

No, one big thing that we face all the time is benchmarking, >> right? Um, we don't have enough data sets in the wild uh which have not already been leaked to these AI agents. Um uh there are lot of audit firms who do audits but their audits are private. uh in public they will only say that okay this bug this contract or this solution is buggy but they will not identify where the fault emanates from and fault localization like I said is a hard problem so if academic community has to take these data sets they don't know how to run with it right so there has to be a dedicated effort to create a public data set of recent issues where recent

contracts and recent solutions where issues have been identified in their full glory so that it allows the community who is building very specific FV tools to take those data sets and run with it and come up with more scalable and more accurate technologies. So this is one big issue that academic community is facing at the moment. >> It sounds like uh we have our work cut out for us in what we should be doing next to sort of bridge this gap. Uh but thank you for for the answer. Uh so I'm just looking at the time and I think we have uh just enough time for one final question and u for that I would like to ask you what do you think actually makes an AI security assessment really trustworthy.

Um so Devcon has a lot of uh people from you know var part of the ecosystem uh but a large population are also users and and users who really want to understand uh whether or not they can trust the security assessments of you know all the bridges all the uh oracles all the rollups that they use. So uh and and you know a lot of the talks are are are about AI assisted security. So what do you think would actually make an AI uh driven security assessment trustworthy? [snorts] Um so that's a loaded question and I have a slightly controversial opinion.

Um if AI security has to move the way it is currently moving um then uh trust is out of window right trust as a word I mean what makes something trustworthy trustworthy itself is a very complex term right uh you could have verified a system end to end and yet it would not be trustworthy right so um and here is an example right so um this actually goes back to the the the first question that we were uh discussing about what is verification and what are the limits of verifiability right in fact you know so let me let me touch upon

that aspect very very quickly I know we are left with only 50 seconds u verification in addition to safety property and security properties also involve uh you know checking against obligations contractual obligations in in you know if if you're talking about Ethereum contracts right or solitary contracts whether the business logic or in other words in common parlance it's called um uh functional properties whether they hold or not right now and if if they don't hold then you would have shown that uh against some technical security uh articulations the contract would be correct but suddenly

some uh fault will manifest right So I think for AI security to move ahead, I think the future is to essentially be more specification oriented and gate it gate AI's outputs uh with proper verification um um and witness uh synthesis which means that verification not in the wild verification associated or rather augmented with witness witness generation, right? So, verification of a very particular kind where you actually show me the witness leading to an exploit if I have found one, right? So, I think uh in in short, I think the

future is neurosymbolic, right? So, you combine the AI layers with symbolic decision procedures in the back end. Wonderful. And I think that's all the time we have today. Thank you so much. >> [music]