Sage Journals: Discover world-class research

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. 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.

Keywords

Information flow control fault tolerant systems quorum replication language-based security distributed systems

Get full access to this article

View all access options for this article.

References

Abadi, Access control in a core calculus of dependency, in: 11th ACM SIGPLAN Int’l Conf. on Functional Programming, ACM, New York, NY, USA, 2006, pp. 263–273. doi:10.1145/1159803.1159839.

Arden,

Gollamudi,

Cecchetti,

Chong and

A.C.

Myers, A calculus for flow-limited authorization, Technical Report, 2021. doi:10.48550/ARXIV.2104.10379.

Arden,

Liu and

A.C.

Myers, Flow-limited authorization, in: 28th IEEE Computer Security Foundations Symp, CSF, 2015, pp. 569–583.

Arden,

Liu and

A.C.

Myers, Flow-limited authorization: Technical Report, Technical Report, 1813–40138, Cornell University Computing and Information Science, 2015.

Arden and

A.C.

Myers, A calculus for flow-limited authorization, in: 29th IEEE Computer Security Foundations Symp, CSF, 2016, pp. 135–147.

Bessani,

Sousa and

E.E.

Alchieri, State machine replication for the masses with BFT-SMaRt, in: Dependable Systems and Networks (DSN), 2014 44th Annual IEEE/IFIP International Conference on, IEEE, 2014, pp. 355–362.

Castro and

Liskov, Practical Byzantine fault tolerance and proactive recovery, ACM Trans. on Computer Systems20 (2002), 2002.

Cecchetti,

A.C.

Myers and

Arden, Nonmalleable information flow control, in: 24th ACM Conf. on Computer and Communications Security (CCS), 2017, pp. 1875–1891.

M.R.

Clarkson and

F.B.

Schneider, Quantification of integrity, in: Proc. IEEE Computer Security Foundations Symposium, 2010, pp. 28–43.

10.

Dawson and

Donovan, The breadth of Shamir’s secret-sharing scheme, Computer & Security (1994).

11.

R.B.

Findler and

Felleisen, Contracts for higher-order functions, SIGPLAN Not.37(9) (2002), 48–59. doi:10.1145/583852.581484.

12.

J.-Y.

Girard, Une extension de L’interpretation de gödel a L’analyse, et son application a L’elimination des coupures dans L’analyse et la theorie des types, in: Studies in Logic and the Foundations of Mathematics, Vol. 63, Elsevier, 1971, pp. 63–92.

13.

J.-Y.

Girard, Interpretation fonctionelle et elimination des coupure dans l’arithmetic d’ordre superieur, Ph. D. Thesis, L’universite Paris VII, 1972.

14.

Gollamudi,

Chong and

Arden, Information flow control for distributed trusted execution environments, in: 32nd IEEE Computer Security Foundations Symp, CSF, 2019.

15.

Hunt and

Sands, A quantale of information, in: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), 2021. doi:10.1109/CSF51468.2021.00031.

16.

Lamport, The Part-time Parliament, ACM Trans. on Computer Systems16(2) (1998), 133–169. doi:10.1145/279227.279229.

17.

Lamport, The PlusCal algorithm language, in: Theoretical Aspects of Computing – ICTAC 2009,

Leucker and

Morgan, eds, Springer, Berlin, Heidelberg, 2009, pp. 36–60. ISBN 978-3-642-03466-4. doi:10.1007/978-3-642-03466-4_2.

18.

Liu,

Arden,

M.D.

George and

A.C.

Myers, Fabric: Building open distributed systems securely by construction, J. Computer Security25(4–5) (2017), 319–321. doi:10.3233/JCS-0559.

19.

Mondal,

Algehed and

Arden, Applying consensus and replication securely with FLAQR, in: IEEE Computer Security Foundations Symp (CSF), 2022, pp. 163–178. doi:10.1109/CSF54842.2022.9919637.

20.

A.C.

Myers and

Liskov, Protecting privacy using the decentralized label model, ACM Transactions on Software Engineering and Methodology9(4) (2000), 410–442. doi:10.1145/363516.363526.

21.

Nakamoto, Bitcoin: A peer-to-peer electronic cash system, Consulted1(2012) (2008), 28.

22.

Pottier and

Simonet, Information flow inference for ML, in: 29th ACM Symp. on Principles of Programming Languages (POPL), 2002, pp. 319–330.

23.

J.C.

Reynolds, Towards a theory of type structure, in: Programming Symposium, Springer, 1974, pp. 408–425. doi:10.1007/3-540-06859-7_148.

24.

Shamir, How to share a secret, Communications of the ACM22(11) (1979), 612–613. doi:10.1145/359168.359176.

25.

Wadler and

R.B.

Findler, Well-typed programs can’t be blamed, in: Programming Languages and Systems,

Castagna, ed., Springer, Berlin, Heidelberg, 2009, pp. 1–16. ISBN 978-3-642-00590-9.

26.

C.-C.

Yang,

T.-Y.

Chang and

M.-S.

Hwang, A (t,n) multi-secret sharing scheme, in: Applied Mathematics and Computation, 2004, pp. 483–490.

27.

Zdancewic and

A.C.

Myers, Robust declassification, in: 14th IEEE Computer Security Foundations Workshop (CSFW), 2001, pp. 15–23, ISSN 1063-6900. doi:10.1109/CSFW.2001.930133.

28.

Zeldovich,

Boyd-Wickizer and

Mazières, Securing distributed systems with information flow control, in: 5th USENIX Symp. on Networked Systems Design and Implementation (NSDI), 2008, pp. 293–308.

29.

Zheng and

A.C.

Myers, End-to-end availability policies and noninterference, in: 18th IEEE Computer Security Foundations Workshop (CSFW), 2005, pp. 272–286. doi:10.1109/CSFW.2005.16.

30.

Zheng and

A.C.

Myers, A language-based approach to secure quorum replication, in: 9th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), 2014.

Flow-limited authorization for consensus,replication,and secret sharing 1

Abstract

Keywords

Get full access to this article

References