Secure Information Flow in a Multi-Threaded Imperative Language

13 years 8 months ago

Download users.cs.fiu.edu

Previously, we developed a type system to ensure secure information ﬂow in a sequential, imperative programming language [VSI96]. Program variables are classiﬁed as either high or low security; intuitively, we wish to prevent information from ﬂowing from high variables to low variables. Here, we extend the analysis to deal with a multithreaded language. We show that the previous type system is insuﬃcient to ensure a desirable security property called noninterference. Noninterference basically means that the ﬁnal values of low variables are independent of the initial values of high variables. By modifying the sequential type system, we are able to guarantee noninterference for concurrent programs. Crucial to this result, however, is the use of purely nondeterministic thread scheduling. Since implementing such scheduling is problematic, we also show how a more restrictive type system can guarantee noninterference, given a more deterministic (and easily implementable) schedulin...

Geoffrey Smith, Dennis M. Volpano

Real-time Traffic