SM207-1 Attack-defense trees for computer security  
Admin  
Encadrant : Barbara KORDY
Labo/Organisme : IRISA
URL : http://people.irisa.fr/Barbara.Kordy/internships.php
Ville : Rennes

Description  

An attack-defense tree (ADTree) is an AND-OR 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 real-life 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é



SM207-2 AUTOMATIC MINIMIZATION OF LARGE SYSTEMS OF EQUATIONS  
Admin  
Encadrant : Tribastone MIRCO
Labo/Organisme : IMT School for Advanced Studies
URL : sysma.imtlucca.it :
Ville : Lucca (Italy)

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 real-world 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 real-world systems.

The work will be carried out at IMT School for Advanced Studies Lucca, one of Italy's six schools of excellence for post-graduate 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 high-profile CS venues can be expected as an output of this work.
URL sujet détaillé : :

Remarques :



SM207-3 Vérification de systèmes distribués communiquant par messages  
Admin  
Encadrant : Aurélie HURAULT
Labo/Organisme : IRIT
URL : https://www.irit.fr/-Equipe-ACADIE-
Ville : Toulouse

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; pi-calculus 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/sujet-master-ens-2016.pdf

Remarques : Co-encadrement : Philippe Quéinnec (queinnec.fr)



SM207-4 Termination checking in Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the
λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus
with dependent types and an equivalence relation on
types generated by the user-defined 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 :



SM207-5 Proof tactics in Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus with dependent types and an equivalence relation on types generated
by user-defined 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 user-defined 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 :



SM207-6 Refinement in Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus with dependent types and an equivalence relation on types generated by user-defined 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 user-defined 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 :



SM207-7 Interactive proofs with Dedukti  
Admin  
Encadrant : Frédéric BLANQUI
Labo/Organisme : LSV
URL : http://rewriting.gforge.inria.fr/
Ville : Cachan

Description  

Dedukti is a formal proof checker based on a logical framework called the λΠ-calculus modulo, which is an extension of the simply-typed lambda-calculus with dependent types and an equivalence relation on types generated by the user-defined 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 user-defined 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 :




Last modification : 2016-09-23 18:40:52 laurent.lefevre@ens-lyon.fr View source.