Title: Verification of control flow based security properties
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. We introduce a formalism based on a two-level linear time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrate 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. For a given formula in the temporal logic, we prove that there exists a bound on the size of the states that have to be considered in order to assure the validity of the formula: this reduces the problem to finite state model checking. Finally, we instantiate the framework to the security architecture proposed for Java (JDK 1.2).
Publication Year: 2003
Publication Date: 2003-01-20
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 120
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot