- Interests
- Types
CS Colloquium - Formal Methods or Usable Security: Why Not Both?
Feb 14, 2025
03:30 PM - 04:30 PM
2 West Washington Street, Iowa City, IA 52240
Speaker
McKenna McCall
Abstract
Formal methods research involves using mathematical techniques to specify and verify properties of software and hardware systems. In security and privacy research, formal methods can lead to strong, provable security guarantees—and typically leave questions about how humans might interact with these systems unanswered. Indeed, formal methods and usable security are traditionally distinct areas of research. In this talk, I will demonstrate how techniques from both research areas can be applied—or even combined—to create solutions that are simultaneously mathematically rigorous and usable. In one project, we revisit static analysis tools for home IoT users from a usable security lens and investigate the usability and utility of the workflow involved in using the tools. Later in the talk, I will describe a project with a formal methods focus where we propose a new technique for preventing undesirable information flows on the web. We argue that this approach is usable in more realistic scenarios than what is proposed by prior work—without sacrificing security.
Bio
McKenna McCall is a postdoctoral researcher in the Software and Societal Systems Department at Carnegie Mellon University supervised by Lorrie Cranor and Lujo Bauer. She received her PhD from Carnegie Mellon University in 2023, advised by Limin Jia. McKenna’s research spans fields from information flow control and programming languages to security and privacy for home IoT and confidential computing. She is particularly interested in research where formal methods and usable security intersect, and combines techniques from both research areas to produce results that incorporate mathematical rigor as well as usability.
Individuals with disabilities are encouraged to attend all University of Iowa–sponsored events. If you are a person with a disability who requires a reasonable accommodation in order to participate in this program, please contact in advance at