2015 IEEE Symposium on Security and Privacy (SP) (2015)
San Jose, CA, USA
May 17, 2015 to May 21, 2015
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SP.2015.55
Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level "symbolic machine" and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety, in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy's rules embodies a high-level specification characterizing a useful security property. Last, we show how the symbolic machine itself can be implemented in terms of a hardware rule cache and a software controller.
Registers, Monitoring, Concrete, Hardware, Transfer functions, Safety
A. A. Amorim et al., "Micro-Policies: Formally Verified, Tag-Based Security Monitors," 2015 IEEE Symposium on Security and Privacy (SP), San Jose, CA, USA, 2015, pp. 813-830.