Verification and Synthesis of Information Flow Secure Hardware Designs

The increasing number of hardware-based security attacks along with prevalence of embedded systems in critical applications necessitate robust methods for designing digital circuits with regards to security expectations. However, state of the art secure hardware design practices are mainly based on manual code review and security audit which do not provide formal guarantees of security despite being time-consuming and cumbersome. Thus, a systematic approach for identifying and fixing security vulnerabilities in hardware designs is required.Information flow analysis presents a coherent and systematic method for evaluation of broad types of security policies. Information flow models capture how security-critical data propagates through a system by augmenting the design with security labels. Therefore, evaluating the security labels of the critical components could substitute manual inspection of the design for information leakage. Such analysis accelerates, automates, and formalizes assessment of information flow security properties. This dissertation shows how various security policies such as confidentiality, integrity and timing side-channel can be formalized utilizing information flow tracking (IFT) in hardware designs.Following this formalization, this thesis presents four practical tools -- RTLIFT and Clepsydra for verification of timing-sensitive information flow properties, VeriSketch for synthesis and enforcement of timing-sensitive information flow properties, and lastly an error localization framework for automated inspection of verification failures. Leveraging advances in formal methods and commercial EDA software, the presented tools augment the traditional hardware design cycle with sound and automated security analysis