Grassroots Logic Programs: A Secure, Multiagent, Concurrent, Logic Programming Language
Ehud Shapiro
TL;DR
Grassroots Logic Programs (GLP) offer a secure, multiagent, concurrent logic-programming language built to implement distributed grassroots platforms on cryptographically identified devices. By introducing paired single-reader/single-writer variables and attestations, GLP enables authenticated, tamper-evident communication and code integrity verification within the grassroots social graph, with proofs of safety, monotonicity, and blockchain-like security properties. The paper extends GLP to multiagent settings (maGLP), proves the approach is grassroots, and details a robust grassroots social graph protocol (cold calls, introductions) that supports secure social networking, messaging, and group communication. An implementation-ready path for smartphones (via Dart/Flutter and TEEs) is provided, along with security analyses and a discussion of related work, positioning GLP as a practical foundation for secure, decentralized grassroots platforms like social networks, currencies, and federations.
Abstract
Grassroots platforms are distributed applications run by\linebreak cryptographically-identified people on their networked personal devices, where multiple disjoint platform instances emerge independently and coalesce when they interoperate. Their foundation is the grassroots social graph, upon which grassroots social networks, grassroots cryptocurrencies, and grassroots democratic federations can be built. Grassroots platforms have yet to be implemented, the key challenge being faulty and malicious participants: without secure programming support, correct participants cannot reliably identify each other, establish secure communication, or verify each other's code integrity. We present Grassroots Logic Programs (GLP), a secure, multiagent, concurrent, logic programming language for implementing grassroots platforms. GLP extends logic programs with paired single-reader/single-writer (SRSW) logic variables, providing secure communication channels among cryptographically-identified people through encrypted, signed and attested messages, which enable identity and code integrity verification. We present GLP progressively: logic programs, concurrent GLP, multiagent GLP, augmenting it with cryptographic security, and providing smartphone implementation-ready specifications. We prove safety properties including that GLP computations are deductions, SRSW preservation, acyclicity, and monotonicity. We prove multiagent GLP is grassroots and that GLP streams achieve blockchain security properties. We present a grassroots social graph protocol establishing authenticated peer-to-peer connections and demonstrate secure grassroots social networking applications.