SHF: Small: Gradual Information Flow Control

This project focuses on enhancing program security by controlling how information flows within software, a concept known as Information-Flow Control (IFC). Imagine a program handling sensitive data, like medical records or financial transactions; IFC ensures that this sensitive information doesn't accidentally leak to unauthorized parts of the program or to external users. Traditionally, developers choose between two methods: static enforcement, which checks for security issues before the program runs, offering strong guarantees but requiring more upfront effort, or dynamic enforcement, which monitors information flow as the program runs, requiring less initial effort but potentially introducing runtime overheads and weaker guarantees. This project takes inspiration from "gradual typing," a technique that allows programmers to seamlessly blend these approaches, choosing the right balance of static and dynamic security checks for different parts of their code. The project’s novelties are in bridging the existing gap between theoretical concepts of gradual IFC and their practical implementation and application in real-world scenarios. The project's impacts are in enabling more flexible and efficient development of secure software, making it easier for developers to build applications that protect secure information without sacrificing performance or programmer productivity. The project addresses the theoretical and practical challenges of gradual IFC. On the theoretical front, the investigator mechanizes the noninterference proof for LambdaIFCStar, a gradual IFC language, ensuring its security properties are formally verified using tools like Agda. The project also explores a space-efficient semantics for LambdaIFCStar to optimize its memory usage. From a practical perspective, the investigator implements LambdaIFCStarPlus, an extended version of LambdaIFCStar, by developing a new compiler called GriftIFC. This compiler, based on the existing Grift framework, incorporates security types and coercions, and aims to provide an efficient implementation of gradual IFC. Through case studies in domains such as blockchain, e-voting, and mobile applications, the project evaluates the expressiveness of LambdaIFCStarPlus and analyzes the performance overheads of gradual IFC compared to purely static or dynamic IFC systems. The project's outcomes include open-source releases of mechanized proofs, the GriftIFC compiler, prototype applications, and a performance benchmark suite. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.