Back to University of Twente portal
| author: | Sophie Lathouwers |
| title: | VerCors support for SecCSL |
| keywords: | security, verification, separation logic |
| topics: | Logics and semantics |
| committee: |
Marieke Huisman
, Sophie Lathouwers |
Description
Ernst and Murray1 recently proposed SecCSL, a concurrent separation logic for proving information flow security properties.
In the FMT group we have developed the VerCors program verifier which uses concurrent separation logic to reason about the correctness of programs.
In this project, we want to investigate how we could adapt the VerCors verifier to support SecCSL.
The following steps would be necessary:
- Understand SecCSL
- Understand the VerCors architecture
- Investigate how to adapt VerCors to Support SecCSL
- Implement the necessary changes
References
[1] "SecCSL: Security Concurrent Separation Logic" by G. Ernst and T. Murray (CAV 2019) https://doi.org/10.1007/978-3-030-25543-5_13