Toward a methodology for unified verification of hardware/software co-designs

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 verications approaches generally rely on dierent 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)