Defending against memory buffer overflow attacks is a daunting proposition for computer software developers.

Failing to carefully specify appropriate inputs opens the door for hackers to insert malicious code by overwhelming a system’s memory space with unanticipated inputs.

But how do you plan for every possible type of input a hacker could use? You turn to Vijay Ganesh.

An electrical and computer engineering professor at the University of Waterloo, Ganesh has developed a number of SMT/SAT solvers: cybersecurity programs that generate test inputs, letting developers pinpoint and address vulnerabilities before their software hits the market.

When he started his research in the early 2000s, people told him the challenge was so impossibly complex that he was wasting his time. You can never come up with an algorithm to solve these kinds of equations, his colleagues said, since the number of potential inputs is exponentially large.

Cybersecurity solution narrows possibilities

Ganesh proved them wrong.

Although their observation is true in theory, in most cases the number of possibilities can be narrowed down to a manageable amount based on the fact that software isn’t a random collection of code.

“What we’re saying is that often the kind of constraints we get from practical applications tend to have a lot of structure to them,” Ganesh explains. “At first glance, it might seem that the search space is two to the millionth for some of these formulas, but in practice it would be much smaller because of all the structures you can leverage.”

Ganesh was lured to Waterloo in 2012 after completing a PhD at Stanford University and a research position at the Massachusetts Institute of Technology (MIT). It was an easy choice for him.

“Waterloo has a fantastic reputation in America,” he says. “Whenever I go back to MIT or Stanford and say I’m teaching at Waterloo, they’re very proud of me.”

Since arriving, Ganesh has racked up distinctions including an Ontario Early Researcher Award, an IBM Faculty Award and his second Google Research Award, not to mention several best-paper honours. He attributes much of that success to the quality of his research team.

Research team ‘absolutely fantastic’

“I have an absolutely fantastic group of students,” he says.

Recognition has opened doors to collaborations with the likes of Google, IBM and Microsoft, where Ganesh’s cybersecurity algorithms are helping ensure their software is more robust, reliable and secure.

While seeing his work applied in practical settings has been very satisfying, Ganesh is also excited by more esoteric applications.

“There are problems that mathematicians would like to solve but they cannot by human reasoning alone,” he says. “My long-term goal in the next five years is to apply these tools to prove theorems in mathematics that are otherwise difficult or perhaps even impossible for humans alone to prove.”

It wouldn’t be the first time Ganesh has tackled intractable problems and triumphed.