Visible to the public A Formal Model for the Automatic Configuration of Access Protection Units in MPSoC-Based Embedded Systems

TitleA Formal Model for the Automatic Configuration of Access Protection Units in MPSoC-Based Embedded Systems
Publication TypeConference Paper
Year of Publication2020
AuthorsDörr, T., Sandmann, T., Becker, J.
Conference Name2020 23rd Euromicro Conference on Digital System Design (DSD)
Date PublishedAug. 2020
ISBN Number978-1-7281-9535-3
Keywordsabstract permission declarations, access permissions, access protection, access protection unit, authorisation, code generation, composability, configuration code, data protection, dedicated access protection units, Embedded systems, formal model, Hardware, heterogeneous system-on-chip platforms, information flow requirements, information flow tracking, internal communication links, Metrics, model-based design, MPSoC-based embedded systems, multiple processing cores, multiprocessing systems, multiprocessor system-on-chip, on-chip isolation, pubcrawl, Real-time Systems, resilience, Resiliency, Safety, safety-critical embedded system, safety-critical software, security, security-critical embedded system, system-level isolation, system-on-chip, Timing

Heterogeneous system-on-chip platforms with multiple processing cores are becoming increasingly common in safety-and security-critical embedded systems. To facilitate a logical isolation of physically connected on-chip components, internal communication links of such platforms are often equipped with dedicated access protection units. When performed manually, however, the configuration of these units can be both time-consuming and error-prone. To resolve this issue, we present a formal model and a corresponding design methodology that allows developers to specify access permissions and information flow requirements for embedded systems in a mostly platform-independent manner. As part of the methodology, the consistency between the permissions and the requirements is automatically verified and an extensible generation framework is used to transform the abstract permission declarations into configuration code for individual access protection units. We present a prototypical implementation of this approach and validate it by generating configuration code for the access protection unit of a commercially available multiprocessor system-on-chip.

Citation Keydorr_formal_2020