New Assistant Professor Evan Johnson Takes a Mathematical Approach to Cybersecurity

For Evan Johnson, cybersecurity is a field defined by a deceptively simple question: How do you make sure software doesn’t do something?

That question has taken Johnson from hacking competitions as an undergraduate to research on airplane firmware and, eventually, to the study of how computer systems can be mathematically proven to be secure. Now, as an incoming assistant professor at NYU Tandon, he will continue working at the intersection of cybersecurity and programming languages, where he focuses on some of the most security-critical pieces of modern computing systems.

Johnson grew up in Bloomington, Illinois, a small college town about 45 minutes from Urbana-Champaign. He was involved in science clubs in school before enrolling at the University of Illinois Urbana-Champaign to study computer engineering. It was there that he first became interested in cybersecurity through a student club that organized hacking competitions, giving participants simulated security problems to solve.

Near the end of his undergraduate career, Johnson began research with professor Kirill Levchenko. His first project involved looking for security vulnerabilities in airplane firmware. His introduction to the work was memorable: Levchenko gave him a box containing the circuit boards that made up the flight management computer of a Boeing 737 and told him to extract the firmware and investigate what he found.

The project was conducted in collaboration with Stefan Savage at the University of California, San Diego, a connection that eventually brought Johnson to UCSD for his PhD. Working with Savage and Deian Stefan, he studied technologies for sandboxing software. Sandboxing can limit what happens when an attacker exploits a program, potentially allowing the compromised application to fail without giving an attacker access to sensitive information elsewhere on the system.

Johnson was drawn to cybersecurity in part because of how deeply it requires researchers to understand the technology they are protecting.

“You get to kind of work on every layer of the tech stack,” he says.

Security can require knowledge of hardware, operating systems, compilers and programming languages because vulnerabilities in one layer can affect the behavior of the others. For Johnson, that systems-level perspective is one of the field's biggest attractions.

His current research focuses on the portions of those systems that are particularly important for maintaining security. An operating system may contain an enormous amount of code, but only relatively small sections, such as a bootloader, may be responsible for enforcing critical security guarantees. Johnson uses a technique called formal verification to examine these components.

The approach involves describing a system's behavior precisely enough to construct a logical proof that the system is correct. In one of his recent projects, Johnson formally verified an operating system to show that it correctly secured users' data. The operating system is used in systems including Chromebooks and some Windows machines.

NYU's combination of cybersecurity and programming-languages expertise was a major attraction for Johnson. At Tandon, he expects to collaborate with Justin Cappos, whose research also involves sandboxing software and limiting the impact of exploits. He is also looking forward to working with programming-languages researchers at NYU's Courant Institute.

“I kind of work at the intersection of PL and security,” Johnson says. “Courant has the PL people, and there are a lot of security people at Tandon.”

Johnson will also bring his approach to the classroom. This fall, he will teach NYU's main undergraduate and graduate security course. He has redesigned portions of the course to reflect a changing software landscape, particularly the rise of artificial intelligence tools that can generate large amounts of code.

As AI makes writing code faster, Johnson argues, understanding and evaluating existing code becomes increasingly important. Students will work with a small web browser designed specifically for the course, learning to understand its existing code, identify its assumptions and assess whether changes introduce new problems. Even if students use AI to modify the software, they will need to determine whether those changes have unintended consequences elsewhere.

AI is also beginning to influence Johnson's research area. Researchers are experimenting with using large language models to generate the proofs required for formal verification, although Johnson says the results remain mixed. Still, he sees promising ideas emerging.