Other: ISTRICE lunch colloqium: ISTRICE lunch colloqium

AGENDA:

12.00 - 12.10 h.     Welcome

12.10 - 12.45 h.     Marieke Huisman

                            Title: "Scheduler-specific Confidentiality for Multi-threaded Programs and Its logic-based Verification"

Abstract:
Observational determinism has been proposed in the literature as a way to ensure confidentiality for multi-threaded programs. Intuitively, a program is observationally deterministic if the behavior of the public variables is deterministic, i.e., independent of the private variables. Several formal definitions of observational determinism exist, but all of them have shortcomings; for example they accept insecure programs or they reject too many innocent programs. Besides, the role of schedulers was ignored in all the proposed definitions of observational determinism. A program that is secure under one kind of scheduler might not be secure when executed with a different scheduler. The existing definitions do not ensure that an accepted program behaves securely under the used scheduler.
Therefore, in this talk we propose a new formalization of scheduler-specific observational determinism. It accepts programs that are secure when executed under a specific scheduler. Moreover, it is less restrictive on harmless programs under a particular scheduling policy. We discuss the properties of our definition and argue why it better approximates the intuitive understanding of observational determinism.
In addition, we discuss how our definition can be verified, using model checking. We use the idea of self-composition and we rephrase the observational determinism properties for a single program C as temporal logic formulas over the program C executed in parallel with an independent copy of itself. Thus two states reachable during the execution of C are combined into a reachable program state of the self-composed program. This allows to compare two program executions in a single temporal logic formula. The actual characterization is done in two steps. First we discuss how stuttering equivalence can be characterized as a temporal logic formula. Observational determinism is then expressed in terms of the stuttering equivalence characterization. This results in a conjunction of an LTL and a CTL formula, that are amenable to model checking.

12:45 – 13:20 h.    Dusko Pavlovic 

                            Title: "Emergent behaviors as a security resource"

Abstract:

In modern cryptography, computational complexity is used as a resource: the assumptions about the attacker's computational limitations are used as pivot points to lever system's security. In this talk, I will put forward the idea that the logical complexity of emergent behaviors is a similar resource, as yet untapped. The underlying assumption is that emergent behaviors are hard to describe and predict not only for the system designers, but also for the attackers. The task of formalizing and utilizing the concepts of logical complexity and of the hardness of descriptions leads into a space of methods spanned by two different mathematical toolkits: of algorithmic information, and of epistemic games. I will briefly describe the underlying theories, and explore their potential applications in security. Can they be used to turn the tables of complexity on the attacker?

 13.20 -13.30 h.     AOB