Keeta-Konsens formal verifiziert: Sicherheit unter byzantinischen Fehlern bewiesen
Modeling and Verification of Keeta's Consensus [pdf]
Die Blockchain Keeta nutzt einen neuartigen zweiphasigen, clientgesteuerten Konsensalgorithmus für grenzüberschreitende Zahlungen. Diese Arbeit präsentiert die erste formale Spezifikation des Algorithmus in Quint und verifiziert sie mit dem Model Checker TLC unter einem byzantinischen Fehlermodell. Die Ergebnisse zeigen, dass der Algorithmus die Übereinstimmung (Agreement) bei einer festen, gleichgewichteten Repräsentantenmenge garantiert, und argumentieren, dass diese Sicherheitseigenschaft auf beliebig viele Repräsentanten verallgemeinerbar ist. Zudem werden Bedingungen aufgezeigt, unter denen ein umkämpftes Konto dauerhaft gesperrt werden kann. Das maschinell prüfbare Modell dient als wiederverwendbares Artefakt für zukünftige Forschung.
Die Sicherheitseigenschaften eines Konsensalgorithmus sind spezifisch für sein Design und müssen für jedes neue Protokoll unabhängig etabliert werden.