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

No abstract is available for this paper.

• Publication year

  2015

• Venue

  IEEE Symposium on Security and Privacy

• Publication date

  2015-05-17

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/SP.2015.55
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Architectural Support for Software-Defined Metadata Processing

  2015cited by this paper
• Beyond the PDP-11: Architectural Support for a Memory-Safe C Abstract Machine

  2015cited by this paper
• CCFI: Cryptographically Enforced Control Flow Integrity

  2015cited by this paper
• Out of Control: Overcoming Control-Flow Integrity

  2014cited by this paper
• Portable Software Fault Isolation

  2014cited by this paper
• Cryptographically Enforced Control Flow Integrity

  2014cited by this paper
• Hardware-assisted fine-grained control-flow integrity: Towards efficient protection of embedded systems against software exploitation

  2014cited by this paper
• Information Flow Control in WebKit's JavaScript Bytecode

  2014cited by this paper
• The CHERI capability model: Revisiting RISC in an age of risk

  2014cited by this paper
• Stitching the Gadgets: On the Ineffectiveness of Coarse-Grained Control-Flow Integrity Protection

  2014cited by this paper
• FADE: A programmable filtering accelerator for instruction-grain monitoring

  2014cited by this paper
• Modular control-flow integrity

  2014cited by this paper
• WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking

  2014cited by this paper
• Temporal Mode-Checking for Runtime Monitoring of Privacy Policies

  2014cited by this paper
• Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis

  2014cited by this paper
• KCoFI: Complete Control-Flow Integrity for Commodity Operating System Kernels

  2014cited by this paper
• A Theory of Information-Flow Labels

  2013cited by this paper
• Hardware-Enforced Comprehensive Memory Safety

  2013cited by this paper
• Coq: the world's best macro assembler?

  2013cited by this paper
• Layout Randomization and Nondeterminism

  2013cited by this paper
• Practical Control Flow Integrity and Randomization for Binary Executables

  2013cited by this paper
• On Layout Randomization for Arrays and Functions

  2013cited by this paper
• Sancus: Low-cost Trustworthy Extensible Networked Devices with a Zero-software Trusted Computing Base

  2013cited by this paper
• The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier

  2013cited by this paper
• All Your IFCException Are Belong to Us

  2013cited by this paper
• High-level separation logic for low-level code

  2013cited by this paper
• Low-fat pointers: compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security

  2013cited by this paper
• Testing noninterference, quickly

  2013cited by this paper
• SoK: Eternal War in Memory

  2013cited by this paper
• Information-Flow Security for a Core of JavaScript

  2012cited by this paper
• The CompCert Memory Model, Version 2

  2012cited by this paper
• Hardware Support for Safety Interlocks and Introspection

  2012cited by this paper
• RockSalt: better, faster, stronger SFI for the x86

  2012cited by this paper
• Flexible dynamic information flow control in Haskell

  2012cited by this paper
• CHERI: a research platform deconflating hardware virtualisation and protection

  2012cited by this paper
• Enforceable Security Policies Revisited

  2012cited by this paper
• High-performance parallel accelerator for flexible and efficient run-time monitoring

  2012cited by this paper
• Disjunction Category Labels

  2011cited by this paper
• Preliminary design of the SAFE platform

  2011cited by this paper
• SIFT: a low-overhead dynamic information flow tracking architecture for SMT processors

  2011cited by this paper
• ARMor: Fully verified software fault isolation

  2011influential reference
• Provably correct inline monitoring for multithreaded Java-like programs

  2010cited by this paper
• Permissive dynamic information flow analysis

  2010cited by this paper
• On Protection by Layout Randomization

  2010cited by this paper
• CETS: compiler enforced temporal safety for C

  2010cited by this paper
• Flexible and Efficient Instruction-Grained Run-Time Monitoring Using On-Chip Reconfigurable Fabric

  2010cited by this paper
• Composing expressive runtime security policies

  2009cited by this paper
• SoftBound: highly compatible and complete spatial memory safety for c

  2009cited by this paper
• Efficient purely-dynamic information flow analysis

  2009influential reference
• Native Client: A Sandbox for Portable, Untrusted x86 Native Code

  2009cited by this paper
• Formal verification of a realistic compiler

  2009cited by this paper
• Control-flow integrity principles, implementations, and applications

  2009cited by this paper
• Flexible Hardware Acceleration for Instruction-Grain Program Monitoring

  2008cited by this paper
• FlexiTaint: A programmable accelerator for dynamic taint propagation

  2008cited by this paper
• Engineering Heap Overflow Exploits with JavaScript

  2008cited by this paper
• Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

  2008cited by this paper
• Effective memory protection using dynamic tainting

  2007cited by this paper
• TIARA: Trust Management, Intrusion-tolerance, Accountability, and Reconstitution Architecture

  2007cited by this paper
• Raksha: a flexible information flow architecture for software security

  2007cited by this paper
• Computability classes for enforcement mechanisms

  2006cited by this paper
• XFI: software guards for system address spaces

  2006cited by this paper
• SPEC CPU2006 benchmark descriptions

  2006cited by this paper
• Architectural support for software-based protection

  2006cited by this paper
• CCured: type-safe retrofitting of legacy software

  2005cited by this paper
• Defeating memory corruption attacks via pointer taintedness detection

  2005cited by this paper
• Edit automata: enforcement mechanisms for run-time security policies

  2005cited by this paper
• Secure program execution via dynamic information flow tracking

  2004cited by this paper
• Minos: Control Data Attack Prevention Orthogonal to Memory Model

  2004cited by this paper
• A bisimulation for dynamic sealing

  2004cited by this paper
• Beyond stack smashing: recent advances in exploiting buffer overruns

  2004cited by this paper
• A Minimal Trusted Computing Base for Dynamically Ensuring Secure Information Flow

  2001cited by this paper
• Enforceable security policies

  2000cited by this paper
• IRM enforcement of Java stack inspection

  2000cited by this paper
• QuickCheck: a lightweight tool for random testing of Haskell programs

  2000cited by this paper
• SASI enforcement of security policies: a retrospective

  1999cited by this paper
• Efficient software-based fault isolation

  1994cited by this paper
• LOCK trek: navigating uncharted space

  1989cited by this paper
• Protection in programming languages

  1973influential reference
• Protection in Programming

  1973cited by this paper
• Computer Security Technology Planning Study

  1972cited by this paper
• Formal verification of a C-like memory model and its uses for verifying program transformations

  year unknowncited by this paper

• ARM MTE Performance in Practice (Extended Version)

  2026cites this paper
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs

  2024cites this paper
• Flexible Runtime Security Enforcement with Tagged C

  2023cites this paper
• Control Flow and Pointer Integrity Enforcement in a Secure Tagged Architecture

  2023cites this paper
• Hardware-assisted mechanisms to enforce control flow integrity: A comprehensive survey

  2022cites this paper
• MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

  2022cites this paper
• Survey of Approaches and Techniques for Security Verification of Computer Systems

  2022cites this paper
• TAG: Tagged Architecture Guide

  2022influential citation
• Survey of Approaches for Security Verification of Hardware/Software Systems

  2022cites this paper
• Cross-Language Attacks

  2022cites this paper
• Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities

  2022cites this paper
• SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine

  2022influential citation
• A Security Analysis of Labeling-Based Control-Flow Integrity Schemes

  2022cites this paper
• On the Monitorability of Session Types, in Theory and Practice (Extended Version)

  2021cites this paper
• When Good Components Go Bad: Formally Secure When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise Compilation Despite Dynamic Compromise

  2021influential citation
• Keeping Safe Rust Safe with Galeed

  2021cites this paper
• SCALPEL: Exploring the Limits of Tag-enforced Compartmentalization

  2021cites this paper
• Formalizing Stack Safety as a Security Property

  2021cites this paper
• SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation

  2021influential citation
• A Survey on RISC-V Security: Hardware and Architecture

  2021cites this paper
• Security Properties for Stack Safety

  2021cites this paper
• Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process

  2020cites this paper
• Language-Based Web Session Integrity

  2020cites this paper
• LIO*: Low Level Information Flow Control in F

  2020cites this paper
• BoundWarden: Thread-enforced spatial memory safety through compile-time transformations

  2020cites this paper
• Towards formally verified compilation of tag-based policy enforcement

  2020cites this paper
• StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities

  2019cites this paper
• Beyond Labels: Permissiveness for Dynamic Information Flow Enforcement

  2019cites this paper
• The Quest for Formally Secure Compartmentalizing Compilation

  2019influential citation
• Memory Safety Preservation for WebAssembly

  2019cites this paper
• The high-level benefits of low-level sandboxing

  2019cites this paper
• A Brief Tour of Formally Secure Compilation

  2019cites this paper
• Linear capabilities for fully abstract compilation of separation-logic-verified code

  2019cites this paper
• When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

  2018influential citation
• Exploring Robust Property Preservation for Secure Compilation

  2018cites this paper
• GARUDA: Designing Energy-Efficient Hardware Monitors From High-Level Policies for Secure Information Flow

  2018cites this paper
• Intel MPX Explained

  2018cites this paper
• Protecting the Stack with Metadata Policies and Tagged Hardware

  2018cites this paper
• Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation

  2018cites this paper
• Software Fault Isolation for Robust Compilation

  2018cites this paper
• Principles of Secure Processor Architecture Design

  2018cites this paper
• A small and adaptive coprocessor for information flow tracking in ARM SoCs

  2018cites this paper
• The Dover inherently secure processor

  2017cites this paper
• A Methodology For Micro-Policies

  2017influential citation
• SAFETY ON UNTRUSTED NETWORK DEVICES (SOUND)

  2017cites this paper
• Formally Secure Compilation

  2017cites this paper
• Formally Secure Compilation

  2017cites this paper
• Formally Secure Compilation

  2017cites this paper
• Formally Secure Compilation Last updated : September 1 , 2017 General Information

  2017influential citation
• Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)

  2017cites this paper
• Formally Secure Compilation Last updated : January 3 , 2017 General Information

  2017cites this paper
• The Meaning of Memory Safety

  2017influential citation
• A Formal Model for Capability Machines

  2016influential citation
• Poster: Towards a Fully Abstract Compiler Using Micro-Policies

  2016cites this paper
• Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation

  2016influential citation
• Survey of Approaches for Security Verification of Hardware/Software Systems

  2016cites this paper
• Micro-policies for Web Session Security

  2016cites this paper
• Beyond Good and Evil: Formalizing the Security Guarantees of Low-Level Compartmentalization

  2016influential citation
• Semantically Aware Foundation Environment (SAFE) for Clean-Slate Design of Resilient, Adaptive Secure Hosts (CRASH)

  2016cites this paper
• P-TAXI : enforcing memory safety with programmable tagged architecture

  2016cites this paper
• Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization

  2016cites this paper
• Secure Compilation Using Micro-Policies ( Extended Abstract )

  2015cites this paper
• A verified information-flow architecture

  2014cites this paper
• Testing noninterference, quickly

  2013cites this paper
• Internship Topics on SECOMP: Formally Secure Compilation of Compartmentalized C Programs

  year unknowncites this paper
• Draft Alpha is for Address ! The Essence of Memory Safety

  year unknowncites this paper