Ensuring Privacy in Presence Awareness Systems: An Automated Verification Approach

Providing information about other users and their activities is a central function of many collaborative applications. The data that provide this "presence awareness" are usually automatically generated and highly dynamic. For example, services such as AOL Instant Messenger allow users to observe the status of one another and to initiate and participate in chat sessions. As such services become more powerful, privacy and security issues regarding access to sensitive user data become critical. Two key software engineering challenges arise in this context: 1) Policies regarding access to data in collaborative applications have subtle complexities, and must be easily modifiable during a collaboration; 2) Users must be able to have a high degree of confidence that the implementations of these policies are correct. In this paper, we propose a framework that uses an automated verification approach to ensure that such systems conform to complex policies. Our approach takes advantage of VeriSoft, a recent tool or systematically testing implementations of concurrent systems, and is applicable to a wide variety of specification and development platforms for collaborative applications. We illustrate the key features of our framework by applying it to the development of a presence awareness system, and describe some important and subtle errors that were found using our approach.