The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
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.
How it got here
How it got here
agent via openalex
Added
2026-10-25 18:42 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{deamorim2015micropolicies,
title = {Micro-Policies: Formally Verified, Tag-Based Security Monitors},
author = {Arthur Azevedo de Amorim and Maxime Dénès and Nick Giannarakis and Cătălin Hriţcu and Benjamin C. Pierce and Antal Spector-Zabusky and Andrew P. Tolmach},
year = {2015},
journal = {Proceedings - IEEE Symposium on Security and Privacy/Proceedings of the ... IEEE Symposium on Security and Privacy},
publisher = {IEEE Computer Society},
pages = {813--830},
doi = {10.1109/sp.2015.55},
}