UC Riverside

Hardware has become an increasingly attractive target for attackers, yet we still largely lack tools that enable us to analyze large designs for security flaws. Information flow tracking (IFT) models provide an approach to verifying a hardware design's adherence to security properties related to isolation and reachability. However, existing precise IFT models are usually too complex to actually use. Queries may fail to finish even for small designs when verifying relatively simple properties. It is possible to create less complex models, but these come at the cost of a severe loss of precision - -they frequently indicate a property fails when in fact it passes, which means verification requires extensive additional manual investigation. We present a new method to bridge the chasm between precision and complexity in a finer-grained, controlled, and disciplined manner. Our method allows using the most appropriate precision/complexity tradeoff for the design size and available computing resources, meaning it is now possible to create models that are not too complex to be usable, but which offer more precision (fewer false positives) than was previously possible.