Fine-grained Information Flow for Concurrent Computation.


Channel communication is an important means of information
sharing for concurrent processes. Whether communications can
be successfully performed or not is a non-negligible factor
in the information flow security of concurrent systems.
Correspondingly, the "presence" of communications has been
treated as a separate aspect to the "content" of them for
confidentiality. In the integrity case, motivated by
computational phenomena such as Message Authentication
Codes and Denial of Service attacks, we study new
combinations of protection levels for presence and content.
A bisimulation-based process-algebraic security property is
proposed and its meta-theoretical properties are examined.

Sharing communication channels between multiple data paths
creates the need for having different protection levels for
different data content. On top of the separate treatment of
presence and content, we study content-dependent flow policies
for the confidentiality of data. In the setting of synchronously
communicating processes, we propose a compositional security
property and enforce it by an information flow type system. The
impact of deterministic scheduling on the security of systems
is examined, leading to a scheduler-independency result.