Automatic Generation of Assertions for Detection of Firmware Vulnerabilities Through Alignment of Symbolic Sequences
IEEE Transactions on Emerging Topics in Computing(2022)
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 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.
MoreTranslated text
Key words
Firmware vulnerabilities,assertion generation,symbolic simulation
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined