Skip to content
☰
Discover CHERI
Why CHERI
Why CHERI
Why CHERI?
Vulnerabilities in Everyday Technology
Why Existing Defences Are Not Enough
Approaches to Memory Safety
CHERI and Rust
Understand CHERI
Understand CHERI
The History of CHERI
How does CHERI work?
Bringing CHERI to your product
CHERI and Existing Software
FAQ
Resources
Resources
Videos & Presentations
Documentation & Guides
Academic Papers
Glossary
Papers and authors
Adopt
Business Case
Business Case
The Cost of Memory Unsafety
The Strategic Case for CHERI
The Return on Security Investment
Assurance & Adoption
Assurance & Adoption
Case Studies
The CHERI Enabled Programme
CHERI Enabled Products
Policy
Policy
Public Policy and CHERI
Cybersecurity Regulation
Critical Infrastructure & Resilience
Build
Software Developers
Software Developers
Building Secure Software
Choose a Platform
Run CHERI in Simulation
Install a Toolchain
Build Your First Application
Tutorials & Training
Port Existing Software
Build Compartments
Downloads
Technical FAQ
Technology
Technology
CHERI and Rust - Technical Overview
Capabilities
Tags & Validity
Bounds
Permissions
Provenance
Sealing
Spatial Memory Safety
Temporal Memory Safety
Compartmentalisation
Hybrid Systems
Pure-Capability Systems
Platforms
Platforms
Platform Comparison
Morello
CHERIoT
Sonata
FPGA Platforms
Simulators
CHERI Products
Hardware
Return an unused Morello Board
Software Ecosystem
Software Ecosystem
Software Ecosystem
LLVM & Clang
Rust
CheriBSD
CHERI Linux
Zephyr
Debugging Tools
All software
CHERI Alliance
About & Governance
About & Governance
About the CHERI Alliance
Mission & Role
Collaboration Principles
Accelerating CHERI together
CHERI Trademark
Leadership
Leadership
Members
Governing Board
Working Groups
Ambassadors
Membership
Membership
Why Join?
Membership Benefits & Options
Contact the Alliance
Legal & Policies
Legal & Policies
Code of Conduct
Competition Law Statement
Intellectual Property Policy
Trademark Policy
Export Controls
Privacy
News & Events
News & Analysis
News & Analysis
Latest News
Subscribe to our Newsletter
Press Resources
Events & Archive
Events & Archive
Upcoming Events
Past Events
CHERI Blossoms Conference
CHERITech Conference
People & Opportunities
People & Opportunities
Speakers
Alliance Members
Contact the Alliance
News and events
People
Ricardo Almeida
Ricardo Almeida
Publications
Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour
Image preview
Close
×
