Checking Opacity of Vulnerable Critical Systems On-The-Fly

Opacity is a security property capturing a system's ability to keep a subset of its behavior hidden from passive, but knowledgeable, observers. In this paper we use the formal definitions of opacity in three of its forms (simple opacity, -step weak opacity and -step strong opacity), basing on finite Labeled Transition Systems as a model. Then we present efficient algorithms for verifying opacity in all these forms within the context of a hybrid, on-the-fly approach. This approach is based on the construction of a Symbolic Observation Graph (SOG) that allows not only the abstraction of the systems behavior but also the preservation of the structure necessary for conducting opacity checking. Our preliminary experimental results are promising and demonstrate effectiveness facing the state-explosion problem which represents the main drawback of existing model checking techniques.

Abstract Diagnosis for tccp using a Linear Temporal Logic

Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge.In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, isvalidw.r.t. atccpprogram. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.