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

Tracking Information Flows in Interactive and Object-Oriented Programs

Willard Rafnsson (Institutionen för data- och informationsteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2012. - 192 s.
[Licentiatavhandling]

This thesis improves the current state of the art on information-flow control of interactive and object-oriented programs, respectively. Given a policy which specifies which information flows are permitted in a program, the objective here is to ensure that only flows satisfying the policy can occur. The challenge is to develop a sane policy and an automated, permissive enforcement mechanism for said policy. For interactive programs, we give a progress-sensitive noninterference (PSNI) policy which takes into account the confidentiality level of the presence of messages. We show that the finer granularity obtained through presence levels makes PSNI parallel compositional, and we give a proven-sound, static, flow-sensitive type-based enforcement of PSNI. We show that for deterministic interactive programs, it suffices to consider simple stream-based attackers. We develop in this setting a progress-bounded noninterference (PBNI) which bounds the leak through progress observations to a logarithm of the number of observable inputs to the program. We combine a static, flow-sensitive type-based enforcement for a progress-insensitive noninterference policy and a output-buffering program transformation to a hybrid enforcement of PBNI for a language inspired by JavaScript. The enforcement tracks flows through hithero untreaded language constructs, such as event propagation, event hierarchies and event handler switching. For object-oriented programs, we present a static, flow-sensitive type system for tracking flows through lazy static class initializations with persistent failures, a language construct in languages such as Java and C#, untreated by tools such as Jif. We show how a class initialization status can be utilized as a covert channel for moving 1 bit of information, and show that the type system enforces a termination-insensitive notion of noninterference.

Nyckelord: information security, information flow, program analysis, static analysis, dependency analysis, privacy, confidentiality



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2012-05-03.
CPL Pubid: 157281

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för data- och informationsteknik (Chalmers)

Ämnesområden

Informations- och kommunikationsteknik
Programvaruteknik

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


Limiting Information Leakage in Event-based Communication


Examination

Datum: 2012-05-25
Tid: 10:00
Lokal: EC
Opponent: David Clark, Department of Computer Science, University College London, United Kingdom

Ingår i serie

Technical report L - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University 1652-876X