Secure computing systems design through formal micro-contracts

Michel A. Kinsy, Novak Boskov

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationGLSVLSI 2019 - Proceedings of the 2019 Great Lakes Symposium on VLSI
PublisherAssociation for Computing Machinery
Number of pages6
ISBN (Electronic)9781450362528
StatePublished - May 13 2019
Externally publishedYes
Event29th Great Lakes Symposium on VLSI, GLSVLSI 2019 - Tysons Corner, United States
Duration: May 9 2019May 11 2019

Publication series

NameProceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI


Conference29th Great Lakes Symposium on VLSI, GLSVLSI 2019
Country/TerritoryUnited States
CityTysons Corner


  • Abstract level
  • Formal methods
  • Layered composition
  • Micro-contracts
  • Secure system design
  • Security

ASJC Scopus subject areas

  • Engineering(all)


Dive into the research topics of 'Secure computing systems design through formal micro-contracts'. Together they form a unique fingerprint.

Cite this