Méthodes FormellesAxe: SciLex
Coordinateur : Hubert Comon Lundh, LSV, ENS Cachan
Productions Scientifiques :
Financement Labex en : 2014/2015
Financements adossés au GT
- CDD Ingénieur de recherche du 01/09/2017 - 01/09/2018
- CDD Ingénieur de recherche du 01/09/2017 - 01/09/2018 (prolongation après congé de maternité)
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.