Guaranteeing that information processed in computing systems remains confidential is vital for many software applications. To this end, language-based security mechanisms enforce fine-grained access control policies for program variables to prevent secret information from leaking through unauthorized access. However, approaches for language-based security by information flow control mostly work post-hoc, classifying programs into whether they comply with information flow policies or not after the program has been constructed. Means for constructing programs that satisfy given information flow control policies are still missing. Following the correctness-by-construction approach, we propose a development method for specifying information flow policies first and constructing programs satisfying these policies subsequently. We replace functional pre- and postcondition specifications with confidentiality properties and define rules to derive new confidentiality specifications for each refining program construct. We discuss possible extensions including initial ideas for tool support. Applying correctness-by-construction techniques to confidentiality properties constitutes a first step towards security-by-construction.

Short bio

Ina Schaefer is full professor and head of the Institute of Software Engineering and Automotive Informatics at Technische Universität Braunschweig, Germany. She received her PhD in 2008 at Technische Universität Kaiserslautern and was a Postdoc at Chalmers University, Gothenburg, Sweden. Her research interests include constructive and analytic approaches for developing correct software systems, with a particular focus on software variability and evolution, as well as re-engineering techniques for legacy software systems. The main application areas of her research are in automotive and automation.