Invention Grant
- Patent Title: Verifying firmware binary images using a hardware design and formal assertions
-
Application No.: US15784615Application Date: 2017-10-16
-
Publication No.: US11010477B2Publication Date: 2021-05-18
- Inventor: Ashish Darbari
- Applicant: Imagination Technologies Limited
- Applicant Address: GB Kings Langley
- Assignee: Imagination Technologies Limited
- Current Assignee: Imagination Technologies Limited
- Current Assignee Address: GB Kings Langley
- Agency: Potomac Law Group, PLLC
- Agent Vincent M DeLuca
- Priority: GB1617532 20161014
- Main IPC: G06F21/57
- IPC: G06F21/57 ; G06F21/51

Abstract:
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.
Public/Granted literature
- US20180107825A1 Verifying Firmware Binary Images Using a Hardware Design and Formal Assertions Public/Granted day:2018-04-19
Information query