Micro-Policies: Formally Verified, Tag-Based Security Monitors
| Autor: | Andrew Tolmach, Benjamin C. Pierce, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Nick Giannarakis, Catalin Hritcu, Maxime Dénès |
|---|---|
| Přispěvatelé: | Department of Computer and Information Science [Pennsylvania] (CIS), University of Pennsylvania [Philadelphia], Programming securely with cryptography (PROSECCO ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Langages de programmation, types, compilation et preuves (GALLIUM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), National Technical University of Athens [Athens] (NTUA), Department of Computer Science [Portland] (CS), Portland State University [Portland] (PSU), University of Pennsylvania, Programming securely with cryptography (PROSECCO) |
| Rok vydání: | 2015 |
| Předmět: |
tagged hardware architecture
reference mon-itors Computer science CPU cache Principle of least privilege 0211 other engineering and technologies Compartmentalization (information security) 02 engineering and technology Index Terms-security computer.software_genre Security policy [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Software 0202 electrical engineering electronic engineering information engineering Coq refinement [INFO]Computer Science [cs] formal verification Formal verification machine-checked proofs memory safety 021110 strategic defence & security studies Programming language business.industry dynamic enforcement metadata 020207 software engineering compartmentalization least privilege Metadata control-flow integrity Operating system low-level code dynamic sealing business isolation computer |
| Zdroj: | IEEE Symposium on Security and Privacy 2015 IEEE Symposium on Security and Privacy 2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813-830, ⟨10.1109/SP.2015.55⟩ |
| Popis: | International audience ; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|