CAPVerDE


Computer-Aided Privacy Verification and Design Engineering Tool

CAPVerDE is a work-in-progress project that is an Integrated Tool Environment for Privacy Verification in Software Architectures.

Violations of the privacy of users can happen if data protection is not a fundamental part of the development process of a software system. The principle of Privacy by Design (PbD) therefore stipulates the consideration of privacy as a default feature.

We have developed an integrated tool environment called CAPVerDE that provides a formal description language of software architectures and helps a designer by automatically verifying statements about the storage and origin of personal data at the architectural level.

CAPVerDE allows the designer to specify privacy properties in a formal description language and transforms them into SMT statements.

 

Versions

1.0 (rejected FM paper)
Basic version that supports properties related to the access, knowledge, storage, and sharing of data.
Executables / Code

1.05 (PST paper)
Refined version that supports probabilistic properties regarding access and knowledge.
Executables / Code

1.15 (IFIPSEC paper)
Extended version that supports purpose limitation properties.
Executables / Code

Full Architecture of the Medical Register


Model of the real-life medical data case study, as mentioned in IFIP Sec 2019 paper "Automatically Proving Purpose Limitation in Software Architectures".

1.16 (CPDP paper)
Extended version that supports performing a (GDPR-compliant) Data Protection Impact Assessment.
Executables / Code

Please read the documentation included in the ZIP file for correct installation.

 

System Requirements

Windows 10 64 bit SP1:

  • Oracle Java SE min. V9
  • Visual c++ 2013 redistributable for visual studio 2013 (for MathSAT)
  • MatSAT 5 SMT Solver windows 64-bit x86 min. V5.5.2 www.mathsat.fbk.eu


Linux/Ubuntu min. V17

  • Oracle Java SE min. V9
  • MatSAT 5 SMT Solver Linux 64-bit x86 min. V5.5.2 www.mathsat.fbk.eu



Mac OS 10.13.6 High Sierra

  • Oracle Java SE min. V9
  • MatSAT 5 SMT Solver Linux 64-bit x86 min. V5.5.2 www.mathsat.fbk.eu


Known bugs:
Glib/GTK critical messages during linux startup