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
-
This paper proposes a novel method for automatically inferring message flow specifications from the communication traces of a system-on-chip (SoC) design that captures messages exchanged among the components during a system execution. The inferred message flows characterize the communication and coordination of components in a system design for realizing various system functions, and they are essential for SoC validation and debugging. The proposed method relieves the burden of manual development and maintenance of such specifications on human designers. Our method also uses a new accuracy metric, acceptance ratio, to evaluate the quality of the mined specifications instead of the specification size often used in the previous work, enabling more accurate specifications to be mined. Furthermore, this paper introduces the concept of essential causalities to enhance the accuracy of the message flow mining and accelerate the mining process. The effectiveness of the proposed method is evaluated on both synthetic traces and traces generated from executing several system models in GEM5. In both cases, the proposed method achieves superior accuracies compared to a previous approach. Additionally, this paper includes some practical use cases.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3474376.3487286
