Description
Date depot: 1 janvier 1900
Titre: Assisting the Design of Secured Applications for Embedded Systems
Directeur de thèse:
Ludovic APVRILLE (LTCI (EDMH))
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
The Intelligent Transport Systems (ITS) arose several years ago pushing the design of secured applications for the automotive industry. The ITS paradigm envisages the infrastructure not only for exchanging information between cars, but with the infrastructure. Such network of mobile and fixed communicating entities pursues several goals. Many of them are in the scope of driver/car safety. As ITS technology arises, in-car applications become distributed, what exposes them to new risks like viruses, disclosure of sensitive information, car impersonation, Denial of Services, etc. Indeed, the misuse of applications and/or transfers in the in-vehicular communication may affect vehicle's behavior and compromise the entire distributed network of neighbor cars, therefore security plays a considerable role.
To achieve a certain level of applications assurance, formal verification is indeed needed. Formal techniques may help to increase the level of assurance of ITS solutions. However, to successfully perform verification, several questions have to be addressed. For instance, how to integrate approaches in the engineering design process to verify and ensure system correctness (HW and SW). Even if we agree that certain properties ensure expected behavior, systems' complexity imposes several restrictions, e.g., with respect to the state explosion problem. Along with that, targetted properties may range from safety to security what demands a verification methodology and framework amenable for both. In addition, distributed systems may be required to satisfy a complex set of security requirements, ranging from integrity to privacy.
Taking into account identified issues, the thesis targets a formal framework for:
a. Representation of embedded systems (HW-SW)
b. Representation of security properties
c. Representation of challengers, e.g., attackers, misusers
d. Verification of properties with respect to challengers
Last but not least, the formal framework should also effectively consider constraints imposed by embedded in-car systems.
Doctorant.e: Pedroza Bernal Juan Gabriel