ENS de Cachan, pavillon des jardins: comment y aller
Abstract: Opacity is a security property formalizing the absence of secret information. A secret predicate $\varphi$ over the runs of a system $G$ is opaque to a user having partial observability over $G$ if this user can never infer from the observation of a run of $G$ that the run belongs to $\varphi$. But secrecy in the real world rarely means absence of secret information as potential covert channel are hardly avoidable. In this talk we address the problem of verification of opacity in the presence of controlled opacity disclosure. Observational power of users is controlled by a device, called an {\em observer}. We first introduce a very general observer called {\em Orwellian} observer where the set of events the user can observe depends as well on previous events as on subsequent ones. We show that checking whether a system is opaque w.r.t. an Orwellian observer is PSPACE-complete. Next, we illustrate relevancy of our results by proving how most declassification properties can reduce to opacity w.r.t. Orwellian observers including intransitive non-interference property with selective declassification.
Abstract: Model-based testing has mainly focused on models where currency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order to test such concurrent systems, we choose to use Petri nets as specifications and define a concurrent conformance relation named co- ioco. We propose a test generation algorithm based on Petri net unfolding able to build a complete test suite w.r.t our co-ioco conformance relation. In addition we propose several testing criteria based on dedicated notions of complete prefixes that selects a manageable test suite.