Pattern matching information flow using GADT

Eric Lindahl, Victor Winter

Research output: Contribution to conferencePaperpeer-review

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.

Original languageEnglish (US)
Pages255-262
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

Conference

Conference3rd International Conference on Information Warfare and Security, ICIW 2008
CountryUnited States
CityOmaha, NE
Period4/24/084/25/08

Keywords

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

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Information Systems

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

Cite this