Symbolic simulation of firmware allows to automatically find execution paths triggering undesired behaviors that could hide vulnerabilities. However, once an unexpected behavior is identified, understanding its origin is an even more challenging task for the verification engineer. While several static and dynamic tools exist for detecting vulnerabilities, the same is not true for identifying their causes. This paper is intended to fill in the gap by proposing an automatic framework for catching the source of IP vulnerabilities. Given an unwanted behavior, in the form of a propositional logic assertion, the framework exploits symbolic simulation and a sequence alignment algorithm to generate a set of temporal assertions that represent the minimum sequence of firmware instructions necessary for triggering the related vulnerability. In this way, the designer can effectively identify the cause of the vulnerability and fix it. Experimental results show the efficacy of the methodology in terms of efficiency and effectiveness.

Automatic generation of assertions for detection of firmware vulnerabilities through alignment of symbolic sequences

Samuele Germiniani
;
Alessandro Danese
;
Graziano Pravadelli
2020

Abstract

Symbolic simulation of firmware allows to automatically find execution paths triggering undesired behaviors that could hide vulnerabilities. However, once an unexpected behavior is identified, understanding its origin is an even more challenging task for the verification engineer. While several static and dynamic tools exist for detecting vulnerabilities, the same is not true for identifying their causes. This paper is intended to fill in the gap by proposing an automatic framework for catching the source of IP vulnerabilities. Given an unwanted behavior, in the form of a propositional logic assertion, the framework exploits symbolic simulation and a sequence alignment algorithm to generate a set of temporal assertions that represent the minimum sequence of firmware instructions necessary for triggering the related vulnerability. In this way, the designer can effectively identify the cause of the vulnerability and fix it. Experimental results show the efficacy of the methodology in terms of efficiency and effectiveness.
firmware vulnerabilities
assertion generation
symbolic simulation
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/1057780
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact