Constructing independently verifiable privacy-compliant type systems for message passing between black-box components

DOI10.1007/978-3-030-03592-1_11zbMATH Open1403.68038arXiv1901.10892OpenAlexW2886280752MaRDI QIDQ1629964FDOQ1629964

Authors: Robin Adams, S. Schupp 

Publication date: 7 December 2018

Abstract: Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.

Full work available at URL: https://arxiv.org/abs/1901.10892

Recommendations

• Privacy by typing in the \(\pi\)-calculus
• Type checking privacy policies in the \(\pi\)-calculus
• Formal verification of differential privacy for interactive systems (extended abstract)
• Defining privacy is supposed to be easy
• Differential Privacy and Security

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Preserving Secrecy Under Refinement
• Datacentric semantics for verification of privacy policy compliance by mobile applications

Cited In (7)

• Privacy by typing in the \(\pi\)-calculus
• Datacentric semantics for verification of privacy policy compliance by mobile applications
• Diagrammatically Formalising Constraints of a Privacy Ontology
• Type checking privacy policies in the \(\pi\)-calculus
• Static checking of GDPR-related privacy compliance for object-oriented distributed systems
• A universally composable framework for the privacy of email ecosystems
• Purpose-based policy enforcement in actor-based systems

This page was built for publication: Constructing independently verifiable privacy-compliant type systems for message passing between black-box components

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1629964)