YoVDO

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

Offered By: IEEE via YouTube

Tags

IEEE Symposium on Security and Privacy Courses Formal Verification Courses Security Policies Courses Memory Safety Courses Control-Flow Integrity Courses

Course Description

Overview

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.

Syllabus

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


Taught by

IEEE Symposium on Security and Privacy

Tags

Related Courses

Sensor Security
IEEE via YouTube Tracking Ransomware End-to-end
IEEE via YouTube Cinderella - Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation
IEEE via YouTube Algorithmic Transparency via Quantitative Input Influence - Theory and Experiments with Learning Systems
IEEE via YouTube Bitcoin Over Tor Isn't a Good Idea
IEEE via YouTube