  Realizing flow security in a concurrent environment is extremely challenging,
primarily due to non-deterministic nature of execution. The difficulty is
further exacerbated from a security angle if sequential threads disclose
control locations through publicly observable statements like print, sleep,
delay, etc. Such observations lead to internal and external timing attacks.
Inspired by previous works that use classical Hoare style proof systems for
establishing correctness of distributed (real-time) programs, in this paper, we
describe a method for finding information leaks in concurrent programs through
the introduction of leaky assertions at observable program points. Specifying
leaky assertions akin to classic assertions, we demonstrate how information
leaks can be detected in a concurrent context. To our knowledge, this is the
first such work that enables integration of different notions of
non-interference used in functional and security context. While the approach is
sound and relatively complete in the classic sense, it enables the use of
algorithmic techniques that enable programmers to come up with leaky assertions
that enable checking for information leaks in sensitive applications.
