Generating hardware security logic
The present disclosure includes systems and techniques relating to information flow and hardware security for digital devices and microprocessor systems. In general, in one implementation, a technique includes: receiving a hardware design specifying an implementation for information flow in a hardware configuration; receiving one or more labels annotating the hardware design; receiving a security property specifying a restriction relating to the one or more labels for implementing a secure information flow in the hardware configuration; designating each of the one or more labels to a corresponding security level in accordance with the specified restriction; and automatically assigning a respective value to each of the one or more labels in the hardware design, wherein each respective value is determined in accordance with the corresponding security level designated for each of the one or more labels.
1. A method performed by data processing apparatus, the method comprising:
receiving an initial hardware design specifying an implementation for information flow in hardware circuitry, wherein the initial hardware design comprises at least two variables relating to the information flow;
receiving one or more security labels annotating the initial hardware design, wherein each of the one or more security labels corresponds to a respective variable of the at least two variables;
receiving, in a high-level security language, a security property specifying a restriction on the information flow in the hardware circuitry, and, thus, the security property defining secure information flow in the hardware circuitry, wherein the security property specifies a relationship between the variables;
designating each of the one or more security labels to a corresponding security level in accordance with the specified restriction by generating, based on the security property, an ordering structure specifying a hierarchical order comprising at least two security levels;
generating a modified hardware design including automatically assigning a respective value to each of the one or more security labels in the initial hardware design based on the generated ordering structure, wherein each respective value is determined in accordance with the corresponding security level designated for each of the one or more security labels, wherein automatically assigning values to the security labels includes translating the security property from the high-level language into gate-level hardware logic; and
processing the automatically assigned label values to create a representation of security logic for the hardware circuitry, wherein the security logic implements the secure information flow defined by the security property.
2. The method of claim 1 , wherein the hierarchical order of the at least two security levels comprises a higher security level corresponding to a more restricted label specified in the security property and a lower security level corresponding to a less restricted label specified in the security property.
3. The method of claim 1 , wherein the ordering structure is generated as a security lattice.
4. The method of claim 1 , wherein the processing comprises:
optimizing the security logic based on the received security property by removing circuity from the security logic or adding circuity to the security logic in accordance with the security property.
5. The method of claim 4 , wherein the processing comprises:
performing one or more logic analysis functions using the optimized security logic,
wherein the one or more logic analysis functions comprises: formal verification, simulation, and hardware emulation.
6. The method of claim 1 , wherein the processing comprises:
deploying the security logic to implement circuitry in fabrication or FPGA.
7. An apparatus, comprising:
a processor; and
a memory storing program instructions that when executed cause the processor to perform operations comprising:
receiving an initial hardware design specifying an implementation for information flow in hardware circuitry, wherein the initial hardware design comprises at least two variables relating to the information flow;
receiving one or more security labels annotating the initial hardware design, wherein each of the one or more security labels corresponds to a respective variable of the at least two variables;
receiving, in a high-level security language, a security property specifying a restriction on the information flow in the hardware circuitry, and, thus, the security property defining secure information flow in the hardware circuitry, wherein the security property specifies a relationship between the variables;
designating each of the one or more security labels to a corresponding security level in accordance with the specified restriction by generating, based on the security property, an ordering structure specifying a hierarchical order comprising at least two security levels;
generating a modified hardware design including automatically assigning a respective value to each of the one or more security labels in the initial hardware design based on the generated ordering structure, wherein each respective value is determined in accordance with the corresponding security level designated for each of the one or more labels, wherein the operation of automatically assigning values to the security labels includes translating the security property from the high-level language into gate-level hardware logic; and
processing the automatically assigned label values to create a representation of security logic for the hardware circuitry, wherein the security logic implements the secure information flow defined by the security property.
8. The apparatus of claim 7 , wherein the hierarchical order of the at least two security levels comprises a higher security level corresponding to a more restricted label specified in the security property and a lower security level corresponding to a less restricted label specified in the security property.
9. The apparatus of claim 7 , wherein the ordering structure is generated as a security lattice.
10. The apparatus of claim 7 , wherein the operation of processing comprises:
optimizing the security logic based on the received security property by removing circuity from the security logic or adding circuity to the security logic in accordance with the security property.
11. The apparatus of claim 10 , wherein the operation of processing comprises:
performing one or more logic analysis functions using the optimized security logic,
wherein the one or more logic analysis functions comprises: formal verification, simulation, and hardware emulation.
12. The apparatus of claim 11 , wherein the operation of processing comprises:
deploying the security logic to implement circuitry in fabrication or FPGA.