-
Applying consensus and replication securely with FLAQR
Authors:
Priyanka Mondal,
Maximilian Algehed,
Owen Arden
Abstract:
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. Unfor…
▽ More
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.
△ Less
Submitted 9 May, 2022;
originally announced May 2022.
-
Multi-Execution Lattices Fast and Slow
Authors:
Maximilian Algehed,
Cormac Flanagan
Abstract:
Methods for automatically, soundly, and precisely guaranteeing the noninterference security policy are predominantly based on multi-execution. All other methods are either based on undecidable theorem proving or suffer from false alarms. The multi-execution mechanisms, meanwhile, work by isolating security levels during program execution and running multiple copies of the target program, once for…
▽ More
Methods for automatically, soundly, and precisely guaranteeing the noninterference security policy are predominantly based on multi-execution. All other methods are either based on undecidable theorem proving or suffer from false alarms. The multi-execution mechanisms, meanwhile, work by isolating security levels during program execution and running multiple copies of the target program, once for each security level with carefully tailored inputs that ensure both soundness and precision. When security levels are hierarchically organised in a lattice, this may lead to an exponential number of executions of the target program as the number of possible ways of combining security levels grows. In this paper we study how the lattice structure for security levels influences the runtime overhead of multi-execution. We additionally show how to use Galois connections to gain speedups in multi-execution by switching from lattices with high overhead to lattices with low overhead. Additionally, we give an empirical evaluation that corroborates our analysis and shows how Galois connections have potential to speed up multi-execution.
△ Less
Submitted 25 March, 2021;
originally announced March 2021.
-
Transparent IFC Enforcement: Possibility and (In)Efficiency Results
Authors:
Maximilian Algehed,
Cormac Flanagan
Abstract:
Information Flow Control (IFC) is a collection of techniques for ensuring a no-write-down no-read-up style security policy known as noninterference. Traditional methods for both static and dynamic IFC suffer from untenable numbers of false alarms on real-world programs. Secure Multi-Execution (SME) promises to provide secure IFC without modifying the behaviour of already secure programs, a propert…
▽ More
Information Flow Control (IFC) is a collection of techniques for ensuring a no-write-down no-read-up style security policy known as noninterference. Traditional methods for both static and dynamic IFC suffer from untenable numbers of false alarms on real-world programs. Secure Multi-Execution (SME) promises to provide secure IFC without modifying the behaviour of already secure programs, a property known as transparency. Implementations of SME exist for the web and as plug-ins to several programming languages. Furthermore, SME can in theory work in a black-box manner, meaning that it can be programming language agnostic, making it perfect for securing legacy or third-party systems. As such SME, and its variants like Multiple Facets (MF) and Faceted Secure Multi-Execution (FSME), appear to be a family of panaceas for the security engineer. The question is, how come, given all these advantages, that these techniques are not ubiquitous in practice? The answer lies, partially, in the issue of runtime and memory overhead. SME and its variants are prohibitively expensive to deploy in many non-trivial situations. Why is this the case? On the surface, the reason is simple. The techniques in the SME family all rely on the idea of multi-execution, running all or parts of a program multiple times to achieve noninterference. Naturally, this causes overhead. However, the goal in the IFC community has been to overcome these overheads. In this paper we argue that there are fundamental reasons to expect this not to be possible and prove two key theorems: 1. All transparent enforcement is polynomial time equivalent to multi-execution. 2. All black-box enforcement takes time exponential in the number of principals in the security lattice. We also answer, in the affirmative, an open question about the possibility of transparently enforcing the TINI security condition.
△ Less
Submitted 25 May, 2020;
originally announced May 2020.
-
Dynamic IFC Theorems for Free!
Authors:
Maximilian Algehed,
Jean-Philippe Bernardy,
Catalin Hritcu
Abstract:
We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of…
▽ More
We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of the libraries in terms of type abstraction.
△ Less
Submitted 22 February, 2024; v1 submitted 10 May, 2020;
originally announced May 2020.
