Back to Search
Start Over
[Untitled]
- Source :
- Higher-Order and Symbolic Computation. 15:209-234
- Publication Year :
- 2002
- Publisher :
- Springer Science and Business Media LLC, 2002.
-
Abstract
- Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style (CPS) as a means of proving that such languages enforce noninterference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features and linear continuations. Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state.
- Subjects :
- Structure (mathematical logic)
Property (philosophy)
Theoretical computer science
Computer science
Semantics (computer science)
Programming language
computer.software_genre
Computer Science Applications
Control flow
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Secrecy
Continuation-passing style
State (computer science)
Information flow (information theory)
computer
Software
Subjects
Details
- ISSN :
- 13883690
- Volume :
- 15
- Database :
- OpenAIRE
- Journal :
- Higher-Order and Symbolic Computation
- Accession number :
- edsair.doi...........8c4882c2dcf6c959a7bd3159eede3e82