Privacy protection by typing in ubiquitous computing systems

•A novel privacy type system is proposed to protect the privacy of context information in ubiquitous computing systems.•The subject reduction property of the proposed type system is formally established to guarantee that a well-typed process can only reduce to well-typed processes.•The soundness of the proposed type system is also formally established to ensure that well-typed processes do not violate the privacy requirements of any context information in the system, nor give rise to run-time errors during reduction.•The pragmatics of the proposed type system is illustrated using a case study of an infostation-based mobile communication system where the identity and the location information of the sender must not be disclosed.•The simulation results of the system show that the users can communicate anonymously without the risk of revealing their location information.

Ubiquitous computing systems collect and share a great deal of information upon the users and their environment; including private or highly sensitive personal information. Unless users are confident enough that their privacy is protected, many will be deterred from using such systems. This paper proposes a privacy type system that controls the behaviour of concurrent, context-aware and mobile processes to ensure that private information is not accidentally disclosed. We prove the subject reduction property and the soundness of the proposed type system; which guarantee that a well-typed process cannot accidentally disclose private information. We demonstrate the pragmatics of our approach with a case study.