Distributed systems are an increasingly crucial part of modern computing infrastructure, yet the existing technology for ensuring their security and reliability is lacking. This research addresses the problem of building distributed systems and reasoning about their security by developing programming languages that provide better abstractions for describing security policies and communication protocols.
The starting point for this project is existing work on security-typed languages, which protect data confidentiality and integrity. This research generalizes these information-flow policies to make them more dynamic, enabling them to accommodate the changing environment in which distributed systems run. For example, dynamic information-flow policies should integrate cleanly with traditional authentication and access control mechanisms to provide end-to-end guarantees about data confidentiality.
The second stage of this project is to develop language technology that applies dynamic security policies to distributed programs. The idea for this part of the research is to develop a theoretical basis for secure distributed computing using existing process calculi augmented with a heterogeneous trust model and the policy language outlined above. In this setting, types describe communication protocols, properties of which can be verified statically by the compiler. The result will be a programming language with a sound type system that aids the programmer in writing correct, security-critical distributed programs.
