Faculty of Engineering and Natural Sciences
Specification and Refinement of Confidentiality Requirements
Thomas Santen, TU Berlin
While today it is widely accepted that security is an important concern for almost every IT system, it still is very hard to build verifiably secure systems. One of the reasons for this is that confidentiality requirements address different kinds of properties than the usual safety or liveness properties, which are well-understood and for which mature description and verification techniques exist. Confidentiality properties are second-order properties that - implicitly or explicitly - need to take the probabilistic behavior of the IT system and its environment into account. Furthermore, they usually are not compositional and not preserved by standard refinement relations, which express the usual correctness conditions for an implementation to meet a specification. The talk discusses state-of-the-art approaches to specify confidentiality and introduces a formal framework for confidentiality-preserving refinement that captures the essential conditions for deriving correct and secure implementations.
Dr Thomas Santen is assistant professor at Berlin University of Technology, Germany. He studied Computer Science at the universities of Erlangen and Karlsruhe, Germany. He received a Ph.D. from Berlin University of Technology on the formal analysis of behavioral conformance in object-oriented systems using an interactive theorem prover. Dr Santen's research interests include systems and software engineering for secure systems, in particular security requirements engineering, formal models of confidentiality and privacy, and also model-based test automation, and formal verification of dependability properties.
Wednesday, Feb 21, 2007, 14:40-15:30, FENS G016