Automatic Generation of Assertions for Detection of Firmware Vulnerabilities Through Alignment of Symbolic Sequences

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 article 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.