Date: October 16
Place: A008
Chairs: Emmanuel Jeandel
Session 1 : 8h30-10h
8h30-9h00 : Hubert Godfroy
A theory of reflexive computation based on soft intuitionistic logic
Computational Reflection is a paradigm in which the computational mechanisms controls the different levels of data interpretation. It can be decomposed into two processes: (i) reification, which turns a program into a data and (ii) reflection, which, inversely, installs a data as a program or a context in order to be run. We present a logical account of reflection based on a confluent lambda-calculus. We define a type assignment system called Soft Intuitionistic Logic (SIL) in which we introduce the exponential modality $!$ of linear logic. The duality between reification and reflection is to be found in the soft promotion rule and in the dereliction rule. We also show that SIL is a framework in which partial evaluation can be efficiently performed. Finally, we add a control operator, which reifies its evaluation context. Thus a program may have full control of its computational state. We extend the type system SIL with classical logic and semantics is provided by Krivine abstract machine. We establish the soundness of our type system.
9h00-9h30 : Alicia Filipiak
Designing an EMV-compliant payment protocol for mobile devices
We devise a payment protocol that can be securely used on mobile devices, even infected by malicious applications. Our protocol only requires a light use of Secure Elements, which significantly simplify certification procedures and protocol maintenance. It is also fully compatible with the EMV-SDA protocol and allows off-line payments for the users as well as untrackability regarding a merchant for the client. We provide a formal model and full security proofs of our protocol using the TAMARIN prover.
9h30-10h00 : Remi Nazin
Human Machine : From Interaction to Integration
Currently used paradigms in Human-System-Interaction design tend to conceive the human operator as a simple set of constraints upon the artefactual system thus understanding interaction as a passive relation. An answer to this problem can be found by substituting the interactive paradigm by an integrative one. Instead of considering the operator as a set of constraints, a Human-System-Integration paradigm aims to conceive it as a part of the global system which is the artefact in use. This means that the human part of the overall system should possess a similar status than a technical one even if they are not of the same nature at all.
A good example of the problem is found in forthcoming spatial exploration programs which will furthermore amplify the problems of behavior and performance risk mitigation such as the effect of long term missions on motor skills, cognitive functions and their impact on task performance. It imposes us to think anew the interactions between human and automation in the novel context of missions with a great crew autonomy, no resupply and the need to accommodate vehicle/habitat design in function of possibly evolutive mission attributes.
“Human machine” (HM) is a concept integrating cyber-physical systems and biological systems. As a scientifc challenge, HM is about the conception of a theoretical framework dedicated to human machine integration and its modeling, from epistemology to formal and experimental methods. As a practical challenge, HM is about correct design for enhancement and reliable engineering of human systems integration, from human-machine interaction to sociotechnical system, their behavior and their performances. One notable problem with this approach resides in that of its propensity for reductionism, seen as the candid way to integration in the sense that it allows ad extremum simplifcation by means of the hypothesis that human beings are mere machines. Genuine integration could not follow this path because of the inextinguishable specificities of biological objects.
Following these specificities, the purpose of integrativism is the development and provision of an unified framework for human behaviour prediction and control which find its roots in physiology and allows to construct a model of the human individual, from the cellular scale to the social one. In order to achieve this general model of human beingness in a more and more autonomous technical ecosystem it is important to inspect the foundations of behavioral sciences so that the apparatus can be designed to take into account the different scales that constitute the complexity of any biological system and furthermore of any Human-Integrated technical one.
10h-10h30 Pause café
Session 2 : 10h30-12h30
10h30-11h00 : Imen Sayar
Articulation between formal and semi-formal activities in the development of software
My PhD thesis is situated in the context of formal development of safety critical software and systems. Our goal is to bridge the gap between the two different worlds : formal and semi-formal coming from the client. In the former, we are using the Event-B formal method and in the later we are working with requirements. We focus on the interactions that can take place between them.
In our approach, we are handling a system composed of requirements, their corresponding Event-B models and the links between them. In order to improve the quality of the whole system, we propose to:
– structure the client-requirements by rewriting them in order to
– make them more readable,
– evolve the requirements alternatively with the refinements of the Event-B models. We gradually establish links and a glossary between them in every step of the development,
– use the verification and validation tools to detect the incoherences, omissions and imprecisions in both requirements and specification,
– consider the validation activity as a rigorous process, starting from re-quirements structuration before the system is built until Event-B models animation and model-checking.
We apply our approach on two big critical complex systems : the hemodialysis machine and the landing gears.
11h00-11h30 : Ludovic Robin
Automated verification of protocols using low-entropy secrets
In E-commerce protocols, such as the well known 3D-Secure protocol, there is an additional check of client authenticity using mobile phones. Confirmation codes emitted on these channels are short due to human interaction and this could benefit to an attacker that may break the security through brute-force attack.
In this talk we will present a new attacker model that take into account these brute-force abilities and discuss their automated verification.
11h30-12h : Souad Kerroubi
Towards Contextualized Dependent Event-B Models : Application to Voting Systems
Nous rappelons que l’objectif de cette thèse rentre dans le cadre du projet IMPEX. Nous nous sommes intéressés à la problèmatique de la contextualisation dans la preuve des systèmes informatiques. Cette notion a été le centre d’intérêt dans de nombreux travaux qui se fondent sur les ontologies et l’Intelligence Artificielle. Nous avons apporté des éléments de réponse dans le cadre du formalisme B événementiel. Nous avons montré que cette notion n’est pas absolue et qu’elle est toujours relative à un focus qui se concrétise par les actions entreprises dans les systèmes étudiés. En raisonnant sur la structure du formalisme B événementiel nous avons proposé trois répartitions suivant les approches basées sur la logique en IA qui se fondent sur la théorie des situations : i) Le contexte de contraintes ; ii) Le contexte d’hypothèses ; iii) Le contexte de dépendances défini comme combinaisons de situations et de contraintes.
Par ailleurs, la construction des preuves dans le formalisme B événementiel est exhsibée par raffinement. Ce mécanisme sous ses différentes formes (horizontales et verticales) contextualise les preuves ce qui permet l’élimination des conflits et des ambiguïtés pour affirmer les relations de confiance entre les parties impliquées dans le système et apporter plus de garanties sur les propriétés à vérifier. Notre étude a montré que tant qu’il existe des relations qui établissent une équivalence sémantique entre les contraintes, le raffinement reste une bonne approche qui garantit des constructions de modèles correctes et qui, par ailleurs, peut substituer la relation de subsomption dans les ontologiques.
Alors qu’en théorie des situations le contexte est défini comme une amalgamation de situations et de contraintes qui traduit une dépendance, le point de vue ontologique a démontré que le contexte est perçu comme un “moment universel” ie : un concept dont l’existence dépend de concepts intentionnels (actions). Vu de cet angle, le contexte comme connaissances minimales situe les systèmes dans l’espace et dans le temps. Nous avons donc proposé un nouveau mécanisme fondé sur la notion de dépendances entre composants dans le B événementiel. La preuve par dépendance repose essentiellement sur l’existence de situations dans lesquelles une partie peut dépendre de l’autre. En faisant le parallèle avec le B événementiel, les situations sont interprétées comme des états en B et les contraintes comme des contextes B, et en confondant le moment universel à la terminaison qui nécessite une certaine stabilité, nous pouvons affirmer qu’une dépendance dans le formalisme B événementiel se traduit par la donnée d’un ensemble de valeurs d’état d’un composant dans le formalisme B événementiel qui satisfait les contraintes définies dans les contextes au sens B événementiel de l’autre partie.
Nous nous sommes basé sur les travaux [2, 1] qui définissent des modèles relationnels pour le formalisme B événementiel et l’étendent aux aspects temporels afin de définir la terminaison avec persistance dans ce formalisme et ainsi définir le principe de dépendance entre deux composants B événementiels. Cette extension requiert l’ajout de nouvelles obligations de preuves.
Notre approche s’est articulée sur les protocoles de vote qui représentent un bon candidat pour illustrer ce principe. Nous avons donc développé des patrons de conception pour les protocoles de vote et exprimé plusieurs propriétés de sûreté dans ces systèmes, particulièrement les propriétés de confidentialité/d’anonymat, d’éligibilité ainsi que la vérifiabilité dans résultats du dépouillement fournis par le système.
12h00-12h30 : Pierre Kimmel
Three extensions and variations of BI logic
BI logic, introduced in 1999 by O’Hearn and Pym, is an extension of intuitionnistic logic that expresses the sharing and separating of resources. Several variations of this logic and proof methods for it have been presented lately, since one of its children, separation logic (2002), has had a huge impact on software verification. We are developing three different extensions variations of BI that could be of major interest for similar uses:
* Linear Temporal BI logic (LTBI) : a linear temporal extension that could lead to a new approach of branching time logics
* Epistemic Resource Logic (ERL) : an epistemic extension that uses resources as access condition that is aimed to model access control and security protocols.
* Hybrid Resource Logic (HRL) : a new way of formalizing BI with explicit resource labels. This would both allow an axiomatization of BI and many other variations and extend the expressiveness of those logics.
