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

Toward a methodology for unifi ed veri cation of hardware/software co-designs

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

PROOFS 2015, Security Proofs for Embedded Systems, 17 September 2015, Saint-Malo, France / To be published in Journal of Cryptographic Engineering (JCEN), Springer

Critical and private 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 o er 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 eciency of these solutions raises challenges since software and hardware veri cations approaches generally rely on di erent representations. The paper rst sketches an ideal security veri cation solution naturally handling both hardware and software components. Next, it proposes an evaluation  of  formal  veri cation  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 Hal Bibtex

Titre:Toward a methodology for unifi ed veri cation of hardware/software co-designs
Mots Clés:hardware/software co-design, embedded system veri cation, security, ProVerif, tools
Type:Conférence
Langue:English
Ville:Saint-Malo
Pays:FRANCE
Date:
Département:Sécurité numérique
Eurecom ref:4668
Copyright: © Springer. Personal use of this material is permitted. The definitive version of this paper was published in PROOFS 2015, Security Proofs for Embedded Systems, 17 September 2015, Saint-Malo, France / To be published in Journal of Cryptographic Engineering (JCEN), Springer and is available at :
Bibtex: @inproceedings{EURECOM+4668, year = {2015}, title = {{T}oward a methodology for unifi ed veri cation of hardware/software co-designs}, author = {{L}ugou, {F}lorian and {A}pvrille, {L}udovic and {F}rancillon, {A}ur{\'e}lien}, booktitle = {{PROOFS} 2015, {S}ecurity {P}roofs for {E}mbedded {S}ystems, 17 {S}eptember 2015, {S}aint-{M}alo, {F}rance / {T}o be published in {J}ournal of {C}ryptographic {E}ngineering ({JCEN}), {S}pringer}, address = {{S}aint-{M}alo, {FRANCE}}, month = {09}, url = {http://www.eurecom.fr/publication/4668} }
Voir aussi: