SM2071 Attackdefense trees for computer security


Description


An attackdefense tree (ADTree) is an ANDOR tree representing how an attacker may compromise a system and how a defender can protect it against potential attacks. Nodes of ADTrees are labeled with (collections of) actions that the attacker and the defender need to perform in order to reach their goals. ADTrees extend the industrially recognized model of attack trees with nodes representing countermeasures. ADTrees may also assist the security analysts in the process of quantitative evaluation of security scenarios, by integrating algorithms to estimate parameters such as the cost, the impact or the probability of a successful attack.
With the help of ADTrees, one can express how to protect a system against potential attacks. In practice, however, preventive countermeasures may not be fully effective and may be difficult or expensive to deploy. This is why, in some situations, the attacks are not prevented in advance and instead defensive countermeasures are used once an attack occurs. Security training is an example of a preventive countermeasure; blocking a credit card after its theft illustrates a reactive countermeasure. A practical an industrially pertinent formal tool for security evaluation and risk assessment must therefore be able to differentiate between preventions and reactions.
The objective of this master project is to increase the expressive power of ADTrees by integrating reactive countermeasures into the model.
The objective of the project will be reached by addressing the following two research goals: 1. Develop mathematical foundations for ADTrees with preventive and reactive countermeasures. 2. Propose quantitative evaluation techniques for ADTrees with preventive and reactive countermeasures.
The extended model of ADTrees with preventions and reactions will be validated in a reallife case study. The case study will be performed with one of our industrial partners specialized in risk assessment and consulting. The underlying goal is to verify the usability of the proposed formalization as well as to test the efficiency and the scalability of the developed algorithms. URL sujet détaillé : people.irisa.fr/Barbara.Kordy/internships/master_internship_ADTrees.pdf
:
Remarques : le stage sera rémunéré





SM2072 AUTOMATIC MINIMIZATION OF LARGE SYSTEMS OF EQUATIONS


Description


A significant hindrance to our capability of modeling many natural and engineered systems is the challenge in solving large systems of equations. This has led to a number of approaches aimed at taming complexity by means of abstraction and simplification techniques, developed across many disciplines such as control theory, ecology, economics, informatics, and systems biology.
The subject of this internship proposal is to progress a recent line of investigation on the automatic reduction of systems of ordinary differential equations using techniques grounded in foundational theories of computer science, such as behavioral equivalences and partition refinement algorithms.
Currently available results concern exact notions of minimization, where from a reduced model one can precisely recover the dynamics of the original system. Starting from this, we propose three possible future directions of work, also motivated by specific realworld applications in machine learning, systems biology, and electrical networks:
 The development of novel exact notions of minimization to capture still uncovered aggregation patterns.
 The development of approximate variants where larger reductions are possible at the expense of introducing a (hopefully controllable) error in the reduced model.
 The development of equivalence relations checked through statistical sampling, to help overcome computational difficulties in particularly challenging realworld systems.
The work will be carried out at IMT School for Advanced Studies Lucca, one of Italy's six schools of excellence for postgraduate education. As the research is part of an ongoing collaboration with Microsoft Research Cambridge and the University of Oxford, interested candidates might also have the opportunity of stays at these institutions in order to develop part of their project. Publication in highprofile CS venues can be expected as an output of this work. URL sujet détaillé :
:
Remarques :





SM2073 Vérification de systèmes distribués communiquant par messages


Description


Complex distributed applications are built by composing distributed services/processes/peers. These peers asynchronously interact with messages. As there exist many asynchronous communication models (with various guarantees on delivery order, faults etc) corresponding to the diversity of deployment platforms, the correctness of the composition is not trivial. Ideally, this correctness is formally and automatically verified: formalization is required to ensure confidence in the case of critical systems; automation is needed to facilitate changes.
Our team have developed a framework based on TLA+ (transition systems) to verify the asynchronous composition of services. Several communication models are available and generic results to compare these models have been discovered and proved. This framework is currently limited to a fixed number of peers without dynamic creation of peers or of communication channels. A demo can be played with at http://vacs.enseeiht.fr/.
The objectives are:  to discover the framework and to extend it to allow the description of parameterized systems; this also requires to extend the peer description language (currently CCS; picalculus may be a solution);  to extend the framework so that messages and transitions carry applicative values;  to extend the framework to allow dynamic creation of peers, of communication channels, and their exchange. The three objectives require both theoretical work (to identify the relevant abstractions), formalization (to describe them in TLA+) and development (to integrate them in the framework). URL sujet détaillé : http://hurault.perso.enseeiht.fr/sujetmasterens2016.pdf
Remarques : Coencadrement : Philippe Quéinnec (queinnec.fr)





SM2074 Termination checking in Dedukti


Description


Dedukti is a formal proof checker based on a logical framework called the λΠcalculus modulo, which is an extension of the simplytyped lambdacalculus with dependent types and an equivalence relation on types generated by the userdefined rewrite rules. Proofs generated by some automated theorem provers or proof assistants can be checked in Dedukti by encoding function definitions and axioms by rewrite rules. But, for Dedukti to behave well, the rewrite rules must satisfy some properties like confluence, preservation of typing and termination. The goal of this internship is to develop a termination checker for Dedukti. Such a termination checker could later be extended to other languages like Coq, Agda or Haskell, and participate to the international competition of termination provers. URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/termin.pdf
Remarques :





SM2075 Proof tactics in Dedukti


Description


Dedukti is a formal proof checker based on a logical framework called the λΠcalculus modulo, which is an extension of the simplytyped lambdacalculus with dependent types and an equivalence relation on types generated by userdefined rewrite rules. Proofs generated by some automated theorem provers or proof assistants can be checked in Dedukti by encoding function definitions and axioms by rewrite rules. But, currently, no proof assistant fully uses all the features of Dedukti, which allows arbitrary userdefined rewrite rules (e.g. (x + y) + z → x + (y + z), where + is itself defined by other rules). Such rules are indeed necessary if one wants to ease the use of dependent types and, for instance, be able to define types for representing simplicial sets of arbitrary dimensions, ∞categories or models of Voevodsky's homotopy type theory. The goal of this internship is to develop a set of basic tactics for trying to solve Dedukti subgoals automatically, or help develop Dedukti proofs interac tively. URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/tactics.pdf
Remarques :





SM2076 Refinement in Dedukti


Description


Dedukti is a formal proof checker based on a logical framework called the λΠcalculus modulo, which is an extension of the simplytyped lambdacalculus with dependent types and an equivalence relation on types generated by userdefined rewrite rules. Proofs generated by some automated theorem provers or proof assistants can be checked in Dedukti by encoding function definitions and axioms by rewrite rules. But, currently, no proof assistant fully uses all the features of Dedukti, which allows arbitrary userdefined rewrite rules. We therefore would like to develop a tool for interactively building Dedukti proofs using all the features of Dedukti. But, to scale up and be able to handle large developments, especially with dependent and polymorphic types, we need to allow the users to write down incomplete terms (e.g. the type of the elements of a list), and provide an inference engine for finding out the missing subterms. The goal of this internship is then to develop such a refinement engine for Dedukti. URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/unif.pdf
Remarques :





SM2077 Interactive proofs with Dedukti


Description


Dedukti is a formal proof checker based on a logical framework called the λΠcalculus modulo, which is an extension of the simplytyped lambdacalculus with dependent types and an equivalence relation on types generated by the userdefined rewrite rules. Proofs generated by some automated theorem provers or proof assistants can be checked in Dedukti by encoding function definitions and axioms by rewrite rules. But, currently, no proof assistant fully uses all the features of Dedukti, which allows arbitrary userdefined rewrite rules. The goal of this internship is to develop an interface for Dedukti, that is, a tool for enabling users to build Dedukti proofs interactively. URL sujet détaillé : http://rewriting.gforge.inria.fr/divers/interface.pdf
Remarques :





