Towards Specification and Verification of Information Flow in Concurrent Java-like Programs

@TechReport{Bruns14a,
  author	= {Daniel Bruns},
  title		= {Towards Specification and Verification of Information Flow
		   in Concurrent {Java-}like Programs},
  year		= 2014,
  month		= mar,
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  language	= {english},
  number	= {2014-5},
  series	= {Karlsruhe Reports in Informatics},
  url		= {https://publikationen.bibliothek.kit.edu/1000039446},
  urn		= {urn:nbn:de:swb:90-394465},
  issn		= {2190-4782},
  license	= {https://creativecommons.org/licenses/by-nc-nd/3.0/},
  abstract	= {Today, nearly all personal computer systems are
		   multiprocessor systems, allowing multiple programs to be
		   executed in parallel while accessing a shared memory. At
		   the same time, computers are increasingly handling more and
		   more data. Ensuring that no confidential data is leaked to
		   untrusted sinks remains a major quest in software
		   engineering. Formal verification, based on theorem proving,
		   is a powerful technique to prove both functional
		   correctness and security properties such as absence of
		   information flow. Present verification systems are sound
		   and complete, but often lack efficiency and are only
		   applicable to sequential programs. Concurrent programs are
		   notorious for all possible environment actions have to be
		   taken into account.
		   
		   In this paper, we point out steps towards a formal
		   verification methodology for information flow in concurrent
		   programs. We consider passive attackers who are able to
		   observe public parts of the memory at any time during
		   execution and to compare program traces between different
		   executions. Our approach consists of two main elements: (i)
		   formalizing properties on whether two executions are
		   indistinguishable to such an attacker in a decidable logic,
		   and (ii) defining a technique to reason about executions of
		   concurrent programs by regarding a single thread in
		   isolation. The latter is based on the rely/guarantee
		   approach.}
}