Jonathan Aldrich

*Please note: this CyLab seminar is open only to partners and Carnegie Mellon University faculty, students, and staff.

Speaker:
Jonalthan Aldrich
Professor of Computer Science and Software Engineering
Carnegie Mellon University

Talk Title:
(Sub)-structural Information Flow: A Simple, Scalable, and General Foundation for Security Reasoning

Abstract:
Information flow is a foundational property underlying a wide variety of security issues. Type systems are a promising approach to reasoning about information flow, but the complexity of previously proposed approaches has limited adoption. We propose a new foundation for information flow types: (sub-)structural information flow. Rather than placing constraints on polymorphic labels, we build information flow types as a structural set lattice. The resulting system is not only significantly simpler and more scalable, it also for the first time positions declassification as compatible with noninterference, rather than in opposition to it. Our approach, presented in recent papers at OOPSLA'25 and POPL'26, can be extended to substructural labels in order to support capabilities, quantitative information leakage, sandboxing, authorization protocols, and more. In addition to security applications, we are studying a novel theory of type system usability that emerges from our approach as well as related work in Rust lifetime tracking. This is joint work with Hemant Gouni and Frank Pfenning.

Bio:
Jonathan Aldrich is a Professor of Computer Science and Software Engineering at Carnegie Mellon University, where he directs the Master of Software Engineering program. He is the coauthor (with Michael Scott) of the textbook Programming Language Pragmatics, 5th edition. His research combines programming languages, software engineering, and human-computer interaction to explore how the way we express software affects our ability to engineer software at scale. A particular theme of much of his work is improving software quality and programmer productivity through better ways to express structural and behavioral aspects of software design within source code. Aldrich has contributed to ownership, typestate checking, modular and gradual verification techniques, and usability in programming language and type system design. For his work specifying and verifying architecture, he received a 2006 NSF CAREER award, the 2007 Dahl-Nygaard Junior Prize, and an ICSE test of time award. Outside the university, he serves on the ACM Publications Board and is the CTO of Noteful, a startup delivering an educational app for music theory and note reading.

Upcoming Events

Browse All Upcoming Events