论文标题
与FLAQR安全应用共识和复制
Applying consensus and replication securely with FLAQR
论文作者
论文摘要
可用性对于分布式系统的安全至关重要，但是保证可用性很难，尤其是当系统的参与者可能恶意采取行动时。法定人数复制协议提供了完整性和可用性：在多个独立主机上复制数据和计算，这些主机的法定人数必须同意应用于数据的所有操作的输出。不幸的是，这些协议的开销很高，很难为特定应用程序的需求进行校准。理想情况下，开发人员可以使用高级抽象来共识和复制来编写容忍度的代码，这是通过构造确保的。本文介绍了Quorum Replication（FLAQR）的流量限制授权，这是一种核心计算，用于构建具有异质法定重复协议的分布式应用程序，同时执行端到端信息安全性。我们的类型系统可确保以违反其类型级规格的方式来确保良好的flaqr程序无法_fail_（经历无法恢复的错误）。我们提出了非干预定理，这些定理表征了FLAQR在存在，复制和失败的存在下的机密性，完整性和可用性，以及在有限数量下的多数Quorum协议类别的LIVISE定理。
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.
