US 11,989,299 B2
Verifying firmware binary images using a hardware design and formal assertions
Ashish Darbari, Abbots Langley (GB)
Assigned to Imagination Technologies Limited, Kings Langley (GB)
Filed by Imagination Technologies Limited, Kings Langley (GB)
Filed on Jan. 26, 2021, as Appl. No. 17/158,798.
Application 17/158,798 is a continuation of application No. 15/784,615, filed on Oct. 16, 2017, granted, now 11,010,477.
Claims priority of application No. 1617532 (GB), filed on Oct. 14, 2016.
Prior Publication US 2021/0150031 A1, May 20, 2021
This patent is subject to a terminal disclaimer.
Int. Cl. G06F 21/57 (2013.01); G06F 21/51 (2013.01)
CPC G06F 21/572 (2013.01) [G06F 21/51 (2013.01); G06F 2221/033 (2013.01)] 14 Claims
OG exemplary drawing
 
1. A hardware monitor arranged to detect illegal firmware instructions in a firmware binary image based on a hardware design for an electronic device configured to execute the firmware binary image, detect illegal firmware instructions in the firmware binary image, and stop execution of the firmware binary image upon detection of an illegal firmware instruction, the hardware monitor comprising:
monitor and detection logic configured to:
detect that an instantiation of the hardware design has stopped execution of the firmware binary image; and
detect that the instantiation of the hardware design implements a decode of an illegal firmware instruction; and
assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more formal assertions that assert a formal property that states that if a stop of firmware binary image execution has been detected, that decode of an illegal firmware instruction has, or has not, been detected.