Méthodes FormellesAxe: SciLex
Coordinateur : Hubert Comon Lundh, LSV, ENS Cachan
Objectif :
Productions Scientifiques :
Financement Labex en : 2014/2015
Documents :
Financements adossés au GT
- CDD Ingénieur de recherche du 01/09/2017 – 01/09/2018
- Tuteurs: Chantal Keller, Stephane Graham-Lengrand
- Nom du candidat : Valentin Blot
- Laboratoires concernés : LRI, LIX
- Nom du projet: De la vérification de preuves à la démonstration automatique
- CDD Ingénieur de recherche du 01/09/2017 – 01/09/2018 (prolongation après congé de maternité)
- Tuteurs: Ulrich Kühne, Laurent Fribourg, LSV, Jean-Luc Danger, Telecom ParisTech, Hubert Comon Lundh
- Nom du candidat : Maha Naceur
- Laboratoires concernés : Telecom Paris Tech, LSV
- Nom du projet: PROCRAST – Provable Complete Runtime-Checking for Hardware Security and Trustability
The overall goal of the proposed project is to investigate run-time verification using hardware monitors in the context of security. In particular, we plan to establish metrics for the quality of a security specification based on coverage notions for formal verification. The findings shall be implemented in a tool that will be capable of generating HDL code for hardware monitors from a security specification, and answer questions on the completeness or coverage of the specification.
Preliminary results and methodology have been presented at the TRUDEVICE workshop on Trustworthy Manufacturing and Utilization of Secure Devices, collocated with the Design, Automation, and Test in Europe (DATE) conference in March 2018. In the remaining four months of the project(due to a maternal leave of the associated post-doctoral researcher), we will complete the tool for run-time monitor generation and study its impact on a set of standard hardware Trojan horse benchmarks.