Secure computing systems design through formal micro-contracts

Two enduring concepts in computer system design are abstraction levels and layered composition. The design generally takes a layered approach where each layer implements a different abstraction of the system. The layers communicate through interfaces that are designed to support functional specification of the system as a whole. Traditionally, these layers and interfaces have primarily focused on functionality and efficiency-performance, power and area. Security-related issues are often overlooked or deferred until later in the design cycle or applied as add-ons when some security features are explicitly required. The challenge with this approach is that chasing security implications of certain design decisions along the multiple layers is a complex and error-prone task. Therefore, in this work, we are introducing the notion of "security micro-contracts" or simply "micro-contracts". We propose a novel secure computer systems design approach through minimal contracts-micro-contracts-between adjacent layers. These contracts have strict structures that contain security-relevant details of each connected layer and the secure-properties that have to be preserved to assure confidentiality, integrity and availability of the data of interest. Micro-contracts may be used as (i) basic formalism for proving security properties of computing systems both in the software and hardware layers and across them or (ii) run time security policy checks.