Time: Wednesday 28. November 2018, 15:00\n
\nPlace: 324/170\n
Title: Sound Full-Stack Formal Verification of Distributed Systems\n
\nSpeaker:\nChristoph Sprenger, ETH Zürich\n
\nJoint work with David Basin, Martin Clochard, Marco Eilers, Tobias Klenze, Markus Legner, Peter Müller, Fabio Pakk, Ralf Sasse, and Felix Wolf.\n
\nAbstract:\n
\nFull-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.\n
---------------------------------------\n
\nTime: Thursday 29. November 2018, 10:00\n
\nPlace: 324/240\n
Title:\nUnderstanding Attestation:\nAnalyzing Protocols that use Quotes\n
\nSpeaker:\nJoshua D. Guttman. Joint work with John D. Ramsdell\n
\nAbstract:\n
\nAttestation 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.\nThis 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.\nWe 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.
X-ALT-DESC;FMTTYPE=text/html:
Time: Wednesday 28. November 2018, 15:00\n
\nPlace: 324/170\n
Title: Sound Full-Stack Formal Verification of Distributed Systems\n
\nSpeaker:\nChristoph Sprenger, ETH Zürich\n
\nJoint work with David Basin, Martin Clochard, Marco Eilers, Tobias Klenze, Markus Legner, Peter Müller, Fabio Pakk, Ralf Sasse, and Felix Wolf.\n
\nAbstract:\n
\nFull-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.\n
---------------------------------------\n
\nTime: Thursday 29. November 2018, 10:00\n
\nPlace: 324/240\n
Title:\nUnderstanding Attestation:\nAnalyzing Protocols that use Quotes\n
\nSpeaker:\nJoshua D. Guttman. Joint work with John D. Ramsdell\n
\nAbstract:\n
\nAttestation 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.\nThis 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.\nWe 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.
URL:https://www.dtu.dk/sitecore/content/institutter/compute/dtu_compute_old/forside/kalender/2018/11/speaker-christoph-sprenger DTSTAMP:20260512T172500Z UID:{A0F2A114-579F-440C-8067-E60C5E4B73FF}-20181128T140000Z-20181128T140000Z LOCATION: DTU Compute, Building 324, room 170/240 END:VEVENT END:VCALENDAR