Why You Must Make Your DEV Team Formally Verify Their New Feature Before Deployment

Morning everyone. My name is Rahul and today I'm going to be presenting on topic look twice before you're done. Uh it's a small presentation on why you should formally verify any software that you run on your servers. So unlike the olden days deleting the prod and backup data is not the only way to ruin your IT IT team's day. With the rise of AI and large language models, Microsoft claims that almost 50% of the code that's on GitHub right now is AI generated. What you all don't know is that 50% of the code that AI generates is also has a lot of security vulnerabilities in them because of the kind of data they're trained on. Most of

the code that's being written may be malicious on purpose or it can also be it can also be written by people who are not experienced enough to write secure code. which means that when you use chat GPD, cursor or any other AI assist to assist your coding, it might just be vulnerability as a service. So you need to be really careful on what you what code you push to your GitHub repos. It's especially prevalent with the junior and the interns who try to do wipe coding where they code only using prompts and not look at the program at all where it leads to disasters when it comes to application development. So cyber's all about adapting to the

situation, right? We as cyber security professionals must must adapt to what's happening at the moment. Access management before has protected the production database from unauthorized changes. We've had a massive improvement in backup protocols that ensure recovery and resilience of business operations during even the worst of disasters. But why is it that in the development phase of CI/CD pipelines and software life cycles that a lot of input is taken from the DevOps teams or the software engineering team and the managers but not enough input is being taken from the cyber team who's going to manage most of the inputs that's going to come as requests to these apps when they're actually on the servers. You guys have

to actually look into what kind of requests are coming in and if they use or misuse cases. So it's really important that the cyber cyber security team is also involved heavily from the beginning of the development phase. How can this be achieved? By formal verification. So what is formal verification? Think of it like your program being turned into a switchboard with a bunch of switches. What do I mean by that in technical terms is that your program is turned into a set of boolean math equations. So you have each statement that's being passed into low-level code that is kind of turned into a resulting value that results in either true or false. So it's easier for

us to compare it against certain verification conditions or patterns that are known that are most known common vulnerabilities. Think of buffer overflow conditions or tightness matches. I'm pretty sure the red team might actually understand a bit more of these but if you are not much well versed in code that's fine too. All you need to know is that there are certain patterns that we can find in a program that will make that will let you know that yes there is a high chance that it can be exploited. So using these using some opensource tools or which are highly flexible and customizable will ensure that you catch these errors early on into the development phase before

they are even pushed to the production. They are well tested. So when you use these tools in the CI/CD pipelines or and you encourage your developers to do so you're not asking them to do software testing just for software functionality but also for software security which I feel that is a must have a bigger importance being placed on them as we go on you can say cool but I don't make websites or software where can I use these tools there are wide use cases for such tools of formal verification that's just goes goes beyond everyday software development. You don't have to be in the software testing or the software development team to use these tools or

incorporate them to your workflow. Are you defining network protocols for your routers? Are you defining network architecture that with a lot of config files in your home lab or maybe in the lab at your organization or are you handling cryptocurrency transactions in Ethereum or Bitcoin that are defined by contracts? A lot of layman a lot of the common people do not know what the Bitcoin contracts or the Ethereum contracts are and if they want to make investments or if they want to do something uh with these contracts it's better to verify them using these tools or you are working in a critical environment like healthcare or the timesensitive systems like in a hedge fund where you define distributed

systems where a lot of these times these company companies use timesensitive systems where they have to make a lot of uh monetary transactions within seconds and a delay of even a millisecond can cause a lot of loss for that company. So if you're going to write something that works at a critical environment or if something is of high importance, verifying that the applications work as intended and the system is distributed with resources as intended in the configuration files goes a long way. Or you can just use this in a CTF challenge to see if a code is vulnerable or not. the the limitation is only based on what tool what the tool is targeted for and

there are a lot of tools for let's just go for an example right so I'm going to use a general C example of a C code nothing too fancy it's I've simplified it as much as I can um if you can see here in this code uh on the integer array there are three values and I'm trying to access an array that's a number that comes after the number 30 which doesn't exist. There is no I'm trying to access a data that doesn't exist. So if we leave code like this unchecked in the GitHub profile uh in the GitHub repo which is eventually run on servers. Obviously in this scenario a compiler might catch it. But in large

cases where there is a lot of memory handling when such codes run on repositories, you can have arbitrary code execution which is basically like a person can manipulate the memory to do uh execute any code any code he wants or extract data that's on the RAM. So when I use a tool like ESBMC uh which is one of the open source tools that's available as a formal verification tool and I pass this code as a test input file as you can see in the red box that's highlighted with the command. It gives me an exact counter example and the kind of vulnerability that's found in the exact line of code that is present in the software or in that

particular line of code that's there. So it can help the programmers detect security vulnerabilities or like coding mal practices. Um and and at the same time it can allow for people for people who work in cyber security teams to easily identify errors in code uh which can lead to a security vulnerability without having to read every single line of the program. So it's a tool that verifies a lot of C C++ programs or even Python and Java. It's versatile and the current research of this tool also involves self-healing code with the use of LLMs. It automatically catches areas that are security that have a lot of security vulnerabilities and it kind of restructures the code and pushes it back

to the repository so that it doesn't have the it so that the errors are fixed. Let's take a real life example of an Ethereum contract this time. U the last example was a bit more simple and this might get a little bit technical but promise uh it won't be too hard. An Ethereum contract is in a sense is like a blockchain contract. So a blockchain contract is basically like any legal document or contract that's written in a program. Let's say I write a contract that says if I pay $1 to the other person, they might give me $5 back. That's a contract and it'll be in a blockchain. King of Ether Throne was one such contract that was a very well-known

Ponzi scheme from back in the day when Ethereum was just introduced and and it was the height of Bitcoin and blockchain technology. A lot of people lost money to this Ponzi scheme. But on a quick scan of that file using this tool called myill which is also open source and it's really customizable. It tells you quickly if the code that you that the the exact line of code if it's vulnerable if the contract is malicious or what exact how exactly you might get exploited on paying to that contract or subscribing to that contract. So if it's a lot of output here, but if you can see at the top when I ran this using my it gave me

a small summary of what that exa exact exploit is. Any sender can withdraw their ether from the contract account. That means that any sender can withdraw the money that they've deposited into the contract and that and and arbitrary senders can verify the business logic carefully. It's it's just a lot of words that mean that any person who has contributed some money to the contract can take all the money away from you. So it's if so this might indicate the Ponzi schemes before you might which you might fall for it if you don't know what you're actually doing. So how can you actively incorporate such tools within your workflow? You can encourage developers to add these tools

into their CI/CD pipelines for automatic checks before pushing the code to the repository. Since it's not some heavy testing where they have to write unit codes for unit testing codes for it's not a big ask to ask them to add this to GitHub workflows or GitHub actions where this is automatically run and it will give you an output saying where exactly went wrong and it's a small fix. So I feel that encouraging them to adopt these technologies and include in including yourself into the development process as a cyber security team and I actively contributing to the security of the application during the development process can really help you out. There [clears throat] are general tools for

verification in different languages. The two examples I've showed you is only for C, C++, Python. The first one and the second one is very blockchain specific depending on if you want to know about how many how much resources it consumes and all that stuff. But there are verification tools that are very specific for different specific needs. If you want to talk about configuration of network, network configuration, formal verifications, there are tools for that as well. It's about choosing the tool that you need. Most of these tools have open source alternatives as well which allows for further customization and it gives you the flexibility to define your own rules and patterns. As long as there's a pattern

where there's a vulnerability, you can define what exact grammar of code or configuration that you want them to follow and you can customize that and you can let your team have a specific set of rules that can be internal as well depending on what you're programming. So I'm just giving a tiny look under the hood of how these formal verification tools really work. This part might just be a bit more technical. Your programs are first generated into tokens just like a compiler like go to statements which is a very low-level representation of the code. In case of blockchain contracts is done in bite code level. These are then converted into true false boolean expressions called semantic

model theories or SMT formulas. And these formulas are then solved against certain conditions called verification conditions if satisfied mean a vulnerability is present. These solves are usually done by SAT solvers which are a separate kind of mathematical uh engines that are built as back end for these uh uh formal verifiers and they are really important in solving boolean equations. So thank you so much for attending my talk today and I hope you have taken some [applause]

[applause] uh you're open for any questions if we still have time. >> Yeah, >> please. Um, in my experience, I'm not a developer. I've worked security for years. When you ask develop in my experience, um, when you ask developers to run these two, a lot of them I think [clears throat] have a fear that it's a personal attack on their ability. And there is I've seen a certain amount of reluctance >> for people to um be put under the spotlight on their work on their code to be put into the spotlight because a lot of people working remotely developing in their own bedrooms and suddenly when you put a spotlight on them >> yeah it sort of I think it I think there fear

or there is a fear that it interferes with their creativity and their flare because they created something really nice and somebody that that's a really good question because as coming from a background of software engineer who has moved into cyber security I really understand that particular point of asking us to do something where we point out the flaws and be like hey this is wrong fix it but here's the thing cyber security as a profession is a little bit different from DevOps and that's different from software engineering, you each have your own expertise and security is a collective issue. It's a collective responsibility. So, it's not an easy conversation to approach in general. Yes. But it's a challenge that we must

overcome if we need if our ultimate aim is to build secure software that works perfectly as intended. It's in in fact these tools, the formal verification tools that I've mentioned are not something that work just like a compiler. So if a programmer makes any syntax errors or when he's typing out and when he makes some kind of like spelling mistakes or something, it points out saying, "Hey, in this exact line of code, you've made this mistake." This tool just takes it a step further and lets him know that [clears throat] him or her know that there's a problem in these three lines of code. How about restructuring them somewhere somehow different? If you don't, this problem

can occur. So when you have when you break down the big problems as such it can really help uh bring the team together to build secure software. So yeah hope that answers the question. Thank you. [applause]