Ecole d'ingénieur et centre de recherche en Sciences du numérique

SMASHUP: a toolchain for unified verification of hardware/software co-designs

Lugou, Florian; Apvrille, Ludovic; Francillon, Aurélien

Journal of Cryptographic Engineering, Special Section on Proofs, November 2016

Critical and privacy-sensitive applications of smart and connected objects such as health-related objects are now common, thus raising the need to design these objects with strong security guarantees. Many recent works offer practical hardware-assisted security solutions that take advantage of a tight cooperation between hardware and software to provide system-level security guarantees. Formally and consistently proving the efficiency of these solutions raises challenges since software and hardware verifications approaches generally rely on different representations. The paper first sketches an ideal security verification solution naturally handling both hardware and software components. Next, it proposes an evaluation of formal verification methods that have already been proposed for mixed hardware/software systems, with regards to the ideal method. At last, the paper presents a conceptual approach to this ideal method relying on ProVerif, and applies this approach to a remote attestation system (SMART).

Document Doi Hal Bibtex

Titre:SMASHUP: a toolchain for unified verification of hardware/software co-designs
Mots Clés:Hardware/software co-design, Embedded system verification, Security, ProVerif, Tools
Type:Journal
Langue:English
Ville:
Date:
Département:Sécurité numérique
Eurecom ref:5062
Copyright: © Springer. Personal use of this material is permitted. The definitive version of this paper was published in Journal of Cryptographic Engineering, Special Section on Proofs, November 2016 and is available at : http://dx.doi.org/10.1007/s13389-016-0145-2
Bibtex: @article{EURECOM+5062, doi = {http://dx.doi.org/10.1007/s13389-016-0145-2}, year = {2016}, month = {11}, title = {{SMASHUP}: a toolchain for unified verification of hardware/software co-designs}, author = {{L}ugou, {F}lorian and {A}pvrille, {L}udovic and {F}rancillon, {A}ur{\'e}lien}, journal = {{J}ournal of {C}ryptographic {E}ngineering, {S}pecial {S}ection on {P}roofs, {N}ovember 2016}, url = {http://www.eurecom.fr/publication/5062} }
Voir aussi: