Workshop on
Foundations of Computer Security - FCS'03
Ottawa, Canada, 26-27 June 2003
A 3-Valued Logic for the Specification and the Verification of
Security Properties
Béchir Ktari (Laval University - Canada)
Abstract
The main intent of this paper is the definition of a 3-valued logic for the
specification and the verification of security properties. This is a part of a
large initiative that we undertook a few years ago to address malicious code
detection in commercial off-the-shelf software products. Building on top of
the existing approaches, we have established a framework that stems from a
combination of self-certified code technology and model-checking
techniques. In this paper, we propose a logic with a 3-valued semantics in
order to be able to reason under uncertainty. We also endow our logic with a
tableau-based proof system that is proven to be finite, and to be sound and
complete with respect to the denotational semantics of the logic. Furthermore,
we propose some ideas that may lead to important future extensions. For
instance, we show how the use of variables and types can lead to a more
efficient verification.