IFV: Information Flow Verification at the Pre-silicon Stage Utilizing Static-Formal Methodology

By Rasheed Kibria, Farimah Farahmandi, Mark Tehranipoor
University of Florida

Abstract

Modern system-on-chips (SoCs) are becoming prone to numerous security vulnerabilities due to their ever-growing complexity and size. Therefore, a comprehensive security verification framework is needed at the very early stage of the SoC design lifecycle. The datapath of a complex SoC design may be vulnerable to information leakage and data integrity issues. The designers might be unaware of hidden information flow paths present in a particular SoC design at the pre-silicon stage, which can eventually lead to severe data breaches. Hence, it is crucial to develop a novel framework that comprehensively identifies the presence of such paths. Moreover, novel mathematical metrics need to be formulated to perform an exhaustive quantitative assessment of the detected information leakage paths. It will assist designers in quantifying the security risk level associated with these data propagation paths, ultimately making them aware of the potential implications of these leakage paths. In this paper, we propose an information flow verification framework that utilizes a combination of static and formal methodologies to identify information flow paths based on a mathematical metric for quantifying the security risk level of the detected paths. Our experiments across numerous open-source designs, varying in size and complexity, demonstrate the efficacy of the proposed framework for identifying severe information leakage and data integrity issues at the pre-silicon stage of the design lifecycle.

Index Terms — Static verification, Formal methods, Information security, SoC security verification

To read the full article, click here