Language-based security (the use of programming language abstractions and techniques for security) holds the promise of efficient enforcement of strong, formal, fine-grained, application-specific information security guarantees. However, language-based security has not yet reached its potential, and is not in widespread use for providing rich information security guarantees.
This research makes language-based security techniques more practical, and thus helps improve the information security of new and existing computer systems. It does so through three complementary approaches.
First, this project develops techniques to make information security guarantees proportional to programmer effort, which both reduces the cost of entry for attaining formal information security guarantees, and allows incremental improvement of a program?Äôs security guarantees, as resources and requirements allow. Second, this project develops new ways to express and reason about rich information-security requirements, such as the required release of information, availability requirements, production of audit logs, and anonymity requirements. Third, information security in concurrent settings is addressed by exploring synergies with newly developed concurrent language mechanisms.
Techniques and mechanisms resulting from these explorations will be incorporated into a new programming language that helps programmers build computer systems with formal, fine-grained, application-specific information security guarantees.
