Combined Security and Schedulability Analysis for MILS Real-Time Critical Architectures

Real-time critical systems have to comply with stringent timing constraints, otherwise, disastrous consequences can occur at runtime. A large effort has been made to propose models and tools to verify timing constraints by schedulability analysis at the early stages of system designs. Fewer efforts have been made on verifying the security properties in these systems despite the fact that sinister consequences can also happen if these properties are compromised. In this article, we investigate how to jointly verify security and timing constraints. We show how to model a security architecture (MILS) and how to verify both timing constraints and security properties. Schedulability is investigated by the mean of scheduling analysis methods implemented into the Cheddar scheduling analyzer. Experiments are conducted to show the impact that improving security has on the schedulability analysis.