6 Search Results for "Zălinescu, Eugen"

Document
DOI: 10.4230/LIPIcs.DISC.2022.12
Liveness and Latency of Byzantine State-Machine Replication

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)

Abstract
Byzantine state-machine replication (SMR) ensures the consistency of replicated state in the presence of malicious replicas and lies at the heart of the modern blockchain technology. Byzantine SMR protocols often guarantee safety under all circumstances and liveness only under synchrony. However, guaranteeing liveness even under this assumption is nontrivial. So far we have lacked systematic ways of incorporating liveness mechanisms into Byzantine SMR protocols, which often led to subtle bugs. To close this gap, we introduce a modular framework to facilitate the design of provably live and efficient Byzantine SMR protocols. Our framework relies on a view abstraction generated by a special SMR synchronizer primitive to drive the agreement on command ordering. We present a simple formal specification of an SMR synchronizer and its bounded-space implementation under partial synchrony. We also apply our specification to prove liveness and analyze the latency of three Byzantine SMR protocols via a uniform methodology. In particular, one of these results yields what we believe is the first rigorous liveness proof for the algorithmic core of the seminal PBFT protocol.
Cite as

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. Liveness and Latency of Byzantine State-Machine Replication. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 12:1-12:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2022.12,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Liveness and Latency of Byzantine State-Machine Replication}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.12},
  URN =		{urn:nbn:de:0030-drops-172037},
  doi =		{10.4230/LIPIcs.DISC.2022.12},
  annote =	{Keywords: Replication, blockchain, partial synchrony, liveness}
}
Document
DOI: 10.4230/OASIcs.FAB.2022.5
Fork Accountability in Tenderbake

Authors: Antonella Del Pozzo and Thibault Rieutord

Published in: OASIcs, Volume 101, 5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022)

Abstract
This work investigates the Fork Accountability problem in the BFT-Consensus-based Blockchain context. When there are more attackers than the tolerated ones, BFT-Consensus may fail in delivering safety. When this occurs, Fork Accountability aims to account for the responsible processes for that safety violation. As a case study, we consider Tenderbake when the assumption on the maximum number of Byzantine validators - participants involved in creating the next block - does not hold anymore. When a fork occurs, there are more than one-third of Byzantine validators, and we aim to account for the responsible validators to remove them from the system. In this work, we compare three different approaches to implementing accountability in the case of a fork. In particular, we show that in the case of a fork, if we do not modify Tenderbake or we enrich it with a reliable broadcast communication abstraction, then we can account Byzantine processes only in particular scenarios. Contrarily, if we change Tenderbake such that the exchanged messages also carry extra information (which size is proportional to the duration of the current consensus computation), then we can account for Byzantine processes in all kinds of scenarios; however, at the cost of unbounded message size and unbounded local memory.
Cite as

Antonella Del Pozzo and Thibault Rieutord. Fork Accountability in Tenderbake. In 5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022). Open Access Series in Informatics (OASIcs), Volume 101, pp. 5:1-5:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{delpozzo_et_al:OASIcs.FAB.2022.5,
  author =	{Del Pozzo, Antonella and Rieutord, Thibault},
  title =	{{Fork Accountability in Tenderbake}},
  booktitle =	{5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022)},
  pages =	{5:1--5:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-248-8},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{101},
  editor =	{Tucci-Piergiovanni, Sara and Crooks, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FAB.2022.5},
  URN =		{urn:nbn:de:0030-drops-162723},
  doi =		{10.4230/OASIcs.FAB.2022.5},
  annote =	{Keywords: Blockchain, BFT-Consensus, Fork Accountability}
}
Document
DOI: 10.4230/OASIcs.FAB.2021.1
Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains

Authors: Lăcrămioara Aştefănoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci-Piergiovanni, and Eugen Zălinescu

Published in: OASIcs, Volume 92, 4th International Symposium on Foundations and Applications of Blockchain 2021 (FAB 2021)

Abstract
First-generation blockchains provide probabilistic finality: a block can be revoked, albeit the probability decreases as the block "sinks" deeper into the chain. Recent proposals revisited committee-based BFT consensus to provide deterministic finality: as soon as a block is validated, it is never revoked. A distinguishing characteristic of these second-generation blockchains over classical BFT protocols is that committees change over time as the participation and the blockchain state evolve. In this paper, we push forward in this direction by proposing a formalization of the Dynamic Repeated Consensus problem and by providing generic procedures to solve it in the context of blockchains. Our approach is modular in that one can plug in different synchronizers and single-shot consensus. To offer a complete solution, we provide a concrete instantiation, called {{Tenderbake}}, and present a blockchain synchronizer and a single-shot consensus algorithm, working in a Byzantine and partially synchronous system model with eventually synchronous clocks. In contrast to recent proposals, our methodology is driven by the need to bound the message buffers. This is essential in preventing spamming and run-time memory errors. Moreover, {{Tenderbake}} processes can synchronize with each other without exchanging messages, leveraging instead the information stored in the blockchain.
Cite as

Lăcrămioara Aştefănoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci-Piergiovanni, and Eugen Zălinescu. Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains. In 4th International Symposium on Foundations and Applications of Blockchain 2021 (FAB 2021). Open Access Series in Informatics (OASIcs), Volume 92, pp. 1:1-1:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{astefanoaei_et_al:OASIcs.FAB.2021.1,
  author =	{A\c{s}tef\u{a}noaei, L\u{a}cr\u{a}mioara and Chambart, Pierre and Del Pozzo, Antonella and Rieutord, Thibault and Tucci-Piergiovanni, Sara and Z\u{a}linescu, Eugen},
  title =	{{Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains}},
  booktitle =	{4th International Symposium on Foundations and Applications of Blockchain 2021 (FAB 2021)},
  pages =	{1:1--1:23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-196-2},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{92},
  editor =	{Gramoli, Vincent and Sadoghi, Mohammad},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FAB.2021.1},
  URN =		{urn:nbn:de:0030-drops-139877},
  doi =		{10.4230/OASIcs.FAB.2021.1},
  annote =	{Keywords: Blockchain, BFT-Consensus, Dynamic Repeated Consensus}
}
Document
DOI: 10.4230/LIPIcs.DISC.2020.23
Making Byzantine Consensus Live

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 179, 34th International Symposium on Distributed Computing (DISC 2020)

Abstract
Partially synchronous Byzantine consensus protocols typically structure their execution into a sequence of views, each with a designated leader process. The key to guaranteeing liveness in these protocols is to ensure that all correct processes eventually overlap in a view with a correct leader for long enough to reach a decision. We propose a simple view synchronizer abstraction that encapsulates the corresponding functionality for Byzantine consensus protocols, thus simplifying their design. We present a formal specification of a view synchronizer and its implementation under partial synchrony, which runs in bounded space despite tolerating message loss during asynchronous periods. We show that our synchronizer specification is strong enough to guarantee liveness for single-shot versions of several well-known Byzantine consensus protocols, including HotStuff, Tendermint, PBFT and SBFT. We furthermore give precise latency bounds for these protocols when using our synchronizer. By factoring out the functionality of view synchronization we are able to specify and analyze the protocols in a uniform framework, which allows comparing them and highlights trade-offs.
Cite as

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. Making Byzantine Consensus Live. In 34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 23:1-23:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2020.23,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Making Byzantine Consensus Live}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020.23},
  URN =		{urn:nbn:de:0030-drops-131013},
  doi =		{10.4230/LIPIcs.DISC.2020.23},
  annote =	{Keywords: Byzantine consensus, blockchain, partial synchrony, liveness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.590
Failure-aware Runtime Verification of Distributed Systems

Authors: David Basin, Felix Klaedtke, and Eugen Zalinescu

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
Prior runtime-verification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome these limitations, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the real-time logic MTL that efficiently handles out-of-order message deliveries and operates in the presence of failures. Our algorithm uses a three-valued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure. We establish the algorithm's soundness and provide completeness guarantees. We also show that it supports distributed system monitoring, where multiple monitors cooperate and exchange their observations and conclusions.
Cite as

David Basin, Felix Klaedtke, and Eugen Zalinescu. Failure-aware Runtime Verification of Distributed Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 590-603, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{basin_et_al:LIPIcs.FSTTCS.2015.590,
  author =	{Basin, David and Klaedtke, Felix and Zalinescu, Eugen},
  title =	{{Failure-aware Runtime Verification of Distributed Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{590--603},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.590},
  URN =		{urn:nbn:de:0030-drops-56194},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.590},
  annote =	{Keywords: Runtime verification, monitoring algorithm, real-time logics, multi-valued semantics, distributed systems, asynchronous communication}
}
Document
DOI: 10.4230/OASIcs.TrustworthySW.2006.691
Relating two standard notions of secrecy

Authors: Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data { t s}. Reach-ability-based secrecy means that { t s} should never be disclosed while equi-valence-based secrecy states that two executions of a protocol with distinct instances for { t s} should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far. This paper initiates a systematic investigation of situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries in the case of symmetric encryption, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.
Cite as

Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch. Relating two standard notions of secrecy. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{zalinescu_et_al:OASIcs.TrustworthySW.2006.691,
  author =	{Zalinescu, Eugen and Cortier, V\'{e}ronique and Rusinowitch, Micha\"{e}l},
  title =	{{Relating two standard notions of secrecy}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.691},
  URN =		{urn:nbn:de:0030-drops-6911},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.691},
  annote =	{Keywords: Verification, security protocols, secrecy, applied-pi calculus}
}
  • Refine by Author
  • 2 Bravo, Manuel
  • 2 Chockler, Gregory
  • 2 Del Pozzo, Antonella
  • 2 Gotsman, Alexey
  • 2 Rieutord, Thibault
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Distributed algorithms
  • 2 Theory of computation → Distributed computing models

  • Refine by Keyword
  • 2 BFT-Consensus
  • 2 Blockchain
  • 2 blockchain
  • 2 liveness
  • 2 partial synchrony
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2022
  • 1 2006
  • 1 2015
  • 1 2020
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact