Session Types and Phase Distinctions for Noninterference
Abstract
The purpose of this research is to investigate the development of programming language techniques to express and enforce constraints on the flow of information in a program. Type systems are the most widely applicable tool for enforcing such restrictions within and among programs. The aim of the project is to investigate the development of suitable type systemsfor information flow security in two settings, and to understand their inter-relationship. In each case, the goal is to state and prove non-interference properties of programs that ensure the independence of non-sensitive outputs on sensitive inputs to a system. Both methods draw on the method of logical relations to establish these properties.The first setting is that of session types for communicating programs. In their most basic form session types express the protocols for interaction among programs that interact along data-carrying communication channels. A key characteristic of session types is that they are able to track changes of state in a computation using methods drawn from substructural logic. The intent ofthe investigation is to extend session types to track information flow in a composite program using refinement types that encode security levels of data.The second setting is that of program modules which govern the construction of programs from separable, reusable components. Type systems for modularity are primarily concerned with the interfaces between components, which ensure that the effects of changes to a module implementation on other modules in a system can be tightly controlled. The project will investigate the extension of module type systems to express information flow dependencies among components using a generalization of the phase distinction between static and dynamic aspects of a program to account for a richer hierarchy of security levels.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 07, 2023
- Source ID
- FA95502110385
Entities
People
- Stephanie Balzer
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- United States Air Force