Making Software Safer - Monmouth Magazine

Modern software often juggles sensitive dada, user privacy, and performance demands, all while operating in unpredictable, real-world conditions. In that environment, verification—the process of ensuring a program works as intended—is a critical form of quality control. But for today’s increasingly complex software systems, that control isn’t always easy to achieve.

Earlier this year, Weihao Qu, Ph.D., received a two-year grant from the National Science Foundation to develop a new software verification framework— one that allows more detailed, accurate analysis, particularly in programs that use mutable arrays, a data structure that can be difficult to test.

We asked Qu, an assistant professor in the Department of Computer Science and Software Engineering, about the challenges of verification and what he hopes to achieve through this work.

Why is software verification important?

Take a simple program like a login system, which people basically use for every application today. The danger is that it might leak your personal password information via side-channel attacks if the software is not written well.

But to verify that a login system doesn’t leak information, analyzing just one run of the program isn’t enough. That’s why we use what’s called relational reasoning—a method for comparing two different versions, or runs, of a program to see how they relate to each other. It’s a way of checking relationships between programs or program states, such as whether two security-related processes handle information in a similar way.

So, for the example of the login system, if we can compare two runs of the same login software, we can make sure that, no matter what the input is, whether the password is 100 digits or just two digits, the difference between the running time of the two runs is always zero or small. That consistency means the software is invulnerable to side-channel attacks. In other words, it will not leak your personal information.

How will you be using this grant to improve the software verification process?

There is already a lot of research in relation to software verification, and I have done some research work in this area. However, there is still one specific area that is particularly challenging, and that is programs that use mutable arrays.

Arrays are places that store data in a database in an ordered way. They’re important for verification because many programs use them to hold and manipulate information like lists of numbers, names, or other records.

Once a regular array is created, it doesn’t change, so it’s easier for testers to check that the program works correctly. But mutable arrays can change as the program runs, which makes verification more challenging.

Software testers have to consider not just the initial setup of the array but also every possible way it might change over time. This means more scenarios to check, more chances for mistakes, and a greater need to carefully track how the data moves so that the program can be trusted to work correctly.

My framework captures the behavior of individual array elements instead of treating arrays as a whole, which leads to significantly more detailed and accurate verification results.

What does that look like in practice?

When a programmer writes a program, we can add something to the programming language called a type system, which is like a set of rules that helps keep information organized and consistent so that a program runs smoothly. It makes sure numbers are treated like numbers, words are treated like text, and so on.

If a programmer uses mutable arrays and their program doesn’t clearly state what kind of data belongs inside, the type system can suggest or automatically fill in the missing information. A type system is valuable because it guides the process of keeping data safe and consistent, reducing error and making complex programs easier to verify.

But I developed a type system where a programmer has to follow its rules as specified in the system. So, if they write something that does not follow my rule, then the program won’t run. If they do follow the rules I define in the system, then the program will be verified, and it’s safe to run.

What is the end goal, or deliverable, of your project? Is it a product or a method that other organizations can use?

The end goal is a product, a piece of software, that people can buy. But it’s also a theory that can guide people to explore relational software verification for aspects of programming beyond mutable arrays, which is just one aspect of software programming.