CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Securing Interactive Systems

Willard Rafnsson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2014. ISBN: 978-91-7385-989-9.- 208 s.

This thesis provides means to achieve end-to-end information-flow security in interactive systems. The elusiveness of this problem stems from the fact that interaction patterns, primitives, synchronous communication and nondeterminism combine in ways where seemingly innocuous systems compromise security in unexpected ways under interaction. We study what it means for interactive systems to not leak information about confidential behavior into observable behavior in a nondeterministic setting. We focus on two properties: progress-sensitive noninterference (PSNI), requiring that observable behavior is invariant to confidential input, and progress-insensitive noninterference (PINI), permitting confidential input to impede the ability of a system to make progress on its observable output. The latter is a popular target of information-flow security enforcement mechanisms, e.g. JSFlow, Paragon, LIO and Jif. We formalize PINI and PSNI extensionally, based on the view the attacker has on the interaction. To identify the essense of interactive systems security, we explore classes of attacks PSNI and PINI must guarantee protection against, and find previous work ignores classes of attacks powered by varied presence of input -- a high-bandwidth channel in the concurrent setting. This is due to limitations in the model used for system environments. To address this, we devise a new, preservation-based, formalization of noninterference. Since preservation-based noninterference guarantees secure systems interact securely, it is compositional; we prove this for a core of combinators, and derive from it a rich language of security-preserving combinators. While both PSNI and PINI are preserved under arbitrary wirings, the latter is not preserved fairly; it relies fundamentally on lack of scheduling fairness to guarantee security of interactions, and is therefore unfit autonomous interactive systems security. To facilitate building secure systems in parts, we advance secure multi-execution (SME): a combinator which repairs insecurities. SME thus makes any interactive system, secure or not, readily pluggable into a secure composed system. We prove soundness for all fair schedulers, and redesign SME to enforce PSNI, obtaining a more semantics-preserving combinator. We give a language-independent model for information release in SME. For scenarios where semantics must be preserved, we present type-based enforcements of PSNI and PINI. The type systems guarantee absence of leaks through challenging constructs e.g. dynamic event handlers and lazy class initialization. Lastly, we give a combinator which places a logarithmic bound on leaks through progress. Together with the type-based enforcement of PINI, we get a permissive hybrid enforcement of a stronger property.

Nyckelord: semantics-based security, language-based security, information-flow security, information-flow control, program analysis, runtime enforcement, program transformation, concurrency, parallelism, multi-threading, scheduling, fairness, covert channels

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-04-10. Senast ändrad 2016-11-09.
CPL Pubid: 196584


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)


Informations- och kommunikationsteknik

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:

Limiting Information Leakage in Event-based Communication

Securing interactive programs

Securing Class Initialization in Java-like Languages

Secure multi-execution: Fine-grained, declassification-aware, and transparent


Datum: 2014-04-29
Tid: 10:00
Lokal: HC4
Opponent: Prof. Fred B. Schneider, Department of Computer Science, Cornell University, Ithaca, USA

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 3670