On formalism in specifications

November 8, 2016November 11, 2019 ~ Adrian Colyer ~ 4 Comments

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

A comprehensive formal security analysis of OAuth 2.0

November 7, 2016November 11, 2019 ~ Adrian Colyer ~ 2 Comments

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

Using Crash Hoare Logic for Certifying the FSCQ File System

February 12, 2016 ~ Adrian Colyer ~ 2 Comments

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

Chapar: Certified Causally Consistent Distributed Key-Value Stores

February 8, 2016 ~ Adrian Colyer ~ 1 Comment

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

Moving Fast with Software Verification

November 20, 2015 ~ Adrian Colyer ~ 3 Comments

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

IronFleet: Proving Practical Distributed Systems Correct

October 15, 2015 ~ Adrian Colyer ~ 10 Comments

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

SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems

March 25, 2015 ~ Adrian Colyer ~ 6 Comments

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

Combining static model checking with dynamic enforcement using the Statecall Policy Language

March 23, 2015 ~ Adrian Colyer ~ 2 Comments

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

How to write a 21st Century Proof

January 12, 2015 ~ Adrian Colyer ~ 5 Comments

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

Use of Formal Methods at Amazon Web Services

November 24, 2014 ~ Adrian Colyer ~ 18 Comments

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

the morning paper

a random walk through Computer Science research, by Adrian Colyer
Made delightfully fast by strattic

Formal methods