Friday, April 13 at 11:00, Euleur Bleu, by Suykung Yu (KAIST)
The Racket Way
Friday, April 6 at 10:00, Euler Violet, by Matthew Flatt (University of Utah)
The design of the Racket programming language (http://racket-lang.org) reflects a philosophy of programming where (1) everything is a program, (2) concepts are programming-language constructs, and (3) the programming language is extensible. This talk is a demonstration of what the Racket way means, and it includes a tour of a language for writing prose documents, a language for creating slide presentations, constructs for language extensibility and language creation, OS-like programming-language constructs, and examples that put those pieces together.
Resugaring: Lifting Semantic Features through Syntactic Sugar
Friday, April 6 at 11:00, Euler Violet, by Shiram Krishnamurthi (Brown University)
Syntactic sugar is pervasive in language technology. It is used to shrink the size of a core language; to define domain-specific languages; and even to let programmers extend their language. Unfortunately, syntactic sugar is eliminated by transformation, so when the system provides feedback, it is in terms of a program that is unfamiliar to the authors. Thus, tool authors are forced to choose between their convenience and that of the programmer.
We address this conflict by showing how to lift core language features to present them in terms of the surface syntax. We have performed this research over three different features: execution traces, binding, and type rules. In each case we identify properties expected of the lifting and prove that our techniques satisfy these.
More broadly, though syntactic sugar is a central area of programming languages, it remains under-represented in the research literature. We briefly present some other elements of a research agenda for this area.
Friday, April 6 at 14:00, Euler Violet, by Colin Vidal (Inria INDES)
Massively Interactive Music (MMI)
Friday, April 6 at 14:30, Euler Violet, by Bertrand Petit (Inria INDES)
The 8 and 9 December 2017, during a festival of Contemporary Music, a show called “Golem” was presented. The show included two sessions of five minutes where the public has the control of the music using their smartphones. We called this sessions “Massively Interactive Music” in the sense that in the actual context of the show we had up to 90 people interacting with the sound system. The technology used for control system was based on the last research on Web development using multitier and Reactive Synchronous programming allowing fast and reliable development. MMI rises different kind of challenges:
- development, how to fast develop and prototype the shows, hop and hiphop
- aesthetics,what are the criteria to evaluate the quality of an interactive session
- human interface, what are the good interactions and how to manage them.
On the Effectiveness, Integrity and Semantics of CSP
Friday, April 6 at 15:00, Euler Violet, by Francis Somé (Inria INDES)
Content Security Policy (CSP) is a security mechanism that can be deployed by web applications to protect against various classes of attacks, in particular Cross-Site Scripting (XSS). It works by declaring a list of origins which are trusted, thereby instructing browsers to block content from any other unstrusted origin. Strict-CSP is the current evolution of CSP, aims at easing CSP adoption by web applications, while preventing CSP bypasses due to JSONP and open redirections. We show that Strict-CSP fails at preventing trivial XSS attacks occuring whithin scripts already present in a web page.
In this presentation, we will discuss how one could still use Strict-CSP while ensuring its effectiveness at preventing attacks. Then, we will show how to ensure the integrity of CSP and preserve a match between CSP static and runtime semantics, as browser extensions, very widespread, represent a serious threat to the security of web applications because of their ability to modify CSP and inject content directly in web pages.
DSL in Cybersecurity: From provable security to secure cryptographic implementations
Wednesday, April 4 at 11:00, Euler Violet, by Gilles Barthe (Imdea Sofware)
Building secure cryptographic implementations is notoriously hard. In this talk, I will outline a general methodology that delivers formal guarantees on assembly-level implementations through a combination of ideas from deductive program verification, program analysis, and verified compilation I will also outline the relevance of formal methods and programming languages in the broader context of cryptography.
Wednesday, April 4 at 10:00, Euler Violet, by Hubert Comon (ENS Cachan)
We consider the problem of proving that two scenarios are indistinguishable by an active adversary: the adversary is interacting with one of the two scenarios and wins if, in the end, it is able to guess with which one it was interacting. The two scenarios are indistinguishable if the winning probability of the adversary is not significantly different from 1/2. This problem arises, for instance, when we want to get formal guarantees that the privacy (or anonymity) is preserved by some application. Such indistinguishability proofs rely on cryptographic assumptions and are usually completed using cryptographic game transformations. This is for example what is performed by the provers EasyCrypt and CryptoVerif. In this talk, relying on a work of Adrien Koutsos, we will introduce a decision algorithm for indistiguishability, given a set of game transformations.
Security Testing beyond Functional Tests
Wednesday, April 4 at 9:00, Euler Violet, by David Basin (ETH Zurich)
Security testing is omnipresent. But what is it? And what distinguishes it from functional testing? To answer these questions and shed light on the scope and reach of existing testing methods, we present a theory of security testing. Our theory is based on the basic distinction between system specifications and security requirements. Specifications describe a system’s desired behavior over its interface. Security requirements, in contrast, specify desired properties of the world the system lives in. We propose the notion of a security rationale, which supports reductive security arguments for deriving a system specification and assumptions on the system’s environment sufficient for fulfilling stated security requirements. These reductions give rise to two types of tests: those that test the system with respect to its specification and those that test the validity of the assumptions about the adversarial environment. It is the second type of tests that distinguishes security testing from functional testing and defies systematization and automation.
[Paper on topic available here]
HDR Defense Tamara Rezk : Secure Programming
Tuesday, April 3 at 13:30, amphi Kahn, by Tamara Rezk (Inria INDES)
This event regards an habilitation defense summarising 10 years of work on the topic of secure programming. During the talk, Tamara will briefly describe her work divided in 4 subdomains of secure programming: programs using cryptography, web security, privacy, and secure compilation.
- Prof. Hubert Comon-Lundh – ENS Cachan
- Prof. Yassine Lakhnech – University Joseph Fourier
- Prof. John C. Mitchell – Standford University
- Prof. David Basin – ETH Zurich
- Prof. Michael Hicks – University of Maryland
- Prof. Shriram Krishnamurthi – Brown University
- Prof. Bruno Martin – University of Nice-Sophia Antipolis
From natural semantics to type-based program analysis
Thursday, September 7 at 16:00, Kahn K1, by Thomas Jensen (Inria Rennes, Celtique)
In this talk, I’ll address the question of how to define (and possibly even derive) a program analysis from the semantic definition of a programming language. Abstract interpretation provides a recipe for such derivational program analysis. I’ll review some work on the relation between abstract interpretation and type-based analysis and present some more recent work on how to obtain such analyses from Kahn-style natural semantics in a systematic fashion.
Case Studies on iOS and TOR Browser: Why Limiting Access is not Enough to Block Fingerprinting
Tuesday, September 5 at 9:30, Fermat F102, by Gábor György Gulyás (Inria Grenoble, Privatics)
Several recent studies have demonstrated that people show large behavioural uniqueness. This has serious privacy implications as most individuals become increasingly re-identifiable in large datasets or can be tracked while they are browsing the web using only a couple of their attributes, called as their fingerprints. Often, the success of these attacks depend on explicit constraints on the number of attributes learnable about individuals, i.e., the size of their fingerprints. These constraints can be budget as well as technical constraints imposed by the data holder. For instance, Apple restricted the number of applications that can be called by another application on iOS in order to mitigate the potential privacy threats of leaking the list of installed applications on a device. In this work, we address the problem of identifying the attributes (e.g., smartphone applications) that can serve as a fingerprint of users given constraints on the size of the fingerprint. We give the best fingerprinting algorithms in general, and discuss their effectiveness on several real-world datasets.
Our results show that current privacy guards limiting the number of attributes that can be queried about individuals is insufficient to mitigate their potential privacy risks in many practical cases.
Evaluating and Applying Software Visualization
Monday, July 10 at 14:00, F102, by Alexandre Bergel (University of Chile)
Understanding software execution is known to be difficult. Unfortunately, printing in the console has been King for over half a century. Although many aspects of the software development process have improved during the last decade (e.g., source code versioning, code editing), software profilers and debuggers are unfortunately close to the same state they were when the C language was alone to reign. This presentation highlights applications and evaluations of a number of software visualizations.
Type Specialization Without Static Type Analysis
Tuesday, June 27 at 11:00, F102, by Marc Feeley (University of Montreal)
Dynamic programming languages have a rich semantics where operations of the language have a meaning that depends on the run time type of the arguments. It is of prime importance for optimizing compilers to predict the type of the values in order to specialize the generated code for the specific types encountered when executing the program. The traditional approach is to perform a static type analysis. For a variety of reasons, this often yields less than ideal results in dynamic programming languages. Our work has researched a new approach, Basic Block Versioning (BBV), for JIT compilers that performs on-the-fly type specialization at low cost and better precision. The presentation will give an overview of BBV and some recent extensions to higher order languages with first class functions and closures.
Full abstraction: how low should we go?
Wednesday, June 7 at 16:00, Amphi Kahn, by Frank Piessens (Katholieke Universiteit Leuven)
Attacks against application software happen in many cases at a lower level of abstraction than the application’s source code. Exploitation of buffer overflows, session hijacking, memory scanning malware, man-in-the-middle attacks and controlled channel attacks are some prominent examples: in each of these cases, the attacks rely on detailed aspects of the compiler and/or run-time infrastructure on which the application is executing and could be prevented by adequately hardening the execution infrastructure.
In this talk, I will discuss how one can specify formally the security requirements imposed on such execution infrastructure by using Martin Abadi’s insight that security of the translation of a high-level programming language to a lower-level language can be formalized by requiring that translation to be fully abstract.
Then I will go on to discuss our past and ongoing work of securing the execution infrastructure of imperative (C or Java-like) programs. In order to use full abstraction as a security objective, one should model the execution infrastructure as a compiler to a target level language, and an interesting question is how low-level that target language should be. I will discuss secure compilation to machine code with either Intel SGX style protection mechanisms, or support for capabilities, and I will illustrate that these target languages are not yet low enough to model relevant attacks that can be launched by a malicious operating system or hypervisor.