3.1 Parallelism, concurrency, and distribution

Concurrency management is at the heart of diffuse programming. Since the execution platforms are highly heterogeneous, many different concurrency principles and models may be involved. Asynchronous concurrency is the basis of shared-memory process handling within multiprocessor or multicore computers, of direct or fifo-based message passing in distributed networks, and of fifo- or interrupt-based event handling in web-based human-machine interaction or sensor handling. Synchronous or quasi-synchronous concurrency is the basis of signal processing, of real-time control, and of safety-critical information acquisition and display. Interfacing existing devices based on these different concurrency principles within Hop or other diffuse programming languages will require better understanding of the underlying concurrency models and of the way they can nicely cooperate, a currently ill-resolved problem.

3.2 Web, functional, and reactive programming

We are studying new paradigms for programming Web applications that rely on multi-tier functional programming. We have created a Web programming environment named Hop. It relies on a single formalism for programming the server-side and the client-side of the applications as well as for configuring the execution engine.

Hop is a functional language based on the Scheme programming language. That is, it is a strict functional language, fully polymorphic, supporting side effects, and dynamically type-checked. Hop is implemented as an extension of the Bigloo Scheme compiler that we develop. In the past, we have extensively studied static analyses (type systems and inference, abstract interpretations, as well as classical compiler optimizations) to improve the efficiency of compilation in both space and time.

As a Hop DSL, we have created HipHop, a synchronous orchestration language for web and IoT applications. HipHop facilitates the design and programming of complex web/IoT applications by smoothly integrating three computation models and programming styles that have been historically developed in different communities and for different purposes: i) Transformational programs that simply compute output values from input values, with comparatively simple interaction with their environment; ii) asynchronous concurrent programs that perform interactions between their components or with their environment with uncontrollable timing, using typically network-based communication; and iii) synchronous reactive programs that react to external events in a conceptually instantaneous and deterministic way.

3.3 Security of diffuse programs

The main goal of our security research is to provide scalable and rigorous language-based techniques that can be integrated into multi-tier compilers to enforce the security of diffuse programs. Research on language-based security has been carried on before in former Inria teams. In particular previous research has focused on controlling information flow to ensure confidentiality.

Typical language-based solutions to these problems are founded on static analysis, logics, provable cryptography, and compilers that generate correct code by construction. Relying on the multi-tier programming language Hop that tames the complexity of writing and analysing secure diffuse applications, we are studying language-based solutions to prominent web security problems such as code injection and cross-site scripting, to name a few.

4.1 Web

The Web is the natural application domain of the team. We are designing and implementing multitier languages for helping the development of Web applications. We are creating static and dynamic analyses for Web security. We are conducting empirical studies about privacy preservation on the Web.

4.2 Internet of Things

More recently, we have started focusing on Internet of Things (IoT) applications. They share many similarities with Web applications so most of the methodologies and expertises we have developed for the Web apply to IoT but the restricted hardware resources made available by many IoT devices demand new developments and new research explorations.

5.1 Awards

• Bertrand Petit and Manuel Serrano received the Reviewers' Choice Award  16 of the Programming Journal for their work on interactive music using reactive programming languages.
• Tamara Rezk and her coauthors outside Indes received a honorable mention from Intel: the Intel Security Award 2021 for her work done in 2020 on microarchitectural semantics  14.

6.1 New software

7.1 Web Reactive Programming

Participants: Jayanth Krishnamurthy, Manuel Serrano.

Computer systems that react continuously to their environment at a rate set by the environment form a class of the so-called reactive systems. They differ from classical computing systems which takes the input at the start of execution and produce output before terminating. Furthermore, they also differ from traditional interactive systems like operating systems which endlessly interact with their environment at their own speed (in contrast to the speed determined by the environment). A reactive system can be perceived as a black box that perpetually receives some input events as external stimuli and reacts to them by producing some output events as their behavior. This output may successively affect the production of later stimuli by the environment.

HipHop, which is the language used in this study is based on Esterel's semantics. It is a synchronous reactive DSL for JavaScript, built on top of Hop.js for applying the Esterel programming model to the world of web and IoT where programs are sent over networks. HipHop can be used to develop complex web application interfaces and IoT controllers, which are dynamic in nature. HipHop blends Esterel's synchrony with JavaScript's asynchrony, simplifying the cooperation between synchronous and asynchronous activities that are typical in these application domains. HipHop differs from Esterel in having its own syntax and programming model adapted to the web. For example, HipHop supports partial reconfiguration of programs between two synchronous reactions, while maintaining consistency of the control state.

The expressiveness and the flexibility of Esterel dialects come with a downside: the debugging, and more precisely the error reporting is difficult because errors detected by the runtime system are loosely connected with locations in the program source code. This is a major difficulty, especially for programmers not deeply accustomed with the programming model. Improving the error messages the compiler and the runtime system report is then a major issue and is the subject of ongoing researches in the team. This year we have developed and implemented a technique that isolates the fragments of the program that are responsible for an error when it occurs. The technique we propose applies to the compilation technique HipHop uses to transform a source program into an equivalent electric circuit using techniques developed for the Esterel programming language. The improved error messages are built by isolating parts in the generated circuit - minimizing the size of causality error cycles using an iterative process.

The method of causality error analysis and debugging proceeds by building on classical graph algorithms, which are applied to the graph of nets composing the circuit generated by the HipHop compiler. This enables programmers to narrow down to smaller error positions in source code. We have shown the results and advantages of application of our debugging approach in a real life project developed using HipHop. This work has been presented at the Principles and Practice of Declarative Programming conference 5.

7.2 Implementation of Dynamic Languages

Participants: Manuel Serrano.

Dynamic languages are particularly difficult to implement efficiently because most of their expressions have all sorts of different meanings that involve all sorts of different executions that are not distinguished by any syntactic or type annotation. For instance considering JavaScript, “obj.prop” might i) fetch property prop from obj, ii) scan the linked list of obj's prototype chain and fetch prop from another object, iii) call a user defined function if prop is an accessor, iv) allocate a fresh object if obj is a primitive value, or v) evaluate yet another user function if obj is a proxy object. Checking all the possible interpretations and executing the appropriate one literally, that is treating the language specification as an algorithm, delivers unacceptably slow performance. All fast implementations use alternative strategies. Amongst all the possible interpretations, they favor the one that corresponds to the most frequent situation, for which they elaborate a faster execution plan, and, as importantly, for which they elaborate a fast guard that ensures the preservation of the language semantics. Typically, that is what inline caches and hidden classes achieve. Using a single test, the comparison of the object's hidden class with the inline cache, we know if the property is to be read directly from the object and, if so, at which offset. The common intuition is that only dynamic compilers, a.k.a., JIT compilers, can handle dynamic languages efficiently because this heuristic-based strategy requires having the program and the data on hand in order to generate efficient code. We view this position as too extreme, as it is oblivious to other characteristics of static compilers (AoT) that might make them competitive.

• AoT compilers can allocate conceptually infinite resources for analyzing and optimizing the program because they run before execution. This opens opportunities to conceive and deploy new optimizations that are out of reach of JIT compilers for which compilation time and compilation resource consumption matter.
• AoT compilers are efficient even for brief executions while JIT compilers need the execution to last sufficiently long to benefit from gathered profiled data. This should give AoT compilers an advantage for executing programs such as shell commands or cloud computing microservices.
• New techniques have been proposed to adapt JIT-style heuristics-based approach to AoT compilation. These studies have shown that if indeed a JavaScript expression involves many different interpretations, typically only one is used over and over again and guessing it before the execution is not too difficult.

As few are committed to developing optimizing AoT JavaScript compilers, we rely too heavily on our intuition to answer the question whether AoT compilers can deliver performance comparable to JIT compilers. To provide the elements of a proper scientific comparison, we have built Hopc, an AoT compiler for JavaScript. We have compared its performance with those of production JIT compilers and we have shown that on many new tests, its performance is close to those of JIT compilers 1. We read this as a strong indication that an AoT compiler that optimizes the whole core language and the whole set of libraries could compete with the fastest JIT compilers. We intend to pursue this exploration in the coming years.

7.3 Session Types

Participants: Ilaria Castellani.

Session types describe communication protocols involving two or more participants by specifying the sequence of exchanged messages and their functionality (sender, receiver and type of carried data). They may be viewed as the analogue, for concurrency and distribution, of data types for sequential computation. Originally conceived as a static analysis technique for an enhanced version of the $\pi$-calculus, session types have been subsequently embedded into a range of functional, concurrent, and object-oriented programming languages.

The aim of session types is to ensure safety properties for sessions, such as the absence of communication errors (no type mismatch in exchanged data) and deadlock-freedom (no standstill until all participants are terminated). Multiparty session types often target also the liveness property of progress or lock-freedom (no participant waits forever), which is stronger than deadlock-freedom.

While binary sessions can be described by a single session type, multiparty sessions require two kinds of types: a global type that describes the whole session protocol, and local types that describe the individual contributions of the participants to the protocol. The key requirement to achieve safety properties such as deadlock-freedom is that the local types of the processes implementing the participants be obtained as projections from the same global type. To ensure progress, global types must satisfy additional well-formedness requirements.

What makes session types particularly attractive is that they offer several advantages at once: 1) static safety guarantees, 2) automatic check of protocol implementation correctness, based on local types, and 3) a strong connection with linear logics and with concurrency models such as communicating automata, graphical choreographies and message-sequence charts.

During the past year we have further investigated the relationship between multiparty session types and concurrency models, focussing on Event Structures  17, a canonical model for concurrent computation. As most of our previous work on this subject, this research has been pursued in collaboration with colleagues from the Universities of Eastern Piedmont and Turin.

7.4 Micro-architectural attacks

Participants: Lesly-Ann Daniel, Tamara Rezk.

Previously, in 2020, we had developed an analyzer for constant-time called Binsec/Rel. Binsec/Rel analyses timing-leaks attacks. These attacks can be captured via a security property called constant-time, which states that the execution time of an application does not depend on the dynamic path of the execution. Our analyzer works at binary-level and is based on symbolic execution with dedicated optimizations for constant-time analysis. In particular, we complement relational symbolic execution with a new on-the-fly simplification to maximize sharing in the memory and formally prove that our analysis is correct for bug-finding and bounded-verification. In 2021, we extended this analyzer to handle microarchitectural attacks. The new analyzer is called Binsec/Haunted 3. We first modeled the semantics of hardware with microarchitectural features to model timing-side channels and attacks such as Spectre that can be used e.g., in the cloud, to learn all kind of confidential information from the cloud's customers. Our obtained hardware semantics supports out-of-order and speculative execution by modeling reorder buffers and transient instructions, respectively. It assumes that attackers have complete control over microarchitectural features (e.g., the branch target predictor), and uses adversarial execution directives to model the adversarys control over predictors. The Binsec/Haunted analyzer was based on this semantics and scales to detect Spectre-PHT vulnerabilities in binaries of cryptographic libraries. It also works for Spectre-STL attacks and helped to uncover inconsistencies between different Spectre defenses. The analyzers have helped to disclose that popular compilers cannot be trusted to preserve constant-time and that popular counter-measures for Spectre vulnerabilities may also introduce other variants of the vulnerability. Binsec/Rel and Binsec/Haunted constitute the contributions in the PhD thesis of Lesly-Ann Daniel, who defended on November 12th, 2021. We have also worked in adding phases to the Jazmin compiler in order to obtain code certified as free of Spectre PHT and STL attacks. Our works on microarchitectural attacks have been presented in major security conferences 3, 2.

7.5 JavaScript security

Participants: Yoonseok Ko, Heloise Maurel, Tamara Rezk, Manuel Serrano.

Previously to 2021, we developed a compiler, called Mashic, that takes a client-side web application as input to transform it in such a way that gadgets are included with iframes. The guarantees of the compiler are: if the gadget is not malicious, then the functionality of the compiled code is the same as the original one. If the mashup is malicious, all the attacks are neutralized and left with no effect on trusted code. During the current period, with the intention of obtaining a compiler applicable to IoT applications, we have generalized the Mashic compiler to be independent from the browsers and, in particular, of any browser built-in isolation mechanisms. We called the generalization SecureJS 4, and it can used for JavaScript running in IoT devices. SecureJS passes the test suites of the ECMAScript5 specification in diverse JavaScript engines such as V8, Hop, and JerryScript. As a continuation of this work, we have studied more flexible JavaScript security policies, in particular a security policy that will allow us to express sharing of JavaScript objects via declassification. This kind of policies can be implemented for example by membrane patterns from the object capability model and could be used to prove formally the security property that the secure subset of EcmaScript provides. We also studied JavaScript and PHP security by means of analyzers to detect XSS vulnerabilities using neural networks 6. We compare two different code representations based on Natural Language Processing (NLP) and Programming Language Processing (PLP) and experiment with models based on different neural network architectures for static analysis detection of vulnerabilities in PHP and Node.js. We train and evaluate the models using synthetic databases. Using the generated PHP and Node.js databases, we compare our results with a well-known static analyzer for PHP code, ProgPilot, and a known scanner for Node.js, AppScan static mode. Our analyzers using neural networks overcome the results of existing tools in all cases but are limited to only a reduced number of lines of code.

8.1 International initiatives

8.2 European initiatives

8.3 National initiatives

9.1 Promoting scientific activities

Tamara Rezk gave a talk for undergraduates at University of Córdoba in May 2021 to promote scientific careers.

9.2 Teaching - Supervision - Juries

10.1 Publications of the year

10.2 Cited publications

• 13 inproceedingsG.Gérard Boudol and I.Ilaria Castellani. Permutation of transitions: an event structure semantics for CCS and SCCS.REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency354LNCSSpringer1988, 411--427
  back to text
• 14 inproceedingsS.Sunjay Cauligi, C.Craig Disselkoen, K. V.Klaus V. Gleissenthall, D.Dean Tullsen, D.Deian Stefan, T.Tamara Rezk and G.Gilles Barthe. Constant-Time Foundations for the New Spectre Era.2020 Programming Language Design and Implementation (PLDI'20)PLDI '20London, United Kingdom2020, URL: https://hal.inria.fr/hal-03141383
  back to text
• 15 articleM.Mogens Nielsen, G.Gordon Plotkin and G.Glynn Winskel. Petri Nets, Event Structures and Domains, Part I.Theoretical Computer Science1311981, 85--108
  back to textback to text
• 16 articleB.Bertrand Petit and M.Manuel Serrano. Skini:Reactive Programming for Interactive Structured Music.The Art, Science, and Engineering of ProgrammingJune 2020
  HALback to text
• 17 inproceedingsG.G. Winskel. An introduction to event structures.REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency354LNCSHeidelbergSpringer1988, 364--397
  back to text
• 18 phdthesisG.G. Winskel. Events in Computation.University of Edinburgh1980
  back to textback to text