Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems

Issue title: Concurrency Specification and Programming (CS&P'2002), Part 1

Article type: Research Article

Authors: De Francesco, Nicolette | Santone, Antonella | Tesei, Luca

Affiliations: Dipartimento di Ingegneria della Informazione, Università di Pisa, Italy | RCOST - Research Centre on Software Technology, University of Sannio, Benevento, Italy | Dipartimento di Informatica, Università di Pisa, Italy

Abstract: We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and model checking: by abstract interpretation we build a finite representation (transition system) of the behavior of the program. Then we model check the the abstract transition system with respect to the security properties, expressed by a set of temporal logic formulae. The approach allows certifying more programs than previous methods do. The main point is that we are able to check more carefully the scope of indirect information flows.

Keywords:

Journal: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 195-211, 2003