TL;DR
This paper presents a formal verification approach for a compiler that enforces source-level security policies through hardware-assisted tagging, ensuring correctness in policy preservation during compilation.
Contribution
It extends source language semantics with tag-based monitoring and verifies that the compiler preserves this behavior, using a Coq-verified prototype called Tagine.
Findings
Successfully formalized source-level tag monitoring semantics.
Verified that the compiler preserves monitoring behavior.
Developed a verified prototype compiler in Coq.
Abstract
Hardware-assisted reference monitoring is receiving increasing attention as a way to improve the security of existing software. One example is the PIPE architecture extension, which attaches metadata tags to register and memory values and executes tag-based rules at each machine instruction to enforce a software-defined security policy. To use PIPE effectively, engineers should be able to write security policies in terms of source-level concepts like functions, local variables, and structured control operators, which are not visible at machine level. It is the job of the compiler to generate PIPE-aware machine code that enforces these source-level policies. The compiler thus becomes part of the monitored system's trusted computing base -- and hence a prime candidate for verification. To formalize compiler correctness in this setting, we extend the source language semantics with its…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
