Verifying firmware binary images using a hardware design and formal assertions
摘要:
Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more assertions that assert that if a stop of firmware execution has been detected, that a decode of an illegal firmware instruction has (or has not) been detected. The hardware monitor may be used by a formal verification tool to exhaustively verify that the firmware boot image does not comprise an illegal firmware instruction, or during simulation to detect illegal firmware instructions in a firmware boot image.
信息查询
0/0