@conference {14755,
	title = {Verified Enforcement of Security Policies for Cross-Domain Information Flows},
	booktitle = {IEEE Military Communications Conference, 2007. MILCOM 2007},
	year = {2007},
	month = {2007/10/29/31},
	pages = {1 - 7},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {We describe work in progress that uses program analysis to show that security-critical programs, such as cross-domain guards, correctly enforce cross-domain security policies. We are enhancing existing techniques from the field of Security-oriented Programming Languages to construct a new language for the construction of secure networked applications, SELINKS. In order to specify and enforce expressive and fine-grained policies, we advocate dynamically associating security labels with sensitive entities. Programs written in SELINKS are statically guaranteed to correctly manipulate an entity{\textquoteright}s security labels and to ensure that the appropriate policy checks mediate all operations that are performed on the entity. We discuss the design of our main case study : a web-based Collaborative Planning Application that will permit a collection of users, with varying security requirements and clearances, to access sensitive data sources and collaboratively create documents based on these sources.},
	keywords = {Collaboration, Computer languages, Data security, Educational institutions, Government, Information analysis, Information filtering, Information filters, Information security, Vehicles},
	isbn = {978-1-4244-1513-7},
	doi = {10.1109/MILCOM.2007.4455189},
	author = {Swamy,Nikhil and Hicks, Michael W. and Tsang,Simon}
}
