General Data Protection Regulation (GDPR)
Tuesday, February 26, 2019 at 15:00, room F321, by Cristiana Santos ( University of Toulouse)
General Data Protection Regulation (GDPR) in the new Data Protection Regulation in the EU that came in force on May 25, 2018. GDPR demands special restrictions on processing of personal data. In this talk, Cristiana will explain the definition of personal data, the legal basis of processing and the legal requirements on consent that have to be meet by data controllers and data processors.
Enforcing session integrity in the Wild Wild Web
Tuesday, February 5, 2019 at 14:00, room Conference room, I3S, by Stefano Calzavara ( Università Ca’ Foscari Venezia)
Web sessions allow users to get authenticated access to their favourite online services, like social networks, e-mail services and e-commerce websites. Unfortunately, web sessions are fragile and can be attacked at many different levels, leading to security flaws which can be as severe as account takeover. Automatically enforcing desirable security guarantees on web session implementations is an important research direction to make the Web a safer place, but it’s also an extremely hard task, given the highly heterogeneous nature of existing web applications. In this talk, I will present the most common attacks against web sessions and I will discuss automated solutions designed to detect and prevent such attacks, while dealing with the compatibility challenges inherent to the complexity of the modern Web.
The seminar organised by FORUM NUMERICA, UCAJEDI “Networks, Information and Digital Society” Academy.
Effective Visualization of Object Allocation Sites
Friday, December 21, 2018 at 11:00, room TBA, by Alexandre Bergel (University of Chili)
Profiling the memory consumption of a software execution is usually carried out by characterizing calling-context trees. However, the plurality nature of this data-structure makes it difficult to adequately and efficiently exploit in practice. As a consequence, most of anomalies in memory footprints are addressed either manually or in an ad-hoc way.
We propose an interactive visualization of the execution context related to object productions. Our visualization augments the traditional calling-context tree with visual cues to characterize object allocation sites. We performed a qualitative study involving eight software engineers conducting a software execution memory assessment. As a result, we found that participants find our visualization as beneficial to characterizing a memory consumption and to reducing the overall memory footprint.
INDES Workshop on Web Applications Security and Privacy
Testing for integrity flaws in web sessions
Monday, October 29, 2018 at 10:30, Euler Violet, by Stefano Calzavara (Università Ca’ Foscari Venezia)
Web sessions are fragile, they have been attacked at many different levels. Attacks against web session integrity are particularly concerning, because they allow the attacker to intrude on honest users’ sessions by forging requests which get authenticated on the victim’s behalf. We review existing countermeasures against such attacks, discussing subtle implementation pitfalls which may entirely void protection. We then propose convenient testing strategies to discover these bad implementation practices on existing websites, which we make available in a browser extension called Dredd. We use Dredd to assess the security of popular websites from the Alexa ranking, uncovering several new vulnerabilities.
Enforcing Content Security by Default within Web Browsers
Monday, October 29, 2018 at 11:00, Euler Violet, by Christoph Kerschbaumer (Mozilla Corporation)
Web browsers were initially designed to retrieve resources on the world wide web in a static manner such that adding security checks in select locations throughout the codebase sufficiently provided the necessary security guarantees of the web. Even though systematic security checks were always performed,those security checks were sprinkled throughout the codebase. Over time, various specifications for dynamically loading content have proven that such a scattered security model is error-prone. Instead of opting into security checks wherever resource loads are initiated throughout the codebase, we present an approach where security checks are performed by default. By equipping every resource load with a loading context (which includes information about who initiated the load, the load type, etc.), our approach enforces an opt-out security mechanism performing security checks by default by consulting a centralized security manager. In addition, the added load context allows to provide the same security guarantees for resource loads which encounter a server-side redirect.
TBA
Monday, October 29, 2018 at 11:00, Euler Violet, by Andrei Sabelfeld (Chalmers University of Technology )
Past Sessions
Journey to Find Bugs in JavaScript Web Applications in the Wild
Friday, April 13, 2018 at 11:00, Euleur Bleu, by Suykung Yu (KAIST)
Analyzing real-world JavaScript web applications is a challenging task. On top of understanding the semantics of JavaScript, it requires modeling of web documents, platform objects, and interactions between them. Not only the JavaScript language itself but also its usage patterns are extremely dynamic. JavaScript can generate code and run it during evaluation, and most web applications load JavaScript code dynamically.
Such dynamic characteristics of JavaScript web applications make pure static analysis approaches inapplicable.
In this talk, we present our attempts to analyze JavaScript web applications in the wild mostly statically using various approaches. From pure JavaScript programs to JavaScript web applications using platform-specific libraries and dynamic code loading, we explain technical challenges in analyzing each of them and how we built an open-source analysis framework for JavaScript, SAFE, that addresses the challenges incrementally.
In spite of active research accomplishments in analysis of JavaScript web applications, many issues still remain to be resolved such as events, callback functions, and hybrid web applications. We discuss possible future research directions and open challenges.
The Racket Way
Friday, April 6, 2018 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, 2018 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.
HipHop.js
Friday, April 6, 2018 at 14:00, Euler Violet, by Colin Vidal (Inria INDES)
Web applications are characterized by rich and persistent interactions between users and distant services, which involve a wide variety of asynchronous events that applications must handle. This orchestration problem is known to be difficult, especially when JavaScript callbacks are the only available tool.
In this talk, I will present the Hiphop.js domain-specific language which is designed to orchestrate web applications. It is a JavaScript- based Esterel implementation variant that is adapted to the web with full compatibility with JavaScript and support for run-time dynamicity.
Massively Interactive Music (MMI)
Friday, April 6, 2018 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, 2018 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, 2018 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.
Deciding Indistiguishability
Wednesday, April 4, 2018 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, 2018 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, 2018 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.
HDR Jury:
- 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, 2017 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, 2017 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, 2017 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, 2017 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, 2017 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.
