Conference item icon

Conference item

A formal CHERI-C semantics for verification

Abstract:

CHERI-C extends the C programming language by adding hardware capabilities, ensuring a certain degree of memory safety while remaining efficient. Capabilities can also be employed for higher-level security measures, such as software compartmentalization, that have to be used correctly to achieve the desired security guarantees. As the extension changes the semantics of C, new theories and tooling are required to reason about CHERI-C code and verify correctness. In this work, we present a form...

Expand abstract
Publication status:
Accepted
Peer review status:
Peer reviewed

Actions


Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Balliol College
Role:
Author
ORCID:
0000-0002-2462-2782
Publisher:
Springer Publisher's website
Series:
Lecture Notes in Computer Science
Acceptance date:
2022-12-23
Event title:
29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Event location:
Paris, France
Event website:
https://etaps.org/2023/tacas
Event start date:
2023-04-22
Event end date:
2023-04-27
Language:
English
Keywords:
Pubs id:
1324727
Local pid:
pubs:1324727
Deposit date:
2023-01-21

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP