loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
14th IEEE Computer Security Foundations Workshop (CSFW'01)
A New Type System for Secure Information Flow
Cape Breton, Novia Scotia, Canada
June 11-June 13
ISBN: 0-7695-1146-5
Geoffrey Smith, Florida International University
Abstract: With the variables of a program classified as L (low, public) or H (high, private), we wish to prevent the program from leaking information about H variables into L variables. Given a multi-threaded imperative language with probabilistic scheduling, the goal can be formalized as a property called probabilistic noninterference. Previous work identified a type system sufficient to guarantee probabilistic noninterference, but at the cost of severe restrictions: to prevent timing leaks, H variables were disallowed from the guards of while loops. Here we present a new type system that gives each command a type of the form \tau_1 cmd \tau_2; this type says that the command assigns only to variables of level \tau_1 (or higher) and has running time that depends only on variables of level \tau_2 (or lower). Also we use types of the form \tau cmd n for commands that terminate in exactly n steps. With these typings, we can prevent timing leaks by demanding that no assignment to an L variable may sequentially follow a command whose running time depends on H variables. As a result, we can use H variables more flexibly; for example, under the new system a thread that involves only H variables is always well typed. The soundness of the type system is proved using the notion of probabilistic bisimulation.
Citation:
Geoffrey Smith, "A New Type System for Secure Information Flow," csfw, pp.0115, 14th IEEE Computer Security Foundations Workshop (CSFW'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.