Daniel Gracia Pérez

dblp:34/1782 · also Daniel Pérez 0003 · DBLP profile ↗
← Back
15ranked-venue papers
3as first author
5since 2021 · last 2025
—ORCID · conflict

Domains — the database's venue-derived domains; a paper can count in several

Systems, architecture and hardware · 6 · 2 first-author · 2 since 2021Software engineering, systems software and programming languages · 5 · 1 first-author · 3 since 2021Theory of computation · 2 · 2 since 2021Artificial intelligence and machine learning · 1 · 1 first-authorDatabases, data management, data science and information retrieval · 1 · 1 first-authorHuman-computer interaction and ubiquitous computing · 1Applied, interdisciplinary, general and emerging computing · 1
YearPublicationVenuePosition
2025 Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities
abstract
The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack (TSS). The open-source library tpm2-tss is a popular implementation of the TSS. Vulnerabilities in its code could allow attackers to recover sensitive information and take control of the system. This article presents a case study on formal verification of tpm2-tss using the Frama-C verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool. We present several difficulties and tool limitations we faced, illustrate them with examples and describe solutions that allowed us to verify functional properties and the absence of runtime errors for a representative subset of functions. In particular, their verification required several lemmas proved in the interactive proof assistant Coq . We describe our verification results and desired tool improvements necessary to achieve a full formal verification of the target code.
Yani Ziani, Téo Bernier, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez
Formal Aspects Comput.5
2024 Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez
TAP4
2023 Securing a RISC-V architecture: A dynamic approach
abstract
The SecureV (also known as SecV) project offers an innovative, open-source hardware, secure, and high-performance processor core based on the RISC-V ISA. The originality of the approach lies in the integration of a complete solution to increase security based on dynamic code transformation, covering 4 of the 5 NIST11National Institute of Standards and Technology functions of cybersecurity via monitoring (identify, detect), obfuscation (protect), and dynamic adaptation (react).
Sébastien Pillement, Maria Mendez Real, J. Pottier, T. Nieddu, Bertrand Le Gal, Sébastien Faucou, Jean-Luc Béchennec, Mikaël Briday, Sylvain Girbal, Jimmy Le Rhun, Olivier Gilles, Daniel Gracia Pérez, André Sintzoff, Jean-Roch Coulon
DATE12
2023 Towards Formal Verification of a TPM Software Stack
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
iFM4
2023 Securing IIoT communications using OPC UA PubSub and Trusted Platform Modules
abstract
In the Industry 4.0 context, data are a valuable asset that must be protected. Ensuring the confidentiality and integrity of the data exchanged by the IIoT devices is challenging, especially when those devices are out of the companies premises or easily accessible (we call them out-premise devices). These devices become primary targets for attackers as a way to compromise data and cause damage to infrastructure or people. OPC UA PubSub provides the appropriate mechanisms to build scalable (e.g. one-to-many) secure and interoperable solutions with end-to-end encryption. However, authentication of IIoT devices remains a sensitive question, as it requires to securely embedding secrets. We present a novel approach based on open source software aiming to secure out-premise devices authentication, enabling the confidentiality and integrity of data exchanges with the rest of the system. Our approach uses a Trusted Platform Module as a secure element to protect the secrets embedded on devices. We further apply the approach on a predictive maintenance use case and evaluate the security level of our solution in such use case.
Olivier Gilles, Daniel Gracia Pérez, P.-A. Brameret, V. Lacroix
J. Syst. Archit.2
2019 Improving Prediction Accuracy of Memory Interferences for Multicore Platforms
abstract
Memory interferences may introduce important slowdowns in applications running on COTS multi-core processors. They are caused by concurrent accesses to shared hardware resources of the memory system. The induced delays are difficult to predict, making memory interferences a major obstacle to the adoption of COTS multi-core processors in real-time systems. In this article, we propose an experimental characterization of applications' memory consumption to determine their sensitivity to memory interferences. Thanks to a new set of microbenchmarks, we show the lack of precision of a purely quantitative characterization. To improve accuracy, we define new metrics quantifying qualitative aspects of memory consumption and implement a profiling tool using the VALGRIND framework. In addition, our profiling tool produces high resolution profiles allowing us to clearly distinguish the various phases in applications' behavior. Using our microbenchmarks and our new characterization, we train a state-of-the-art regressor. The validation on applications from the M I B ENCH and the PARSEC suites indicates significant gain in prediction accuracy compared to a purely quantitative characterization.
Cédric Courtaud, Julien Sopena, Gilles Muller, Daniel Gracia Pérez
RTSS4
2018 Job-shifting: An algorithm for online admission of non-preemptive aperiodic tasks in safety critical systems
Ali Syed, Daniel Gracia Pérez, Gerhard Fohler
J. Syst. Archit.2
2017 DREAMS Toolchain: Model-Driven Engineering of Mixed-Criticality Systems
abstract
Mixed-criticality systems (MCS) aim at boosting the integration density in safety-critical systems, resulting into efficient systems, while simultaneously providing increased performance. The DREAMS project provides a cross-domain architectural style for MCS based on networked, virtualized multi-cores controlled by hierarchical resource managers. However, the availability of a platform is only one side of the coin: deploying mixed-critical applications to shared resources typically requires design-time configurations (e.g., to ensure real-time constraints or separation constraints mandated by safety regulations). These configurations are the outcome of complex optimization problems which are intractable in a manual process that also hardly can guarantee the consistency of all deployable artefacts nor their traceability to the requirements. However, existing toolchains lack support for MCS integration, and particularly DREAMS' advanced platform capabilities. We present an integrated model-driven toolchain and the underlying metamodels covering all relevant aspects of MCS including applications, timing, platforms, deployments, configurations and annotations for extra-functional properties such as safety. The approach focuses on the left branch of the V-cycle, and ranges from product-line and design space exploration to resource allocation and configuration generation. We report on the integration of exploration tools and a reconfiguration graph synthesizer, and evaluate the resulting toolchains in two use cases consisting of a product-line of wind power control applications and an avionic subsystem respectively.
Simon Barner, Alexander Diewald, Jörn Migge, Ali Syed, Gerhard Fohler, Madeleine Faugère, Daniel Gracia Pérez
MoDELS7
2017 Schedulability analysis for global fixed-priority scheduling of the 3-phase task model
abstract
Scheduling real-time applications on general purpose multicore platforms is a challenging problem from a timing analysis perspective. Such platforms expose uncontrolled sources of interference whenever concurrent accesses to memory are performed. The non-deterministic bus and memory access behavior complicates the estimations of applications' worst-case execution times (WCET). The 3-phase task model seems a good candidate to circumvent the uncontrolled sources of interference by isolating concurrent memory accesses. A task is divided in three successive phases; first, the task loads its instruction and data in a local memory, then it executes non-preemptively using those pre-loaded instructions and data, and finally, the modified data are pushed back to main memory. Following this execution model, tasks never access the bus during their execution phase. Instead, all the bus accesses are performed during the first and third phases. In this paper, we focus on the global fixed-priority scheduling of the 3-phase task model. A new schedulability test is derived by modelling the interference happening on the bus rather than the interference on the cores as in the state-of-the-art techniques. The effectiveness of the test is evaluated by comparing it against the state-of-the-art.
Cláudio Maia, Geoffrey Nelissen, Luís Nogueira, Luís Miguel Pinho, Daniel Gracia Pérez
RTCSA5
2017 Online admission of non-preemptive aperiodic mixed-critical tasks in hierarchic schedules
abstract
Operational safety is one of the major issues in modern industrial applications. For safety critical systems, the verification and validation efforts can be reduced using temporal isolation enforced by hierarchic schedules. In 2012, Lackorzyiiski et al. demonstrated that reserving bandwidth for event-triggered (ET) activities in hierarchic schedules may lead to significant bandwidth loss. In contrast to the bandwidth reservation techniques, online admission of ET activities can help reduce bandwidth losses. However, the state-of-the-art approaches for online admission of ET activities (i) cannot be utilized in hierarchic systems and (ii) incur significant scheduling overheads. In this paper, we present a flexible scheduler design for online admission of non-preemptive a periodic tasks in a hierarchic time-triggered environment. Our approach circumvents the bandwidth loss issue in hierarchic systems, and can be implemented on top of a variety of hypervisor interfaces. In order to provide offline guarantees, we also provide a necessary test for our approach. Through evaluation, we demonstrate that our approach efficiently utilizes processor bandwidth and only incurs small overheads for a safety critical system. The experimental study also shows that our approach is comparable, in terms of execution overheads, to the state-of-the-art preemptive non-hierarchic approaches.
Ali Syed, Gerhard Fohler, Daniel Gracia Pérez
RTCSA3
2016 A closer look into the AER Model
abstract
Commercial-of-the-shelf based multi-core systems present timing anomalies that cannot be ignored by the real-time systems community due to their unpredictable behaviour. These timing anomalies, often caused by applications' uncontrolled accesses to shared resources such as the components in the memory hierarchy or in the I/O subsystem, introduce interference that may lead to deadline misses if the problem is neglected. The Acquisition Execution Restitution (AER) execution model was previously proposed to circumvent this problem and, therefore, mitigate inter-task interference. In this model, applications decouple communication (acquisition and restitution phases) from the actual execution in a way that at most one acquisition or restitution phase is in execution at any instant of time while the execution phase of different tasks can progress in parallel on multiple cores. Thus, keeping each task's derived worst-case execution time closer to the one measured in isolation. In this paper, we study the AER execution model and compare it against a global Earliest Deadline First (EDF) approach where interferences are considered. Our results show that a priority assignment heuristic which assigns the priorities based on the tasks' periods dominates all the other proposed heuristics and that due to interference it can also schedule task sets which are not schedulable by using the global EDF approach.
Cláudio Maia, Luís Nogueira, Luís Miguel Pinho, Daniel Gracia Pérez
ETFA4
2009 The GERMANA Database
abstract
A new handwritten text database, GERMANA, is presented to facilitate empirical comparison of different approaches to text line extraction and off-line handwriting recognition. GERMANA is the result of digitising and annotating a 764-page Spanish manuscript from 1891, in which most pages only contain nearly calligraphed text written on ruled sheets of well-separated lines. To our knowledge, it is the first publicly available database for handwriting research, mostly written in Spanish and comparable in size to standard databases. Due to its sequential book structure, it is also well-suited for realistic assessment of interactive handwriting recognition systems. To provide baseline results for reference in future studies, empirical results are also reported, using standard techniques and tools for preprocessing, feature extraction, HMM-based image modelling, and language modelling.
Daniel Gracia Pérez, Lionel Tarazón, Oriol Ramos Terrades, Alfons Juan-Císcar
ICDAR1
2009 Adaptation from partially supervised handwritten text transcriptions
abstract
An effective approach to transcribe handwritten text documents is to follow an interactive-predictive paradigm in which both, the system is guided by the user, and the user is assisted by the system to complete the transcription task as efficiently as possible. This approach has been recently implemented in a system prototype called GIDOC, in which standard speech technology is adapted to handwritten text (line) images: HMM-based text image modelling, n-gram language modelling, and also confidence measures on recognized words. Confidence measures are used to assist the user in locating possible transcription errors, and thus validate system output after only supervising those (few) words for which the system is not highly confident. Here, we study the effect of using these partially supervised transcriptions on the adaptation of image and language models to the task.
Daniel Gracia Pérez, Alberto Sanchís, Alfons Juan-Císcar
ICMI2
2004 A New Optimized Implemention of the SystemC Engine Using Acyclic Scheduling
abstract
SystemC is rapidly gaining wide acceptance as a simulation framework for SoC and embedded processors. While its main assets are modularity and the very fact it is becoming a de facto standard, the evolution of the SystemC framework (from version 0.9 to version 2.0.1) suggests the environment is particularly geared toward increasing the framework functionalities rather than improving simulation speed. For cycle-level simulation, speed is a critical factor as simulation can be extremely slow, affecting the extent of design space exploration. In this article, we present a fast SystemC engine that, in our experience, can speed up simulations by a factor of 1.93 to 3.56 over SystemC 2.0.1. This SystemC engine is designed for cycle-level simulators and for the moment, it only supports the subset of the SystemC syntax (signals, methods) that is most often used for such simulators. We achieved greater speed (1) by completely rewriting the SystemC engine and improving the implementation software engineering, and (2) by proposing a new scheduling technique, intermediate between SystemC dynamic scheduling technique and existing static scheduling schemes. Unlike SystemC dynamic scheduling, our technique removes many if not all useless process wake-ups, while using a simpler scheduling algorithm than in existing static scheduling techniques.
Daniel Gracia Pérez, Gilles Mouchard, Olivier Temam
DATE1
2004 MicroLib: A Case for the Quantitative Comparison of Micro-Architecture Mechanisms
abstract
While most research papers on computer architectures include some performance measurements, these performance numbers tend to be distrusted. Up to the point that, after so many research articles on data cache architectures, for instance, few researchers have a clear view of what are the best data cache mechanisms. To illustrate the usefulness of a fair quantitative comparison, we have picked a target architecture component for which lots of optimizations have been proposed (data caches), and we have implemented most of the performance-oriented hardware data cache optimizations published in top conferences in the past 4 years. Beyond the comparison of data cache ideas, our goals are twofold: (1) to clearly and quantitatively evaluate the effect of methodology shortcomings, such as model precision, benchmark selection, trace selection..., on assessing and comparing research ideas, and to outline how strong is the methodology effect in many cases, (2) to outline that the lack of interoperable simulators and not disclosing simulators at publication time make it difficult if not impossible to fairly assess the benefit of research ideas. This study is part of a broader effort, called MicroLib, an open library of modular simulators aimed at promoting the disclosure and sharing of simulator models.
Daniel Gracia Pérez, Gilles Mouchard, Olivier Temam
MICRO1