A tool for verifying noninterference property for HDL

Hardware description languages started to adopt high-level functionalities. Through the flexibility of high-level programming, hardware designers can leverage object-oriented programming and functional programming paradigms to specify the hardware for quicker design time. This transition to high-level hardware descriptions created a new set of problems about verifying their noninterference property. By extending a high-level HDL, this thesis shows how to approach and solve this new set of problems and thus preventing information leakage. SecChisel (based on Chisel HDL) gives the ability to design circuits which have algorithmically verifiable noninterference property. SecChisel handles the creation of temporary variables and cascaded propagation of security tags to these new variables which are unique problems that only occurs when the host language creates an intermediate representation of the designed circuit. SecChisel algorithmically verifies a design by transforming and modeling the design in a satisfiability modulo theory (SMT) solver. By building and verifying hardware designs, we demonstrate that SecChisel provides a simple way to verify circuit design's noninterference property at compile time with no overhead.