Dynamic Updating - Complete Publications

[1] Boniface Hicks, Kiyan Ahmadizadeh, and Patrick McDaniel. Understanding practical application development in security-typed languages. In 22nd Annual Computer Security Applications Conference (ACSAC), Miami, Fl, December 2006. [ bib | .pdf ]
Security-typed languages are an evolving tool for implementing systems with provable security guarantees. However, to date, these tools have only been used to build simple "toy" programs. As described in this paper, we have developed the first real-world, security-typed application: a secure email system written in the Java language variant Jif. Real-world policies are mapped onto the information flows controlled by the language primitives, and we consider the process and tractability of broadly enforcing security policy in commodity applications. We find that while the language provided the rudimentary tools to achieve low-level security goals, additional tools, services, and language extensions were necessary to formulate and enforce application policy. We detail the design and use of these tools. We also show how the strong guarantees of Jif in conjunction with our policy tools can be used to evaluate security. This work serves as a starting point-we have demonstrated that it is possible to implement real-world systems and policy using security-typed languages. However, further investigation of the developer tools and supporting policy infrastructure is necessary before they can fulfill their considerable promise of enabling more secure systems.

[2] Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic. Managing policy updates in security-typed languages. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06), July 2006. to appear. [ bib | .pdf ]
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 rolebased 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 flow. 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.

[3] Boniface Hicks, Dave King, Patrick McDaniel, and Michael Hicks. Trusted declassification: High-level policy for a security-typed language. In ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, Ottawa, Canada, June 10 2006. To appear. [ bib | .pdf ]
Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of nonin- terference which ensures that high-security data will not be observ- able on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassifi- cation to selectively leak high security information, e.g. when per- forming a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult.

In this paper, we propose a simple idea we call trusted declas- sification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declar- atively specify which declassifiers they trust so that all informa- tion flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java- like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have imple- mented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.

[4] Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic. Dynamic updating of information-flow policies. In Proceedings of the Foundations of Computer Security Workshop (FCS '05), March 2005. [ bib | .pdf ]
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 for 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.

[5] Boniface Hicks, Dave King, Patrick McDaniel, and Michael Hicks. Trusted declassification: High-level policy for a security-typed language. Technical Report NAS-TR-0033-2006, Networking and Security Research Center, Department of Computer Science, Pennsylvania State University, March 2006. [ bib | .pdf ]
Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterference for all their data. Unfortunately, real programs almost always require the use of noninterference-violating flows introduced by declassification. This causes the global policy to break down and obscures the meaning of security labels. These languages suffer from the lack of an alternative, global policy which can handle declassifications. In this paper, we present a security-typed, object-oriented language which allows trusted declassifications based on a global policy. We prove the soundness of our language as well as a modified form of noninterference, which we call noninterference modulo trusted declassification. We implement our declassification mechanism and global security policy in Jif and provide some examples which motivate its use.