The WeSP Project - Formal Methods


The WeSP project addresses security, privacy and trust in the context of web and location-based services. It focuses on building tools to enable users to effectively control their privacy, and using formal methods to validate policy languages developed in the context of online social networking.

Our efforts on the use of formal methods techniques and tools for social-networking can be situated on several axis. We have written Matelas, a predicate calculus model for social-networking that allows for social-network content, privacy policies in social networks, and social-network friendship relations. We used the B tool AtelierB to write Matelas, and work is on the way to refine Matelas to a C code library. Matelas was presented in the ABZ formal methods in Canada 2010. You can reach our paper here, written by Néstor Cataño and Camilo Rueda.

We are also working in the definition of Poporo, a Proof Carrying Code (PCC) based framework in which Matelas C library functionalities can be extended. A Human Computer Interaction (HCI) based paper describing Poporo can be reached here. The paper was written by Nestor Catano, Vassilis Kostakos, and Ian Oakley. A formal methods document presenting Poporo can be found here. The work envisioned in this document is currently led by Néstor Cataño and Sorren Hanvey.

C libraries extensions are to be programmed in Java. We are using The Java Modeling Language (JML) to verify that Java extensions comply with Matelas. Hence, Tim Wahls at Dickinson College, Néstor Cataño, and Camilo Rueda are working on a translation from B to JML. For historical reasons, we call this translation “The Baker’s Recipe to translate B machines into JML”. A paper describing the recipe and its implementation in the ABTools has been submitted to TAP 2011 in Zurich.