ERD

Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Cornucopia: Temporal Safety for CHERI Heaps

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Islaris: Verification of Machine Code Against Authoritative ISA Semantics

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Two Mechanisations of WebAssembly 1.0

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Verified security for the Morello capability-enhanced prototype Arm architecture

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

VIP: Verifying Real-World C Idioms with Integer-Pointer Casts

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

CheriABI - Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Repairing and mechanising the JavaScript relaxed memory model

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Exploring C semantics and pointer provenance

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

N3005: A Provenance-aware Memory Object Model for C. Working Draft Technical Specification ISO/IEC TS 6010:2023 (E)

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

N2577: A Provenance-aware Memory Object Model for C. ISO/IEC JTC1/SC22/WG14 N2577

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

The Cerberus C semantics

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Periodic Reporting for period 3 - ELVER (Engineering with Logic and Verification: Mathematically Rigorous Engineering fo...

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Technical Report UCAM-CL...

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Technical Report UCAM-CL...

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

RefinedC: automating the foundational verification of C code with refined ownership types

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Isla: Integrating Full-Scale {ISA} Semantics and Axiomatic Concurrency Models

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

CN: Verifying systems C code with separation-logic refinement types

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

CHERI C/C++ Programming Guide. Technical Report UCAM-CL-TR-947

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

An Introduction to CHERI. Technical Report UCAM-CL-TR-941

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Relaxed virtual memory in Armv8-A

Project: ELVER

Updated at: 27-04-2024

Show more information

Project acronym ELVER

Resources

Selected filters:

Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS

Cornucopia: Temporal Safety for CHERI Heaps

Islaris: Verification of Machine Code Against Authoritative ISA Semantics

Two Mechanisations of WebAssembly 1.0

Verified security for the Morello capability-enhanced prototype Arm architecture

VIP: Verifying Real-World C Idioms with Integer-Pointer Casts

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

CheriABI - Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment

Repairing and mechanising the JavaScript relaxed memory model

Exploring C semantics and pointer provenance

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture

N3005: A Provenance-aware Memory Object Model for C. Working Draft Technical Specification ISO/IEC TS 6010:2023 (E)

N2577: A Provenance-aware Memory Object Model for C. ISO/IEC JTC1/SC22/WG14 N2577

The Cerberus C semantics

Periodic Reporting for period 3 - ELVER (Engineering with Logic and Verification: Mathematically Rigorous Engineering fo...

Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Technical Report UCAM-CL...

Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Technical Report UCAM-CL...

RefinedC: automating the foundational verification of C code with refined ownership types

Isla: Integrating Full-Scale {ISA} Semantics and Axiomatic Concurrency Models

CN: Verifying systems C code with separation-logic refinement types

CHERI C/C++ Programming Guide. Technical Report UCAM-CL-TR-947

An Introduction to CHERI. Technical Report UCAM-CL-TR-941

Relaxed virtual memory in Armv8-A