Availability is crucial to the security of distributed systems, but guaranteeing availability is hard, especially when participants in the system may act maliciously. Quorum replication protocols provide both integrity and availability: data and computation is replicated at multiple independent hosts, and a quorum of these hosts must agree on the output of all operations applied to the data. Unfortunately, these protocols have high overhead and can be difficult to calibrate for a specific application's needs. Ideally, developers could use high-level abstractions for consensus and replication to write fault-tolerant code by that is secure by construction. This paper presents Flow-Limited Authorization for Quorum Replication (FLAQR), a core calculus for building distributed applications with heterogeneous quorum replication protocols while enforcing end-to-end information security. Our type system ensures that well-typed FLAQR programs cannot_fail_ (experience an unrecoverable error) in ways that violate their type-level specifications. We present noninterference theorems that characterize FLAQR's confidentiality, integrity, and availability in the presence of consensus, replication, and failures, as well as a liveness theorem for the class of majority quorum protocols under a bounded number of faults.
翻译:对分布式系统的安全至关重要,但保证可用性非常困难,特别是当系统参与者可能恶意地采取行动时。 法定人数复制协议提供完整性和可用性:数据和计算在多个独立主机复制,数据和计算在多个独立主机复制,这些主机的法定人数必须就数据应用的所有操作的产出达成一致。 不幸的是,这些协议有很高的间接费用,并且可能难以根据特定应用程序的需要校准。 理想的情况是,开发者可以使用高层次的抽象来达成共识和复制,从而以建筑安全的方式写出防故障代码。 本文展示了对免责复制( FLAQR) 的保密性、 完整性和可获取性的有限授权( FLAQR), 这是用于在实行端到端的信息安全的同时, 以不同法定人数复制协议的方式构建分布式应用程序的核心计算。 我们的系统确保, 完善型的 FLAQR 程序无法以违反其类型规格的方式( 经历无法弥补的错误) 。 我们展示了FLQR 的保密性、 完整性和可用性在存在共识、 复制和故障中具有多数性协议约束的缺陷。