6.2.1 Bigloo

• Keyword: Compilers
• Functional Description: Bigloo is a Scheme implementation devoted to one goal: enabling Scheme based programming style where C(++) is usually required. Bigloo attempts to make Scheme practical by offering features usually presented by traditional programming languages but not offered by Scheme and functional programming. Bigloo compiles Scheme modules. It delivers small and fast stand alone binary executables. Bigloo enables full connections between Scheme and C programs, between Scheme and Java programs.
• Release Contributions: modification of the object system (language design and implementation), new APIs (alsa, flac, mpg123, avahi, csv parsing), new library functions (UDP support), new regular expressions support, new garbage collector (Boehm's collection 7.3alpha1).
• URL: http://www-sop.inria.fr/teams/indes/fp/Bigloo/
• Contact: Manuel Serrano
• Participant: Manuel Serrano

6.2.2 Hop

• Keywords: Programming language, Multimedia, Iot, Web 2.0, Functional programming
• Scientific Description:

  The Hop programming environment consists in a web broker that intuitively combines in a single architecture a web server and a web proxy. The broker embeds a Hop interpreter for executing server-side code and a Hop client-side compiler for generating the code that will get executed by the client.

  An important effort is devoted to providing Hop with a realistic and efficient implementation. The Hop implementation is validated against web applications that are used on a daily-basis. In particular, we have developed Hop applications for authoring and projecting slides, editing calendars, reading RSS streams, or managing blogs.

• Functional Description: Multitier web programming language and runtime environment.
• URL: http://hop.inria.fr
• Contact: Manuel Serrano
• Participant: Manuel Serrano

6.2.3 IFJS

• Name: Infomation Flow monitor inlining for JavaScript
• Keyword: Cybersecurity
• Functional Description: The IFJS compiler is applied to JavaScript code. The compiler generates JavaScript code instrumented with checks to secure code. The compiler takes into account special features of JavaScript such as implicit type coercions and programs that actively try to bypass the inlined enforcement mechanisms. The compiler guarantees that third-party programs cannot (1) access the compiler internal state by randomizing the names of the resources through which it is accessed and (2) change the behaviour of native functions that are used by the enforcement mechanisms inlined in the compiled code.
• URL: http://www-sop.inria.fr/indes/ifJS/
• Contact: Tamara Rezk

6.2.4 Hiphop.js

• Name: Hiphop.js
• Keywords: Web 2.0, Synchronous Language, Programming language
• Functional Description: HipHop.js is an Hop.js DLS for orchestrating web applications. HipHop.js helps programming and maintaining Web applications where the orchestration of asynchronous tasks is complex.
• URL: http://hop-dev.inria.fr/hiphop
• Contacts: Manuel Serrano, Gérard Berry

6.2.5 Server-Side Protection against Third Party Web Tracking

• Keywords: Privacy, Web Application, Web, Architecture, Security by design, Program rewriting techniques
• Functional Description:

  We present a new web application architecture that allows web developers to gain control over certain types of third party content. In the traditional web application architecture, a web application developer has no control over third party content. This allows the exchange of tracking information between the browser and the third party content provider.

  To prevent this, our solution is based on the automatic rewriting of the web application in such a way that the third party requests are redirected to a trusted third party server, called the Middle Party Server. It may be either controlled by a trusted party, or by a main site owner and automatically eliminates third-party tracking cookies and other technologies that may be exchanged by the browser and third party server

• URL: http://www-sop.inria.fr/members/Doliere.Some/essos/
• Contact: Francis Doliére Some

6.2.6 webstats

• Name: Webstats
• Keywords: Web Usage Mining, Statistic analysis, Security
• Functional Description: The goal of this tool is to perform a large-scale monthly crawl of the top Alexa sites, collecting both inline scripts (written by web developers) and remote scripts, and establishing the popularity of remote scripts (such as Google Analytics and jQuery). With this data, we establish whether the collected scripts are actually written in a subset of JavaScript by analyzing the different constructs used in those scripts. Finally, we collect and analyze the HTTP headers of the different sites visited, and provide statistics about the usage of HTTPOnly and Secure cookies, and the Content Security Policy in top sites.
• URL: https://webstats.inria.fr
• Contacts: Francis Doliére Some, Tamara Rezk, Nataliia Bielova

6.2.7 Skini

• Name: Platform for creation and execution for audience participative music
• Keywords: Music, Interaction, Web Application, Synchronous Language
• Functional Description: Skini is a platform form designing et performing collaborative music. It is based on two musical concept: pattern and orchestration. The orchestration is design using HipHop.js.
• Release Contributions: Can be use for performance and création.
• Contact: Bertrand Petit

7.2.1 HipHop.js

HipHop is a reactive JavaScript DSL on Hop. In the domain of reactive programming, causality errors - wherein a signal's presence/absence may depend circularly on another signal giving rise to causality issues. Before the discussed work started on the HipHop compiler, the support by the HipHop run-time for causality errors was limited to pointing out the presence of causal dependencies as an error during a reaction by the HipHop machine and rejection of the program. Our work started on providing a more elaborate debugging support for HipHop programmers.

HipHop and HipHop applications have been published in a conference paper this year 14.

This year, we have completed the implementation of the HipHop.js web reactive synchronous language and we have mainly focused our effort on the programming and debugging environment.

Once the run-time rejects a program due to causality error, the HipHop program which is compiled into set of nets called net-list, will have the nets that are not participating in a reaction. We take these nets as a digraph and proceed with Depth First search algorithm to identify strongly connected components among them using Tarjan's algorithm. The nets in strongly connected components are the ones participating in Causal cycles. Further, since a strongly connected component can have smaller sub components which are strongly connected, we used the technique proposed by F. Bourdoncle to further refine the strongly connected components to smaller sub components pointing to smallest causality cycle that can be easily managed by the programmer. We take these smallers subcomponents and process the information available in the nets to identify and point out the source locations that are contributing to causality errors. The programmers can resolve these smaller cycles and then incrementally identify next bigger cycle if any. Once the cycle locations are identified, we presented their locations with visual markers on Emacs editor. Further, this approach was extended to popular IDEs like Vscode and Atom editors. We are preparing a research paper that will describe this work.

Recently visual programming tool kits like Blockly have become very popular with non - cs background programmers. We are extending HipHop programming to Blockly so that musicians can use HipHop for interactive music generation. We intend to bring in the causality debugging support to Blockly programmers as a future work.

7.2.2 Interactive Music Composition

Skini is a programming methodology and an execution environment for interactive structured music. With this system, the composer programs his scores in the HipHop synchronous reactive language. They are then executed, or played, in live concerts, in interaction with the audience. The system aims at helping composers to find a good balance between the determinism of the compositions and the nondeterminism of the interactions with the public. Each execution of a Skini score yields to a different but aesthetically consistent interpretation.

This work raises many questions in the musical fields. How to combine composition and interaction?How to control the musical style when the audience influences what is to play next?What are the possible connections with generative music? These are important questions for the Skini system but they are out of the scope of this work that focuses exclusively on the computer science aspects of the system. From that perspective, the main questions are how to program the scores and in which language? General purpose languages are inappropriate because their elementary constructs (i.e., variables, functions, loops, etc.) do not match the constructions needed to express music and musical constraints. We show that synchronous programming languages are a much better fit because they rely on temporal constructs that can be directly used to represent musical scores and because their malleability enables composers to experiment easily with artistic variations of their initial scores.

We have published a journal paper 12 that focuses on scores programming. It exposes the process a composer should follow from his very first musical intuitions up to the generation of a musical artifact. The paper presents some excerpts of the programming of a classical music composition that it then precisely relates to an actual recording. Examples of techno music and jazz are also presented, with audio artifact, to demonstrate the versatility of the system. Finally, brief presentations of past live concerts are presented as an evidence of viability of the system. A second paper  17 focuses on the production of generative music with Skini.

7.3.1 Multiparty Sessions with Internal Delegation

We have investigated a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. In this view, delegation is an inter-session mechanism which requires session interleaving. Hence it falls outside the descriptive power of global types, which specify single multiparty sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. In our work, we adopt a different view of delegation, by allowing participants to delegate tasks to each other within the same multiparty session. This way, delegation occurs within a single session (whence the name “internal delegation”) and may be captured by its global type. We present a session type system based on global types with internal delegation, and show that it ensures the usual safety properties of multiparty sessions, together with a progress property.

This work has been published in a special issue of the journal Theoretical Computer Science dedicated to Maurice Nivat 11.

7.3.2 Global Types and Event Structure Semantics for Asynchronous Multiparty Sessions

In previous work we explored the relationship between synchronous multiparty sessions and Event Structures (ESs), a well-known concurrency model introduced in the early 80's. We considered a core multiparty session calculus where sessions are described as networks of sequential processes (each process implementing a participant), equipped with standard global types. We proposed an interpretation of networks as Flow Event Structures (FESs), a subclass of Winskel's Stable Event Structures, as well as an interpretation of global types as Prime Event Structures (PESs), the simplest class of ESs. Since the syntax of global types does not allow all the concurrency among communications to be explicitly represented, the events of the associated PES need to be defined as equivalence classes of communication sequences up to permutation equivalence. We showed that when a network is typable by a global type, the FES semantics of the former is equivalent, in a precise technical sense, to the PES semantics of the latter.

In the work 21, we undertake a similar endeavour in the asynchronous setting. This involves devising a new notion of global type for asynchronous sessions. The type system for asynchronous sessions is expected to be more permissive than the one for synchronous sessions. For instance, consider a session with two participants each of which wishes to first send a message to the other one and then receive a message from the other one. This session is stuck if communication is synchronous but not if communication is asynchronous.

We start by considering a core session calculus as in the synchronous case, where networks are endowed with a queue and they act on this queue by performing outputs or inputs: an output stores a message in the queue, while an input fetches a message from the queue. The intuition for our new asynchronous global types is quite simple: to split communications in the type into outputs and inputs, and to equip the type with a queue, thus mimicking very closely the behaviour of asynchronous networks. The well-formedness conditions for global types must now take into account also the content of the queue. Essentially, this amounts to requiring that each input appearing in the type be justified by a preceding output in the type or by a message in the queue, and vice versa, that each output in the type or message in the queue be matched by a corresponding input in the type.

The contribution of 21 is twofold: 1) We propose an original type system for asynchronous multiparty sessions, which accounts for asynchronous communication in a more natural way than existing approaches, while remaining decidable. Our type system ensures the classical safety properties of sessions as well as progress; 2) We present an Event Structure semantics for asynchronous sessions and for asynchronous global types, and we show that these two semantics agree.

This paper has been submitted for journal publication.

7.5.1 ClockworK: Timing Leaks in popular IoT application platforms

This work focuses on timing leaks under remote execution. A key difference is that the remote attacker does not have a reference point of when a program run has started or finished, which significantly restricts attacker capabilities. We propose an extensional security characterization that captures the essence of remote timing attacks. We identify patterns of combining clock access, secret branching, and output in a way that leads to timing leaks. Based on these patterns, we design Clockwork, a monitor that rules out remote timing leaks. We implement the approach for JavaScript, leveraging JSFlow, a state-of-the-art information flow tracker. We demonstrate the feasibility of the approach on case studies with IFTTT, a popular IoT app platform, and VJSC, an advanced JavaScript library for e-voting.

7.5.2 Spectre attacks

The constant-time programming discipline (CT) is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of microarchitectural attacks makes constant-time as it exists today far less useful. This work lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries

7.5.3 Binsec/Rel

Writing CT code is challenging as it demands to reason about pairs of execution traces (2- hypersafety property) and it is generally not preserved by the compiler, requiring binary-level analysis. Unfortunately, current verification tools for CT either reason at higher level (C or LLVM), or sacrifice bug-finding or bounded-verification, or do not scale. We tackle the problem of designing an efficient binary-level verification tool for CT providing both bug-finding and bounded-verification. The technique builds on relational symbolic execution enhanced with new optimizations dedicated to information flow and binary-level analysis, yielding a dramatic improvement over prior work based on symbolic execution. We implement a prototype, BINSEC/REL, and perform extensive experiments on a set of 338 cryptographic implementations, demonstrating the benefits of our approach in both bug-finding and bounded-verification. Using BINSEC/REL, we also automate a previous manual study of CT preservation by compilers. Interestingly, we discovered that gcc -O0 and backend passes of clang introduce violations of CT in implementations that were previously deemed secure by a state-of-the-art CT verification tool operating at LLVM level, showing the importance of reasoning at binary-level.

9.1.1 Inria associate team not involved in an IIL

9.1.2 Inria international partners

We are collaborating with Universidad de Chile (Santiago Chile) and Universidad Nacional del Centro de la Provincia de Buenos Aires (Argentina) on the Detection strategies based on Software Metrics for Multitier JavaScript. Our main collaborators are Alexandre Bergel and Santiago Vidal. This project was due to end in 2019 but because of the political situation in Chile first, and Covid second, we have had to suspend our collaboration for two years. We hope we will be able this year to complete the initiated studies. If the context permit, M. Serrano will visit A. Bergel in December 2021. In the meantime S. Vidal collaborates with T. Rezk and H. Maurel.

9.2.1 FP7 & H2020 Projects

9.3.1 ANR CISC

The CISC project (Certified IoT Secure Compilation) is funded by the ANR for 42 months, starting in April 2018. The goal of the CISC project is to provide strong security and privacy guarantees for IoT applications by means of a language to orchestrate IoT applicatoins from the microcontroller to the cloud. Tamara Rezk coordinates this project, and Manuel Serrano, Ilaria Castellani and Nataliia Bielova participate in the project. The partners of this project are Inria teams Celtique, Indes and Privatics, and Collège de France.

9.3.2 ANR PrivaWeb

The PrivaWeb project (Privacy Protection and ePrivacy Compliance for Web Users) is funded by the ANR JCJC program for 48 months, started in December 2018. PrivaWeb aims at developing new methods for detection of new Web tracking technologies and new tools to integrate in existing Web applications that seamlessly protect privacy of users.

Nataliia Bielova (PRIVATICS project-team) coordinates this project.

9.3.3 PIA ANSWER

The ANSWER project (Advanced aNd Secured Web Experience and seaRch) is funded by PIA program for 36 months, starting January 1, 2018. The aim of the ANSWER project is to develop the new version of the http://www.qwant.com search engine by introducing radical innovations in terms of search criteria as well as indexed content and users’ privacy. The partners of this project include QWANT and Inria teams Wimmics, Indes, Neo and Diana.

10.1.1 Scientific Events: Organisation

• Tamara Rezk organized the 2020 Shonan meeting 159 on Web Security, together with Limin Jia (Carnegie Melon University) and Sukyoung Ryu (KAIST), inviting experts in web security from academy and industry. The meeting was canceled a week before its date due to COVID and moved to March 2022;

10.1.2 Invited Talks

• Manuel Serrano gave a keynote conference at the FDL conference about Web Reactive Programming and HipHop.js (http://www.fdl-conference.org/).

10.1.3 Leadership within the Scientific Community

• Ilaria Castellani was the chair of the IFIP TC1 WG 1.8 on Concurrency Theory from June 2014 to December 2020. http://www.ifip-tc1.org/

  https://concurrency-theory.org/organizations/ifip

• Tamara Rezk is a member of the Steering Committee of the PriSC workshop.

10.1.4 Research Administration

• Manuel Serrano is vice-head of the Inria Evaluation Committee. As such he co-organizes all the grants, promotions juries and the juries of the national recruiting campaigns. He also co-organizes all the team evaluation seminars.
• Ilaria Castellani was the chair of the “jury d'admissibilité” for the recruitment of junior researchers in the INRIA Centre of Grenoble Rhône Alpes.
• Ilaria Castellani is a member of INRIA’s “Comité Parité et Égalité des Chances”. In the Centre of INRIA Sophia Antipolis, she is a member of the “Comité Scientifique du Colloquium”. Within UCA (Université Côte d'Azur), she is a member of the organising committee of the “Forum Numerica” seminar series.

10.2.1 Teaching

• Tamara Rezk taught two courses (master level) at University of Nice-Sophia Antipolis: Web Security (28 ETD) and Cryptographic proofs (28 ETD).

10.2.2 Supervision

• Postdoc: Yoon Seok Ko, Secure JavaScript, 1/10/2018-, Tamara Rezk, Manuel Serrano.
• PhD in progress: Jayanth Krishnamurthy, Secure Reactive Web Programming, 12/09/2018, Manuel Serrano.
• PhD in progress: Bertrand Petit, Musique Massivement Interactive, 12/09/2017, Manuel Serrano. PhD defended in July 2020.
• PhD in progress : Héloïse Maurel, Statically Identifying Security Vulnerabilities using Deep Learning 1/10/2018, Tamara Rezk
• PhD in progress : Mohamad Ellaz, Implementation and analysis of cryptographic libraries, 1/12/2017, Benjamin Grégoire and Tamara Rezk
• PhD in progress : Lesly-Ann Daniel, Security analysis of binary code, 1/10/2018, Sébastien Bardin and Tamara Rezk
• PhD in progress : Adam Khayam, Semantics of Multitier Languages, 1/07/2019, Alan Schmitt and Tamara Rezk
• PhD in progress: Ignacio Tiraboschi, Analysis for IoT Security, Xavier Rival and Tamara Rezk

10.2.3 Juries

• Tamara Rezk was a jury member of the national Inria competition CRCN/ISFP 2020.
• Tamara Rezk was a Phd jury member (Rapporteur) of Sebastian Poeplau (supervisor: Aurélien Francillon), EURECOM, 2020.

10.3.1 Internal or external Inria responsibilities

• Tamara Rezk was part of the Editorial Board of the blog Binaire of Le Monde.

International journals

• 11 articleIlariaI. Castellani, MariangiolaM. Dezani-Ciancaglini, PaolaP. Giannini and RossR. Horne. Global types with internal delegationTheoretical Computer Science807February 2020, 26
  HALDOIback to text
• 12 article BertrandB. Petit and ManuelM. Serrano. Skini:Reactive Programming fo Interactive Structured Music The Art, Science, and Engineering of Programming June 2020
  HAL back to text

International peer-reviewed conferences

• 13 inproceedings IuliaI. Bastys, MussardM. Balliu, TamaraT. Rezk and AndreiA. Sabelfeld. Clockwork: Tracking Remote Timing Attacks In Proceedings of the IEEE Computer Security Foundations Symposium (CSF) Virtual, France June 2020
  HAL
• 14 inproceedingsGérardG. Berry and ManuelM. Serrano. HipHop.js: (A)Synchronous reactive web programmingPLDI '20 - 41st ACM SIGPLAN International Conference on Programming Language Design and ImplementationLondon UK, United KingdomJuly 2020, 533-545
  HALDOIback to text
• 15 inproceedingsMohamadM. El Laz, BenjaminB. Grégoire and TamaraT. Rezk. Security Analysis of ElGamal Implementations17th International Conference on Security and CryptographyLieusaint - Paris, FranceJuly 2020, 310-321
  HALDOI
• 16 inproceedingsManuelM. Serrano and Robert BruceR. Findler. Dynamic property caches: a step towards faster JavaScript proxy objectsCC '20 - 29th International Conference on Compiler ConstructionSan Diego CA, United StatesFebruary 2020, 108-118
  HALDOIback to text

Conferences without proceedings

• 17 inproceedings BertrandB. Petit and ManuelM. Serrano. Generative Music Using Reactive Programming International Computer Music Conférence Santiago, Chile July 2021
  HAL back to text

Doctoral dissertations and habilitation theses

• 18 thesis BertrandB. Petit. Time and duration : from synchronous reactive programming to music composition Université Côte d'Azur July 2020
  HAL

Reports & preprints

• 19 report AnneA. Canteaut, Miguel AngelM. Fernández, LucL. Maranget, SophieS. Perin, MarioM. Ricchiuto, ManuelM. Serrano and EmmanuelE. Thomé. Évaluation des Logiciels Inria January 2021
  HAL
• 20 report AnneA. Canteaut, Miguel AngelM. Fernández, LucL. Maranget, SophieS. Perin, MarioM. Ricchiuto, ManuelM. Serrano and EmmanuelE. Thomé. Software Evaluation Inria January 2021
  HAL
• 21 misc IlariaI. Castellani, MariangiolaM. Dezani-Ciancaglini and PaolaP. Giannini. Global types and event structure semantics for asynchronous multiparty sessions February 2021
  HAL back to text back to text