Pattern matching information flow using GADT

Eric Lindahl, Victor L Winter

Research output: Contribution to conferencePaper

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 - Jan 1 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

Fingerprint

Pattern matching
Set theory
Computer programming languages
Processing
Secure communication

Keywords

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

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Information Systems

Cite this

Lindahl, E., & Winter, V. L. (2008). Pattern matching information flow using GADT. 255-262. Paper presented at 3rd International Conference on Information Warfare and Security, ICIW 2008, Omaha, NE, United States.

Pattern matching information flow using GADT. / Lindahl, Eric; Winter, Victor L.

2008. 255-262 Paper presented at 3rd International Conference on Information Warfare and Security, ICIW 2008, Omaha, NE, United States.

Research output: Contribution to conferencePaper

Lindahl, E & Winter, VL 2008, 'Pattern matching information flow using GADT' Paper presented at 3rd International Conference on Information Warfare and Security, ICIW 2008, Omaha, NE, United States, 4/24/08 - 4/25/08, pp. 255-262.
Lindahl E, Winter VL. Pattern matching information flow using GADT. 2008. Paper presented at 3rd International Conference on Information Warfare and Security, ICIW 2008, Omaha, NE, United States.
Lindahl, Eric ; Winter, Victor L. / Pattern matching information flow using GADT. Paper presented at 3rd International Conference on Information Warfare and Security, ICIW 2008, Omaha, NE, United States.8 p.
@conference{b4c7d36e998a4d65a710892438777d7f,
title = "Pattern matching information flow using GADT",
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.",
keywords = "GADT, Information flow, Non-interference, Security policies, Static analysis, Type systems",
author = "Eric Lindahl and Winter, {Victor L}",
year = "2008",
month = "1",
day = "1",
language = "English (US)",
pages = "255--262",
note = "3rd International Conference on Information Warfare and Security, ICIW 2008 ; Conference date: 24-04-2008 Through 25-04-2008",

}

TY - CONF

T1 - Pattern matching information flow using GADT

AU - Lindahl, Eric

AU - Winter, Victor L

PY - 2008/1/1

Y1 - 2008/1/1

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

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

KW - GADT

KW - Information flow

KW - Non-interference

KW - Security policies

KW - Static analysis

KW - Type systems

UR - http://www.scopus.com/inward/record.url?scp=84896541771&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84896541771&partnerID=8YFLogxK

M3 - Paper

SP - 255

EP - 262

ER -