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
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
▼
How CHERI Capabilities work
Spatial Memory Safety
Temporal Memory Safety
Compartmentalisation
Hybrid Systems
Pure-Capability Systems
CHERI and Rust - Technical Overview
Platforms
Platforms
▼
CHERI Products
Morello
Return an unused Morello Board
CHERIoT
Sonata
FPGA Platforms
Simulators
Software Ecosystem
Software Ecosystem
▼
Software Ecosystem
LLVM & Clang
Rust
CheriBSD
CHERI Linux
CHERI Zephyr
Debugging Tools
All repositories
CHERI Alliance
▼
About & Governance
About & Governance
▼
About the CHERI Alliance
Mission & Role
Collaboration Principles
Accelerating CHERI together
CHERI Trademark
Leadership
Leadership
▼
The vision behind the Alliance
Governing Board
Working Groups
Ambassadors
Membership
Membership
▼
CHERI Alliance Members
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
About CHERI Blossoms Conferences
About CHERITech Conferences
People & Opportunities
People & Opportunities
▼
Speakers
CHERI Alliance Members
Contact the Alliance
Contact Us
Home
News and events
People
Ian Stark
Ian Stark
Publications
Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour
Rigorous Engineering for Hardware Security: Formal Modelling and Proof in the CHERI Design and Implementation Process
Image preview
Close
×
