RISC-V has emerged as a compelling alternative to proprietary instruction set architectures, distinguished by its openness, extensibility, and modularity. As the ecosystem matures, attention has turned to building confidential computing foundations, notably Trusted Execution Environments (TEEs) and secure enclaves, to support sensitive workloads. These efforts explore a variety of design directions, yet reveal important trade-offs. Some approaches achieve strong isolation guarantees, but fall short in scalability or broad adoption. Others introduce defenses, such as memory protection or side-channel resistance, although often with significant performance costs that limit deployment in constrained systems. Lightweight enclaves address embedded contexts, but lack the advanced security features demanded by complex applications. In addition, early-stage development, complex programming models, and limited real-world validation hinder their usability. This survey reviews the current landscape of RISC-V TEEs and secure enclaves, analyzing their architectural principles, strengths, and weaknesses. To the best of our knowledge, this is the first work to present such a consolidated view. Finally, we highlight open challenges and research opportunities, aiming toward establishing a cohesive and trustworthy RISC-V trusted computing ecosystem.

This paper introduces a formal approach allowing the performance evaluation of Flexible Manufacturing Systems (FMS) while considering the whole system behavior (operation, transport and preparation) as well as its possible components failure. The proposed approach is based on a generic Generalized Stochastic Petri nets (GSP-nets) model. The introduced GSP-net model represents the basic operation of the FMS elements (machines and material handling systems) as well as their fail and recovery aspects. The existing formal verification GSP-nets methods are exploited, and especially the state space generation and handling, in order to deduce a set of performance indicators helping the FMS designers when scheduling the production. Extracted indicators allow to enhance the decision process and the system efficiency. An important advantage of the introduced approach is that it is parameterized. Thus, it may be adapted to a large class of existing FMSs. The instantiation of the presented GSP-nets model to the specific features of the studied FMS is made by colored tokens.

One of the persistent challenges in formally verifying distributed and concurrent systems is the combinatorial growth of the state space, a phenomenon known as the state explosion problem. The number of potential configurations for these systems increases significantly with scale and interconnection, rendering exhaustive analysis computationally costly or even infeasible. To address this problem, researchers have been resorting to modular design approaches that divide an intricate system into smaller, independently verifiable components. Based on an in-depth examination of the strengths and limitations of current works in the literature, we suggest parallelizing the construction of the Reduced Distributed State Space (RDSS), which is an abstract and condensed representation that leverages the subdivision of the system into separate modules. To this end, we propose a generalized distributed architecture that defines the roles of a central coordinator and multiple worker modules, along with their communication points for synchronizing the RDSS building. This architecture is then concretely implemented using the Robot Operating System (ROS 2) framework, which provides robust primitives such as topics and services for inter-process communication, making the distributed execution both scalable and maintainable. Our method ensures stuttering equivalence with the global system and enables the scalable verification of local LTL\X properties using each module’s metagraph, without the need to explore the full RDSS. This implementation lays the foundation for modular model checking in distributed environments. Its effectiveness is demonstrated through a cooperative patrolling case study, which serves not only to validate the correctness of the proposed algorithm but also to observe its distributed behavior through simulated executions.

Backdoor attacks pose a serious threat to small language models (SLMs) because compromised models can behave normally on benign inputs while producing attacker-specified outputs when a hidden trigger is activated. Existing defenses commonly require model retraining, operate only before deployment, rely on input-level signals, or incur excessive inference overhead. This paper presents AEGIS (Activation Evaluation and Guardrail for Inference Security), a non-invasive runtime framework for detecting backdoor-induced anomalies in transformer representations. AEGIS dynamically monitors equidistant internal layers, mean-pools and concatenates their hidden states, and compresses the resulting high-dimensional representation into a 64-dimensional latent space. A hybrid compression mechanism uses zero-shot principal component analysis for predominantly linear text representations and a lightweight autoencoder for nonlinear or multimodal representations. Detection is then performed entirely on the GPU using cosine distance from a centroid calibrated on clean data, without modifying or retraining the protected model. We evaluate AEGIS across Mistral-7B, Qwen2.5-7B, a 4-bit QLoRA-backdoored Qwen2.5-1.5B model, and a BadNets-backdoored Vision Transformer, covering simulated latent and PEFT-style attacks, genuine fine-tuned backdoors, FP16 inference, and 4-bit NF4 quantization. Across seven experimental scenarios, AEGIS achieves AUROC values between 0.95 and 1.00, true-positive rates between 86% and 100%, and detection latency between 0.47 and 2.40 ms. It obtains AUROC = 1.00 and 100% true-positive rate against the genuinely fine-tuned QLoRA backdoor, while achieving AUROC=0.997 against the fine-tuned visual BadNets attack. Under 4-bit quantization, it retains AUROC=0.95 with 1.50 ms latency and a 4.52 GB memory footprint. These results demonstrate that GPU-native latent-space monitoring can provide effective, retraining-free backdoor detection for real-time transformer inference.