Pattern matching information flow using GADT

Eric Lindahl, Victor Winter

Research output: Contribution to conferencePaperpeer-review


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.

Original languageEnglish (US)
Number of pages8
StatePublished - 2008
Event3rd International Conference on Information Warfare and Security, ICIW 2008 - Omaha, NE, United States
Duration: Apr 24 2008Apr 25 2008


Conference3rd International Conference on Information Warfare and Security, ICIW 2008
Country/TerritoryUnited States
CityOmaha, NE


  • GADT
  • Information flow
  • Non-interference
  • Security policies
  • Static analysis
  • Type systems

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Information Systems


Dive into the research topics of 'Pattern matching information flow using GADT'. Together they form a unique fingerprint.

Cite this