Actions
  • shareshare
  • link
  • cite
  • add
add
auto_awesome_motion View all 3 versions
Research software . Software . 2019

Asphalion: Trustworthy Shielding Against Byzantine Faults

Rahli, Vincent; Vukotic, Ivana;
Open Access
Abstract
Asphalion is a Coq-based framework for verifying the correctness of implementations of fault-tolerant systems. It especially provides features to verify the correctness of hybrid fault-tolerant systems (such as the MinBFT protocol http://www.di.fc.ul.pt/~bessani/publications/tc11-minimal.pdf), where normal components (that can for example fail arbitrarily) trust some special components (that can for example only crash on failure) to provide properties in a trustworthy manner. Asphalion allows running such trusted-trustworthy components inside Intel SGX enclaves. More details are provided here: https://vrahli.github.io/articles/asphalion-long.pdf
Subjects

Formal verification, Distributed systems, State machine replication, Fault-tolerance, Crash fault-tolerance, Byzantine fault-tolerance, Hybrid fault-tolerance, MinBFT, Intel SGX, Trusted components, Coq, Compositional reasoning, Knowledge calculus

moresidebar