< Retour au sommaire
Model Specification Language for Formal Verification of Consent Properties on Models and Code
Myriam Clouet le
Lieu: salle 1073, bât 862
Abstract
Recent privacy laws and regulations raise the stakes in verifying
that a software system respects user consent. Even if the current
state of the art shows that privacy by design and formal methods
can help, ensuring the validity of privacy properties, in particular
consent properties, at different stages of software development, is
still hard. This paper proposes a step forward for solving this issue
by introducing a new tool, named CASTT, that allows 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 model specification language
named CSpeL, which allows to specify the key elements involved in
consent and the relationships between them. We evaluate our tool
on two use cases targeting different application domains (healthcare
and website).
Download slides