Paschal Amusuo

Paschal Amusuo, a PhD student in Purdue University’s Elmore Family School of Electrical and Computer Engineering, is addressing some of the most pressing challenges in software security—earning national recognition in the process. Amusuo is a finalist for the highly competitive 2025 Qualcomm Innovation Fellowship and has presented his work at the prestigious 2025 International Conference on Software Engineering. He is a student of James Davis, assistant professor of electrical and computer engineering.

Amusuo’s research tackles two critical problems that impact the security and reliability of the software systems we all rely on, from smartphones and cloud apps to industrial and aviation infrastructure. He believes in a vulnerability free world and is working to equip software engineers with the tools to validate the security and reliability of third-party code they use and the proprietary code they write. Amusuo’s experience in dealing with security vulnerabilities has led to internships with major technology companies, Google and Qualcomm. His research protects software engineers from vulnerabilities in third-party code they use, while helping them find vulnerabilities in the code they write.

“Software vulnerabilities threaten the security of critical systems,” said Amusuo. “My research develops more cost-effective methods to discover these flaws early, providing formal security guarantees for in-house code with runtime guarantees for third-party libraries. By giving engineers practical tools and security guarantees, we aim to prevent vulnerabilities before software deployment and move toward a future where only secure software is released.”

One key focus of his work is third-party software code. Developers frequently use prewritten components—like the widely known Log4j library—to build applications faster and more efficiently. However, these components often have unrestricted access to the broader system, regardless of how trustworthy they are. If a vulnerability exists in one of these third-party libraries, attackers can exploit it and compromise the entire application.

Amusuo proposes a shift in thinking. Inspired by Zero-Trust Architecture, a model that assumes no part of a system should be trusted by default, he applies this principle within the application itself. His system, ZTD-SYS, and a prototype for Java applications, ZTD-JAVA, enables software engineers to limit the privileges of third-party code and monitor their behavior at runtime. Evaluation results of ZTDJAVA show that it successfully blocks exploits of known dependency vulnerabilities, has zero performance overhead and is easy to configure. This new way of thinking significantly reduces the risk of compromise while keeping applications efficient and user-friendly. Amusuo goal is to make ZTDJAVA a suitable replacement for the deprecated Java Security Manager.

Amusuo’s second area of research—which forms the basis of his Qualcomm Innovation Fellowship recognition—addresses how developers ensure the correctness of their own code.

Formal verification offers a rigorous method for proving that software behaves as expected under all conditions, much like how a mathematical proof guarantees a theorem. But while powerful, formal verification can be difficult to apply to large, real-world systems. That’s where unit proofing comes in—breaking down real-world softwareinto manageable pieces using unit proofs to verify each one individually (a process very similar to unit testing).

Through an in-depth study of unit proofing practices at organizations like Amazon Web Services (AWS), Amusuo found that current approaches are often manual, inconsistent, and prone to error. In some cases, flawed unit proofs can even obscure serious software defects rather than reveal them.

To address this, Amusuo has developed a research framework to support more reliable and efficient unit proofing. He created a new systematic process for creating unit proofs that reduced the time to verify software by 16x and has so far led to the discovery of 20 zero-day security vulnerabilities.  He is currently working on building tools to facilitate this unit proofing process, including helping engineers decompose software into verifiable components, write accurate unit proofs, repair faulty ones, and keep them updated as the software evolves. He is also exploring how program analysis techniques and large language models—such as those behind tools like ChatGPT—can automate portions of this process.

His goal is to create an ecosystem where software verification is cheap enough that it can be applied during software development, across a broader range of software systems. If successful, this approach could transform how software is tested—reducing reliance on traditional methods like fuzzing or unit testing—and help engineers discover critical code-level bugs and security vulnerabilities earlier and more consistently.