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

Asphalion: Trustworthy Shielding Against Byzantine Faults

Rahli, Vincent; Vukotic, Ivana;
Open Access
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, 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:

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