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

Technical Report

Author(s):Daniel Bruns
Institution:Department of Informatics, Karlsruhe Institute of Technology
Series:Karlsruhe Reports in Informatics
Number:2014-5
Year:2014
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000039446

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.

BibTeX

@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		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000039446},
  urn		= {urn:nbn:de:swb:90-394465},
  issn		= {2190-4782},
  license	= {http://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.}
}