Security-typed languages are a promising method for enforcing security policies. In contrast to dynamic techniques (such as stack inspection), security-typed languages offer a static guarantee that all possible executions of the program are consistent with a given security policy. To achieve this, types in security-typed languages are augmented to include information from the security policy. Type-checking a program in a security-typed language amounts to security checking.

Aside from the obvious benefit of a static proof of compliance with a security policy, security-typed languages also typically offer a strong end-to-end security property called noninterference. Informally, noninterference ensures that the high-security inputs to a program do not influence the low-security outputs of the program.

A downside of most security-typed languages is the simplifying assumption that the security policy remains unchanged for the entire duration of the program's execution. This assumption is not viable for complex, long-running programs and might explain in part the lack of adoption of security-typed languages for the development of real applications.

Changes to policy must be secure: first, the execution of the program after the policy has changed must be consistent with the new policy; second, sensitive information must not be leaked through the state of the policy. Additionally, we also wish to reason about policy evolution to ensure that changes to policy do not inadvertently violate application specific security requirements.

We have begun exploring solutions to this problem in the context of small formal languages. Our approach, so far, has been twofold. First, we use a type-system enriched with security information to reason statically about information flows in the program. Second, we use dynamic techniques (such as runtime inspection of the program source and policy; transactional memory etc.) to ensure that changes to the policy are consistent with both the state of the program as well as prior policies.

This paper presents RX, a new security-typed programming language with features intended to make the management of information-flow policies more practical. Security labels in RX, in contrast to prior approaches, are defined in terms of owned roles, as found in the RT role-based trust-management framework. Role-based security policies allows flexible delegation, and our language RX provides constructs through which programs can robustly update policies and react to policy updates dynamically. Our dynamic semantics use statically verified transactions to eliminate illegal information flows across updates, which we call transitive flows. Because policy updates can be observed through dynamic queries, policy updates can potentially reveal sensitive information. As such, RX considers policy statements themselves to be potentially confidential information and subject to information-flow metapolicies.

[ .pdf | Technical Report (pdf) | Presentation slides (pdf) ]

@MISC{swamy06rx,
  TITLE = {Managing Policy Updates in Security-Typed Languages},
  AUTHOR = {Nikhil Swamy and Michael Hicks and 
            Stephen Tse and Steve Zdancewic},
  NOTE = {Submitted for publication},
  MONTH = {February},
  YEAR = 2006
}

Applications that manipulate sensitive information should ensure end-to-end security by satisfying two properties: sound execution and some form of noninterference. By the former, we mean the program should always perform actions in keeping with its current policy, and by the latter we mean that these actions should never cause high-security information to be visible to a low-security observer. Over the last decade, security-typed languages have been developed that exhibit these properties, increasingly improving so as to model important features of real programs. No current security-typed language, however, permits general changes to security policies in use by running programs. This paper presents a simple information flow type system that allows for dynamic security policy updates while ensuring sound execution and a relaxed form of noninterference we term noninterference between updates. We see this work as an important step toward using language-based techniques to ensure end-to-end security for realistic applications.

[ .pdf ]

@INPROCEEDINGS{hicks05secupdate,
  AUTHOR = {Michael Hicks and Stephen Tse and 
            Boniface Hicks and Steve Zdancewic},
  TITLE = {Dynamic Updating of Information-Flow Policies},
  BOOKTITLE = {Proceedings of the International Workshop on 
               Foundations of Computer Security (FCS)},
  MONTH = {June},
  LOCATION = {Chicago, IL},
  YEAR = {2005}
}