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.