Wiki
Clone wikipublic / Seminar
Upcoming talks
07-12-2020: Client-Server Sessions in Linear Logic
Speaker: Zesen Qian
Time: 12:00-13:00
Location: Lille Aud and Zoom
Abstract: We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formulate a system of session types based on Classical Linear Logic with coexponentials, which is well-suited for modelling client-server interactions. Applying the same design choices to exponentials leads to a type of linear streams, which can be used to interpret generators.
Work with G. A. Kavvos, Lars Birkedal
30-11-2020: Actris: session-type based reasoning in separation logic
Speaker: Jonas Kastberg
Time: 12:00-13:00
Location: Lille Aud and Zoom
Abstract: Message-passing is a principled approach to writing concurrent software. To verify message-passing behaviour in a scalable fashion, it is useful to have a first class approach to reasoning about it. Such an approach should integrate seamlessly with other low-level concurrency reasoning, as combining message passing with other concurrency mechanisms, such as locks, is commonplace.
In this talk I will present our work "Actris", a logical framework for thread-local reasoning about message passing, which combines separation logic with session types, originally presented at POPL'20. In doing so, I will cover the Actris protocol mechanism of "dependent separation protocols", showing how they can be used to verify a set of feature-rich examples, including the integration with lock-based concurrency. I will additionally present a recent extension of Actris to Actris 2.0, introducing the novel idea of "subprotocols", inspired by that of asynchronous session subtyping, to fully exploit the expressivity of asynchronous message passing. I will then provide insight into the model of Actris, based on step-indexing, and how we managed to fully mechanise it in Coq, by building it on top of the Iris logical framework. Finally, I will show how dependent separation protocols have been used to prove type soundness of an expressive session type system, using the technique of semantic typing, to draw a formal connection between the dependent separation protocols and the session types that inspired them.
23-11-2020: Towards Language-Based Mitigation of Traffic Analysis Attacks
Speaker: Jeppe Blaabjerg
Time: 12:00-13:00
Location: Zoom
Abstract: Traffic analysis attacks pose a major risk for online security. Distinctive patterns in communication act as fingerprints, enabling adversaries to de-anonymise communicating parties or to infer sensitive information.
Despite the attacks being known for decades, practical solutions are scarce. Network layer countermeasures have relied on black box padding schemes that require significant overheads in latency and bandwidth to mitigate the attacks, without fundamentally preventing them, and the problem has received little attention in the language-based information flow literature. Language-based methods provide a strong foundation for fundamentally addressing security issues, but previous work has overwhelmingly assumed that interactive programs communicate over secure channels, where messages are undetectable by unprivileged adversaries. This assumption is too strong for online communication where packets can be trivially observed by eavesdropping.
In this talk, I will present SELENE, a small language for principled, provably secure communication over channels where packets are publicly observable, and I will demonstrate how our program level defence can minimise the latency and bandwidth overheads induced compared with program-agnostic defence mechanisms. As a consequence of the attacker model, the language is restrictive. However, we believe that our results constitute a step towards practical, secure online communication.
16-11-2020: High level overview of formally verified security
Speaker: Bas Spitters
Time: 13:00-14:00
Location: Lille Aud and Zoom
Abstract : I will give a high level overview of the work going on in my group and how the topics fit together.
09-11-2020: Coq Extraction: new targets, new challenges
Speaker: Danil Annenkov
Time: 12:00-13:00
Location: Zoom
Abstract : Extraction is a technique allowing for obtaining a program in a conventional functional language from Coq implementation. The standard Coq extraction targets OCaml, Haskell and Scheme. During the last decade, many new functional languages have emerged, including the languages for programming of smart contracts -- programs executed on a blockchain. Moreover, functional features are available in several mainstream programming languages. The standard extraction is not suitable for targeting these languages and is not formally verified. We address these problems by developing an extraction framework based on MetaCoq's verified erasure. Our framework extends MetaCoq with extraction of types and data type definitions along with a verified optimisation procedure for removing dead code after erasure. The optimisation procedure is not specific to our project and it was recently integrated into the verified Coq compiler CertiCoq. We will discuss challenges of these new extraction targets and demonstrate applications of our extraction framework to functional smart contract languages, Elm and Rust.
Joint work with Mikkel Milo,Jakob Botsch Nielsen and Bas Spitters.
02-11-2020: Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code
Speaker: Aïna Linn Georges
Time: 12:00-13:00
Location: Zoom
Abstract : A capability machine is a kind of CPU which supports fine-grained privilege separation using capabilities (a pointer carrying a certain amount of authority). In this talk, I will present a methodology for verifying the functional correctness of capability machine programs that call (or are called by) unknown and potentially malicious code. The key aspects to the approach is a program logic for reasoning about known code, and a logical relation which provides a specification for unknown code. The entire setup has been mechanized in Coq using the Iris framework: https://github.com/logsem/cerise The methodology I will present was used (but left somewhat implicit) in recent work about a fast and secure calling convention for capability machine programs, which can be found at https://iris-project.org/pdfs/2021-popl-ucaps-final.pdf
26-10-2020: IFC Theorems for Free!
Speaker: Maximilian Algehed
Time: 12:00-13:00
Location: Zoom
Abstract :
Information Flow Control (IFC) is a collection of techniques for ensuring that programs behave in a secure way. Specifically, these techniques ensure the so called Noninterference security condition. In short, the public output of a program cannot depend on its secret inputs.
Recently, techniques have been developed to provide programmers with IFC languages in the form of libraries embedded in host languages with strong type systems. By using the abstraction mechanisms of the host language, these libraries are able to ensure strong relational invariants that guarantee noninterference.
In this work, we show how to prove that such libraries do in fact do what they advertise on the box. Specifically, we show how to use the parametricity theory of Bernardy et al. to prove noninterference both for static (i.e. type system-based) and dynamic (i.e. semantics based) IFC libraries.
19-10-2020: Contextual refinement of the Michael-Scott queue
Speaker: Simon Friis Vindum
Time: 12:00-13:00
Location: Zoom
Abstract: This talk will present the Michael-Scott queue (MS-queue), a fast and practical queue. A correctness criterion for concurrent data-structures is that they are contextual refinements of their concurrent counterparts. I’ll recall the notion of contextual refinement and explain how to use the Iris and ReLoC logics to prove contextual refinements for concurrent data structures in general and the Michael-Scott queue in particular. The talk is based on recent work I did together with Lars Birkedal (https://www.cs.au.dk/~birke/papers/2021-ms-queue.pdf).
05-10-2020: Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Speaker: Léon Gondelman
Time: 12:00-13:00
Location: Zoom
Abstract: In this presentation we are going to talk about modular specification and verification of causally-consistent distributed database, a data structure that guarantees causal consistency among replicas of the database.
With causal consistency, different replicas can observe different data on the same key, yet it is guaranteed that all data are observed in a causally related order: if a node N observes an update X originating at node M, then node N must have also observed the effects of any other update Y that took place on node M before X. Causal consistency can, for instance, be used to ensure in a distributed messaging application that a reply to a message is never seen before the message itself.
We will see how one can specify and verify a concrete implementation of such a distributed data structure in a way that supports modular verification of full functional correctness properties of clients and servers. Our approach is conducted using Aneris, a higher-order distributed separation logic for an ML-like programming language with network primitives for programming distributed systems.
We will demonstrate that proposed specifications are useful, by proving the correctness of small, but tricky, synthetic examples involving causal dependency and by verifying a session manager library implemented on top of the distributed database. Through those examples, we will see that the approach is highly modular, each component being verified in isolation, relying only on the specifications (not the implementations) of other components. The content of this talk corresponds to a recent work that the Aneris team (Abel, Amin, Lars, Léon, Simon) did on that subject. All the results of that work are formalized in the Coq proof assistant using the Aneris/Iris infrastructure and are presented in the paper that can be found online https://cs.au.dk/~gregersen/papers/2021-ccddb.pdf
21-09-2020: Mechanized Logical Relations for Termination-Insensitive Noninterference
Speaker: Simon Gregersen
Time: 12:00-13:00
Location: Zoom
Abstract: This talk will be about my recent work with Johan, Amin, and Lars on a novel semantic model of an expressive information-flow control type system. Notably, our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed—but semantically sound—components, which we have demonstrated through several interesting examples. I will spend a fair amount of time on why this problem is challenging and less time on understanding the technical solutions.
For those who are interested, a preprint is available at https://cs.au.dk/~gregersen/papers/2021-tiniris.pdf.
14-09-2020: Sketches of a RaTT: Fitch-style modal calculi for reactive programming
Speaker: Christian Uldal Graulund
Time: 12:00-12:45
Location: InCuba Lille Aud
Abstract: In this talk, I will describe the work I have been doing during my PhD. Namely, working with calculi for reactive programming, with the aim of creating a dependent type theory for reactive programming (RaTT). In particular, I will describe Simply RaTT and the extension Lively RaTT. Both of these are simply typed Fitch-style modal calculi for reactive programming. The former is, to our knowledge, the first use of the Fitch-style approach to functional reactive programming (FRP). The modal approach to FRP has been gaining popularity in recent years, but has previously been presented in the more traditional dual context approach. In the Simply RaTT paper, we provide operational semantics and prove the absence of implicit space leaks via a step-indexed Kripke logical relation.
In the Lively RaTT paper, we show how to extend Simply RaTT with (temporal) inductive types. We show how the usual problem with inductive types in systems with guarded recursion, that least and greatest fixpoints coincide, can be resolved by considering the next modality of LTL a sub-modality of the modality used for guarded recursion. We give an encoding of "fair" streams and prove it to be fair. The proofs uses an extension of the Simply RaTT logical relations.
Previous talks
Updated