Linard Arquint, ETH Zürich
From 12.00 until 13.30
At CNB/F/110 (Lunch) + CAB H 52 (Seminar), ETH Zurich
CNB/F/110 (Lunch) + CAB H 52 (Seminar), ETH Zurich
Abstract:
Recent bugs in implementations, such as Heartbleed or in the Matrix chat application, demonstrate that formally verifying security properties for protocol models is an important first step but not enough to also guarantee them for implementations. We present a bottom-up verification approach to prove trace-based security properties directly on the level of existing implementations. The trace, recording relevant actions performed by all protocol participants, is made explicit but is only present at verification-time. Targeting existing implementations poses several additional challenges that we tackle by making the following contributions: (1) Our approach treats the global trace as a concurrent data structure and does not restrict the adversary. In particular, the granularity of methods has no influence on the considered interleavings. (2) We clearly separate the implementation from the trace and all annotations that are needed for verification. The so-called ghost code will be erased by the compiler and thus do not affect the implementation’s runtime behavior. Therefore, our approach does not impose restrictions on how implementations represent the program state. In particular, we support heap-manipulating programs. (3) We employ the same logic that we use to reason about heap manipulations to prove security properties. This not only simplifies the proof of certain security properties but also enables proving additional security properties, such as injective agreement.
Join us in CNB/F/110 (Lunch) + CAB H 52 (Seminar).