Premium
Checking security properties by model checking
Author(s) -
De Francesco Nicoletta,
Lettieri Giuseppe
Publication year - 2003
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.272
Subject(s) - model checking , computer science , covert channel , theoretical computer science , programming language , kripke structure , abstraction model checking , control flow graph , control flow , representation (politics) , cloud computing security , operating system , cloud computing , security information and event management , politics , law , political science
A method is proposed for checking security properties in programs written in high‐level languages. The method is based on the model checking technique. The SMV tool is used. The representation of the program is a Kripke structure modelling the control flow graph enriched with security information. The properties considered are secure information flow and the absence of covert channels caused by program termination. The formulae expressing these security properties are given using the logic CTL. Copyright © 2003 John Wiley & Sons, Ltd.