avatar

Lelio Brun

Postdoctoral research scientist in Computer Science

National Institute of Informatics

Biography

I am a postdoctoral research scientist in the ZT-IoT project at NII in Tokyo.
I work with Ichiro Hasuo and Taro Sekiyama on applying formal methods to ensure security of IoT (Internet of Things) systems.

I defended my PhD thesis in 2020, Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset, written under the supervision of Marc Pouzet and Timothy Bourke.

Interests

  • Functional programming
  • Synchronous languages
  • Proof assistants
  • Security protocols analysis

Education

  • PhD in Computer Science, 2020
    École normale supérieure - PSL Research University
  • MSc in Computer Science (MPRI), 2016
    Université Paris Cité
  • MSc in Aerospace Engineering, 2013
    ISAE-ENSMA

Publications

  • Automated Security Analysis for Real-World IoT Devices

     ·  Lelio Brun, Ichiro Hasuo, Yasushi Ono, Taro Sekiyama
    HASP'23
    Abstract

    Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities.

    In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.

    Cite
    @inproceedings{brun_automated_2023,
    	address = {New York, NY, USA},
    	series = {{HASP}'23},
    	title = {Automated {Security} {Analysis} for {Real}-{World} {IoT} {Devices}},
    	copyright = {All rights reserved},
    	isbn = {9798400716232},
    	url = {https://www.leliobrun.net/publication/hasp23/paper.pdf},
    	doi = {10.1145/3623652.3623667},
    	abstract = {Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities. 
    
    In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.},
    	language = {en},
    	booktitle = {Proceedings of the 12th {International} {Workshop} on {Hardware} and {Architectural} {Support} for {Security} and {Privacy}},
    	publisher = {Association for Computing Machinery},
    	author = {Brun, Lelio and Hasuo, Ichiro and Ono, Yasushi and Sekiyama, Taro},
    	month = oct,
    	year = {2023},
    	pages = {29--37},
    }
    DOI Slides
  • Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

     ·  Lélio Brun, Christophe Garion, Pierre-Loïc Garoche, Xavier Thirioux
    EMSOFT'23 Best paper
    Abstract

    Model-based design tools like SCADE Suite and Simulink are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.

    We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.

    Cite
    @article{brun_equation-directed_2023,
    	series = {{EMSOFT}'23},
    	title = {Equation-{Directed} {Axiomatization} of {Lustre} {Semantics} to {Enable} {Optimized} {Code} {Validation}},
    	volume = {22},
    	copyright = {All rights reserved},
    	issn = {1539-9087},
    	url = {https://www.leliobrun.net/publication/emsoft23/paper.pdf},
    	doi = {10.1145/3609393},
    	abstract = {Model-based design tools like SCADE Suite and Simulink are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.
    
    We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.},
    	language = {en},
    	number = {5s},
    	journal = {ACM Trans. Embed. Comput. Syst.},
    	author = {Brun, Lélio and Garion, Christophe and Garoche, Pierre-Loïc and Thirioux, Xavier},
    	month = sep,
    	year = {2023},
    	pages = {151:1--151:24},
    }
    DOI HAL Slides
  • Faites-vous confiance à votre thermostat ?

     ·  Lélio Brun
    Interstices
    Abstract

    Certains systèmes logiciels qui interagissent avec le monde réel ne doivent échouer sous aucun prétexte, au risque de provoquer des catastrophes. Comment s’assurer que ces systèmes sont sûrs ? En particulier, quel degré de confiance accorder au processus de traduction de ces logiciels vers du code exécutable ?

    Cite
    @article{brun_faites-vous_2022,
    	title = {Faites-vous confiance à votre thermostat ?},
    	copyright = {All rights reserved},
    	url = {https://interstices.info/faites-vous-confiance-a-votre-thermostat/},
    	abstract = {Certains systèmes logiciels qui interagissent avec le monde réel ne doivent échouer sous aucun prétexte, au risque de provoquer des catastrophes. Comment s’assurer que ces systèmes sont sûrs ? En particulier, quel degré de confiance accorder au processus de traduction de ces logiciels vers du code exécutable ?},
    	language = {fr},
    	journal = {Interstices},
    	author = {Brun, Lélio},
    	month = jun,
    	year = {2022},
    }
    HAL
  • Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset

     ·  Lélio Brun
    GDR GPL accessit prize
    Abstract

    Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like Scade and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre.

    In this thesis we present Vélus, a Lustre compiler verified in the interactive theorem prover Coq. We develop semantic models for the various languages in the compilation chain, and build on the verified CompCert C compiler to generate executable code and give an end-to-end correctness proof. The main challenge is to show semantic preservation between the dataflow paradigm and the imperative paradigm, and to reason about byte-level representations of program states.

    We treat, in particular, the modular reset construct, a primitive for resetting subsystems. This necessitates the design of suitable semantic models, compilation algorithms and corresponding correctness proofs. We introduce a novel intermediate language into the usual clock-directed modular compilation scheme of Lustre. This permits the implementation of compilation passes that generate better sequential code, and facilitates reasoning about the correctness of the successive transformations of the modular reset construct.

    Cite
    @phdthesis{brun_mechanized_2020,
    	type = {Doctoral {Thesis}},
    	title = {Mechanized {Semantics} and {Verified} {Compilation} for a {Dataflow} {Synchronous} {Language} with {Reset}},
    	copyright = {All rights reserved},
    	url = {https://www.leliobrun.net/files/thesis.pdf},
    	abstract = {Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like Scade and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre.
    
    In this thesis we present Vélus, a Lustre compiler verified in the interactive theorem prover Coq. We develop semantic models for the various languages in the compilation chain, and build on the verified CompCert C compiler to generate executable code and give an end-to-end correctness proof. The main challenge is to show semantic preservation between the dataflow paradigm and the imperative paradigm, and to reason about byte-level representations of program states.
    
    We treat, in particular, the modular reset construct, a primitive for resetting subsystems. This necessitates the design of suitable semantic models, compilation algorithms and corresponding correctness proofs. We introduce a novel intermediate language into the usual clock-directed modular compilation scheme of Lustre. This permits the implementation of compilation passes that generate better sequential code, and facilitates reasoning about the correctness of the successive transformations of the modular reset construct.},
    	language = {en},
    	school = {École normale supérieure - PSL Research University},
    	author = {Brun, Lélio},
    	collaborator = {Pouzet, Marc and Bourke, Timothy},
    	month = jul,
    	year = {2020},
    }
    HAL Slides
  • Mechanized semantics and verified compilation for a dataflow synchronous language with reset

     ·  Timothy Bourke, Lélio Brun, Marc Pouzet
    POPL'20
    Abstract

    Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers to translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.

    Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.

    Cite
    @inproceedings{bourke_mechanized_2020,
    	address = {New Orleans, LA, USA},
    	series = {{POPL}'20},
    	title = {Mechanized semantics and verified compilation for a dataflow synchronous language with reset},
    	volume = {4},
    	copyright = {All rights reserved},
    	url = {https://www.leliobrun.net/publication/popl20/paper.pdf},
    	doi = {10.1145/3371112},
    	abstract = {Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers to translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.
    
    Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.},
    	language = {en},
    	booktitle = {Proceedings of the 47th {ACM} {SIGPLAN} {Symposium} on {Principles} of {Programming} {Languages}},
    	publisher = {ACM},
    	author = {Bourke, Timothy and Brun, Lélio and Pouzet, Marc},
    	month = jan,
    	year = {2020},
    	pages = {29},
    }
    DOI HAL Slides Video
  • Towards a Verified Lustre Compiler with Modular Reset

     ·  Timothy Bourke, Lélio Brun, Marc Pouzet
    SCOPES'18
    Abstract

    This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.

    Cite
    @inproceedings{bourke_towards_2018,
    	address = {Sankt Goar, Germany},
    	series = {{SCOPES}'18},
    	title = {Towards a {Verified} {Lustre} {Compiler} with {Modular} {Reset}},
    	copyright = {All rights reserved},
    	isbn = {978-1-4503-5780-7},
    	url = {https://www.leliobrun.net/publication/scopes18/paper.pdf},
    	doi = {10.1145/3207719.3207732},
    	abstract = {This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.},
    	language = {en},
    	booktitle = {Proceedings of the 21st {International} {Workshop} on {Software} and {Compilers} for {Embedded} {Systems}},
    	publisher = {ACM},
    	author = {Bourke, Timothy and Brun, Lélio and Pouzet, Marc},
    	month = may,
    	year = {2018},
    	pages = {14--17},
    }
    DOI HAL Slides
  • A Formally Verified Compiler for Lustre

     ·  Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg
    PLDI'17
    Abstract

    The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

    We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.

    Cite
    @inproceedings{bourke_formally_2017,
    	address = {Barcelona, Spain},
    	series = {{PLDI}'17},
    	title = {A {Formally} {Verified} {Compiler} for {Lustre}},
    	copyright = {All rights reserved},
    	isbn = {978-1-4503-4988-8},
    	url = {https://www.leliobrun.net/publication/pldi17/paper.pdf},
    	doi = {10.1145/3062341.3062358},
    	abstract = {The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.
    
    We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.},
    	language = {en},
    	booktitle = {Proceedings of the 38th {ACM} {SIGPLAN} {Conference} on {Programming} {Language} {Design} and {Implementation}},
    	publisher = {ACM},
    	author = {Bourke, Timothy and Brun, Lélio and Dagand, Pierre-Évariste and Leroy, Xavier and Pouzet, Marc and Rieg, Lionel},
    	month = jun,
    	year = {2017},
    	pages = {586--601},
    }
    DOI HAL Slides Video

Talks

  • Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset

     ·  ENAC
    FAC'21
    Abstract

    Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications.
    Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers to translate such specifications into executable code.
    They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.
    Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover.

    It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code.
    We extend this work to treat a primitive for resetting subsystems.
    Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.

  • Sémantique Mécanisée, Compilation Vérifiée et Compilation Certifiante pour Lustre

     ·  ISAE-SUPAERO
    Séminaire SCALP
    Abstract

    Les spécifications basées sur les schémas-blocs et machines à états sont utilisées pour la conception de systèmes de contrôle-commande, particulièrement dans le développement d’applications critiques.
    Des outils tels que Scade et Simulink/Stateflow sont équipés de compilateurs qui traduisent de telles spécifications en code exécutable.
    Ils proposent des langages de programmation permettant de composer des fonctions sur des flots, tel que l’illustre le langage synchrone à flots de données Lustre.

    Cet exposé présente Vélus, un compilateur Lustre vérifié dans l’assistant de preuves interactif Coq.
    Nous développons des modèles sémantiques pour les langages de la chaîne de compilation, et utilisons le compilateur C vérifié CompCert pour générer du code exécutable et donner une preuve de correction de bout en bout.
    Le défi principal est de montrer la préservation de la sémantique entre le paradigme flots de données et le paradigme impératif, et de raisonner sur la représentation bas niveau de l’état d’un programme.
    En particulier, nous traitons le reset modulaire, une primitive pour réinitialiser des sous-systèmes.
    Ceci implique la mise en place de modèles sémantiques adéquats, d’algorithmes de compilation et des preuves de correction correspondantes.

    Nous présenterons ensuite une autre approche de la compilation vérifiée, dans le cadre d'un travail de recherche actuel sur le compilateur LustreC.
    Ce travail consiste à transformer LustreC en compilateur certifiant, qui génère du code et de la spécification associée prouvée a posteriori par des outils comme Frama-C ou SPARK.

    Video
  • Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset

     ·  IRISA - Inria Rennes
    68NQRT Seminar
    Abstract

    Les spécifications basées sur les schémas-blocs et machines à états sont utilisées pour la conception de systèmes de contrôle-commande, particulièrement dans le développement d'applications critiques.
    Des outils tels que SCADE et Simulink/Stateflow sont équipés de compilateurs qui traduisent de telles spécifications en code exécutable.
    Ils proposent des langages de programmation permettant de composer des fonctions sur des flots, tel que l'illustre le langage synchrone à flots de données Lustre.

    Ce travail de thèse présente Vélus, un compilateur Lustre vérifié dans l'assistant de preuves interactif Coq.
    Nous développons des modèles sémantiques pour les langages de la chaîne de compilation, et utilisons le compilateur C vérifié CompCert pour générer du code exécutable et donner une preuve de correction de bout en bout.
    Le défi principal est de montrer la préservation de la sémantique entre le paradigme flots de données et le paradigme impératif, et de raisonner sur la représentation bas niveau de l'état d'un programme.

    En particulier, nous traitons le reset modulaire, une primitive pour réinitialiser des sous-systèmes.
    Ceci implique la mise en place de modèles sémantiques adéquats, d'algorithmes de compilation et des preuves de correction correspondantes.
    Nous présentons un nouveau langage intermédiaire dans le schéma habituel de compilation modulaire dirigé par les horloges de Lustre.
    Ceci débouche sur l'implémentation de passes de compilation permettant de générer un meilleur code séquentiel, et facilite le raisonnement sur la correction des transformations successives du reset modulaire.

  • Verified Compilation of the Modular Reset, Finally

     ·  CAES CNRS - Centre Paul-Langevin
    SYNCHRON'19
    Abstract

    We present the formalization of the semantics of the modular reset construct of Lustre, and show how to integrate it into Vélus, a Lustre compiler verified in Coq and built on top of CompCert.
    In particular, we introduce a new intermediate language in the compilation chain, specifically designed to handle compilation of the modular reset.

  • Vélus: Towards a Modular Reset

     ·  Centre Inria Rennes - Bretagne Atlantique
    SYNCHRON'17
    Abstract

    We present two ideas in this talk:

    1. A co-inductive based semantics formalization for normalized Lustre
    2. A formalization of the semantics of the modular reset
  • Proving a Lustre Compiler Part 2

     ·  Dominikanerkloster Bamberg
    SYNCHRON'16
    Abstract

    The compilation of block diagram languages like Lustre or Scade often use an intermediary language between the source data-flow code and the target imperative code.
    We recently implemented and verified a translation function in Coq from a simple intermediary language towards the CompCert-accepted Clight language.

    The intermediary language uses an idealized hierarchical memory representation, whereas Clight uses an intricate memory model rather close of the machine.
    Our proof of correctness must consequently tackle alignment, aliasing and padding. We use separation logic predicates developed in CompCert to solve those issues.

  • Génération de code certifié pour Lustre

     ·  Laboratoire de Recherche en Informatique
    GDR GPL LTP 2016
    Abstract

    Les compilateurs de langages schémas-blocs, comme Lustre ou Scade, utilisent souvent un langage intermédiaire entre le code flot de données source et le code impératif cible.
    Nous avons récemment implémenté et vérifié une fonction de traduction dans Coq d'un langage intermédiaire simple vers le langage Clight accepté par le compilateur CompCert.
    Le langage intermédiaire utilise une représentation idéalisée d'une mémoire hiérarchique, alors que Clight utilise un modèle de mémoire sophistiqué assez proche de la machine.
    Notre preuve de correction doit donc confronter les questions d'alignement, d'aliasing, et du padding.
    On se sert des prédicats de séparation développés dans CompCert pour résoudre ces problèmes.

Projects

  • LustreC

    A prototype compiler for Lustre, with verification abilities and certifying compilation in mind.
  • Vélus

    A prototype compiler for Lustre, verified in Coq.
  • Obelisk

    A tool to pretty-print (LaTeX) Menhir grammars.

Experience

  • Postdoctoral research scientist

    NII  ·  ZT-IoT project

    Present
    Formal methods for the security analysis of IoT systems.
  • Postdoctoral research scientist

    ISAE-SUPAERO  ·  IpSC Team (DISC)

    Adding translation validation features to the LustreC Lustre to C compiler through the Frama-C platform.
  • Postdoctoral research engineer

    École normale supérieure / Inria  ·  PARKAS Team

    Adding enumerations and case analysis support to the Vélus Lustre to Assembly compiler verified with the Coq Proof Assistant.
  • Software engineer

    Astek

    Bug tracking and fixing in a large C++ codebase.

Teaching

Teaching assistant

2021/22

2020/21–21/22

2020/21

2017/18

2016/17–18/19

Academic service

Contact

National Institute of Informatics
2 Chome-1-2 Hitotsubashi
101-8430 Chiyoda City
Tokyo, Japan