Model checking security properties of control flow graphs

1 July 2001

journal article
Published by SAGE Publications in Journal of Computer Security

Vol. 9 (3) , 217-250
https://doi.org/10.3233/jcs-2001-9303

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

Keywords

MODEL
CHECKING SECURITY
SECURITY PROPERTIES
SPECIFYING
FLOW
GRAPHS
FORMALISM
SUFFICIENT
SOFTWARE

This publication has 0 references indexed in Scilit: