HAMRAZ: Resilient Partitioning and Replication
HAMRAZ: Resilient Partitioning and Replication
复制标题
DOI：
10.1109/sp46214.2022.9833661
复制
发表时间：
2022-05
期刊：
影响因子：
--
通讯作者：
Xiao Li;F. Houshmand;M. Lesani
中科院分区：
文献类型：
--
作者：
Xiao Li;F. Houshmand;M. Lesani
具有部分信任的子系统需要合作的组织间系统在医疗保健、金融和军事领域很常见。面对恶意拜占庭攻击，最终目标是确保端到端策略的可信性的三个方面：机密性、完整性和可用性。与机密性和完整性相比，可用性的提供和验证常常被回避。本文同时保证了可信度的所有三个方面的端到端策略。它提出了一种安全类型的基于对象的语言、分区转换、操作语义以及用于分区和复制类的信息流类型推理系统。类型系统可证明保证类型良好的方法在这三个属性上不受干扰，并且它们的类型增强了对拜占庭攻击的弹性。给定一个类及其端到端策略的规范，HAMRAZ 工具应用类型推断来自动在拜占庭仲裁系统上放置和复制该类的字段和方法，并综合构建可信的分布式系统。实验显示了所得系统的弹性；他们可以优雅地容忍与指定策略一样强大的攻击。
Inter-organizational systems where subsystems with partial trust need to cooperate are common in healthcare, finance and military. In the face of malicious Byzantine attacks, the ultimate goal is to assure end-to-end policies for the three aspects of trustworthiness: confidentiality, integrity and availability. In contrast to confidentiality and integrity, provision and validation of availability has been often sidestepped. This paper guarantees end-to-end policies simultaneously for all the three aspects of trustworthiness. It presents a security-typed object-based language, a partitioning transformation, an operational semantics, and an information flow type inference system for partitioned and replicated classes. The type system provably guarantees that well-typed methods enjoy noninterference for the three properties, and that their types quantity their resilience to Byzantine attacks. Given a class and the specification of its end-to-end policies, the HAMRAZ tool applies type inference to automatically place and replicate the fields and methods of the class on Byzantine quorum systems, and synthesize trustworthy-by-construction distributed systems. The experiments show the resiliency of the resulting systems; they can gracefully tolerate attacks that are as strong as the specified policies.