FSCD 2018 Invited Speakers
Title of talk
Analysing privacy-type properties in cryptographic protocols
Abstract
Cryptographic protocols aim at securing communications over insecure
networks such as the Internet, where dishonest users may listen to
communications and interfere with them. For example, passports are no more
pure paper documents. Instead, they contain a chip that stores additional information
such as pictures and fingerprints of their holder. In order to ensure privacy, these chips
include a mechanism, i.e. a cryptographic protocol, that does not let
the passport disclose private information to external users.
This is just a single example but of course privacy appears in many other contexts
such as RFIDs technologies or electronic voting.
Formal methods have been successfully applied to automatically analyze
traditional protocols and discover flaws. Privacy-type security
properties (e.g. anonymity, unlinkability, ...) are expressed relying on a notion of behavioral
equivalence, and are actually more difficult to analyse.
We will discuss some recent advances that have been done to analyse automatically
equivalence-based security properties, and we will review some issues
that remain to be solved in this field.
Grigore Rosu
U.of Illinois at Urbana-Champaign, US
See Profile
Title of talk
Formal Design, Implementation and Verification of Blockchain Languages
Abstract
Many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses of the underlying blockchain programming languages or virtual machines. The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines.
We present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal specification. We demonstrate the feasibility of the proposed approach by applying it to two blockchains, Ethereum and Cardano.
Title of talk
Challenges in quantum programming languages
Abstract
In this talk, I will give an overview of some recent
progress and current challenges in the design of quantum programming
languages. Unlike classical programs, which can in principle be
debugged by stopping the program at critical moments and examining the
contents of variables, quantum programs are not amenable to
traditional debugging because the state of a quantum system cannot
usually be examined in a meaningful way. Therefore, we need other
methods for ensuring the correctness of quantum programs, such as
formal verification. For this reason, I advocate the use of strongly
typed, functional programming languages for quantum computing. As far
as functional quantum programming languages are concerned, there is
currently a relatively wide gap between theory and practice. On the
one hand, we have languages with strong theoretical foundations, such
as the quantum lambda calculus, which operate at a relatively low
level of abstraction and lack many features that would be useful to
practical quantum programmers. On the other hand, we have practical
functional quantum programming languages such as Quipper, which is
implemented as an embedded language in Haskell, has many high-level
features, and has been used in large-scale projects, but lacks a
theoretical basis and a strong type system. We have recently attempted
to narrow this gap through a family of languages called Proto-Quipper,
which are designed to offer Quipper-like features while having sound
theoretical foundations. I will give an overview of Quipper and its
most useful features, report on the progress we made with formalizing
fragments of Quipper, and outline several of the still remaining
challenges.
Title of talk
Proof techniques for program equivalence in probabilistic higher-order languages
Abstract
While the theory of functional higher-order languages, starting from lambda-calculi, is a well-established research field, it is only in recent years that the operational semantics of higher-order languages with probabilistic operators has started to be extensively studied. A fundamental notion in the semantics of programming languages is that of program equivalence. In higher-order languages, program equivalence is generally formalized as a contextual equivalence, which can be hard to prove directly. This has motivated the study of proof techniques for contextual equivalence, from inductive ones, such as logical relations, to coinductive ones, mainly in the form of bisimulations. In this talk I will discuss proof techniques for program equivalence in languages combining higher-order and probabilistic features. Several operational methods, traditionally developed in a deterministic setting, have been adapted to probabilistic higher-order languages. I will discuss these proof methods and focus on bisimulation-based techniques, showing how probabilities, combined with different language features, force a number of modifications to the definition of bisimulation.