Algebraic Replicated Data Types: Programming Secure Local-First Software
This paper is about programming support for local-first applications that manage private data locally, but still synchronize data between multiple devices. Typical use cases are synchronizing settings and data, and collaboration between multiple users. Such applications must preserve the privacy and integrity of the user’s data without impeding or interrupting the user’s normal workflow – even when the device is offline or has a flaky network connection.
From the programming perspective, availability along with privacy and security concerns pose significant challenges, for which developers have to learn and use specialized solutions such as conflict-free replicated data types (CRDTs) or APIs for centralized data stores. This work relieves developers from this complexity by enabling the direct and automatic use of algebraic data types – which developers already use to express the business logic of the application – for synchronization and collaboration. Moreover, we use this approach to provide end-to-end encryption and authentication between multiple replicas (using a shared secret), that is suitable for a coordination-free setting. Overall, our approach combines all the following advantages: it (1) allows developers to design custom data types, (2) provides data privacy and integrity when using untrusted intermediaries, (3) is coordination free, (4) guarantees eventual consistency by construction (i.e., independent of developer errors), (5) does not cause indefinite growth of metadata, (6) has sufficiently efficient implementations for the local-first setting.
Wed 19 JulDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00
|Behavioural Types for Local-First Software
Roland Kuhn Actyx AG, Hernan Melgratti University of Buenos Aires, Argentina, Emilio Tuosto Gran Sasso Science Institute, L'Aquila, ItalyDOI
|Algebraic Replicated Data Types: Programming Secure Local-First Software
Christian Kuessner Technische Universität Darmstadt, Ragnar Mogk Technische Universität Darmstadt, Anna-Katharina Wickert TU Darmstadt, Germany, Mira Mezini TU DarmstadtDOI Pre-print
|Modular Verification of State-Based CRDTs in Separation Logic
Abel Nieto Aarhus University, Arnaud Daby-Seesaram ENS Paris Saclay, Léon Gondelman Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus UniversityDOI
|VeriFx: Correct Replicated Data Types for the Masses
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA University Lisbon, Elisa Gonzalez Boix Vrije Universiteit BrusselDOI
|Nested Pure Operation-Based CRDTs
|LoRe: A Programming Model for Verifiably Safe Local-First Software
Julian Haas Technische Universität Darmstadt, Ragnar Mogk Technische Universität Darmstadt, Elena Yanakieva University of Kaiserslautern-Landau, Annette Bieniusa Kaiserslautern, Mira Mezini TU DarmstadtDOI Pre-print