On formalism in specifications Bertrand Meyer, IEEE Software 1985 Following yesterday’s paper that used formal specification methods to resolve ambiguities and uncover potential vulnerabilities in OAuth 2.0, today’s choice is a 1980’s classic from Bertrand Meyer on the merits of formal specification and what it adds beyond natural language descriptions. With thanks once more to … Continue reading On formalism in specifications
Tag: Formal methods
Use of formal methods for constructing and verifying software.
A comprehensive formal security analysis of OAuth 2.0
A comprehensive formal security analysis of OAuth 2.0 Fett et al. CCS '16 Formal methods may not be appropriate in all cases, but there are some places where the rigour they introduce can be a really good idea. Security is one of those places. In today's paper from CCS '16 Fett et al. create a … Continue reading A comprehensive formal security analysis of OAuth 2.0
Using Crash Hoare Logic for Certifying the FSCQ File System
Using Crash Hoare Logic for Certifying the FSCQ File System - Chen et. al 2015 If you found yesterday's look at POSIX file system semantics and the crash recovery of applications built on top a little sobering, then today's paper offers a glimpse of a light at the end of the tunnel. Chen et al. … Continue reading Using Crash Hoare Logic for Certifying the FSCQ File System
Chapar: Certified Causally Consistent Distributed Key-Value Stores
Chapar: Certified Causally Consistent Distributed Key-Value Stores - Lesani et al. 2016 Another POPL '16 paper today. The Chapar framework provides for modular verification of causal consistency for both causally consistent key-value store implementations and for client programs written to use them. §1 also wins the prize for best use of emojis in a research … Continue reading Chapar: Certified Causally Consistent Distributed Key-Value Stores
Moving Fast with Software Verification
Moving Fast with Software Verification - Calcagno et al. 2015 This is a story of transporting ideas from recent theoretical research in reasoning about programs into the fast-moving engineering culture of Facebook. The context is that most of the authors landed at Facebook in September of 2013, when we brought the INFER static analyser with … Continue reading Moving Fast with Software Verification
IronFleet: Proving Practical Distributed Systems Correct
IronFleet: Proving Practical Distributed Systems Correct - Hawblitzel et al. (Microsoft Research) 2015 Every so often a paper comes along that makes you re-evaluate your world view. I happily would have told you that full formal verification of non-trivial systems (especially distributed systems) in a practical manner (i.e. something you could consider using for real … Continue reading IronFleet: Proving Practical Distributed Systems Correct
SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems
SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems - Leesatapornwongsa et al. 2014 This is the second of three papers we'll be looking at this week on the theme of verifying correctness of, and catching bugs in, distributed systems. Yesterday we saw the Statecall Policy Language and associated tool chain … Continue reading SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems
Combining static model checking with dynamic enforcement using the Statecall Policy Language
Combining static model checking with dynamic enforcement using the Statecall Policy Language - Madhavapeddy 2009 We know that getting distributed systems right is hard, and subtle, 'deep' bugs can lurk in both algorithms and implementations. Can we do better than informal reasoning coupled with some unit and integration tests? Evidence suggests we have to do … Continue reading Combining static model checking with dynamic enforcement using the Statecall Policy Language
How to write a 21st Century Proof
How to write a 21st Century Proof - Lamport 2012 In this paper Leslie Lamport shares what he has learned in well over 20 years of writing proofs. I am a computer scientist who was educated as a mathematician. I discovered structured proofs through my work on concurrent (multiprocess) algorithms. These algorithms can be quite … Continue reading How to write a 21st Century Proof
Use of Formal Methods at Amazon Web Services
Use of Formal Methods at Amazon Web Services - Newcombe et al 2014 Leslie Lamport recently gave a talk at the React conference on the specification language TLA. I wasn't there to hear the talk, but I was intrigued enough to dig in and find out a little more. Especially since I have some experience … Continue reading Use of Formal Methods at Amazon Web Services
the morning paper 