Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
CoSMed: a confidentiality-verified social media platform
Bauerei&bgr; T., Pesenti Gritti A., Popescu A., Raimondi F. Journal of Automated Reasoning61 (1-4):113-139,2018.Type:Article
Date Reviewed: Aug 22 2018

What do we mean when we say that a system is verified? In theory it means that certain properties of a system have been proved to hold. In practice, the answer is rather more complicated.

The first thing to clarify is the form of proof: computer scientists have developed a variety of logics, both general and special purpose, for proofs of properties of correspondingly various kinds. The proofs themselves might be by pencil-and-paper or, increasingly, formalized in a computer in some way. Trust in the verification relies on trusting the proof assistant--this is not the place to go any further down that particular rabbit hole, but anyone interested should read MacKenzie [1] and Nipkow et al.’s paper [2] on the Isabelle proof assistant, which is a sophisticated and mature system that assists users to construct machine-checked proofs “by hand” using a battery of existing libraries and tactics.

Now that we have a sense of what will be used to perform the verification, we need to identify what will be verified. Typically (and this is the case here) we work with a model of the real system and argue that this represents the essential properties of the real thing. The authors do something subtly different: the model is a state machine, represented by its step function in the internal language of Isabelle, which is a relatively straightforward functional language. They then use the extraction facility of Isabelle to export this model to Scala, so that it is rendered directly into code that can be executed in a (real) web framework, which could in principle be verified itself, although that is not the focus of this work.

The paper, an extension of a paper published in an established conference series on interactive theorem proving, gives clear explanations of the application domain and the proof, in particular the approach to information flow that the verification uses. Essentially, the authors prove that Alice can only see posts from Bob that were made when they are friends, a property which can change dynamically. So, even if they are currently friends, posts made when they were not are not visible. Technically, this expands the authors’ earlier work on a similar “conference” system in which roles are statically rather than dynamically defined.

The paper gives a clear exposition of the model, the properties proved, and the proof techniques, and I would expect that the work could be reproduced from the descriptions given. What I missed, and what would have added greatly to the value of the paper for others, is an account of how the verification and the modeling interacted. Is it the case that the modeling entirely preceded the verification, so that the model was built correctly from the start, or was it the case that the very process of attempting to verify the system required it to be modified itself? Insights like this would be very valuable to someone embarking upon a similar exercise, and would potentially help readers overcome the considerable learning curve that there is in going from novice to experienced user of systems like this.

Nevertheless, the paper makes a definite contribution to the growing literature on verified systems, and the work in general is particularly noteworthy because it was done in conjunction with a third-sector organization to support their online social media presence.

Reviewer:  Simon Thompson Review #: CR146215 (1811-0575)
1) MacKenzie, D. Mechanizing proof: computing, risk, and trust. MIT Press, Cambridge, MA, 2001.
2) Nipkow, T.; Paulson, L. C.; Wenzel, M. Isabelle/HOL: a proof assistant for higher-order logic (LNCS 2283). Springer, Berlin, Germany, 2002.
Bookmark and Share
  Featured Reviewer  
 
Formal Methods (D.2.4 ... )
 
 
Social Networking (H.3.4 ... )
 
 
Verification (D.4.5 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy