700
7 Countermeasures Against Hardware Trojans
and ultimately ending with the done command. Of course, it has to be said that PSL
is, first of all, a verification language, and the verification layer is the layer where
all instructions developed for SoC customers are only presented for the verification
means to ultimately verify the validity of this property. The assert instruction, for
example, will order the corresponding verification means to check whether a certain
property is present here; in case of its absence, the system will report this error.
By using the entire PSL or only a part of it to describe system properties, we can
automatically generate the necessary components of the tool used to verify and
monitor all instructions ensuring the safety of our designed SoC during operation.
It should be noted that while this effective design process suggested in [90] is
based solely on PSL, a number of other studies used the so-called open library
(OVL) Accelera [109]. OVL is actually not a language, but a library of parametrized
tools of claim verification, some of which can be synthesized directly into hardware.
Of course, instead of creating a general tool for checking the properties specified in
a high-level language such as PSL, the user can select the signals that he wants to
monitor and determine a specific expression that can be estimated at one or several
stages of the SoC tests.
Controller. Of course, a standard controller can be designed either by users themselves or generated based on the main sandboxed components known to the user. It
shall include all standard actions that need to be executed in the event of violation of
a security rule, receipt of the corresponding message of IP actions on an attempt to
introduce a hardware Trojan in the embedded processor and an attempt of unauthorized regulation of data exchange between virtual resources and the corresponding
actual physical resources. The structure of such controller can vary from a simple
finite state machine to a small processor processing any such complex code in the
sandbox.
7.6 Using Mathematical Instruments of Games Theory
and Information Forensic Methods to Counter
Hardware Trojans in Microcircuits
7.6.1 Introduction to the Problem
In one of the previous sections, we considered the possibilities of applying classic
methods of secure software design to solving the problem of detecting and countering
introduction of Trojans in microcircuits and made sure that it brings a good result.
The work [110] presents the results of application of a non-traditional method
of detection of hardware Trojans in ICs using such field of science as adversarial
dynamics [111], which had been previously unknown to microelectronics specialists. Developers of this method were stimulated by the openly published fact of
development and implementation of the special project in the well-known DARPA
7 Countermeasures Against Hardware Trojans
and ultimately ending with the done command. Of course, it has to be said that PSL
is, first of all, a verification language, and the verification layer is the layer where
all instructions developed for SoC customers are only presented for the verification
means to ultimately verify the validity of this property. The assert instruction, for
example, will order the corresponding verification means to check whether a certain
property is present here; in case of its absence, the system will report this error.
By using the entire PSL or only a part of it to describe system properties, we can
automatically generate the necessary components of the tool used to verify and
monitor all instructions ensuring the safety of our designed SoC during operation.
It should be noted that while this effective design process suggested in [90] is
based solely on PSL, a number of other studies used the so-called open library
(OVL) Accelera [109]. OVL is actually not a language, but a library of parametrized
tools of claim verification, some of which can be synthesized directly into hardware.
Of course, instead of creating a general tool for checking the properties specified in
a high-level language such as PSL, the user can select the signals that he wants to
monitor and determine a specific expression that can be estimated at one or several
stages of the SoC tests.
Controller. Of course, a standard controller can be designed either by users themselves or generated based on the main sandboxed components known to the user. It
shall include all standard actions that need to be executed in the event of violation of
a security rule, receipt of the corresponding message of IP actions on an attempt to
introduce a hardware Trojan in the embedded processor and an attempt of unauthorized regulation of data exchange between virtual resources and the corresponding
actual physical resources. The structure of such controller can vary from a simple
finite state machine to a small processor processing any such complex code in the
sandbox.
7.6 Using Mathematical Instruments of Games Theory
and Information Forensic Methods to Counter
Hardware Trojans in Microcircuits
7.6.1 Introduction to the Problem
In one of the previous sections, we considered the possibilities of applying classic
methods of secure software design to solving the problem of detecting and countering
introduction of Trojans in microcircuits and made sure that it brings a good result.
The work [110] presents the results of application of a non-traditional method
of detection of hardware Trojans in ICs using such field of science as adversarial
dynamics [111], which had been previously unknown to microelectronics specialists. Developers of this method were stimulated by the openly published fact of
development and implementation of the special project in the well-known DARPA