Toward a Methodology for Unified Verification of Hardware/Software Co-designs

Florian Lugou 1, 2, 3 Ludovic Apvrille 2, 3 Aurélien Francillon 1
2 LabSoC - System on Chip
LTCI - Laboratoire Traitement et Communication de l'Information
Abstract :

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 re- cent 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 pro- posed 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 at- testation system (SMART).

Complete list of metadatas

https://hal.telecom-paristech.fr/hal-02287183
Contributor : Telecomparis Hal <>
Submitted on : Friday, September 13, 2019 - 4:40:56 PM
Last modification on : Thursday, October 17, 2019 - 12:37:00 PM

Identifiers

  • HAL Id : hal-02287183, version 1

Citation

Florian Lugou, Ludovic Apvrille, Aurélien Francillon. Toward a Methodology for Unified Verification of Hardware/Software Co-designs. PROOFS, Sep 2015, Saint Malo, France. ⟨hal-02287183⟩

Share

Metrics

Record views

6