Verified Enforcement of Security Policies for Cross-Domain Information Flows

TitleVerified Enforcement of Security Policies for Cross-Domain Information Flows
Publication TypeConference Papers
Year of Publication2007
AuthorsSwamy N, Hicks MW, Tsang S
Conference NameIEEE Military Communications Conference, 2007. MILCOM 2007
Date Published2007/10/29/31
ISBN Number978-1-4244-1513-7
KeywordsCollaboration, Computer languages, Data security, Educational institutions, Government, Information analysis, Information filtering, Information filters, Information security, Vehicles

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'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.