Work-in-Progress: DOVE: Pinpointing firmware security vulnerabilities via symbolic control flow assertion mining

In the past decade, the number of reported security attacks exploiting unchecked input firmware values has been on the rise. To address this concerning trend, this work proposes a novel detection framework, called DOVE, capable of identifying unlikely firmware execution flows, specifically those that may reveal a security vulnerability. The DOVE framework operates by leveraging a symbolic simulation of the firmware's execution, paired with a probability computation that can identify unlikely execution flows and provide to the user corresponding formal assertions.