Time: Wednesday 28. November 2018, 15:00
Place: 324/170
Title: Sound Full-Stack Formal Verification of Distributed Systems
Speaker:
Christoph Sprenger, ETH Zürich
Joint work with David Basin, Martin Clochard, Marco Eilers, Tobias Klenze, Markus Legner, Peter Müller, Fabio Pakk, Ralf Sasse, and Felix Wolf.
Abstract:
Full-stack formal verification of distributed systems is characterized by three elements: (1) the construction of abstract system models, which include the networking environment, and proving global properties about it; (2) showing that these properties are preserved down to the real system implementation running the different components' code; and (3) proving additional code-specific properties (such as memory safety and information flow security). In order to bridge the many levels of abstraction between a distributed system's abstract specification and the source code implementing its components, we use a combination of development by compositional stepwise refinement and source code verification based on a separation logic for specifying I/O behavior. I will explain how we have established a sound link between these two techniques. In the process, we have also proved the equivalence of a process calculus with a fragment of the I/O separation logic. We have formalized and proved our soundness results in Isabelle/HOL. This (ongoing) work is part of the verifiedSCION project, whose goal is the full-stack formal verification of functional and security properties of the SCION Internet architecture's routing algorithms and services.
---------------------------------------
Time: Thursday 29. November 2018, 10:00
Place: 324/240
Title:
Understanding Attestation:
Analyzing Protocols that use Quotes
Speaker:
Joshua D. Guttman. Joint work with John D. Ramsdell
Abstract:
Attestation protocols use digital signatures and other cryptographic values to convey evidence of hardware state, program code, and associated keys. They require hardware support such as Trusted Execution Environments or Trusted Platform Modules. Conclusions about attestations thus require reasoning about protocols, relevant hardware services, and possible behaviors of programs jointly.
This paper presents a mechanized approach to modeling these properties. Cryptographic Protocol Shapes Analyzer CPSA now combines protocol analysis with axioms or rules, allowing formalizing hardware and software conclusions.
We use CPSA to model aspects of Intel's SGX mechanism. We model underlying manufacturer-provided protocols, and build modular layers of attestation above this basis. User-level protocols can make trust decisions based on the results of attestation.