Tools For Supporting Manual Auditing At Scale

DeFi Security Summit 2022 · 28 Aug 2022 · 8:20

David Tarditi, VP of Engineering at CertiK, describes the tooling behind manual auditing at industrial scale, with 1,217 projects audited and 4,938 medium-or-higher issues found in six months. A relevancy matcher flags code CertiK has seen before, and source-level and semantic checkers, program visualization and model checking run on every project, with security engineers required to triage findings of minor severity or above. Machine learning groups a database of more than 60,000 findings into about 500 clusters, against 2,400 by a human, to show which new detectors to build, while design flaws still need human auditors.

Speakers

Topics

From DeFi Security Summit 2022, hosted by DeFi Security Summit.

Transcript

And I want to welcome David Tarditi Tarditi, VP of Engineering at CertiK, and he's going to do a presentation on tools for supporting manual audit at scale. Great, thank you. So, thanks everybody. I know this is the last session, uh so I appreciate you're all here. Uh so, I'm going to talk about tools for uh manual auditing at at sort of industrial scale. Uh and the reason uh we want to Why should you like pay attention to this talk? You auditing is a great thing, and we want auditing to be both effective, uh and we want it to be something that people can afford to do. So, you know, people mentioned before auditing is kind of expensive, and it was like taking a long time.

If you can do it at industrial scale, your goal is to make sure that it's um uh both effective, as in it finds bugs, and uh it's also efficient, as in people can afford to do it, and they can get it done soon. So, um uh a little bit about CertiK. Um we do um pretty much a lot of things that were mentioned here today. We do auditing, formal verification, on-chain monitoring. We have a security leaderboard. We also do KYC. We work at everything ranging from the blockchain implementations uh to smart contracts. So, in the last 6 months, um we audited uh 1,217 projects.

Um we found 4,938 security issues that we judged as medium severity or higher. So, um we have severity levels, uh critical, major, medium, and minor. Medium means you might get hacked. Major means like you have a significant risk, and critical means pretty much like the minute you put this out, you're going to get hacked. And so, what we found is that our clients actually value and want manual audits. Um uh there's a couple of reasons. One is that there is a lack of formal specifications.

Uh and then even if you have specs and threat models as people mentioned, you can get them wrong. So, um we actually build tools, um a range of tools covering static analysis, automated verification, and deductive verification. Um and so I want to focus in today on just like what are the tools and things we built to support manual audits. Uh to do 1,200 audits, uh over 1,200 audits in 6 months, that's a lot of audits. You can think we're like completing like I think probably like six audits a day, every calendar day.

Um and so here's the sort of things we do, and the idea is to be operate at scale, um make it um uh efficient and make it effective. The first thing is we have a tool that we call relevancy matcher. So, the question is, have we seen code or this project before? Um you know, when you're operating at that scale, you can't rely on people remembering, "Oh, I've seen a project like that." It has to be automated. Um then we have a range of tools. Uh we have a source level checker, which is like a checker that is not really semantically based. It just looks for uh common patterns that indicate like this code is bad. My favorite example is if you see code that says x equals plus one,

um they probably meant to write x plus equals one. And so, you know, obviously setting a value to one when you meant to increment a value, that's not going to be a good bug. Um then we have things like visual program analyzers. So, a lot of this stuff, these are sort of classic problems, code comprehension. You're an auditor, somebody gives you new code, you know, what's the call graph? Uh what's the contract graph look like? What kinds of roles are there? What are the roles doing? This is like the kind of stuff that hackers will use to take your code apart. Um then we have a semantic level checker. Uh so, this was just sort of mentioned abstract interpretation, but these are data flow analysis, abstract interpretation. These can look for more sophisticated problems like along I have a critical function here along this path, there's no authorization check

making sure that for example that somebody can't just call this function eventually call mint directly from the internet. Then we have defect testing and we have model checking as well. So model checking the idea is that you can have specifications and you can automatically check whether the code meets the specifications or not. Um, so I I know only 5 minutes so I'm going to try to keep it short. So operating at scale. The first thing is we have a workflow system. So all of those tools, they're all knit together with a workflow system. The workflow system lets us scale our auditing down to if you need 3 days of auditing, we can do it. The business logic um, how you string things together, how you ingest the source code, it's all uh automated. So if you need 3 days or 90

days of auditing, we can scale down to that very low end. Um, we run the tools automatically on all projects. We don't give people any choice. Our auditors get no choice. The tools get run and we require security engineers to triage any findings that are minor or above. So, you know, a common problem you have is that like a tool will spit out a warning and then people will ignore it. Um, the thing is if you're a tools expert, what we're getting is we're getting feedback on false positives. So auditors, if they decide this finding isn't valid, they have to give us a reason. And so if you worked in static analysis tools, you know, this is a common problem. How do you get people to tell you that like this isn't working and why is it not working? Um, we have so many findings

that we actually use machine learning to group our manual findings. Because when you're going through, you know, 1,200 audits in 6 months, you can't rely on humans to check everything and knit it together. So we actually have a database of more than 60,000 findings that we built up over time. Um, and what we can do is we actually use machine learning to cluster the findings. We actually analyze our own reports, cluster the findings, and identify what new detectors we should build. So what kinds of new problems are you finding? Um certainly with smart contracts new problems keep coming up. This gives us two things. First of all, it's us So, we actually had a human do this and they came up with 2,400 clusters. That's still a large number of detectors to try

to build. When we applied machine learning we came up with about 500 clusters. And we had counts with them. So, now we know sort of what's important. This gives us feedback on the tool side on false negatives. We get some insight into what are the tools missing that they should have. Um and my main point would be that the data and scale create a positive feedback loop. So, it improves your quality and efficiency. So, you know, I think it's something that as an industry we should aspire to. We should aspire that everybody can get audits. They're high quality and they're um uh efficient. So, thank you. I I'll take any questions right now.

Thank you, David. Any questions for David? Yeah, can I uh huge amount of audits. Uh do you understand the amount of time that uh manually the auditor need to uh look after all these tools? Uh yeah. Yeah, we don't the the tools are really meant to help the auditors and provide a a base level of quality and a base level of efficiency. So, we actually have um uh you know, we actually um expect the auditors to spend significant time and we actually have estimates of that. Um and we can actually uh you know, um uh we actually expect Yeah, the problem

is the tools capture so actually had one more slide. Uh it's hard for the tools to capture higher level issues. So, like if your design is wrong or you've got a logical error like coding errors are easy. Tools are really great at that. On the other hand, if you've got a like a design error tools aren't so good at at that right now. So, really what we want is the manual auditing to focus in on the higher level issues. And you know, logical issues, tools are good and but they could get better. Um, but you know, so the higher up you go in the stack, the harder it is for the tools to detect them. You know, the thing you worry about as a security person is the I know I'm going on I know I've only got two minutes. You worry about the attacks

you don't know about. They added some new functionality and now you can be attacked because the new functionality is like broken in some way or adds an unexpected wrinkle to things. So, I will stop there. Thank you so much. Okay, thanks everybody. Applause for David.