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.
翻译:基层平台是由加密身份认证的用户在其联网个人设备上运行的分布式应用程序,多个独立的平台实例独立涌现,并在互操作时融合。其基础是基层社交图谱,基于此可构建基层社交网络、基层加密货币及基层民主联邦。基层平台尚未实现,关键挑战在于存在故障与恶意参与者:若无安全编程支持,正确的参与者无法可靠地识别彼此、建立安全通信或验证彼此的代码完整性。本文提出基层逻辑程序(GLP),一种用于实现基层平台的安全、多智能体、并发逻辑编程语言。GLP通过配对的单读者/单写者(SRSW)逻辑变量扩展了逻辑程序,通过加密、签名和认证的消息为加密身份认证的用户提供安全通信通道,从而实现身份与代码完整性验证。我们逐步阐述GLP:从逻辑程序、并发GLP、多智能体GLP,到为其增强加密安全性,并提供智能手机实现就绪的规范。我们证明了包括GLP计算为演绎推理、SRSW保持性、无环性与单调性在内的安全性性质。我们证明了多智能体GLP具有基层特性,且GLP流实现了区块链安全属性。我们提出了一种建立认证点对点连接的基层社交图谱协议,并展示了安全的基层社交网络应用。