Abstract

Integrating security policies into security assurance mechanisms to ensure end-to-end behavior is still a challenge. Information flow analysis and type checking are effective methods for the analysis and verification of secure communications and processing. Language-based information flow security models use programming-language for specifying and enforcing security policy. Dependently typed programming is an efficient and powerful way to concisely communicate, represent, and then reason over security policies. In this paper we demonstrate an integration of policy elements in a subset of a language-based information flow security model implemented using dependent type programming. We illustrate how recent advances in type theory in secure domains make available enabling technologies for developing policy aware secure computing.

Key words: GADT, information flow, non-interference, static analysis, type systems, security policies