Enforcement of Timing-Sensitive Security Policies in Runtime Systems

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandling

Standard

Enforcement of Timing-Sensitive Security Policies in Runtime Systems. / Pedersen, Mathias.

Aarhus University, 2019. 216 s.

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandling

Harvard

APA

CBE

MLA

Vancouver

Author

Pedersen, Mathias. / Enforcement of Timing-Sensitive Security Policies in Runtime Systems. Aarhus University, 2019. 216 s.

Bibtex

@phdthesis{4dbc3ad3f7d2490c96c4b5da12d1327d,
title = "Enforcement of Timing-Sensitive Security Policies in Runtime Systems",
abstract = "The work presented in this dissertation focuses on applying information-flow control (IFC) techniques to the construction of secure runtime systems that do not leak sensitive information through their timing behavior. The dissertation also presents applications of IFC to the development of secure programs that require dynamic authorization policies.Chapter 2 presents a series of timing channel attacks on automatic memory management, and a calculus in which the attacks can be formally studied. We then study an enforcement technique for preventing the discovered timing leaks, and prove the enforcement sound using the Coq proof assistant. The enforcement combines a security type system with a secure semantics for garbage collection.Chapter 3 studies the feasibility of implementing the secure garbage collection semantics, and other runtime related activities, like secure thread scheduling. We present a language for implementing such secure runtime components, along with a type system for which we prove that any well-typed program is secure. Thus, runtime system activities can be implemented as a program in the language itself, and the well-typing of the program guarantees that the runtime activity does not leak information through timing.Finally, Chapter 4 studies authorization policies using the Flow-Limited Authorization Model (FLAM), and shows how developers can program with dynamic and decentralized authorization policies while guaranteeing security. Previous work applying FLAM to the development of secure programs has focused on static and fine-grained enforcement techniques, but we argue that FLAM is better suited for a dynamic enforcement of coarse-grained information-flow control.",
author = "Mathias Pedersen",
year = "2019",
month = oct,
language = "English",
publisher = "Aarhus University",

}

RIS

TY - BOOK

T1 - Enforcement of Timing-Sensitive Security Policies in Runtime Systems

AU - Pedersen, Mathias

PY - 2019/10

Y1 - 2019/10

N2 - The work presented in this dissertation focuses on applying information-flow control (IFC) techniques to the construction of secure runtime systems that do not leak sensitive information through their timing behavior. The dissertation also presents applications of IFC to the development of secure programs that require dynamic authorization policies.Chapter 2 presents a series of timing channel attacks on automatic memory management, and a calculus in which the attacks can be formally studied. We then study an enforcement technique for preventing the discovered timing leaks, and prove the enforcement sound using the Coq proof assistant. The enforcement combines a security type system with a secure semantics for garbage collection.Chapter 3 studies the feasibility of implementing the secure garbage collection semantics, and other runtime related activities, like secure thread scheduling. We present a language for implementing such secure runtime components, along with a type system for which we prove that any well-typed program is secure. Thus, runtime system activities can be implemented as a program in the language itself, and the well-typing of the program guarantees that the runtime activity does not leak information through timing.Finally, Chapter 4 studies authorization policies using the Flow-Limited Authorization Model (FLAM), and shows how developers can program with dynamic and decentralized authorization policies while guaranteeing security. Previous work applying FLAM to the development of secure programs has focused on static and fine-grained enforcement techniques, but we argue that FLAM is better suited for a dynamic enforcement of coarse-grained information-flow control.

AB - The work presented in this dissertation focuses on applying information-flow control (IFC) techniques to the construction of secure runtime systems that do not leak sensitive information through their timing behavior. The dissertation also presents applications of IFC to the development of secure programs that require dynamic authorization policies.Chapter 2 presents a series of timing channel attacks on automatic memory management, and a calculus in which the attacks can be formally studied. We then study an enforcement technique for preventing the discovered timing leaks, and prove the enforcement sound using the Coq proof assistant. The enforcement combines a security type system with a secure semantics for garbage collection.Chapter 3 studies the feasibility of implementing the secure garbage collection semantics, and other runtime related activities, like secure thread scheduling. We present a language for implementing such secure runtime components, along with a type system for which we prove that any well-typed program is secure. Thus, runtime system activities can be implemented as a program in the language itself, and the well-typing of the program guarantees that the runtime activity does not leak information through timing.Finally, Chapter 4 studies authorization policies using the Flow-Limited Authorization Model (FLAM), and shows how developers can program with dynamic and decentralized authorization policies while guaranteeing security. Previous work applying FLAM to the development of secure programs has focused on static and fine-grained enforcement techniques, but we argue that FLAM is better suited for a dynamic enforcement of coarse-grained information-flow control.

M3 - Ph.D. thesis

BT - Enforcement of Timing-Sensitive Security Policies in Runtime Systems

PB - Aarhus University

ER -