A formal CHERI-C semantics for verification
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...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2023
|
| _version_ | 1797109544142241792 |
|---|---|
| author | Park, SH Pai, R Melham, T |
| author_facet | Park, SH Pai, R Melham, T |
| author_sort | Park, SH |
| collection | OXFORD |
| description | 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 formal memory model that provides a memory semantics for CHERI-C programs. We present a generalised theory with rich properties suitable for verification and potentially other types of analyses. Our theory is backed by an Isabelle/HOL formalisation that also generates an OCaml executable instance of the memory model. The verified and extracted code is then used to instantiate the parametric Gillian program analysis framework, with which we can perform concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss. |
| first_indexed | 2024-03-07T07:41:43Z |
| format | Conference item |
| id | oxford-uuid:f44ba8f5-7d70-4b85-8931-9cf64591a89e |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:41:43Z |
| publishDate | 2023 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:f44ba8f5-7d70-4b85-8931-9cf64591a89e2023-04-28T11:23:46ZA formal CHERI-C semantics for verificationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f44ba8f5-7d70-4b85-8931-9cf64591a89eEnglishSymplectic ElementsSpringer2023Park, SHPai, RMelham, TCHERI-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 formal memory model that provides a memory semantics for CHERI-C programs. We present a generalised theory with rich properties suitable for verification and potentially other types of analyses. Our theory is backed by an Isabelle/HOL formalisation that also generates an OCaml executable instance of the memory model. The verified and extracted code is then used to instantiate the parametric Gillian program analysis framework, with which we can perform concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss. |
| spellingShingle | Park, SH Pai, R Melham, T A formal CHERI-C semantics for verification |
| title | A formal CHERI-C semantics for verification |
| title_full | A formal CHERI-C semantics for verification |
| title_fullStr | A formal CHERI-C semantics for verification |
| title_full_unstemmed | A formal CHERI-C semantics for verification |
| title_short | A formal CHERI-C semantics for verification |
| title_sort | formal cheri c semantics for verification |
| work_keys_str_mv | AT parksh aformalchericsemanticsforverification AT pair aformalchericsemanticsforverification AT melhamt aformalchericsemanticsforverification AT parksh formalchericsemanticsforverification AT pair formalchericsemanticsforverification AT melhamt formalchericsemanticsforverification |