A Model-Driven Approach to Noninterference

Kurt Stenzel
+, Kuzman Katkalov, Marian Borek, and Wolfgang Reif

Institute for Software & Systems Engineering, University of Augsburg, Germany

 

Abstract

Systems consisting of mobile apps and web services continue to grow in popularity. Guaranteeing that private or sensitive data is treated confidentially in such systems is non-trivial and poses several challenges due to their distributed and platform-specific nature. Information flow control is a formal technique that is used to guarantee the privacy of such data, but is difficult to utilize in practice. We present a model-driven approach which allows to develop such systems with secure information flow using intuitive modeling guidelines. From an abstract system model, partial Java code as well as a formal model is generated automatically and used to verify information flow properties. This paper explains the automatic generation of the formal model and presents several advantages of a model-driven approach for the practical application of information flow control.

Keywords: noninterference, model-driven development, information flow control, formal methods.

 

+: Corresponding author: Kurt Stenzel

Institute for Software- and Systems Engineering Universitaetsstr. 6a, 86159 Augsburg, Germany,

Tel: +49-8215982123, Email: stenzel@informatik.uni-augsburg.de,
Web: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/staff/stenzel/


Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA),

Vol. 5, No. 3, pp. 30-43, September 2014 [pdf]