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 oer 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 verications approaches generally rely on dierent representations. The paper rst sketches an ideal security verication solution naturally handling both hardware and software components. Next, it proposes an
evaluation of formal verication 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)
Type:
Conference
City:
Saint-Malo
Date:
2015-09-17
Department:
Digital Security
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 :
See also: