ProMiS

Scientific objectives

The Spectre vulnerability has recently been reported, which affects most modern processors. The idea is that attackers can extract information about the private data using a timing attack. It is an example of side channel attacks, where secure information flows through side channels unintentionally. How to systematically mitigate such attacks is an important and yet challenging research problem.

We propose to automatically synthesize mitigation of side channel attacks (e.g., timing or cache) using formal verification techniques. The idea is to reduce this problem to the parameter synthesis problem of a given formalism (for instance, variants of the well-known formalism of parametric timed automata). Given a program/system with design parameters which can be tuned to mitigate side channel attacks, our approach will automatically generate provably secure valuations of these parameters. We will use a 3-phase research plan:

1. define formally the problem of timing information leakage;
2. propose optimized parametric model checking algorithms for information leakage checking;
3. propose optimizations and methods translating real-worlds systems and programs into our formalisms to achieve practical scalability.

We plan to deliver a fully automated toolkit which can be automatically applied to real-world systems. This project will benefit from the synergy of 5 scientists in 4 partner labs, with a complementary expertise in security, formal methods and program analysis.

Meetings

Deliverables

Publications

2025

• André, Béchennec, Chattopadhyay, Faucou, Lime, Marinho, Roux, Sun. Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets. SAC 2025.

2024

• Arcile, André. Zone extrapolations in parametric timed automata. ISSE, 2024.
• Ziqi Shuai, Zhenbang Chen, Kelin Ma, Kunlin Liu, Yufeng Zhang, Jun Sun, Ji Wang: Partial Solution Based Constraint Solving Cache in Symbolic Execution. Proc. ACM Softw. Eng. 1(FSE): 2493-2514 (2024)
• Bing Sun, Jun Sun, Wayne Koh, Jie Shi: Neural Network Semantic Backdoor Detection and Mitigation: A Causality-Based Approach. USENIX Security Symposium 2024
• Ghosh, André. Offline and online energy-efficient monitoring of scattered uncertain logs using a bounding model. LMCS, 2024.
• Leclercq, Lime, Roux. On Parametric DBMs and their applications to Time Petri Nets. FORMATS 2024.
• André, Arias, Barbot, Hulin, Kordon, Le, Petrucci. CosyVerif: The Path to Formalisms Cohabitation. Petri Nets 2024.
• André, Arcile, Lefaucheux. Execution-time opacity problems in one-clock parametric timed automata. FSTTCS 2024.
• André, Dépernet, Lefaucheux. The Bright Side of Timed Opacity. ICFEM 2024.
• André, Duflot, Laversa, Lefaucheux. Execution-time opacity control for timed automata. SEFM 2024.
• André, Eichler, Jacobs, Karra. Parameterized Verification of Disjunctive Timed Networks. VMCAI 2024.
• Reimann et al. Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance. SAC 2024.
• Waga, André. Hyper parametric timed CTL. EMSOFT 2024.

2023

• Yifan Jia, Christopher M. Poskitt, Peixin Zhang, Jingyi Wang, Jun Sun, Sudipta Chattopadhyay: Boosting Adversarial Training in Safety-Critical Systems Through Boundary Data Selection. IEEE Robotics Autom. Lett. 8(12): 8350-8357 (2023)
• Arcile, André. Timed automata as a formalism for expressing security: A survey on theory and practice. ACM Computing Surveys, 2023.
• Ghosh, André. MoULDyS: Monitoring of autonomous systems in the presence of uncertainties. SCP, 2023.
• Waga, André, Hasuo. Parametric Timed Pattern Matching. ACM ToSEM 2023.
• André, Lefaucheux, Lime, Marinho, Sun. Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata. TiCSA 2023.
• Altmeyer, André et al. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (invited paper). ECRTS 2023.
• Spriet, Lime, Roux. Timed non-interference under Partial Observability and Bounded Memory. FORMATS 2023. Best paper award.
• Leclercq, Lime, Roux. A state class based controller synthesis approach for Time Petri Nets. Petri Nets 2023.
• André, Lefaucheux, Marinho. Expiring opacity problems in parametric timed automata. ICECCS 2023.

2022

• André, Lime, Marinho, Sun. Guaranteeing timed opacity using parametric timed model checking. ACM TOSEM, 2022.
• André, Lime, Roux. Reachability and liveness in parametric timed automata. LMCS 18(1), 2022.
• Waga, André, Hasuo. Model-Bounded Monitoring of Hybrid Systems. ACM TCPS, 2022.
• Yifan Jia, Christopher M. Poskitt, Jun Sun, Sudipta Chattopadhyay: Physical Adversarial Attack on a Robotic Arm. IEEE Robotics Autom. Lett. 7(4): 9334-9341 (2022)
• Waga, André, Hasuo. Parametric Timed Pattern Matching. ACM TOSEM. 2022.
• Rothstein, Sun, Chattopadhyay. ORIGAMI: Folding Data Structures to Reduce Timing Side-Channel Leakage. Memocode 2022.
• André, Bolat, Lefaucheux, Marinho. strategFTO: Untimed control for timed opacity FTSCS 2022.
• André, Marinho, Petrucci, van de Pol. Efficient Convex Zone Merging in Parametric Timed Automata. FORMATS 2022.
• Long H. Pham, Jun Sun: Verifying Neural Networks Against Backdoor Attacks. CAV (1) 2022: 171-192
• André, Arcile. Zone extrapolations in parametric timed automata. NFM 2022.
• André, Waga, Urabe, Hasuo. Exemplifying parametric timed specifications over signals with bounded behavior. NFM 2022.
• Ghosh, André. Monitoring of scattered uncertain logs using uncertain linear dynamical systems. FORTE 2022.
• Aleksandra Jovanović, Didier Lime, and Olivier H. Roux, Control of Real-time Systems with Integer Parameters. In IEEE Transactions on Automatic Control, 2022. IEEE.

2021

• Yifan Jia, Jingyi Wang, Christopher M. Poskitt, Sudipta Chattopadhyay, Jun Sun, Yuqi Chen: Adversarial attacks and mitigation for anomaly detectors of cyber-physical systems. Int. J. Crit. Infrastructure Prot. 34: 100452 (2021)
• André, Nguyen, Petrucci, Sun. Distributed parametric model checking timed automata under non-Zenoness assumption. FMSD, 2021.
• Étienne André, Didier Lime and Mathias Ramparison. Parametric updates in parametric timed automata. Logical Methods in Computer Science 17:2, pages 13:1-13:67, May 2021. DOI: 0.23638/LMCS-17(2:13)2021 (English) [PDF | BibTeX]
• Étienne André, Didier Lime, Mathias Ramparison and Mariëlle Stoelinga. Parametric analyses of attack-fault trees. Fundamenta Informaticæ 182(1), pages 69-94, September 2021. DOI: 10.3233/FI-2021-2066 (English) [PDF (author version) | BibTeX | data]
• Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In Jan Friso Groote and Kim G. Larsen (eds.), TACAS’21, Springer LNCS 12651, pages 311-329, March 2021. Acceptance rate: 33%. DOI: 10.1007/978-3-030-72016-2_17 (English) [PDF | BibTeX | data]
• Didier Lime, Olivier H. Roux and Charlotte Seidner, Cost Problems for Parametric Time Peri Nets. In Fundamenta Informaticae 183(1-2):97-123, 2021.
• Masaki Waga (和賀 正樹), Étienne André and Ichiro Hasuo (蓮尾 一郎). Model-bounded monitoring of hybrid systems. In Mohammad Al Farque and Meeko Oishi (eds.), ICCPS’21, pages 21-32, May 2021. Acceptance rate: 26%. DOI: 10.1145/3450267.3450531 (English) [PDF (author version) | BibTeX | data | Slides]
• André, Arias, Petrucci, van de Pol. Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. TACAS 2021.
• André, Marinho, van de Pol. A Benchmarks Library for Extended Timed Automata. TAP 2021.
• André. IMITATOR 3: Synthesis of timing parameters beyond decidability. CAV 2021.

2020

• Teck Ping Khoo, Jun Sun, Sudipta Chattopadhyay: Learning Fault Models of Cyber Physical Systems. ICFEM 2020: 147-162.
• Morris, Sun, Chattopadhyay. Systematic Classification of Attackers via Bounded Model Checking. VMCAI 2020.
• Étienne André and Aleksander Kryukov. Parametric non-interference in timed automata. In Yi Li and Alan Liew (eds.), ICECCS’20, pages 37-42, October 2020. Acceptance rate: 33%. DOI: 10.1109/ICECCS51672.2020.00012 (English) [PDF (author version) | data | Slides]

2019

• Étienne André and Sun Jun. Parametric timed model checking for guaranteeing timed opacity. In Yu-Fang Chen, Chih-Hong Cheng and Javier Esparza (eds.), ATVA’19, Springer LNCS 11781, pages 115–130, October 2019. DOI: 10.1007/978-3-030-31784-3_7 (English 🏴󠁧󠁢󠁥󠁮󠁧󠁿) [PDF (author version) | BibTeX | data | Slides]

Selected talks

2020

• Étienne André. Retour d’expérience sur le plan de gestion de données du projet ProMiS. In 3^e journée annuelle de séminaire autour de la science ouverte : les données de la recherche, October 2020. (French 🇫🇷) [Slides]