REASSURE
Secure Runtime Verification for Reliable Real-Time Embedded Software
| NORTE-01-0145-FEDER-028550 PTDC/EEI-COM/28550/2017 4 years (Jul 2018 to Jun 2022) | |
| Summary: | The goal of REASSURE is to improve over the state-of-the-art Runtime Verification (RV) approaches for RTES by developing a new framework that: (1) extends existing runtime monitoring infrastructures capturing system properties (with focus on extra functional properties) with features to guarantee safety and ensuring that monitored data is kept secure without revealing information about the system (no security leak); (2) provides a domain specific language (DSL) and the tools to specify the requirements that must be verified at runtime; (3) automatically generate monitors and deploy them on energy and computing power constrained platforms. The framework developed in REASSURE will be validated within an industrial context. EDISOFT, a company active in critical systems, will provide a relevant case study, based on the RTEMS space-qualified operating system, and will follow the research in the project, advising the project team. This case study will allow to validate the project's tools and methodology by addressing a representative set of requirements, facilitating future exploitation. |
| Funding: | Global: 235KEUR, CISTER: 183KEUR |
| Sponsors: |     |
| Partners: | |
| Contact Person at CISTER: | David Pereira |
11, Jun, 2019
REASSURE progress meeting at U.Minho
On the 11th of June, CISTER Researchers David Pereira and Giann Nandi have participated in a progress meeting of REASSURE, that took place in the premises of the Department of Informatics of University of Minho.
The meeting, which counted also with the participation of REASSURE’s team members José Bacelar Almeida and Jorge Sousa Pinto from HASLab/ INESC TEC, had the purpose of analyzing the results obtained by both teams in this first year of REASSURE, and to plan the next steps for the second year of activities of the project, notably in what concerns the design of Domain Specific Languages and Cyber-Security Support in the design of runtime monitoring architectures.
Particular focus on the work developed by Giann, under his PhD studies, on the formal verification of WSN protocols using the ProVerif Tool, which is the core result described in the paper entitled “Security in Wireless Sensor Networks: A formal verification of protocols” that has been recently accepted in this year’s edition of INDIN 2019 – 17th IEEE International Conference on Industrial Informatics.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Journal Papers
Hubs for VirtuosoNext: Online verification of real-time coordinators CISTER-TR-201101
Guillermina Cledou, José Proença, Bernhard H.C. Sputh, Eric VerhulstScience of Computer Programming, Article No 102566, Elsevier. 1, Mar, 2021, Volume 203.In Press, Journal Pre-proof
Guillermina Cledou, José Proença, Bernhard H.C. Sputh, Eric VerhulstScience of Computer Programming, Article No 102566, Elsevier. 1, Mar, 2021, Volume 203.In Press, Journal Pre-proof
PDFConference or Workshop Papers/Talks
API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 CISTER-TR-220505
Guillermina Cledou, Luc Edixhoven, Sung Shik Jongmans, José Proença36th European Conference on Object-Oriented Programming (ECOOP 2022). 6 to 10, Jun, 2022, Session Types 1. Berlin, Germany.
Guillermina Cledou, Luc Edixhoven, Sung Shik Jongmans, José Proença36th European Conference on Object-Oriented Programming (ECOOP 2022). 6 to 10, Jun, 2022, Session Types 1. Berlin, Germany.
Verification of multiple models of a safety-critical motor controller in railway systems CISTER-TR-220504
José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira, Giann NandiReliability, Safety, and Security of Railway Systems (RSSRail 2022). 1 to 2, Jun, 2022, Safety and new technologies, pp 83-94. Paris, France.
José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira, Giann NandiReliability, Safety, and Security of Railway Systems (RSSRail 2022). 1 to 2, Jun, 2022, Safety and new technologies, pp 83-94. Paris, France.
Real-time MTL with durations as SMT with applications to schedulability analysis CISTER-TR-200703
André Pedro, Martin Leucker, David Pereira, Jorge Sousa Pinto14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020). 11 to 13, Dec, 2020. Hangzhou, China.
André Pedro, Martin Leucker, David Pereira, Jorge Sousa Pinto14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020). 11 to 13, Dec, 2020. Hangzhou, China.
Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Physical Systems CISTER-TR-201002
Giann Nandi, David Pereira, José Proença, Eduardo TovarWork in Progress Session, 41st IEEE Real-Time Systems Symposium (RTSS 2020). 1 to 4, Dec, 2020, pp 395-398. Online.
Giann Nandi, David Pereira, José Proença, Eduardo TovarWork in Progress Session, 41st IEEE Real-Time Systems Symposium (RTSS 2020). 1 to 4, Dec, 2020, pp 395-398. Online.
Implementing Hybrid Semantics: From Functional to Imperative CISTER-TR-201008
Sergey Goncharov, Renato Neves, José Proença17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020). 30, Nov to 4, Dec, 2020, pp 262-282. Online.Lecture Notes in Computer Science, vol 12545.
Sergey Goncharov, Renato Neves, José Proença17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020). 30, Nov to 4, Dec, 2020, pp 262-282. Online.Lecture Notes in Computer Science, vol 12545.
ARx: Reactive Programming for Synchronous Connectors CISTER-TR-200701
José Proença, Guillermina CledouInternational Conference on Coordination Languages and Models (COORDINATION 2020). 15 to 19, Jun, 2020, Coordination Languages, pp 39-56. Online.Held as part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Part of the Lecture Notes in Computer Science book series (LNCS, volume 12134).
José Proença, Guillermina CledouInternational Conference on Coordination Languages and Models (COORDINATION 2020). 15 to 19, Jun, 2020, Coordination Languages, pp 39-56. Online.Held as part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Part of the Lecture Notes in Computer Science book series (LNCS, volume 12134).
A Domain Specific Language for Automotive Systems Integration CISTER-TR-190806
Renato Oliveira, David Pereira, Cláudio Maia, Pedro José Santos45th Annual Conference of the IEEE Industrial Electronics Society (IECON 2019). 14 to 17, Oct, 2019, SS Emerging Solutions for Vehicular Embedded Systems, pp 4483-4488. Lisbon, Portugal.
Renato Oliveira, David Pereira, Cláudio Maia, Pedro José Santos45th Annual Conference of the IEEE Industrial Electronics Society (IECON 2019). 14 to 17, Oct, 2019, SS Emerging Solutions for Vehicular Embedded Systems, pp 4483-4488. Lisbon, Portugal.
Security in Wireless Sensor Networks: A formal verification of protocols CISTER-TR-190506
Giann Nandi, David Pereira, Martín Vigil, Ricardo Moraes, Analúcia Schiaffino Morales, Gustavo Araújo17th IEEE International Conference on Industrial Informatics (INDIN 2019). 22 to 25, Jul, 2019, Safety and Security in Industrial Applications, pp 425-431. Helsinki-Espoo, Finland.
Giann Nandi, David Pereira, Martín Vigil, Ricardo Moraes, Analúcia Schiaffino Morales, Gustavo Araújo17th IEEE International Conference on Industrial Informatics (INDIN 2019). 22 to 25, Jul, 2019, Safety and Security in Industrial Applications, pp 425-431. Helsinki-Espoo, Finland.
Coordination of tasks on a Real-Time OS CISTER-TR-190501
Guillermina Cledou, José Proença, Bernhard H.C. Sputh, Eric Verhulst21st International Conference on Coordination Models and Languages (Coordination 2019). 18 to 21, Jun, 2019. Copenhagen, Denmark.Part of the Lecture Notes in Computer Science book series (LNCS, volume 11533)
Guillermina Cledou, José Proença, Bernhard H.C. Sputh, Eric Verhulst21st International Conference on Coordination Models and Languages (Coordination 2019). 18 to 21, Jun, 2019. Copenhagen, Denmark.Part of the Lecture Notes in Computer Science book series (LNCS, volume 11533)
Conference or Workshop Posters/Demos
Towards the design of a DSL to enable the secure Runtime Monitoring and Verification of Safety-Critical CPS CISTER-TR-190606
Giann NandiPoster presented in 3rd Doctoral Congress in Engineering (DCE 2019). 27 to 28, Jun, 2019. Porto, Portugal.
Giann NandiPoster presented in 3rd Doctoral Congress in Engineering (DCE 2019). 27 to 28, Jun, 2019. Porto, Portugal.
Technical Reports
Implementing Hybrid Semantics: From Functional to Imperative (Extended Version) CISTER-TR-201012
Sergey Goncharov, Renato Neves, José Proença29, Sep, 2020.
Sergey Goncharov, Renato Neves, José Proença29, Sep, 2020.