Micro-Policies - Formally Verified, Tag-Based Security Monitors

Explore a 22-minute IEEE conference talk on formally verified, tag-based security monitors called micro-policies. Delve into a methodology for defining and reasoning about tag-based reference monitors using a high-level "symbolic machine." Examine the implementation of micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety. Learn how the tagging mechanism can protect its own integrity. Discover how the symbolic machine is implemented using a hardware rule cache and software controller. Gain insights into the refinement proofs that demonstrate how the symbolic machine embodies high-level security property specifications.