Securing Interaction Between Threads and the Scheduler in the Presence of Synchronization
The problem of information flow in multithreaded programs remains an important open challenge. Existing approaches to specifying and enforcing information-flow security often suffer from over-restrictiveness, relying on nonstandard semantics, lack of compositionality, inability to handle dynamic threads, inability to handle synchronization, scheduler dependence, and efficiency overhead for the code that results from security-enforcing transformations. This paper suggests a remedy for some of these shortcomings by developing a novel treatment of the interaction between threads and the scheduler. As a result, the authors present a permissive noninterference-like security specification and a compositional security type system that provably enforces this specification.