Dynamic Updates of Security Policies
People Background Objectives Papers Funding
Boniface Hicks
Michael Hicks
Nikhil Swamy
Stephen Tse
Steve Zdancewic

Security policies govern the execution of a program by defining a set of permissible behaviors of the program. For instance, a policy might specify that only a program acting on behalf of Alice or Alice's doctors is permitted to access her health care records.

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.

The objective for this project is to design and implement programming languages that permit security policies to be updated at runtime. We will validate our solution by constructing a large application that models the management of health care records.

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.

Managing Policy Updates in Security-Typed Languages.
Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic.
In Proceedings of the 19th Computer Security Foundations Workshop (CSFW-2006), July 2006

    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) ]

      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

Dynamic Updating of Information-Flow Policies.
Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic.
In Proceedings of the International Workshop on Foundations of Computer Security (FCS), June 2005.

    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 ]

      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}
This work is funded in part by grant CCF-0524036 from the National Science Foundation. The views expressed here do not necessarily represent those of our funding sources.