Model checking security properties of control flow graphs

Article type: Research Article

Authors: Besson, Frédéric^a | Jensen, Thomas^{a; *} | Le Métayer, Daniel^b | Thorn, Tommy^c

Affiliations: [a] IRISA/CNRS, Campus de Beaulieu, F-35042 Rennes Cedex, France | [b] Trusted Logic, 5, rue du Bailliage, F-78000 Versailles, France | [c] BRICS, University of Aarhus, DK-8000 Aarhus C, Denmark

Correspondence: [*] Corresponding author. Tel.: +33 2 99 84 74 78; Fax: +33 2 99 84 71 71; E-mail: [email protected].

Abstract: A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a global security property. This article introduces a formalism based on a linear-time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrates its expressive power with a number of existing properties. We define a minimalistic, security-dedicated program model that only contains procedure call and run-time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. We then show how to instantiate the framework to the security architecture of Java 2 based on stack inspection and privileged method calls.

DOI: 10.3233/JCS-2001-9303

Journal: Journal of Computer Security, vol. 9, no. 3, pp. 217-250, 2001