Making security type systems less ad hoc

Tobias Nipkow; Andrei Popescu

doi:10.1515/itit-2014-1060

Making security type systems less ad hoc

Tobias Nipkow, Andrei Popescu

Default

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

Abstract

We present a uniform, top-down design method for security type systems applied to a parallel while-language. The method takes the following route: from a notion of end-To-end security via a collection of stronger notions of anytime security targeting compositionality to a matching collection of type-system-like syntactic criteria. This method has emerged by distilling and unifying security type system results from the literature while formalizing them in a proof assistant. Unlike in our previous papers on this topic, here we focus entirely on high-level ideas instead of technical proof details.

Original language	English
Pages (from-to)	267-272
Number of pages	6
Journal	IT - Information Technology
Volume	56
Issue number	6
DOIs	https://doi.org/10.1515/itit-2014-1060
State	Published - 28 Dec 2014

Keywords

ACM CCS, Security and privacy, Software and application security, ACMCCS, Computingmethodologies, Concurrent computing methodologies, ACM CCS, Theory of computation, Semantics and reasoning

Access to Document

10.1515/itit-2014-1060

Cite this

@article{af7f28b308a7424793e94c65a4bed59a,

title = "Making security type systems less ad hoc",

abstract = "We present a uniform, top-down design method for security type systems applied to a parallel while-language. The method takes the following route: from a notion of end-To-end security via a collection of stronger notions of anytime security targeting compositionality to a matching collection of type-system-like syntactic criteria. This method has emerged by distilling and unifying security type system results from the literature while formalizing them in a proof assistant. Unlike in our previous papers on this topic, here we focus entirely on high-level ideas instead of technical proof details.",

keywords = "ACM CCS, Security and privacy, Software and application security, ACMCCS, Computingmethodologies, Concurrent computing methodologies, ACM CCS, Theory of computation, Semantics and reasoning",

author = "Tobias Nipkow and Andrei Popescu",

note = "Publisher Copyright: {\textcopyright} 2014 Walter de Gruyter Berlin/Boston 2014.",

year = "2014",

month = dec,

day = "28",

doi = "10.1515/itit-2014-1060",

language = "English",

volume = "56",

pages = "267--272",

journal = "IT - Information Technology",

issn = "1611-2776",

publisher = "De Gruyter Oldenbourg",

number = "6",

}

TY - JOUR

T1 - Making security type systems less ad hoc

AU - Nipkow, Tobias

AU - Popescu, Andrei

PY - 2014/12/28

Y1 - 2014/12/28

N2 - We present a uniform, top-down design method for security type systems applied to a parallel while-language. The method takes the following route: from a notion of end-To-end security via a collection of stronger notions of anytime security targeting compositionality to a matching collection of type-system-like syntactic criteria. This method has emerged by distilling and unifying security type system results from the literature while formalizing them in a proof assistant. Unlike in our previous papers on this topic, here we focus entirely on high-level ideas instead of technical proof details.

AB - We present a uniform, top-down design method for security type systems applied to a parallel while-language. The method takes the following route: from a notion of end-To-end security via a collection of stronger notions of anytime security targeting compositionality to a matching collection of type-system-like syntactic criteria. This method has emerged by distilling and unifying security type system results from the literature while formalizing them in a proof assistant. Unlike in our previous papers on this topic, here we focus entirely on high-level ideas instead of technical proof details.

KW - ACM CCS, Security and privacy, Software and application security, ACMCCS, Computingmethodologies, Concurrent computing methodologies, ACM CCS, Theory of computation, Semantics and reasoning

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

U2 - 10.1515/itit-2014-1060

DO - 10.1515/itit-2014-1060

M3 - Article

AN - SCOPUS:85117225897

SN - 1611-2776

VL - 56

SP - 267

EP - 272

JO - IT - Information Technology

JF - IT - Information Technology

IS - 6

ER -

Making security type systems less ad hoc

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this