Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems

In order to be resilient, a system must be adaptable. Trustworthy adaptation requires that a system can be dynamically reconfigured at run-time without compromising the robustness and integrity of the system. Adaptive MILS extends MILS, a successful paradigm for rigorously developed and assured composable static systems, with reconfiguration mechanisms and a framework within which those mechanisms may be safely and securely employed for adaptation. In this paper, we address the problem of synthesizing at run-time reconfigurations that are trustworthy taking into account the entwining of information flows and reconfigurations. The approach is based on a new extension of the Architecture Analysis & Design Language (AADL), already used for specifying MILS policy architectures, which is now enhanced to specify the configuration state space in terms of parameters, the possible reconfigurations, monitoring properties and the related alarms. Supporting tools have been developed for the run-time synthesis of new architectural configurations that preserve safety and security properties formalized in terms of invariants and information flow.