Formal Modelling of Resilient Data Storage in Cloud

Reliable and highly performant handling of large data stores constitutes one of the major challenges of cloud computing. In this paper, we propose a formalisation of a cloud solution implemented by F-Secure - a provider of secure data storage services. The solution is based on massive replication and the write-ahead logging mechanism. To achieve high performance, the company has abandoned a transactional model. We formally derive a model of the proposed architectural solution and verify data integrity and consistency properties under possible failure scenarios. The proposed approach allows the designers to formally define and verify essential characteristics of architectures for handling large data stores.