Toward Hardware Security Property Generation at Scale

Abstract

Using formal methods requires first developing the properties to be verified, which is a difficult and time-consuming task. This article describes our research on automating the property generation process for information-flow properties that are critical to the security of hardware designs.