[MF01] Access control: Security Design Patterns
Area: Security, software engineering
Description:
The goal of this project is to build design patterns for
the implementation category-based access control systems.
The category-based access control metamodel is a generalisation
of the access control models currently in use. Design patterns
already exist for other access control models, the idea of the
project is to generalise the previous work and produce a set
of flexible design patterns that will facilitate the
implementation of category based access control systems.
[MF02] A Tool for the Analysis of Security Protocols in electronic commerce
Area: Security protocols, electronic commerce, cryptography, deductive methods
Description:
The Intruder Deduction Problem (IDP) consists in verifying whether a secret can be deduced from a set of messages eavesdropped by an attacker. This is a central problem in security analysis of cryptographic protocols. Recently, it has been proved that, under some restrictions that guarantee a separation of the algebraic power and the actual knowledge of the protocol that the potential intruder has, IDP is reduced to the Elementary Deduction Problem EDP. This is a simplified version of IDP where only the algebraic part should be considered.
The goal of this project is to implement an efficient algorithm for the treatment of EDP in a protocol used for electronic commerce. The implementation can be done in any programming language (e.g. Java) that can interact with tools for the computation of matching modulo associativity-commutativity (needed to simulate the capabalities of the intruder).
[MF03] Building certified programs
Area: Type systems, Specifications, Program extraction, certification.
Description:
There are several systems that allow programmers to develop a program
from a formal specification and to derive a proof of correctness. The
result is called a certified program. Certification here means
formal, mechanized verification, preferably with production of
independently checkable certificates. Some of the systems used to
develop certified programs are based on programming languages with
sophisticated type systems, or logical frameworks that allow users to
write the program specification and extract a program that satisfies
the specification. The goal of this project is to study and compare
systems for the development of certified programs.
[MF04] Distributed Access Control Models
Area: Security, Distributed Systems.
Description:
The goal of this project is to study, compare, and implement
access control models for distributed systems. In particular,
the project focuses on dynamic access control models, that take into
account the history of users' actions in order to permit/deny access
to resources.
[MF05] Tools to analyse the use of resources in programs using linear type systems
Area: Types, functional programming, program analysis
Description:
The goal of this project is to study and implement type
systems for linear functional languages and
use recent results on the linearisation of
algorithms to develop compilation techniques for program analysis (resource
usage).
[MF06] Tools for the analysis of category based access control policies
Area: Security, Access control
Description:
The goal of this project is to study the available tools for
the analysis of access control policies (e.g. VAC) and
design a tool that takes into account the characteristics of category-based
access control policies. The tool will be used by
security administrators in order to check that a policy satisfies
the required properties. From a given specification of an access
control policy (in the context of a bank, or a hospital for instance), it should provide information about users, categories,
resources, rights, etc.
[MF07] Declarative languages for Cloud computing
Area: Programming languages, service oriented architectures, compiler techniques
Description:
The goal of this project is to study and compare the
programming languages that have recently been proposed for
"Cloud-programming". The idea is to define the set of features
that a programming language (specifically a declarative one) should
have in order to be well-adapted for the development of applications
for the cloud, and design a declarative language, or
an extension for an existing declarative language, suitable for this
kind of applications.