Semantics-driven design and implementation of high-assurance hardware
Adam M. Procter · MOspace Institutional Repository (University of Missouri) · 2014
Modularity, that is the division of complex systems into less complex and more easily understood parts, is a pervasive concern in computer science, and hardware design is no exception. Existing hardware design languages such as Verilog and VHDL supportmodular design by enabling hardware designers to decomposede signs into structural features that may be developed independently and connected together to form more complex devices. Intherealmofhighassuranceforsecurity, however, this sort of modularity is often of limited utility. Security properties are notoriously non-compositional, i.e. subsystems that independently satisfy some security property cannot necessary be relied upon to maintain that property when operating in tandem. The aim of this research is to establish semantically modular techniques for hard ware design and implementation, in contrast to the conventional structural notion of modularity. A semantically modular design is constructed by adding �layers� of semantic features, such as state and reactivity, one at a time. From the high as surance aspect, semantic modularity enables different layers of semantic features to be reasoned about independently, greatly simplifying the structure of correct ness proofs and improving their reusability. The major contribution of this work is a prototype compiler called ReWire which translates semantically modular hard ware specifications to efficient implementations on FPGAs. In this dissertation I present the design and implementation of the ReWire compiler, along with a num ber of case studies illustrating both the practicality of the ReWire compiler and the elegance of the semantically modular approach to hardware verification.