skip to main content

This content will become publicly available on October 13, 2024

Title: Flow-limited authorization for consensus, replication, and secret sharing

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 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. Additionally, we present an extension to FLAQR that supports secret sharing as a form of declassification and prove it preserves integrity and availability security properties.

more » « less
Award ID(s):
Author(s) / Creator(s):
; ;
Calzavara, Stefano; Naumann, David
Publisher / Repository:
Journal of Computer Security
Date Published:
Journal Name:
Journal of Computer Security
Page Range / eLocation ID:
615 to 645
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. 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 quantify 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. 
    more » « less
  2. Data centers are increasingly equipped with RDMAs. These network interfaces mark the advent of a new distributed system model where a node can directly access the remote memory of another. They have enabled microsecond-scale replicated services. The underlying replication protocols of these systems execute all operations under strong consistency. However, strong consistency can hinder response time and availability, and recent replication models have turned to a hybrid of strong and relaxed consistency. This paper presents RDMA replicated data types, the first hybrid replicated data types for the RDMA network model. It presents a novel operational semantics for these types that considers three distinct categories of methods and captures their re- quired coordination, and formally proves that they preserve convergence and integrity. It implements these semantics in a system called Hamband that leverages direct remote accesses to efficiently implement the required coordination protocols. The empirical evaluation shows that Hamband outperforms the throughput of existing message-based and SMR-based implementations by more than 4x. 
    more » « less
  3. P4 (Programming Protocol-Independent Packet Processors) represents a paradigm shift in network programmability by providing a high-level language to define packet processing behavior in network switches/devices. The importance of P4 lies in its ability to overcome the limitations of OpenFlow, the previous de facto standard for software-defined networking (SDN). Unlike OpenFlow, which operates on fixed match-action tables, P4 offers an approach where network operators can define packet processing behaviors at various protocol layers. P4 provides a programmable platform to create and implement custom network switches/devices protocols. However, this opens a new attack surface for threat actors who can access P4-enabled switches/devices and manipulate custom protocols for malicious purposes. Attackers can craft malicious packets to exploit protocol-specific vulnerabilities in these network devices. This ongoing research work proposes a blockchain-based model to secure P4 custom protocols. The model leverages the blockchain’s immutability, tamperproof ability, distributed consensus for protocol governance, and auditing to guarantee the transparency, security, and integrity of custom protocols defined in P4 programmable switches. The protocols are recorded as transactions and stored on the blockchain network. The model's performance will be evaluated using execution time in overhead computation, false positive rate, and network scalability. 
    more » « less
  4. Oshman, Rotem (Ed.)
    Byzantine quorum systems provide higher throughput than proof-of-work and incur modest energy consumption. Further, their modern incarnations incorporate personalized and heterogeneous trust. Thus, they are emerging as an appealing candidate for global financial infrastructure. However, since their quorums are not uniform across processes anymore, the properties that they should maintain to support abstractions such as reliable broadcast and consensus are not well-understood. It has been shown that the two properties quorum intersection and availability are necessary. In this paper, we prove that they are not sufficient. We then define the notion of quorum subsumption, and show that the three conditions together are sufficient: we present reliable broadcast and consensus protocols, and prove their correctness for quorum systems that provide the three properties. 
    more » « less
  5. null (Ed.)
    Members of the Rhizobiaceae , often carry multiple secondary replicons in addition to the primary chromosome with compatible repABC -based replication systems. Unlike secondary chromosomes and chromids, repABC -based megaplasmids and plasmids can undergo copy number fluctuations and are capable of conjugative transfer in response to environmental signals. Several Agrobacterium tumefaciens lineages harbor three secondary repABC -based replicons, including a secondary chromosome (often linear), the Ti (tumor-inducing) plasmid and the At megaplasmid. The Ti plasmid is required for virulence and encodes a conjugative transfer ( tra ) system that is strictly regulated by a subset of plant-tumor released opines and a well-described acyl-homoserine lactone (AHL)-based quorum-sensing mechanism. The At plasmids are generally not required for virulence, but carry genes that enhance rhizosphere survival, and these plasmids are often conjugatively proficient. We report that the At megaplasmid of the octopine-type strain A. tumefaciens 15955 encodes a quorum-controlled conjugation system that directly interacts with the paralogous quorum sensing system on the co-resident Ti plasmid. Both the pAt15955 and pTi15955 plasmids carry homologs of a TraI-type AHL synthase, a TraR-type AHL-responsive transcription activator, and a TraM-type anti-activator. The traI genes from both pTi15955 and pAt15955 can direct production of the inducing AHL (3-octanoyl- L -homoserine lactone) and together contribute to the overall AHL pool. The TraR protein encoded on each plasmid activates AHL-responsive transcription of target tra gene promoters. The pAt15955 TraR can cross-activate tra genes on the Ti plasmid as strongly as its cognate tra genes, whereas the pTi15955 TraR is preferentially biased toward its own tra genes. Putative tra box elements are located upstream of target promoters, and comparing between plasmids, they are in similar locations and share an inverted repeat structure, but have distinct consensus sequences. The two AHL quorum sensing systems have a combinatorial effect on conjugative transfer of both plasmids. Overall, the interactions described here have implications for the horizontal transfer and evolutionary stability of both plasmids and, in a broad sense, are consistent with other repABC systems that often have multiple quorum-sensing controlled secondary replicons. 
    more » « less