Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq

in ESOP 2018 (2018, April)

Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these ... [more ▼]

Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least n-f out of n replicas survive arbitrary faults. This paper presents Velisarios a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area's reference protocol: PBFT. [less ▲]

A Verified Theorem Prover Backend Supported by a Monotonic Library

in LPAR 2018 (2018)

Validating Brouwer's Continuity Principle for Numbers Using Named Exceptions

in Mathematical Structures in Computer Science (2017)

EventML: Specification, Verification, and Implementation of Crash-Tolerant State Machine Replication Systems

in Science of Computer Programming (2017)

Avoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control

Scientific Conference (2016, December 12)

Intel SGX is the latest processor architecture promising secure code execution despite large, complex and hence potentially vulnerable legacy operating systems (OSs). However, two recent works identified ... [more ▼]

Intel SGX is the latest processor architecture promising secure code execution despite large, complex and hence potentially vulnerable legacy operating systems (OSs). However, two recent works identified vulnerabilities that allow an untrusted management OS to extract secret information from Intel SGX's enclaves, and to violate their integrity by exploiting concurrency bugs. In this work, we re-investigate delayed preemption (DP) in the context of Intel SGX. DP is a mechanism originally proposed for L4-family microkernels as disable-interrupt replacement. Recapitulating earlier results on language-based information-flow security, we illustrate the construction of leakage-free code for enclaves. However, as long as adversaries have fine-grained control over preemption timing, these solutions are impractical from a performance/complexity perspective. To overcome this, we resort to delayed preemption, and sketch a software implementation for hypervisors providing enclaves as well as a hardware extension for systems like SGX. Finally, we illustrate how static analyses for SGX may be extended to check confidentiality of preemption-delaying programs. [less ▲]

Exercising Nuprl's Open-Endedness

in The 5th International Congress on Mathematical Software (2016)

Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML

in EASST (2015)

Coq as a Metatheory for Nuprl with Bar Induction

Scientific Conference (2015)

Towards a Formally Verified Proof Assistant (technical report)

Report (2014)

A Type Theory with Partial Equivalence Relations as Types

Scientific Conference (2014)