TY - GEN
T1 - Context Specification Language for Formally Verifying Consent Properties on Models and Code
AU - Clouet, Myriam
AU - Antignac, Thibaud
AU - Arnaud, Mathilde
AU - Signoles, Julien
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2023/1/1
Y1 - 2023/1/1
N2 - Recent privacy laws and regulations raise the stakes in verifying that software systems respect user consent. The current state of the art shows that privacy by design and formal methods can help. Still, ensuring the validity of privacy properties, in particular consent properties, at different stages of software development, is hard. This paper proposes a step towards solving this issue by introducing a new tool, named CASTT, that allows software engineers to verify consent properties at two different development stages: system modeling and code verification. To describe the system, this paper introduces a new formal context specification language, named CSpeL, to specify the key elements involved in consent and their relationships. The tool is evaluated on two use cases targeting different application domains: healthcare and website. We also evaluate the correctness and the efficiency of our tool.
AB - Recent privacy laws and regulations raise the stakes in verifying that software systems respect user consent. The current state of the art shows that privacy by design and formal methods can help. Still, ensuring the validity of privacy properties, in particular consent properties, at different stages of software development, is hard. This paper proposes a step towards solving this issue by introducing a new tool, named CASTT, that allows software engineers to verify consent properties at two different development stages: system modeling and code verification. To describe the system, this paper introduces a new formal context specification language, named CSpeL, to specify the key elements involved in consent and their relationships. The tool is evaluated on two use cases targeting different application domains: healthcare and website. We also evaluate the correctness and the efficiency of our tool.
KW - Formal Verification
KW - Privacy
KW - Specification Language
UR - https://www.scopus.com/pages/publications/85172416216
U2 - 10.1007/978-3-031-38828-6_5
DO - 10.1007/978-3-031-38828-6_5
M3 - Conference contribution
AN - SCOPUS:85172416216
SN - 9783031388279
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 68
EP - 93
BT - Tests and Proofs - 17th International Conference, TAP 2023, Proceedings
A2 - Prevosto, Virgile
A2 - Seceleanu, Cristina
PB - Springer Science and Business Media Deutschland GmbH
T2 - Proceedings of the 17th International Conference, TAP 2023
Y2 - 18 July 2023 through 19 July 2023
ER -