Title: Robustness of Information Flow Security Under Refinement of Synchronization Primitives


Abstract: Nowadays, we trust personal computers and other computing devices to handle 
 various kinds of private information. To substantiate this trust, we need means to 
protect this confidential information against faulty or even malicious programs. 

Given a suitable security property and a related information flow policy, a program 
can be proven to not leak secrets by means of information flow analyses. However, existing 
security properties are either not suitable for concurrent programs with synchronization 
operations or they depend on very strong assumptions about the execution environment.

In this talk, we address this issue by presenting a novel noninterference-like security 
property. This property accepts many intuitively secure, multi-threaded programs with 
semaphore-based synchronization while it is largely independent from the actual semaphore 
and scheduler implementation that the targeted execution environment employs. Moreover, we 
emphasize the security property's applicability by example programs from different 
application domains of semaphores.