LogSem Seminar talks in 2020
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.
08-06-2020: A Polymorphic Type and Effect System with Boolean Unification
Speaker: Magnus Madsen, Jaco van de Pol
Time: 13:00-14:00
Location: https://aarhusuniversity.zoom.us/j/65045574235
Abstract: We present a simple, practical, and expressive type and effect system based on Boolean constraints. The effect system extends the Hindley-Milner type system, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support type inference by extending Algorithm W with Boolean unification based on the successive variable elimination algorithm.
We implement the type and effect system in the Flix programming language. We perform an in-depth evaluation on the impact of Boolean unification on type inference time and end-to-end compilation time. While the computational complexity of Boolean unification is NP-hard, the experimental results demonstrate that it works well in practice. We find that the impact on type inference time is on average a 1.4x slowdown and the overall impact on end-to-end compilation time is a 1.1x slowdown.
25-05-2020: Nakamoto-Style Blockchain Consensus 101
Speaker: Søren Eller Thomsen
Time: 13:00-14:00
Location: https://aarhusuniversity.zoom.us/j/68049508119
Abstract: This talk will present the basic functionality of a Nakamoto-style consensus mechanism. I will focus on under what circumstances this functionality is provided and how that reflects upon on an ongoing verification effort of a Proof-of-Stake Nakamoto-style blockchain.
18-05-2020: The right answer at the right time: an introduction to time complexity verification using time credits
Speaker: Armaël Gueneau
Time: 13:00-14:00
Location: https://aarhusuniversity.zoom.us/j/65650808630
Abstract: Algorithms textbooks typically contain informal theorems and proofs about the complexity of algorithms, e.g. “binary search runs in O(log n)”. In this talk, I will give a gentle introduction to how one might go and formally verify such claims in a proof assistant, with respect to concrete programs. Formally, I will demonstrate the use of Separation Logic with Time Credits for verifying both the correctness and complexity of concrete code, in a way that scales up from textbook examples to state of the art algorithms. The talk will be based on work that I did during my PhD, but is mostly intended as a general introduction of the topic.
11-05-2020: How to Define Things by Recursion
Speaker: Alex Kavvos
Time: 13:00-14:00
Location: https://aarhusuniversity.zoom.us/j/68849066187
Abstract: A crash course in the basic notions of domain theory.
04-05-2020: Analysis in univalent type theory
Speaker: Auke Booij
Time: 13:00-14:00
Location: https://aarhusuniversity.zoom.us/j/67856492801
Abstract: This talk is a thematic introduction to my thesis work on constructive analysis in univalent type theory. The central role of identity types in univalent type theory allows us to develop constructive analysis in a style highly reminiscent of traditional analysis, but additionally carrying computational content. The description of propositions in univalent type theory is key, and in this talk this is motivated by considering a locatedness structure on the real numbers.
27-04-2020: Blame for Null
Speaker: Abel Nieto
Time: 13:00-14:00
Location: https://aarhusuniversity.zoom.us/j/61149665805
Abstract: Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All of the above also need to interoperate with languages where types remain implicitly nullable, like Java. This leads to runtime errors that can manifest in subtle ways. In this talk, I will show how to reason about the presence and provenance of such nullability errors using the concept of blame from gradual typing. Specifically, I will present a calculus, “lambda null”, where some terms are typed as implicitly nullable and others as explicitly nullable. Just like in the original blame calculus of Wadler and Findler, interactions between both kinds of terms are mediated by casts with attached blame labels, which indicate the origin of errors. On top of lambda null, we then define a second calculus, “stratified lambda null“, which closely models the interoperability between languages with implicit nullability and languages with explicit nullability, such as Java and Scala. The main result is a theorem that states that nullability errors in stratified lambda null can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. By analogy, this would mean that NullPointerExceptions in combined Java/Scala programs are always the result of unsoundness in the Java type system. The result can be summarized with the slogan “explicitly nullable programs can’t be blamed”. The results are formalized in the Coq proof assistant.
30-03-2020: High-assurance modular inversion using Fiat Cryptography
Speaker: Benjamin Salling Hvass
Time: 13:00-14:00
Location: Zoom: https://aarhusuniversity.zoom.us/j/359931396
Abstract:
Crypto-code is highly vulnerable to attacks and therefore a worthwhile target for verification/formalization.
A recent contribution to this area of ‘high-assurance crypto’ is the Fiat Cryptography library which allows synthesis of constant-time and verified code implementing finite field arithmetic (modulo any prime).
The work presented in this talk, is an attempt to extend the Fiat Crypto framework to also be able to generate a verified, constant-time and efficient modular inversion implementation.
This is joint work with Bas Spitters and Diego F. Aranha.
23-03-2020: ∃R-Completeness of Stationary Nash Equilibria in Perfect Information Stochastic Games
Speaker: Steffan Sølvsten
Time: 13:00-14:00
Location: Zoom: https://aarhusuniversity.zoom.us/j/364163471
Abstract: In applications of modelling, verification, and synthesis one can reason about the system in terms of a stochastic game, where the system is pitted against the environment. From such a perspective, it is then of common interest to discern whether there is a strategy, such that the system is always winning in respect to some goal. For this, the concept of Nash equilibria is often used to reason about agents that behave rationally.
We show that the problem of deciding whether in a multi-player perfect information recursive game there exists a stationary Nash equilibrium ensuring each player a certain payoff is ∃R-complete. Combining our result with known gadget games without any stationary Nash equilibrium, we obtain that for cyclic games, just deciding existence of any stationary Nash equilibrium is ∃R-complete, and thereby also existence of a surely winning strategy. This holds for both reachability and safety goals, and for deterministic recursive games.
This work is part of a project with Kristoffer Arnsfelt Hansen.
09-03-2020: Towards Computational Models for Authorization Logics
Speaker: Andrew Hirsch
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: Authorization logics are multi-modal logics used to reason about authorization in distributed systems. Significant work has been done developing proof theory and model theory for authorization logics. However, the model theories built so far cannot represent distribution and communication. This means they can neither be used to inform proof-system design decisions nor to build verification tools.
In this talk, I will introduce current work in building computational models for authorization logics. This interprets proofs as programs, in the style of the propositions-as-types principal. However, unlike previous attempts at propositions-as-types correspondences for authorization logics, we embrace the distributed nature of authorization logics. To do this, we adapt choreographic programming, a programming paradigm for concurrent programming, with modal types. A long-term goal is to build a type theory based on choreographic programming, allowing programmers to build certified secure distributed systems.
09-03-2020: Bi-Intuitionistic Types via Alternating Contexts
** (The talk has been cancelled) **
Speaker: Ranald Clouston
Time: 14:15-15:00
Location: Nygaard meeting room 395
Abstract: Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a binary operator called exclusion, dual to implication. In the early 2000s Crolard designed a type system for this logic, introducing a notion of control operator more restricted than classical call/cc. However this system is flawed, as it is claimed to imply cut-elimination for a sequent calculus of Rauszer, which is now known not to hold. We propose a new type system that is sound and complete for this logic, with a novel notion of ‘alternating’ variable context inspired by work in modal type theory. Alternating contexts allow one to interleave lambda- and mu-variables, with structural symbols interpreted variously as products, sums, and exclusion.
02-03-2020: How programming language research can help securely implement cryptography
Speaker: Alix Trieu
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: Cryptography is a mature research field where clear techniques and methodology to show security of algorithms as reductions of well identified problems are known. However, the art of implementing cryptography is reserved to a few experts. Indeed, it does not suffice that the implementation be functionally correct, but it also needs to be secure. In this talk, I will give a small overview of the concerns that cryptography implementers have to worry about, the countermeasures they came up with and how these map to a well-known property in the language-based security community, namely non-interference. Finally, I will talk about how PL research techniques have and can help to securely implement cryptography.
Disclaimer 1: This will be a whiteboard presentation.
Disclaimer 2: I will give the same talk with slides at the crypto seminar on March 16th.
24-02-2020: Univalent parametricity and refinements for free
Speaker: Andreas Aagaard Lynge
Time: 13:00-13:45
Location: Nygaard meeting room 395
Abstract: I will present parametricity and discuss its relation to univalent parametricity and refinements for free. The parametricity abstraction theorem provides free theorems about polymorphic terms. The abstraction theorem in univalent parametricity similarly provides free theorems. These can be used to transport properties between equivalent types. I will explore on this and discuss benefits of univalent parametricity. Afterwards I introduce refinements for free, a method to apply free theorems from parametricity to transport properties between related structures.
03-02-2020: Enumerating and Counting N-Queens solutions: Between heuristics and structure
Speaker: Irfansha Shaik
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: The N-Queens problem is a 150-year-old classical mathematical problem of placing N queens on an N * N chessboard such that no two queens share the same row, column or a diagonal, i.e. non-attacking queens. The counting N-Queens is the task of counting all such solutions of the N-Queens problem.
There are two main research directions here, one is to find scalable efficient algorithms and the other to find structure in the problem. Despite being a widely researched problem there seems to be a wide gap between finding/using the structure and algorithmic implementations.
In this talk, we will try to bring them together by looking closely at enumeration algorithms and counting algorithms with respect to the constraints of the problem. In Enumeration, we focus on SAT solving perspective with propagation, unsatisfiability and heuristics (given as parameters) where as in counting we utilize the structure of the problem.
This work is part of MSc by Research degree from Swansea University in collaboration with Oliver Kullmann.
13-01-2020: Multimodal Dependent Type Theory
Speaker: Daniel Gratzer
Time: 13:00-14:30
Location: Nygaard meeting room 395
Abstract:
Modalities have proved to be a recurring phenomenon in type theories, arising in both mathematical
and computational contexts. Despite the wide variety of uses, a general framework for modal dependent
type theories has still proven elusive. Each modal situation requires a handcrafted type theory, and
establishing the properties of these type theories requires a significant technical investment.
In this work, we have attempted to isolate a class of modal situations which can be given a single uniform syntax and allow for the typical metatheorems of type theory to be proven once and for all. Our approach generalizes the ideas latent in Nuyts, Vezzosi, and Devriese, and simplifies the forthcoming work by Licata, Shulman, and Riley on a of subset of mode theories. This calculus is sufficiently flexible to model internal parametricity, guarded recursion, and even axiomatic cohesion.
In the interest of giving an interesting talk for everyone, we will focus on modal type theory in general, and discuss the historical approaches and challenges and how our type theory handles these difficulties.
joint work with Lars Birkedal, Alex Kavvos, and Andreas Nuyts