An official website of the United States government
We present SEIF, an exploratory methodology for information flow verification based on symbolic execution. SEIF begins with a statically built overapproximation of the information flow through a design and uses guided symbolic execution to provide a more precise picture of how information flows from a given set of security critical signals. SEIF can recognize and eliminate non-flows with high precision and for the true flows can find the corresponding paths through the design state with high coverage. We evaluate SEIF on two open-source CPUs, an AES core, and the AKER access control module. SEIF can be used to find counterexamples to information flow properties, and also to explore all flows originating from a source signal of interest. SEIF accounts for 86–90% of statically identified possible flows in three open-source designs. SEIF’s search strategies enable exploring the designs for 10-12 clock cycles in 4-6 seconds on average, demonstrating that this new exploratory style of information flow analysis can be practical.
more »
« less
Isadora: Automated Information Flow Property Generation for Hardware Designs
Isadora is a methodology for creating information flow specifications of hardware designs. The methodology combines information flow tracking and specification mining to produce a set of information flow properties that are suitable for use during the security validation process, and which support a better understanding of the security posture of the design. Isadora is fully automated; the user provides only the design under consideration and a testbench and need not supply a threat model nor security specifications. We evaluate Isadora on a RISC-V processor plus two designs related to SoC access control. Isadora generates security properties that align with those suggested by the Common Weakness Enumerations (CWEs), and in the case of the SoC designs, align with the properties written manually by security experts.
more »
« less
- Award ID(s):
- 1816637
- PAR ID:
- 10402174
- Date Published:
- Journal Name:
- ACM Workshop on Attacks and Solutions in Hardware Security
- Page Range / eLocation ID:
- 5 to 15
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Nadel, Alexander; Rozier, Kristin Yvonne (Ed.)Symbolic execution is a powerful verification tool for hardware designs, in particular for security validation. However, symbolic execution suffers from the path explosion problem in which the number of paths to explore grows exponentially with the number of branches in the design. We introduce a new approach, piecewise composition, which leverages the modular structure of hardware to transfer the work of path exploration to SMT solvers. Piecewise composition works by recognizing that independent parts of a design can each be explored once, and the exploration reused. A hardware design with N independent always blocks and at most b branch points per block will require exploration of O((2^b)N) paths in a single clock cycle with our approach compared to O(2^(bN)) paths using traditional symbolic execution. We present Sylvia, a symbolic execution engine implementing piecewise composition. The engine operates directly over RTL without requiring translation to a netlist or software simulation. We evaluate our tool on multiple open-source SoC and CPU designs, including the OR1200 and PULPissimo RISC-V SoC. The piecewise composition technique reduces the number of paths explored by an order of magnitude and reduces the runtime by 97% compared to our baseline. Using 84 properties from the security literature we find assertion violations in open-source designs that traditional model checking and formal verification tools do not find.more » « less
-
null (Ed.)This paper presents Transys, a tool for translating security critical properties written for one hardware design to analogous properties suitable for a second design. Transys works in three passes adjusting the variable names, arithmetic expressions, logical preconditions, and timing constraints of the original property to retain the intended semantics of the property while making it valid for the second design. We evaluate Transys by translating 27 assertions written in a temporal logic and 9 properties written for use with gate level information flow tracking across 38 AES designs, 3 RSA designs, and 5 RISC processor designs. Transys successfully translates 96% of the properties. Among these, the translation of 23 (64%) of the properties achieved a semantic equivalence rate of above 60%. The average translation time per property is about 70 seconds.more » « less
-
A technique to enhance the security of analog circuits using Satisfiability Modulo Theory (SMT) based design space exploration is described. The analog satisfiability (aSAT) technique takes as inputs generic circuit equations and performance constraints and, by exhaustively exploring the design space, outputs transistor sizes that satisfy the given constraints. The aSAT methodology is applied to parameter biasing obfuscation, where the width and length of a transistor are obfuscated to mask circuit properties. The proposed methodology was used in the design of a differential amplifier and an operational amplifier, where the widths and lengths determined through aSAT analysis were shown to meet the target circuit specifications. For the operational amplifier, transistor dimensions determined through aSAT analysis for a set of performance constraints were characterized and were found to meet the performance targets, however, there was a 7 MHz reduction in the gain bandwidth product. The simulated results indicate that the developed design methodology achieves a fast and accurate determination of transistor sizes for target specifications.more » « less
-
Security-critical applications on integrated circuits (ICs) are threatened by probing attacks that extract sensitive information assisted with focused ion beam (FIB) based circuit edit. Existing countermeasures, such as active shield, analog shield, and t-private circuit, have proven to be inefficient and provide limited resistance against probing attacks without taking FIB capabilities into consideration. In this paper, we propose a FIB-aware anti-probing physical design flow, which considers FIB capabilities and utilizes computer-aided design (CAD) tools, to automatically reduce the probing attack vulnerability of an IC’s security-critical nets with minimal extra design effort. The floor-planning and routing of the design are constrained by incorporating three new steps in the conventional physical design flow, so that security-critical nets are protected by internal shield nets with low overhead. Results show that the proposed technique can reduce the vulnerable area exposed to probing on security-critical nets by 100% with all critical nets fully protected for both advanced encryption standard (AES) and data encryption standard (DES) modules. The timing, area, and power overheads are less than 3% per module, which would be negligible in a system-on-chip (SoC) design.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3474376.3487286
