@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} }