-
Mitchell Gerrard (LSL),
Alternating Conditional Analysis
le
Abstract We rely on safety-critical software, so judging its correctness is important. If a pacemaker exhibits buggy behavior, just how buggy is it? Will a patch to some bug also patch other program paths that lead to the same bug? How could we guarantee this? In this talk I will... suite >>
-
Tomáš Dacík (Université Paris-Saclay, LMF),
Deciding Boolean Separation Logic via Small Models and Translation to SMT
le
Abstract In this talk, I will present a decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. The method is based on a model-based translation... suite >>
-
Sébastien Patte (LSL),
Typestates Specification and Verification in Frama-C
le
Abstract Critical software systems need strong safety and security guarantees, since a bug can have very bad consequences. Thus, we need powerful verification techniques, such as formal methods, to assess such systems. Frama-C is an Open-Source platform for formal analysis of C code. It comes with ACSL, a specification language... suite >>
-
Kim Quyen Ly,
Static Analysis in KaSa
le
Abstract This work (2015–2018) advances static analysis in Kappa and its analyzer, KaSa, improving model verification without full simulation. Kappa models biochemical interactions via site-graph rewriting, while KaSa ensures correctness and detects errors. We develop two key techniques: Local Traces, which approximate protein evolution via local transition systems and simplicial... suite >>
-
Fanny Ducel (LORIA/LISN),
Comment caractériser, comprendre et évaluer les biais stéréotypés dans les modèles de langue ?
le
Résumé Les modèles de langue génératifs (aussi dits auto-régressifs), sont de plus en plus utilisés aussi bien dans la communauté scientifique, dans les entreprises que par le grand public. Toutefois, ces systèmes contiennent et amplifient de nombreux biais stéréotypés, qui peuvent contribuer à la stigmatisation et la discrimination de certaines... suite >>
-
Hugo Thievenaz (LSL/CLASS),
Scalable trace-based compile-time memory allocation
le
Abstract This thesis, titled “Scalable trace-based compile-time memory allocation”, studies the use of trace analysis to infer efficient memory allocations. The broader goal is to use program information at runtime as a way to outpace traditional static analysis techniques, which fail to scale for kernels of high dimensions and many... suite >>
-
Fabien Siron (Epita/Asterios Technologies),
Formal verification of real-time safety-critical systems: application to the PsyC language
le
Important note The seminar will be held at Nano-Innov only. There will not be a Livestorm retransmission. Abstract Safety-critical real-time systems have to respect strict timing constraints. Thus, timing constraints must be considered throughout the software development cycle. As exact computation execution time are generally not known during design, logical... suite >>
-
Armaël Guéneau (Inria Saclay),
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
le
Abstract In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds... suite >>
-
Roxane Cohen et Robin David (Quarkslab),
Tackling obfuscated code through variant analysis and Graph Neural Networks.
le
Abstract Existing deobfuscation techniques usually target specific obfuscation passes and assume a prior knowledge of obfuscated location within a program. Also, some approaches tend to be computationally costly. Conversely, few research consider bypassing obfuscation through correlation of various variants of the same obfuscated program or a clear program and a... suite >>
-
Josselin Giet (ENS Paris & Inria Paris),
Analyse de forme avec abstraction de contenu
le
Abstract Les analyses de formes basées sur la logique de séparation utilisent des prédicats inductifs pour synthétiser des propriétés générales sur les structures de données inductives non bornées comme les listes ou les arbres. Ces prédicats sont suffisamment expressifs pour prouver l’absence d’erreurs dues à une manipulation erronée de la... suite >>
-
Myriam Clouet (CEA List, LECS),
Langage de spécification et outil de vérification fondés sur une classification relative au respect de la vie privée
le
Abstract La vie privée est un droit fondamental que l’on retrouve dans plusieurs lois dans le monde entier. Donc, vérifier qu’un système respecte la vie privée est crucial. Cependant, la vie privée est une notion complexe. Assurer qu’un système respecte la vie privée nécessite de vérifier que les propriétés de... suite >>
-
Louis Gauthier (CEA List, LSL),
A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification
le
Abstract ACSL is a behavioral interface specification language for C. It is used by Frama-C, a framework including several formal methods-based techniques for verifying C code with respect to ACSL annotations. Currently, there is no formal definition of the ACSL semantics, which may lead to different, possibly inconsistent, interpretations of... suite >>
-
Loïc Correnson (CEA List, LSL),
Packaging proofs with Why3find
le
Abstract With the increasing maturity of proof assistants, diving into the development of large theories is appealing, but existing toolchains might not scale. Although standard software engineering methods can be applied to mechanized proof development, specific issues shall be addressed. In this article, we focus on the Why3 platform. We... suite >>
-
Cécile Baritel-Ruet (IDEMIA),
Modelization of security policies in different tools
le
Abstract Access control and information flow security policies are among the main security policies for formal verification in certain certification processes. We will discuss how those policies can be formalized and the different challenges for differnet formal toolchains. A special emphasis will be put on confidentiality and integrity. The tools... suite >>
-
Mamy Razafintsialonina (CEA List, LSL et Sorbonne Université),
Réutilisations de caches et d’invariants pour l’analyse statique incrémentale
le
Résumé L’analyse statique de programmes permet aujourd’hui d’analyser des programmes de grande taille, avec une très bonne précision, tout en étant raisonnablement rapide. Néanmoins, les temps d’analyse continuent de se compter en minutes, voire dizaines de minutes, ce qui rend compliqué leur intégration dans les processus de développement : les... suite >>
-
Sylvain Conchon (Université Paris-Saclay, LMF),
The Cubicle Fuzzy Loop: A Fuzzing-based extension for the Cubicle model checker
le
Abstract We present the Cubicle Fuzzy Loop (CFL), a fuzzing-based extension for Cubicle, a model checker for parameterized systems. To prove safety, Cubicle generates invariants, making use of forward exploration strategies like BFS or DFS on finite model instances. However, these standard algorithms are quickly faced with the state explosion... suite >>
-
Soutenance de thèse de
Soline Ducousso (CEA),
Aller de la sûreté à la sécurité en analyse de code : le modèle d'attaquant
le
Abstract Les techniques d’analyse de programme permettent d’éliminer bogues et vulnérabilités logicielles afin d’en améliorer la sûreté et la sécurité, mais elles reposent sur un modèle d’attaquant faible, seulement apte à créer des entrées malicieuses. Cependant, un attaquant avancé peut utiliser une combinaison d’attaques logicielles, micro-architecturales, d’injections de fautes matérielles... suite >>
-
Daniel Mercier (AdaCore),
Towards a solution to the expression problem for compilers: strongly typed nano-passes
[Transparents]
le
Abstract We present a new solution to the problem of (strongly) typing compiler passes when the source and destination language share multiple constructors. We are interested in approaches that limit the amount of boilerplate that needs to be (re)written for each language, while still maintaining a very strict typing discipline.... suite >>
-
Soutenance de thèse de
Romain Xu-Darme (UGA),
Algorithms and evaluation metrics for improving trust in machine learning: application to visual object recognition
le
Meeting ID: 593 962 6342 The integration of decision-making algorithms based on deep neural networks in critical applications - such as healthcare or automotive - depends on their ability to elicit trust in their decision, a major issue that is at the heart of this thesis. More precisely, our work... suite >>
-
Soutenance de thèse de
Romain Xu-Darme (UGA),
Algorithms and evaluation metrics for improving trust in machine learning: application to visual object recognition
le
This is a thesis rehearsal, the actual defense will take place one week later. The integration of decision-making algorithms based on deep neural networks in critical applications - such as healthcare or automotive - depends on their ability to elicit trust in their decision, a major issue that is at... suite >>
-
Francesco Parolini (LIP6 - Sorbonne Université),
Sound Abstract Nonexploitability Analysis
le
Abstract Runtime errors that can be triggered by an attacker are sensibly more dangerous than others, as they not only result in program failure, but can also be exploited and lead to security breaches such as Denial-of-Service attacks or remote code execution. Proving the absence of exploitable runtime errors is... suite >>
-
Délcio Ferramenta (Nova Lincs),
Static Analysis of Android Application Energy Consumption
le
Abstract The use of energy in portable devices is of extreme importance for user satisfaction and the efficient performance of devices. The increasing demand for applications and the abundance of choices in app stores are becoming increasingly prevalent in people’s lives. However, it is essential for users to be aware... suite >>
-
Jérémy Pinguet (Safran Group),
Contribution à la synthèse de contrôleurs neuronaux robustes par imitation
le
Résumé Cette thèse s’intéresse à l’élaboration de systèmes de contrôle par imitation de comportements ou de décisions répondant à des exigences complexes. L’objectif est de réaliser l’apprentissage d’un contrôleur neuronal de façon efficace et robuste sur une base de données regroupant ces comportements. L’approche retenue unifie les outils de la... suite >>
-
Christophe Junke (Parrot Drones),
Retour d expérience autour des systèmes embarqués
le
Abstract Je présente mon parcours professionnel pendant ces dernières années, avec deux segments: le postdoc autour de la compilation de systèmes critiques à base de modèles et mon travail d’ingénieur firmware au sein de Parrot Drones. Pour cela je présente aussi comment fonctionne le développement au sein de l’entreprise et... suite >>
-
Gerard Ekembe (Trinity College Dublin),
Language Extension and Translation: Linking CCS and CSP
le
Abstract CCS and CSP languages have evolved separately for 40+ years, despite efforts begun in the early 2000s to unify both languages. This presentation will show how CCS and CSP can be unified by means of translation. We will notably show how certain decisions in the design of the translation... suite >>
-
Philippe Thierry (Ledger),
Présentation d'un OS sécurisé basé sur un micro-kernel développé en C et Rust
le
Abstract As part of the evolution of its security products, Ledger is working, in preparation for new generations of products, on the implementation of an industrial-grade secure OS for the co-processors surrounding the Secure Element. Until now, the operating systems analyzed as part of a first state of the art... suite >>
-
Dinusha Vatsalan (Macquarie University),
Privacy-Preserving Record Linkage: Technological, Ethical, Adversarial, and Analytical Developments
le
Abstract Personal Identifiable Information (PII) about individuals, such as customers, taxpayers, patients, and mobile application users, is increasingly collected and linked across disparate data sources to enable customized, high-quality, and timely analytical services in a variety of applications. Examples include health applications such as similar patient matching for clinical trials... suite >>
-
Farah Benmouhoub (Université Paris 2),
Improving the Numerical Accuracy of Parallel Programs.
le
Abstract In high performance computing, nearly all the implementations and published experiments use floating-point arithmetic. However, since floating-point numbers are a finite approximation of real numbers, they are therefore prone to accuracy problems due to the accumulated round-off errors. These round-off errors may cause damage whose gravity varies depending on... suite >>
-
Thorsten Holz (CISPA),
Efficient and Scalable Fuzzing of Complex Software Stacks
le
Abstract In this talk, I will give an overview of our recent progress in randomized testing (“fuzzing”) and present some of the methods we have developed in the last few years. These include fuzzing of operating system kernels and hypervisors, grammar-based fuzzing of complex interpreters, and fuzz testing of embedded... suite >>
-
Ambroise Lafont (University of Cambridge),
Dargent: A Silver Bullet for Verified Data Layout Refinement
le
Abstract Systems programmers need fine-grained control over the memory layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations in memory is hard to get right. Traditionally, this problem is addressed... suite >>
-
Sacha-Élie Ayoun (Imperial College),
Gillian – a compositional symbolic execution platform
le
Abstract Gillian is a compositional symbolic execution platform, which allows for 3 kinds of analysis: 1) symbolic testing à la CBMC, 2) semi-automatic compositional verification of separation logic specifications à la Verifast, and 3) automatic compositional testing, based on bi-abduction, à la Infer Pulse. Gillian is parametric: it must be... suite >>
-
Pierre Nigron,
Programs and their proofs in type theory : application to freshness and zero-copy packet processing
le
Abstract Monadic programming is an essential component in the toolbox of functional programmers. For the programmers who sometimes navigate the waters of certified programming in type theory, it is the only means to concisely implement the imperative traits of certain algorithms. Monads open up a portal to the imperative world,... suite >>
-
Caterina Urban (INRIA),
Interpretability-Aware Verification of Machine Learning Software
le
Abstract Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This poses important safety, privacy, and non-discrimination challenges. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen... suite >>
-
Soutenance de thèse de
Grégoire Menguy (CEA List, LSL),
Analyse en boîte noire pour la rétro-ingénierie via acquisition de contraintes et synthèse de code
le
Résumé Les logiciels deviennent de plus en plus grands et complexes. Ainsi, certaines tâches, pourtant cruciales, telles que le test et la vérification de code ou plus généralement la compréhension de code, sont de plus en plus difficiles à réaliser pour un humain. D’où la nécessité de développer des outils... suite >>
-
Julien Vanegue (Bloomberg),
Adversarial Logic
le
Abstract Adversarial logic is a new program logic inspired from incorrectness logic, founded on under-approximation of possible executions, rather than on their over-approximation (as generally done for verification). This new type of logic provides a foundations for bug finding rather than the verification of their absence and admits no false... suite >>
-
Josué Moreau (Université Paris-Saclay, LMF),
Compilation formellement vérifiée d'un langage pour le calcul formel
le
Abstract Nous présentons une ébauche de langage de bas niveau ayant pour but de pouvoir écrire les algorithmes de base du calcul formel. Les structures de données manipulées par ces algorithmes étant principalement des tableaux, c’est sur ces derniers que notre langage se concentre. Nous présentons sa sémantique qui a... suite >>
-
Soutenance de thèse de
Dara Ly (CEA),
vérification dynamique de propriétés mémoire de programmes C
le
La vérification d’assertions à l’exécution est une technique permettant de contrôler, lors de leur exécution, la conformité d’un programme vis-à-vis d’une spécification donnée sous forme d’annotations formelles~: les assertions. Un procédé appelé instrumentation transforme les assertions en code exécutable, de manière à mettre en œuvre un moniteur en ligne pour... suite >>
-
Myriam Clouet (CEA List),
Model Specification Language for Formal Verification of Consent Properties on Models and Code
[Transparents]
le
Abstract Recent privacy laws and regulations raise the stakes in verifying that a software system respects user consent. Even if the current state of the art shows that privacy by design and formal methods can help, ensuring the validity of privacy properties, in particular consent properties, at different stages of... suite >>
-
Soutenance de thèse de
Thibault Martin (CEA List, LSL),
Techniques de test pour des critères de couverture avancés
le
English version below Résumé Dans les dernières décennies, l’essor de l’informatique et d’internet ont grandement bouleversé nos modes de vie. Nos voitures, avions, trains, sont équipés des systèmes informatiques puissants. Nous pilotons certaines de nos centrales nucléaires avec des logiciels et nous sauvons même des vies grâce à des équipements... suite >>
-
Hichem Ait El Hara (OcamlPro),
Présentation d'Alt-Ergo-Fuzz et Benchpress
le
Alt-Ergo est un solveur SMT conçu pour la preuve de programmes et utilisé comme backend par différents outils de vérification logicielle comme Frama-C, SPARK, Why3 entre autres. Pour tester de façon efficace cet outil, nous avons développé Alt- Ergo-Fuzz qui est un outil de test par fuzzing conçu pour Alt-Ergo,... suite >>
-
Grégoire Menguy,
Automated Program Analysis, Revisiting Precondition Inference through Constraint Acquisition
le
Program annotations under the form of function pre/postconditions are crucial for many software engineering and program verification applications. Unfortunately, such annotations are rarely available and must be retrofit by hand. In this paper, we explore how Constraint Acquisition (CA), a learning framework from Constraint Programming, can be leveraged to automatically... suite >>
-
Nathanaël Fijalkow (Laboratoire Bordelais de Recherche en Informatique (LabRI)),
Program synthesis in the machine learning era
le
This talk is a joint talk with the Digicosme vrAI working group. Note that its duration is longer than usual seminars. This talk will be an introduction to the field of program synthesis and the impact that machine learning had on this field. Program synthesis is one of the oldest... suite >>
-
Eric Goubault and Sylvie Putot (Laboratoire d'Informatique de l'école Polytechnique),
Tropical Algebra for Neural Network verification
le
This talk is a joint talk with the Digicosme vrAI working group. In this talk, we will discuss range analyzes for feedforward neural networks, which are basic primitives for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural- network feedback systems. Our approach focuses... suite >>
-
Arthur Correnson (Université de Rennes, Université de Saarland),
Formal Verification of a Lazy Software Model Checker
le
In a world where computers are part of our everyday life, ensuring software systems safety and correctness is crucial. To improve our trust in computer programs, a common approach is to use automated verification tools that are able to analyze a program and inform the users if safety issues, vulnerabilities,... suite >>
-
Mathéo Vergnolle (École Polytechnique),
Vérification de temps constant cryptographique au niveau binaire
le
L’application de la politique de temps constant cryptographique permet de se protéger de certaines attaques par canaux auxiliaires, notamment les attaques temporelles et les attaques par cache. Mais cette politique peut être complexe à mettre en place, elle n’est pas toujours préservée par le compilateur, et par ailleurs le code... suite >>
-
Soutenance de thèse de
Dongho Lee (CEA List, LSL et LMF),
Méthodes Formelles pour les Langages de Programmation Quantiques
le
English version below La soutenance aura lieu uniquement en ligne. Notez qu’il est néanmoins prévu, pour ceux qui le souhaitent, de se retrouver au restaurant L’Alsacien Châtelet à 20h le même jour dont l’adresse est 6 Rue Saint-Bon, 75004 Paris. Si vous souhaitez nous joindre, je vous invite à me... suite >>
-
François Bobot (CEA List),
Présentation générale de Colibri2
le
General Presentation of Colibri2 Colibri2 is a reimplementation of the Colibri CP solver accepting SMTLib goals in OCaml. The presentation will present different choices made: the main engine and architecture of the solver input format, dolmen parser, and link with Why3 search strategy quantifier instanciation supported theories use of Algebraic... suite >>
-
Soutenance de thèse de
Olivier Nicole (CEA List, LSL et ENS),
Vérification automatisée de code système à l'aide d'abstractions mémoire basées sur le typage/Automated Verification of Systems Code using Type-based Memory Abstractions
le
English version below Inscription Si vous prévoyez de venir physiquement, merci de remplir ce court formulaire. Résumé Les logiciels étant des composants essentiels de nombreux systèmes embarqués et de nombreux systèmes d’information, un dysfonctionnement logiciel peut entraîner d’importants dommages ou des failles de sécurité. De nouveaux bugs et de nouvelles... suite >>
-
Alan Schmitt (INRIA Rennes, Celtique project team),
Skeletal Semantics by Example
le
Abstract Skeletal Semantics is both a meta-language to describe semantics of programming languages (skel) and several tools to manipulate these semantics. We present skel through several examples, highlighting how complex features can be captured in a readable way using monads. We then briefly introduce some tools that take these formalizations... suite >>
-
Gilles Dowek (ENS),
Ethical challenges for artificial intelligence
le
Computer science in general and artificial intelligence in particular are nowadays raising several ethical concerns, challenging traditional values such as privacy and accountability. Making a program’s decisions intelligible for the various humans involved in its process is key if they are to be taken accountable. With ethics comes the question... suite >>
-
Amélie Ledein (LMF),
Vers une traduction de K en Dedukti
le
K est un framework sémantique permettant de décrire formellement des sémantiques de langages de programmation. C’est aussi un environnement qui offre différents outils pour aider à la programmation avec les langages spécifiés dans le formalisme. Il est par exemple possible d’exécuter des programmes et de vérifier certaines propriétés sur ceux-ci,... suite >>
-
Soutenance de thèse de
Virgile Robles (CEA List, LSL),
Spécifier et vérifier des exigences de haut-niveau sur des programmes importants: application à la sécurité des programmes C
le
Avertissement En raison des contraintes sanitaires, le nombre de places en présentiel est très restreint, merci de privilégier la visio. Résumé La spécification et la vérification d’exigences haut niveau (comme des propriétés de sécurité, telles que l’intégrité des données ou la confidentialité) reste un défi pour l’industrie, alors que les... suite >>
-
Nikolai Kosmatov (Thales Research and Technology),
Formal Verification of a JavaCard Virtual Machine with Frama-C
le
Formal verification of real-life industrial software remains a challenging task. It provides strong guarantees of correctness, which are particularly important for security-critical products, such as smart cards. Security of a smart card strongly relies on the requirement that the underlying JavaCard virtual machine ensures necessary isolation properties. This talk presents... suite >>
-
Guilhem Lacombe (CEA, List),
Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities
le
In this talk, I will present the work done during my internship at CEA Leti this summer. Certification through auditing allows to ensure that critical embedded systems are secure. This entails reviewing their cryptographic components and checking for dangerous execution paths. This latter task requires the use of specialized tools... suite >>
-
Clément Pascutto (LMF / Tarides),
Ortac: Runtime Assertion Checking for OCaml
le
Runtime assertion checking (RAC) is a convenient set of techniques that lets developers abstract away the process of verifying the correctness of their programs by writing formal specifications and automating their verification at runtime. In this work, we present ortac, a runtime assertion checking tool for OCaml libraries and programs.... suite >>
-
Caterina Urban (INRIA Antique),
An Abstract Interpretation Recipe for Machine Learning Fairness
le
English Version An Abstract Interpretation Recipe for Machine Learning Fairness Abstract Nowadays, machine learning software is increasing used for assisting or even automating decisions with socio-economic impact. In April 2021, the European Commission proposed a first legal framework on machine learning software – the Artificial Intelligence Act — which imposes... suite >>
-
Franck Védrine (LSL),
Synthèse d'invariant pour bibliothèques de calcul: Retour d'expérience sur l'analyse de filtres linéaires
le
Résumé Dans ce talk, je présenterai un analyse utilisée pour générer des invariants de boucle, pour des boucles non bornées. C’est une première étape pour la synthèse d’annotations de type ACSL qui seraient pertinentes pour des bibliothèques de calcul. Ce besoin d’annotations formelles est sous-jacent à plusieurs problématiques: comment juger... suite >>
-
Robin David (Quarkslab),
Greybox Program Synthesis: A New Approach to Attack Dataflow Obfuscation
le
Abstract Obfuscation is getting broadly adopted for a wide range of applications and especially to protect intellectual property (IP) in mobile ecosystem (Android, iOS) and embedded systems at large. It is now ubiquitous, and everyone is unwillingly and unknowingly executing obfuscated code. Throughout adoption it also gained maturity, potency making... suite >>
-
Soutenance de thèse de
Maxime Jacquemin (CEA List, LSL),
Arithmétiques relationnelles pour l'analyse par interprétation abstraite de propriétés de précision numérique
le
Résumé L’arithmétique à virgule flottante est l’approche la plus utilisée pour réaliser des calculs mathématiques reposant sur les nombres réels avec un ordinateur. Cependant, elle souffre d’un défaut: chaque opération peut introduire une erreur, c’est-à-dire une différence avec le résultat que nous aurions obtenu en utilisant des réels. Bien que... suite >>
-
Pierre-Loïc Garoche (ENAC/NASA),
Formal Verification of Control System Software
le
In this talk we will present an approach to apply formal verification techniques, from the theoretical computer science community, to the specific class of control system software and closed-loop control models. All analyses are performed in the state-space domain, easing the code level interpretation of the result. Among the different... suite >>
-
Thibaut Benjamin (CEA LIST, LSL),
CaTT - A type theory for higher categories
le
I will present an approach of the use of formal methods to reason about algebraic structures, with the example of the type theory CaTT. This type theory describes an algebraic structure called weak omega-categories, and it allows for an interactive theorem prover dedicated specifically to reasonning on these structures. Weak... suite >>
-
Khaoula Boukir (CEA LIST, LSL),
Proven implementation of multiprocessor real-time scheduling policies
le
Keywords: Real-time scheduling policy, Real-time operating system, Scheduler implementation, Model-checking Implementing a new scheduling policy within a real-time operating system is not an easy task. Moving from an abstract literary specification of a policy to its implementation within a real platform requires making choices of realization and considering various constraints... suite >>
-
Loïc Correnson (CEA LIST, LSL),
Ivette: developing a modern GUI for Frama-C
le
We are developing Ivette which is a complete redesign of the graphical user interface of Frama-C based on modern technologies from the web. While it is similar to modern graphical interfaces for code analysis tools, out approach focuses on collaboration and on its application to other platforms, tools, and combinations... suite >>
-
Dario Pinto (CEA LIST, LSL),
Open-Source-Case-Studies: feedback from an internship
le
Open-Source-Case-Studies is a set of open-source C code bases intended to provide usage examples of Frama-C, help regression testing, and benchmarking of realistic code. During his internship, Dario Pinto explored this code base using the Eva plug-in to perform several different tasks: analyze code, find issues in the code (and... suite >>
-
Liliana Cucu-Grosjean, StatInf (CEA List),
Statistics to improve cyber-physical systems design
le
Abstract: empirical statistics are often used in the industry to confirm intuitions, but less to provide arguments to prove a cyber-physical systems design. Most of time, this is justified by existing misconceptions while using statistical approaches, while their correct understanding could provide a powerful framework for ensuring compositionable time properties... suite >>
-
Lesly-Ann Daniel (CEA LIST, LSL),
Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level
le
The constant-time programming discipline (CT) is an efficient countermeasure against timing side-channel attacks, requiring the control flow and the memory accesses to be independent from the secrets. Yet, writing CT code is challenging as it demands to reason about pairs of execution traces (2-hypersafety property) and it is generally not... suite >>
-
Yackolley Amoussou-Guenou (CEA LIST, LICIA),
Rational vs Byzantine Players in Consensus-based Blockchains
le
We analyze from the game theory point of view Consensus-based blockchains when participants exhibit rational or Byzantine behavior. Our work is the first to model the Byzantine-consensus based blockchains as a committee coordination game. Our first contribution is to offer a game-theoretical methodology to analyze equilibrium interactions between Byzantine and... suite >>
-
Raphaël Monat (Sorbonne Université, LIP6),
Formal study of the French tax code's implementation
le
The tax code, as a legislative text, defines a mathematical function that computes the income tax of a fiscal household. In order to collect taxes, this function is implemented as an algorithm by the Direction Générale des Finances Publiques (DGFiP), using a domain specific language called M (standing for “Macro-language”).... suite >>
-
Ronny chevalier (HP Labs and CentraleSupélec),
Survivor: A Fine-Grained Intrusion Response and Recovery Approach for Commodity Operating Systems
le
Despite the deployment of preventive security mechanisms to protect the assets and computing platforms of users, intrusions eventually occur. In this talk, we will present a paper that we published at ACSAC’19 (https://www.acsac.org/) describing an approach to to make our operating systems (OSs) and applications more resilient so that they... suite >>
-
Julia Lawall (Inria Paris, LIP6),
Provable Multicore Schedulers with Ipanema
le
An OS-kernel thread scheduler decides which thread runs at a given moment on a given core. A scheduler is thus a key OS service since any bad decision that it makes may lead to cores wasting cycles and may increase application response times. Validating the good behavior of a multicore... suite >>
-
Mathilde Ollivier (CEA LIST, LSL),
How to Kill Symbolic Deobfuscation for Free (or: Unleashing the Potential of Path-Oriented Protections)
le
Code obfuscation is a major tool for protecting software intellectual property from attacks such as reverse engineering or code tampering. Yet, recently proposed (automated) attacks based on Dynamic Symbolic Execution (DSE) shows very promising results, hence threatening software integrity. Current defenses are not fully satisfactory, being either not efficient against... suite >>
-
Père Noël (CEA List),
Algorithme de distribution de cadeau
le
La difficulté de la distribution des cadeaux ne doit pas être sous-estimé:
Bcp d’enfant
Le monde à parcourir
Un seul traineau
suite >>
-
Christophe Charreton (CEA List),
Qbrick, a core development framework for certified quantum programming
[Transparents]
le
Due to the nature of quantum computation, we believe that, in this field, formal verification is meant to play a role similar to that of test development in classical computing. In this talk we present Qbricks, a core programming language for entirely verifiable quantum programming, embedded into Why3. Qbricks both... suite >>
-
Nicolas Vaucher (Secapem),
TAXIA : Système d'aide au pilotage lors de l'engagement des cibles TAXAN
le
Créée en 1957, la société SECAPEM développe des cibles aériennes remorquées pour l’entraînement des Forces armées. La TAXAN est un système de cible utilisé par les armées pour l’entraînement au tir canon air-air et sol-air. Le système est conçu pour être remorqué par un avion et emporté dans un conteneur... suite >>
-
Martin Drago, Félix Tréguer (La Quadrature du Net),
Smart Cities sécuritaires : dangers pour les libertés
le
Créée en 2008, La Quadrature du Net est une association qui défend les libertés dans l’environnement numérique. C’est notamment dans cet objectif qu’elle s’intéresse au déploiement de nouvelles technologies à usages sécuritaire qui cherchent à imposer dans nos villes une surveillance constante : vidéo-analyse intelligente, reconnaissance faciale, logiciels prédictifs, micros,... suite >>
-
Julien Girard (CEA List),
Computational techniques for boosting verification of deep learning algorithms
le
Abstract: For several years now, deep neural networks algorithms have been integrated in a wide range of software. Examples are numerous: object detection, image classification, robotic command and control, speech synthesis, natural language processing, time-data synthesis, etc. However, deep neural network based software display a range of vulnerabilites that still... suite >>
-
Maxime Jacquemin (CEA List),
A Reduced Product of Absolute and Relative Error Bounds for Floating-point Analysis
le
Floating-point numbers are widely used as a computable equivalent of real numbers. However, because the memory of a computer is finite, and because one wants to compute complex equations in no time, floating-point numbers are an approximation of the real numbers with bundles of trade-offs between accuracy and performance. Because... suite >>